Mathlib.Probability.CertifiedFiniteMarkovExpectation
Exact rational interval arithmetic for finite-state Markov kernels, certified normal-CDF transition probabilities, stationary-reward enclosures, and strict policy comparisons.
Interval 22 core · 18 supporting This module lifts Causalean's exact rational scalar intervals to finite sums, vectors, matrices, matrix products, and row-vector actions. ★ intervalMatrixMul_sound★ sound
Finite rational interval linear algebra
This module lifts Causalean's exact rational scalar intervals to finite sums, vectors, matrices, matrix products, and row-vector actions. All computations are performed on rational endpoints, while the soundness theorems relate the computed intervals to real linear algebra.
abbrev IntervalVector reviewed
⚑ flagged
Causalean.Mathlib.Probability.CertifiedFiniteMarkovExpectation
An interval vector assigns one exact rational interval to each coordinate.
Definition (Lean source)
abbrev IntervalMatrix reviewed
⚑ flagged
Causalean.Mathlib.Probability.CertifiedFiniteMarkovExpectation
An interval matrix assigns one exact rational interval to each row and column.
Definition (Lean source)
def ContainsVector reviewed
⚑ flagged
Causalean.Mathlib.Probability.CertifiedFiniteMarkovExpectation
An interval vector contains a real vector when it contains every coordinate.
Definition (Lean source)
parameters
def
ContainsVector I x :
Prop
given by
(I i).Contains (x i)
def ContainsMatrix reviewed
⚑ flagged
Causalean.Mathlib.Probability.CertifiedFiniteMarkovExpectation
An interval matrix contains a real matrix when it contains every entry.
Definition (Lean source)
parameters
def
ContainsMatrix I A :
Prop
given by
(I i j).Contains (A i j)
def VectorSubinterval reviewed
⚑ flagged
Causalean.Mathlib.Probability.CertifiedFiniteMarkovExpectation
Coordinatewise rational interval refinement for vectors.
Definition (Lean source)
parameters
def
VectorSubinterval I J :
Prop
given by
(I i).Subinterval (J i)
def MatrixSubinterval reviewed
⚑ flagged
Causalean.Mathlib.Probability.CertifiedFiniteMarkovExpectation
Coordinatewise rational interval refinement for matrices.
Definition (Lean source)
parameters
def
MatrixSubinterval I J :
Prop
given by
(I i j).Subinterval (J i j)
def intervalSum reviewed
⚑ flagged
Causalean.Mathlib.Probability.CertifiedFiniteMarkovExpectation
The finite interval sum is the ordinary finite sum using outward interval addition.
Definition (Lean source)
def intervalDot reviewed
⚑ flagged
Causalean.Mathlib.Probability.CertifiedFiniteMarkovExpectation
The interval dot product sums outward products of corresponding coordinates.
Definition (Lean source)
def intervalMulVec reviewed
⚑ flagged
Causalean.Mathlib.Probability.CertifiedFiniteMarkovExpectation
Applying an interval matrix to an interval column vector uses interval dot products rowwise.
Definition (Lean source)
def intervalVecMul reviewed
⚑ flagged
Causalean.Mathlib.Probability.CertifiedFiniteMarkovExpectation
Applying an interval row vector to an interval matrix uses interval dot products columnwise.
Definition (Lean source)
def intervalMatrixMul reviewed
⚑ flagged
Causalean.Mathlib.Probability.CertifiedFiniteMarkovExpectation
Interval matrix multiplication computes every entry by an interval dot product.
Definition (Lean source)
def intervalExpectation reviewed
⚑ flagged
Causalean.Mathlib.Probability.CertifiedFiniteMarkovExpectation
The interval reward expectation is the interval dot product of mass and reward vectors.
Definition (Lean source)
theorem intervalMatrixMul_sound reviewed
⚑ flagged
Causalean.Mathlib.Probability.CertifiedFiniteMarkovExpectation
When the first rational interval matrix encloses a real matrix and the second rational interval matrix encloses a real matrix, their interval matrix product encloses the corresponding real matrix product.
Formal statement
hypotheses
conclusion
ContainsMatrix (intervalMatrixMul A B) (M * N)
Proof (Lean source)
theorem intervalMatrixMul_sound {ι κ υ : Type*} [Fintype κ]
{A : IntervalMatrix ι κ} {B : IntervalMatrix κ υ}
{M : Matrix ι κ ℝ} {N : Matrix κ υ ℝ}
(hA : ContainsMatrix A M) (hB : ContainsMatrix B N) :
ContainsMatrix (intervalMatrixMul A B) (M * N) := by
intro i j
exact intervalDot_sound (hA i) (fun k => hB k j)
def scalarSubintervalCheck reviewed
⚑ flagged
Causalean.Mathlib.Probability.CertifiedFiniteMarkovExpectation
Given an inner rational interval and an outer rational interval, the scalar subinterval check is the exact endpoint comparison that accepts exactly when the inner interval lies inside the outer interval.
Definition (Lean source)
structure ScalarIntervalCertificate reviewed
⚑ flagged
Causalean.Mathlib.Probability.CertifiedFiniteMarkovExpectation
A scalar interval certificate records that an exact rational value lies in a reported rational interval, through a checked point-interval refinement.
Definition (Lean source)
parameters
q :
ℚ
I :
assumes
checked :
(RatInterval.point q).Subinterval I
The point interval at the exact value refines the reported interval.
structure FiniteVectorCertificate reviewed
⚑ flagged
Causalean.Mathlib.Probability.CertifiedFiniteMarkovExpectation
A finite-vector certificate records independently checked scalar enclosures for each coordinate of an exact rational vector in a rational interval vector, through one certificate per coordinate.
Definition (Lean source)
parameters
assumes
coordinate :
∀ i, ScalarIntervalCertificate (q i) (I i)
Independently checked certificate for each vector coordinate.
structure FiniteMatrixCertificate reviewed
⚑ flagged
Causalean.Mathlib.Probability.CertifiedFiniteMarkovExpectation
A finite-matrix certificate records independently checked scalar enclosures for each entry of an exact rational matrix in a rational interval matrix, through one certificate per entry.
Definition (Lean source)
parameters
assumes
entry :
∀ i j, ScalarIntervalCertificate (q i j) (I i j)
Independently checked certificate for each matrix entry.
inductive IntervalFoldCertificate reviewed
⚑ flagged
Causalean.Mathlib.Probability.CertifiedFiniteMarkovExpectation
An interval-fold certificate records a proof-producing binary assembly of a list of intervals into one output interval, with the empty-list case and the one-more-interval case checked separately.
Definition (Lean source)
inductive
constructors
nil :
{output : RatInterval} (checked : (RatInterval.point 0).Subinterval output) : IntervalFoldCertificate [] output
The empty list is enclosed by any interval containing the point zero.
cons :
{head tailBound output : RatInterval} {tail : List RatInterval} (tailCertificate : IntervalFoldCertificate tail tailBound) (checked : (head.add tailBound).Subinterval output) : IntervalFoldCertificate (head :: tail) output
A certified tail and one checked addition certify the interval-list sum.
structure CertifiedChunk reviewed
⚑ flagged
Causalean.Mathlib.Probability.CertifiedFiniteMarkovExpectation
A certified chunk records a bounded partial interval sum of a finite interval family, with the selected maximum chunk size, its indices, its reported bound, a size proof, and a local exact-sum refinement proof.
Definition (Lean source)
parameters
fields
Indices assigned to this chunk.
indices :
Finset ι
Caller-supplied interval bound for this chunk.
bound :
The chunk contains no more than the selected number of terms.
size_le :
indices.card ≤ chunkSize
The exact interval sum for this chunk refines its reported bound.
checked :
(∑ i ∈ indices, terms i).Subinterval bound
structure ChunkedSumCertificate reviewed
⚑ flagged
Causalean.Mathlib.Probability.CertifiedFiniteMarkovExpectation
A chunked-sum certificate assembles a finite interval family using a selected chunk-size bound into a reported output interval, through bounded chunk certificates, their pairwise disjointness, their exhaustive coverage, and a checked binary assembly.
Definition (Lean source)
parameters
fields
Independently checked bounded chunks.
chunks :
List (CertifiedChunk terms chunkSize)
No index is counted by two different chunks.
pairwise_disjoint :
(chunks.map (fun c => c.indices)).Pairwise (fun s t => Disjoint s t)
Every index occurs in some chunk.
Chunk bounds are combined only through checked binary additions.
assembly :
IntervalFoldCertificate (chunks.map (fun c => c.bound)) output
theorem sound reviewed
⚑ flagged
Causalean.Mathlib.Probability.CertifiedFiniteMarkovExpectation.ChunkedSumCertificate
When a chunked-sum certificate is supplied, the complete interval sum refines its reported output interval.
Formal statement
hypotheses
conclusion
(intervalSum terms).Subinterval output
Proof (Lean source)
theorem ChunkedSumCertificate.sound {ι : Type*} [Fintype ι] [DecidableEq ι]
{terms : ι → RatInterval} {chunkSize : ℕ} {output : RatInterval}
(c : ChunkedSumCertificate terms chunkSize output) :
(intervalSum terms).Subinterval output := by
have chunk_refinements (cs : List (CertifiedChunk terms chunkSize)) :
Forall₂ RatInterval.Subinterval
(cs.map (fun d => ∑ i ∈ d.indices, terms i))
(cs.map (fun d => d.bound)) := by
induction cs with
| nil => exact .nil
| cons d ds ih => exact .cons d.checked ih
apply RatInterval.subinterval_trans ?_ c.assembly.refines_sum
have hfull : intervalSum terms =
(c.chunks.map (fun d => ∑ i ∈ d.indices, terms i)).sum := by
simpa only [intervalSum, List.map_map, Function.comp_def] using
sum_eq_sum_chunks terms (c.chunks.map (fun d => d.indices))
c.pairwise_disjoint c.covers
rw [hfull]
exact listSum_subinterval (chunk_refinements c.chunks)
abbrev ChunkedDotCertificate reviewed
⚑ flagged
Causalean.Mathlib.Probability.CertifiedFiniteMarkovExpectation
Given left interval-vector factors, right interval-vector factors, a chunk-size bound, and an output interval, a chunked dot-product certificate is the corresponding chunked certificate for outward interval products.
Definition (Lean source)
parameters
def
ChunkedDotCertificate left right chunkSize output :
Type u_1
given by
ChunkedSumCertificate (fun i => (left i).mul (right i)) chunkSize output
18 supporting declarations (lemmas, instances)
-
instAddCommMonoidRatIntervalinstance — Rational intervals form an additive commutative monoid under outward interval addition, with the point interval at zero as identity.instancegiven byclause 1zero := RatInterval.point 0clause 2add := RatInterval.addclause 3add_assoc := by intro I J K apply RatInterval.ext · change (I.lo + J.lo) + K.lo= I.lo+ (J.lo + K.lo) exact add_assoc _ _ _ · change (I.hi + J.hi)+ K.hi = I.hi+ (J.hi + K.hi) exact add_assoc _ _ _clause 4zero_add := by intro I apply RatInterval.ext · change 0 + I.lo= I.lo exact zero_add _ · change 0 + I.hi = I.hi exact zero_add _clause 5add_zero := by intro I apply RatInterval.ext · change I.lo + 0= I.lo exact add_zero _ · change I.hi + 0 = I.hi exact add_zero _clause 6add_comm := by intro I J apply RatInterval.ext · change I.lo + J.lo= J.lo + I.lo exact add_comm _ _ · change I.hi + J.hi = J.hi + I.hi exact add_comm _ _clause 7nsmul := fun n I => Nat.rec (RatInterval.point 0) (fun _ acc => RatInterval.add acc I) nclause 8nsmul_zero := by intro I rflclause 9nsmul_succ := by intro n I rfl -
intervalSum_soundtheorem — Finite outward interval addition contains the sum of any coordinatewise enclosed real family.Proof (Lean source)
theorem intervalSum_sound {ι : Type*} [Fintype ι] {I : ι → RatInterval} {x : ι → ℝ} (hx : ∀ i, (I i).Contains (x i)) : (intervalSum I).Contains (∑ i, x i) := by classical unfold intervalSum refine Finset.induction_on (Finset.univ : Finset ι) ?_ ?_ · change (RatInterval.point 0).Contains (0 : ℝ) simpa only [Rat.cast_zero] using RatInterval.point_sound (0 : ℚ) · intro i s hi ih rw [Finset.sum_insert hi, Finset.sum_insert hi] exact RatInterval.add_sound (hx i) ih -
intervalDot_soundtheorem — An interval dot product contains the real dot product of any two enclosed vectors.hypothesesconclusion(intervalDot I J).Contains (∑ i, x i * y i)Proof (Lean source)
theorem intervalDot_sound {ι : Type*} [Fintype ι] {I J : IntervalVector ι} {x y : ι → ℝ} (hx : ContainsVector I x) (hy : ContainsVector J y) : (intervalDot I J).Contains (∑ i, x i * y i) := by apply intervalSum_sound intro i exact RatInterval.mul_sound (hx i) (hy i) -
intervalMulVec_soundtheorem — Interval matrix-vector multiplication contains the corresponding real matrix-vector product.Proof (Lean source)
theorem intervalMulVec_sound {ι κ : Type*} [Fintype κ] {A : IntervalMatrix ι κ} {x : IntervalVector κ} {M : Matrix ι κ ℝ} {v : κ → ℝ} (hA : ContainsMatrix A M) (hx : ContainsVector x v) : ContainsVector (intervalMulVec A x) (mulVec M v) := by intro i exact intervalDot_sound (hA i) hx -
intervalVecMul_soundtheorem — Interval row-vector multiplication contains the corresponding real row-vector action.Proof (Lean source)
theorem intervalVecMul_sound {ι κ : Type*} [Fintype ι] {x : IntervalVector ι} {A : IntervalMatrix ι κ} {v : ι → ℝ} {M : Matrix ι κ ℝ} (hx : ContainsVector x v) (hA : ContainsMatrix A M) : ContainsVector (intervalVecMul x A) (vecMul v M) := by intro j exact intervalDot_sound hx (fun i => hA i j) -
monotheorem — Coordinatewise refinement preserves containment of a real vector.hypothesesconclusionContainsVector J xProof (Lean source)
theorem ContainsVector.mono {ι : Type*} {I J : IntervalVector ι} {x : ι → ℝ} (hIJ : VectorSubinterval I J) (hx : ContainsVector I x) : ContainsVector J x := by intro i exact RatInterval.Contains.mono (hIJ i) (hx i) -
monotheorem — Coordinatewise refinement preserves containment of a real matrix.hypothesesconclusionContainsMatrix J AProof (Lean source)
theorem ContainsMatrix.mono {ι κ : Type*} {I J : IntervalMatrix ι κ} {A : Matrix ι κ ℝ} (hIJ : MatrixSubinterval I J) (hA : ContainsMatrix I A) : ContainsMatrix J A := by intro i j exact RatInterval.Contains.mono (hIJ i j) (hA i j) -
scalarSubintervalCheck_soundtheorem — When the scalar subinterval check accepts, the inner interval is contained in the outer interval.hypothesesinner outer :h :scalarSubintervalCheck inner outer = trueconclusioninner.Subinterval outerProof (Lean source)
theorem scalarSubintervalCheck_sound {inner outer : RatInterval} (h : scalarSubintervalCheck inner outer = true) : inner.Subinterval outer := by simpa [scalarSubintervalCheck, RatInterval.Subinterval] using (of_decide_eq_true h) -
soundtheorem — When a scalar interval certificate is supplied, its reported interval contains the certificate's rational value as a real number.Proof (Lean source)
theorem ScalarIntervalCertificate.sound {q : ℚ} {I : RatInterval} (c : ScalarIntervalCertificate q I) : I.Contains (q : ℝ) := by exact RatInterval.Contains.mono c.checked (RatInterval.point_sound q) -
soundtheorem — When a finite-vector certificate is supplied, the reported interval vector contains the real vector obtained from its rational coordinates.Proof (Lean source)
theorem FiniteVectorCertificate.sound {ι : Type*} [Fintype ι] {q : ι → ℚ} {I : IntervalVector ι} (c : FiniteVectorCertificate q I) : ContainsVector I (fun i => (q i : ℝ)) := by intro i exact (c.coordinate i).sound -
soundtheorem — When a finite-matrix certificate is supplied, the reported interval matrix contains the real matrix obtained from its rational entries.Proof (Lean source)
theorem FiniteMatrixCertificate.sound {ι κ : Type*} [Fintype ι] [Fintype κ] {q : Matrix ι κ ℚ} {I : IntervalMatrix ι κ} (c : FiniteMatrixCertificate q I) : ContainsMatrix I (fun i j => (q i j : ℝ)) := by intro i j exact (c.entry i j).sound -
refines_sumtheorem — When an interval-fold certificate is supplied, the ordinary interval sum of its input list refines its reported output interval.hypothesesconclusionxs.sum.Subinterval outputProof (Lean source)
theorem IntervalFoldCertificate.refines_sum {xs : List RatInterval} {output : RatInterval} (c : IntervalFoldCertificate xs output) : xs.sum.Subinterval output := by induction c with | nil checked => change (RatInterval.point 0).Subinterval _ exact checked | cons tailCertificate checked ih => exact RatInterval.subinterval_trans (RatInterval.add_mono (RatInterval.subinterval_refl _) ih) checked -
contains_sumtheorem — Given an interval-fold certificate and coordinatewise evidence that each input interval contains its corresponding real value, the reported interval contains the sum of those real values.hypothesesxs :values :List ℝoutput :c :IntervalFoldCertificate xs outputh :Forall₂ (fun I x => I.Contains x) xs valuesconclusionoutput.Contains values.sumProof (Lean source)
theorem IntervalFoldCertificate.contains_sum {xs : List RatInterval} {values : List ℝ} {output : RatInterval} (c : IntervalFoldCertificate xs output) (h : Forall₂ (fun I x => I.Contains x) xs values) : output.Contains values.sum := by induction c generalizing values with | nil checked => cases h rw [List.sum_nil] simpa only [Rat.cast_zero] using RatInterval.Contains.mono checked (RatInterval.point_sound 0) | cons tailCertificate checked ih => cases h with | cons hhead htail => exact RatInterval.Contains.mono checked (RatInterval.add_sound hhead (ih htail)) -
listSum_subintervaltheorem — When each interval in one list refines the corresponding interval in another list, the sum of the first list refines the sum of the second.Proof (Lean source)
theorem listSum_subinterval {xs ys : List RatInterval} (h : Forall₂ RatInterval.Subinterval xs ys) : xs.sum.Subinterval ys.sum := by induction h with | nil => exact RatInterval.subinterval_refl _ | cons hhead htail ih => exact RatInterval.add_mono hhead ih -
sum_eq_sum_chunkstheorem — Given a finite additive family, a list of index chunks, pairwise disjoint chunks, and chunks covering every index, the full finite sum equals the list sum of the chunk sums.hypothesesι M :f :ι → Mhdisjoint :chunks.Pairwise (fun s t => Disjoint s t)hcovers :chunks.foldr (fun s acc => s ∪ acc) ∅ = univconclusion∑ i, f i = (chunks.map (fun s => ∑ i ∈ s, f i)).sumProof (Lean source)
theorem sum_eq_sum_chunks {ι M : Type*} [Fintype ι] [DecidableEq ι] [AddCommMonoid M] (f : ι → M) (chunks : List (Finset ι)) (hdisjoint : chunks.Pairwise (fun s t => Disjoint s t)) (hcovers : chunks.foldr (fun s acc => s ∪ acc) ∅ = univ) : ∑ i, f i = (chunks.map (fun s => ∑ i ∈ s, f i)).sum := by have disjoint_foldr (s : Finset ι) (cs : List (Finset ι)) (h : ∀ t ∈ cs, Disjoint s t) : Disjoint s (cs.foldr (fun t acc => t ∪ acc) ∅) := by induction cs with | nil => simp | cons t ts ih => rw [List.foldr_cons] exact Finset.disjoint_union_right.mpr ⟨h t (by simp), ih (fun u hu => h u (by simp [hu]))⟩ have partition_sum (cs : List (Finset ι)) (h : cs.Pairwise (fun s t => Disjoint s t)) : ∑ i ∈ cs.foldr (fun s acc => s ∪ acc) ∅, f i = (cs.map (fun s => ∑ i ∈ s, f i)).sum := by induction cs with | nil => simp | cons s cs ih => obtain ⟨hs, hcs⟩ := List.pairwise_cons.mp h rw [List.foldr_cons, Finset.sum_union (disjoint_foldr s cs hs), map_cons, List.sum_cons, ih hcs] calc ∑ i, f i = ∑ i ∈ chunks.foldr (fun s acc => s ∪ acc) ∅, f i := by rw [hcovers] _ = (chunks.map (fun s => ∑ i ∈ s, f i)).sum := partition_sum chunks hdisjoint -
containstheorem — Given a chunked-sum certificate and coordinatewise interval containment of real summands, the reported interval contains their full real sum.hypothesesι :chunkSize :ℕoutput :c :ChunkedSumCertificate terms chunkSize outputvalues :ι → ℝhvalues :∀ i, (terms i).Contains (values i)conclusionoutput.Contains (∑ i, values i)Proof (Lean source)
theorem ChunkedSumCertificate.contains {ι : Type*} [Fintype ι] [DecidableEq ι] {terms : ι → RatInterval} {chunkSize : ℕ} {output : RatInterval} (c : ChunkedSumCertificate terms chunkSize output) {values : ι → ℝ} (hvalues : ∀ i, (terms i).Contains (values i)) : output.Contains (∑ i, values i) := by exact RatInterval.Contains.mono c.sound (intervalSum_sound hvalues) -
soundtheorem — When a chunked dot-product certificate is supplied, the library interval dot product refines its reported coordinate interval.hypothesesconclusion(intervalDot left right).Subinterval outputProof (Lean source)
theorem ChunkedDotCertificate.sound {ι : Type*} [Fintype ι] [DecidableEq ι] {left right : IntervalVector ι} {chunkSize : ℕ} {output : RatInterval} (c : ChunkedDotCertificate left right chunkSize output) : (intervalDot left right).Subinterval output := by simpa only [intervalDot] using ChunkedSumCertificate.sound c -
containstheorem — Given a chunked dot-product certificate, left-vector containment, and right-vector containment, the reported interval contains the corresponding real dot product.hypothesesι :chunkSize :ℕoutput :c :ChunkedDotCertificate left right chunkSize outputx y :ι → ℝhx :hy :ContainsVector right yconclusionoutput.Contains (∑ i, x i * y i)Proof (Lean source)
theorem ChunkedDotCertificate.contains {ι : Type*} [Fintype ι] [DecidableEq ι] {left right : IntervalVector ι} {chunkSize : ℕ} {output : RatInterval} (c : ChunkedDotCertificate left right chunkSize output) {x y : ι → ℝ} (hx : ContainsVector left x) (hy : ContainsVector right y) : output.Contains (∑ i, x i * y i) := by exact ChunkedSumCertificate.contains c fun i => RatInterval.mul_sound (hx i) (hy i)
FiniteKernel 16 core · 8 supporting This module defines row-stochastic finite kernels and their action on probability row vectors. ★ contractsL1_of_rationalMinorization
Finite stochastic kernels, contraction, and checked interval recurrences
This module defines row-stochastic finite kernels and their action on probability row vectors. It also provides exact-rational certificates for kernel minorization and for a finite interval recurrence enclosing successive iterates of a real Markov chain.
def IsProbabilityVector reviewed
⚑ flagged
Causalean.Mathlib.Probability.CertifiedFiniteMarkovExpectation
A real vector is a probability vector when its entries are nonnegative and sum to one. This is definitionally membership in Mathlib's standard simplex (see isProbabilityVector_iff_mem_stdSimplex).
Definition (Lean source)
parameters
ι :
Type*
Fintype ι
p :
ι → ℝ
def
IsProbabilityVector p :
Prop
given by
clause 1
i :
0 ≤ p i
clause 2
∑ i, p i = 1
def IsStochasticMatrix reviewed
⚑ flagged
Causalean.Mathlib.Probability.CertifiedFiniteMarkovExpectation
A real square matrix is row-stochastic when every entry is nonnegative and every row sums to one. This is the same condition as membership in Mathlib's Matrix.rowStochastic (see isStochasticMatrix_iff_mem_rowStochastic), stated without its decidable-equality infrastructure.
def markovStep reviewed
⚑ flagged
Causalean.Mathlib.Probability.CertifiedFiniteMarkovExpectation
One Markov step multiplies a row vector by a square matrix. No condition is imposed; it is a step of a Markov chain when the vector is a probability vector and the matrix is row-stochastic.
def markovIterate reviewed
⚑ flagged
Causalean.Mathlib.Probability.CertifiedFiniteMarkovExpectation
The successive row vectors obtained from an initial row vector by repeated multiplication by a fixed square matrix. They are the successive distributions of a Markov chain when the start is a probability vector and the matrix is row-stochastic (see IsStochasticMatrix.iterate_probability).
Definition (Lean source)
parameters
def
markovIterate P p0 :
ℕ → (ι → ℝ)
def IsStationary reviewed
⚑ flagged
Causalean.Mathlib.Probability.CertifiedFiniteMarkovExpectation
A stationary distribution is a probability vector fixed by one Markov step.
Definition (Lean source)
parameters
def
IsStationary P π :
Prop
def l1Distance reviewed
⚑ flagged
Causalean.Mathlib.Probability.CertifiedFiniteMarkovExpectation
The finite ℓ¹ distance is the sum of absolute coordinate differences.
Definition (Lean source)
def ContractsL1 reviewed
⚑ flagged
Causalean.Mathlib.Probability.CertifiedFiniteMarkovExpectation
A square matrix contracts probability vectors in ℓ¹ by a supplied coefficient: the one-step images of any two probability vectors are at most the coefficient times their ℓ¹ distance apart. Row-stochasticity of the matrix is not part of this predicate and is assumed separately.
Definition (Lean source)
parameters
def
ContractsL1 P ρ :
Prop
given by
def Minorizes reviewed
⚑ flagged
Causalean.Mathlib.Probability.CertifiedFiniteMarkovExpectation
A Doeblin minorization says every row of a square matrix dominates the same probability vector scaled by a common mass ε between zero and one. Row-stochasticity of the matrix is not part of this predicate and is assumed separately.
Definition (Lean source)
parameters
def
Minorizes P ε ν :
Prop
structure CertifiedKernel reviewed
⚑ flagged
Causalean.Mathlib.Probability.CertifiedFiniteMarkovExpectation
A certified real kernel packages a stochastic matrix together with an entrywise rational interval table that contains it.
Definition (Lean source)
parameters
fields
Exact rational interval table for the transition entries.
intervals :
IntervalMatrix ι ι
Every real transition entry lies in its reported rational interval.
contains :
ContainsMatrix intervals P
The underlying real transition matrix is row-stochastic.
stochastic :
structure RationalProbabilityVector reviewed
⚑ flagged
Causalean.Mathlib.Probability.CertifiedFiniteMarkovExpectation
A rational probability-vector certificate contains exact nonnegativity and sum checks.
Definition (Lean source)
parameters
ι :
Type*
Fintype ι
fields
Exact rational mass at each state.
value :
ι → ℚ
Every rational mass is nonnegative.
nonneg :
∀ i, 0 ≤ value i
The exact rational masses sum to one.
sum_eq_one :
∑ i, value i = 1
def toReal reviewed
⚑ flagged
Causalean.Mathlib.Probability.CertifiedFiniteMarkovExpectation.RationalProbabilityVector
The real probability vector denoted by an exact rational certificate.
Definition (Lean source)
structure RationalMinorizationCertificate reviewed
⚑ flagged
Causalean.Mathlib.Probability.CertifiedFiniteMarkovExpectation
A rational minorization certificate is checked solely by exact rational nonnegativity, normalization, and entrywise lower-endpoint comparisons.
Definition (Lean source)
parameters
ι :
Type*
Fintype ι
K :
IntervalMatrix ι ι
fields
Common minorization mass.
epsilon :
ℚ
Exact rational minorizing probability vector.
nu :
The common mass is nonnegative.
epsilon_nonneg :
0 ≤ epsilon
The common mass is at most one.
epsilon_le_one :
epsilon ≤ 1
Each interval lower endpoint dominates the minorizing mass at that column.
lower_checked :
∀ i j, epsilon * nu.value j ≤ (K i j).lo
structure FiniteIterateCertificate reviewed
⚑ flagged
Causalean.Mathlib.Probability.CertifiedFiniteMarkovExpectation
A finite iterate certificate stores steps + 2 interval vectors and checks each recurrence inclusion using exact rational interval arithmetic.
Definition (Lean source)
parameters
fields
Number of the penultimate iterate used as the approximation.
steps :
ℕ
Interval table for iterates zero through `steps + 1`.
table :
Fin (steps + 2) → IntervalVector ι
The first interval row contains the exact rational initial distribution.
initial_checked :
∀ i, (RatInterval.point (p0.value i)).Subinterval (table 0 i)
Every next row contains the interval row-vector recurrence from its predecessor.
recurrence_checked :
∀ k : Fin (steps + 1),
VectorSubinterval (intervalVecMul (table k.castSucc) K) (table k.succ)
def terminal reviewed
⚑ flagged
Causalean.Mathlib.Probability.CertifiedFiniteMarkovExpectation.FiniteIterateCertificate
The penultimate stored interval vector is the finite-iterate approximation used for the stationary enclosure.
Definition (Lean source)
parameters
ι :
c :
def
def next reviewed
⚑ flagged
Causalean.Mathlib.Probability.CertifiedFiniteMarkovExpectation.FiniteIterateCertificate
The final stored interval vector encloses one further Markov step and is used to certify the finite-iterate residual.
Definition (Lean source)
theorem contractsL1_of_rationalMinorization reviewed
⚑ flagged
Causalean.Mathlib.Probability.CertifiedFiniteMarkovExpectation
Given a row-stochastic real transition matrix, its containment in an exact rational interval table, and a checked rational minorization certificate for that table, the kernel contracts finite probability vectors in total variation with coefficient one minus the certified minorization mass.
Formal statement
Proof (Lean source)
theorem contractsL1_of_rationalMinorization {ι : Type*} [Fintype ι]
{P : Matrix ι ι ℝ} {K : IntervalMatrix ι ι}
(hP : IsStochasticMatrix P) (hK : ContainsMatrix K P)
(c : RationalMinorizationCertificate K) :
ContractsL1 P (1 - (c.epsilon : ℝ)) := by
exact contractsL1_of_minorization hP (c.sound hK)
8 supporting declarations (lemmas, instances)
-
isProbabilitytheorem — An exact rational probability-vector certificate denotes a real probability vector.Proof (Lean source)
theorem RationalProbabilityVector.isProbability {ι : Type*} [Fintype ι] (p : RationalProbabilityVector ι) : IsProbabilityVector p.toReal := by unfold IsProbabilityVector RationalProbabilityVector.toReal constructor · intro i exact_mod_cast p.nonneg i · exact_mod_cast p.sum_eq_one -
step_probabilitytheorem — A stochastic matrix sends every probability row vector to a probability row vector.hypothesesconclusionProof (Lean source)
theorem IsStochasticMatrix.step_probability {ι : Type*} [Fintype ι] {P : Matrix ι ι ℝ} (hP : IsStochasticMatrix P) {p : ι → ℝ} (hp : IsProbabilityVector p) : IsProbabilityVector (markovStep p P) := by classical rcases hP with ⟨hP_nonneg, hP_sum⟩ rcases hp with ⟨hp_nonneg, hp_sum⟩ constructor · intro j unfold markovStep vecMul dotProduct exact sum_nonneg fun i _ => mul_nonneg (hp_nonneg i) (hP_nonneg i j) · unfold markovStep vecMul dotProduct rw [Finset.sum_comm] calc ∑ i, ∑ j, p i * P i j = ∑ i, p i * ∑ j, P i j := by congr 1 funext i rw [Finset.mul_sum] _ = ∑ i, p i := by simp only [hP_sum, mul_one] _ = 1 := hp_sum -
iterate_probabilitytheorem — Every finite iterate of a probability vector under a stochastic matrix is a probability vector.Proof (Lean source)
theorem IsStochasticMatrix.iterate_probability {ι : Type*} [Fintype ι] {P : Matrix ι ι ℝ} (hP : IsStochasticMatrix P) {p0 : ι → ℝ} (hp0 : IsProbabilityVector p0) (n : ℕ) : IsProbabilityVector (markovIterate P p0 n) := by induction n with | zero => exact hp0 | succ n ih => exact hP.step_probability ih -
soundtheorem — An exact rational minorization certificate soundly minorizes every real kernel contained in its interval table.Proof (Lean source)
theorem RationalMinorizationCertificate.sound {ι : Type*} [Fintype ι] {P : Matrix ι ι ℝ} {K : IntervalMatrix ι ι} (c : RationalMinorizationCertificate K) (hK : ContainsMatrix K P) : Minorizes P (c.epsilon : ℝ) c.nu.toReal := by refine ⟨c.nu.isProbability, ?_, ?_, ?_⟩ · exact_mod_cast c.epsilon_nonneg · exact_mod_cast c.epsilon_le_one · intro i j calc (c.epsilon : ℝ) * c.nu.toReal j = ((c.epsilon * c.nu.value j : ℚ) : ℝ) := by simp only [RationalProbabilityVector.toReal, Rat.cast_mul] _ ≤ ((K i j).lo : ℝ) := by exact_mod_cast c.lower_checked i j _ ≤ P i j := (hK i j).1 -
contractsL1_of_minorizationtheorem — Doeblin minorization by mass ε yields ℓ¹ contraction coefficient 1 - ε.hypothesesconclusionContractsL1 P (1 - ε)Proof (Lean source)
theorem contractsL1_of_minorization {ι : Type*} [Fintype ι] {P : Matrix ι ι ℝ} {ε : ℝ} {ν : ι → ℝ} (hP : IsStochasticMatrix P) (hminor : Minorizes P ε ν) : ContractsL1 P (1 - ε) := by classical rcases hP with ⟨hP_nonneg, hP_sum⟩ rcases hminor with ⟨hν, hε_nonneg, hε_le_one, hminor⟩ rcases hν with ⟨hν_nonneg, hν_sum⟩ intro p q hp hq rcases hp with ⟨hp_nonneg, hp_sum⟩ rcases hq with ⟨hq_nonneg, hq_sum⟩ let Q : Matrix ι ι ℝ := fun i j => P i j - ε * ν j have hQ_nonneg (i j : ι) : 0 ≤ Q i j := by dsimp [Q] linarith [hminor i j] have hQ_sum (i : ι) : ∑ j, Q i j = 1 - ε := by simp only [Q, Finset.sum_sub_distrib] rw [hP_sum] calc 1 - ∑ j, ε * ν j = 1 - ε * ∑ j, ν j := by rw [Finset.mul_sum] _ = 1 - ε := by rw [hν_sum, mul_one] have hcoord (j : ι) : markovStep p P j - markovStep q P j = ∑ i, (p i - q i) * Q i j := by unfold markovStep vecMul dotProduct simp_rw [show ∀ i, P i j = Q i j + ε * ν j by intro i simp only [Q] ring] simp_rw [mul_add] rw [Finset.sum_add_distrib, Finset.sum_add_distrib] have hp_common : ∑ i, p i * (ε * ν j) = ε * ν j := by rw [← Finset.sum_mul, hp_sum, one_mul] have hq_common : ∑ i, q i * (ε * ν j) = ε * ν j := by rw [← Finset.sum_mul, hq_sum, one_mul] rw [hp_common, hq_common] simp only [add_sub_add_right_eq_sub] rw [← Finset.sum_sub_distrib] congr 1 funext i ring unfold l1Distance simp_rw [hcoord] calc ∑ j, |∑ i, (p i - q i) * Q i j| ≤ ∑ j, ∑ i, |(p i - q i) * Q i j| := by exact Finset.sum_le_sum fun j _ => Finset.abs_sum_le_sum_abs _ _ _ = ∑ j, ∑ i, |p i - q i| * Q i j := by congr 1 funext j congr 1 funext i rw [abs_mul, abs_of_nonneg (hQ_nonneg i j)] _ = ∑ i, ∑ j, |p i - q i| * Q i j := Finset.sum_comm _ = ∑ i, |p i - q i| * (1 - ε) := by congr 1 funext i rw [← Finset.mul_sum, hQ_sum] _ = (1 - ε) * ∑ i, |p i - q i| := by rw [Finset.mul_sum] apply Finset.sum_congr rfl intro i hi ring -
table_soundtheorem — Every row of a checked finite interval recurrence contains the corresponding true Markov iterate for any real kernel enclosed by the certified table.hypothesesconclusionContainsVector (c.table k) (markovIterate P p0.toReal k)Proof (Lean source)
theorem FiniteIterateCertificate.table_sound {ι : Type*} [Fintype ι] {P : Matrix ι ι ℝ} {K : IntervalMatrix ι ι} {p0 : RationalProbabilityVector ι} (c : FiniteIterateCertificate K p0) (hK : ContainsMatrix K P) (k : Fin (c.steps + 2)) : ContainsVector (c.table k) (markovIterate P p0.toReal k) := by refine Fin.induction ?_ (fun k ih => ?_) k · intro i exact RatInterval.Contains.mono (c.initial_checked i) (RatInterval.point_sound (p0.value i)) · apply ContainsVector.mono (c.recurrence_checked k) exact intervalVecMul_sound ih hK -
terminal_soundtheorem — The terminal stored row contains the true iterate at the certificate's selected step.hypothesesconclusionContainsVector c.terminal (markovIterate P p0.toReal c.steps)Proof (Lean source)
theorem FiniteIterateCertificate.terminal_sound {ι : Type*} [Fintype ι] {P : Matrix ι ι ℝ} {K : IntervalMatrix ι ι} {p0 : RationalProbabilityVector ι} (c : FiniteIterateCertificate K p0) (hK : ContainsMatrix K P) : ContainsVector c.terminal (markovIterate P p0.toReal c.steps) := by exact c.table_sound hK (castSucc (last c.steps)) -
next_soundtheorem — The last stored row contains the true iterate one step after the selected terminal row.hypothesesconclusionContainsVector c.next (markovIterate P p0.toReal (c.steps + 1))Proof (Lean source)
theorem FiniteIterateCertificate.next_sound {ι : Type*} [Fintype ι] {P : Matrix ι ι ℝ} {K : IntervalMatrix ι ι} {p0 : RationalProbabilityVector ι} (c : FiniteIterateCertificate K p0) (hK : ContainsMatrix K P) : ContainsVector c.next (markovIterate P p0.toReal (c.steps + 1)) := by exact c.table_sound hK (last (c.steps + 1))
Stationary 11 core · 13 supporting This module turns a checked interval recurrence into an a posteriori fixed-point certificate. ★ stationaryRewardInterval_sound★ stationaryRewardInterval_sound_of_chunked
Finite-iterate enclosures of stationary distributions and rewards
This module turns a checked interval recurrence into an a posteriori fixed-point
certificate. An ℓ¹ contraction coefficient converts the last one-step
residual into a stationary-distribution radius; a certified reward bound then
converts that radius into a stationary-expectation interval.
def rewardExpectation reviewed
⚑ flagged
Causalean.Mathlib.Probability.CertifiedFiniteMarkovExpectation
The expectation of a finite reward vector under a real mass vector.
Definition (Lean source)
parameters
ι :
Type*
Fintype ι
p reward :
ι → ℝ
def
rewardExpectation p reward :
ℝ
given by
∑ i, p i * reward i
structure BoundedRewardCertificate reviewed
⚑ flagged
Causalean.Mathlib.Probability.CertifiedFiniteMarkovExpectation
A bounded reward certificate gives entrywise rational enclosures and an exact rational uniform absolute bound on all their endpoints.
Definition (Lean source)
parameters
ι :
Type*
Fintype ι
reward :
ι → ℝ
fields
Rational interval enclosure for each reward coordinate.
intervals :
Each real reward is contained in its coordinate interval.
contains :
ContainsVector intervals reward
Exact rational uniform absolute reward bound.
bound :
ℚ
The uniform bound is nonnegative.
bound_nonneg :
0 ≤ bound
Every interval endpoint has absolute value at most the uniform bound.
endpoints_bounded :
∀ i, (intervals i).maxAbs ≤ bound
def finiteIterateResidualBound reviewed
⚑ flagged
Causalean.Mathlib.Probability.CertifiedFiniteMarkovExpectation
The rational residual bound sums the maximum absolute endpoint of the difference between the terminal interval row and its certified successor.
Definition (Lean source)
parameters
ι :
c :
def
finiteIterateResidualBound c :
ℚ
given by
∑ i, ((c.terminal i).sub (c.next i)).maxAbs
def stationaryErrorRadius reviewed
⚑ flagged
Causalean.Mathlib.Probability.CertifiedFiniteMarkovExpectation
The a posteriori stationary radius is the residual bound divided by one minus the supplied exact rational contraction coefficient. It is a valid radius only for a coefficient strictly below one, as assumed by the enclosure results; at coefficient one the division by zero gives zero by convention.
Definition (Lean source)
parameters
ι :
c :
rho :
ℚ
def
stationaryErrorRadius c rho :
ℚ
given by
finiteIterateResidualBound c / (1 - rho)
def stationaryDistributionInterval reviewed
⚑ flagged
Causalean.Mathlib.Probability.CertifiedFiniteMarkovExpectation
The certified stationary-distribution enclosure expands each terminal coordinate interval by the common a posteriori ℓ¹ radius.
Definition (Lean source)
parameters
ι :
c :
rho :
ℚ
hrho0 :
0 ≤ rho
hrho1 :
rho < 1
def
given by
fun i
=> (c.terminal i).expand (stationaryErrorRadius c rho) (stationaryErrorRadius_nonneg c rho hrho0 hrho1)
def stationaryRewardInterval reviewed
⚑ flagged
Causalean.Mathlib.Probability.CertifiedFiniteMarkovExpectation
The stationary reward interval is the terminal interval expectation widened by the reward bound times the a posteriori stationary radius.
Definition (Lean source)
parameters
def
given by
(intervalExpectation c.terminal r.intervals).expand (r.bound * stationaryErrorRadius c rho) (mul_nonneg r.bound_nonneg (stationaryErrorRadius_nonneg c rho hrho0 hrho1))
theorem stationaryRewardInterval_sound reviewed
⚑ flagged
Causalean.Mathlib.Probability.CertifiedFiniteMarkovExpectation
Given a certified finite transition kernel, a checked finite interval recurrence, a certified bounded reward vector, a rational contraction coefficient, its nonnegativity, its strict upper bound by one, the corresponding contraction guarantee, and a stationary distribution, the computed rational interval contains that distribution's stationary reward expectation.
Formal statement
hypotheses
ι :
kernel :
c :
FiniteIterateCertificate kernel.intervals p0
r :
BoundedRewardCertificate reward
rho :
ℚ
hrho0 :
0 ≤ rho
hrho1 :
rho < 1
hcontract :
ContractsL1 P (rho : ℝ)
π :
ι → ℝ
hπ :
IsStationary P π
conclusion
(stationaryRewardInterval c r rho hrho0 hrho1).Contains (rewardExpectation π reward)
Proof (Lean source)
theorem stationaryRewardInterval_sound {ι : Type*} [Fintype ι]
{P : Matrix ι ι ℝ} {p0 : RationalProbabilityVector ι}
{reward : ι → ℝ} (kernel : CertifiedKernel P)
(c : FiniteIterateCertificate kernel.intervals p0)
(r : BoundedRewardCertificate reward)
(rho : ℚ) (hrho0 : 0 ≤ rho) (hrho1 : rho < 1)
(hcontract : ContractsL1 P (rho : ℝ))
{π : ι → ℝ} (hπ : IsStationary P π) :
(stationaryRewardInterval c r rho hrho0 hrho1).Contains
(rewardExpectation π reward) := by
let p := markovIterate P p0.toReal c.steps
have hterminal : ContainsVector c.terminal p := c.terminal_sound kernel.contains
have hbase : (intervalExpectation c.terminal r.intervals).Contains
(rewardExpectation p reward) := intervalDot_sound hterminal r.contains
have hl1 : l1Distance p π ≤ (stationaryErrorRadius c rho : ℝ) :=
finiteIterate_stationary_l1_le kernel c rho hrho0 hrho1 hcontract hπ
have hperturb : |rewardExpectation π reward - rewardExpectation p reward| ≤
(r.bound : ℝ) * (stationaryErrorRadius c rho : ℝ) :=
(by
rw [abs_sub_comm]
exact (abs_rewardExpectation_sub_le (by exact_mod_cast r.bound_nonneg)
r.bound_sound).trans
(mul_le_mul_of_nonneg_left hl1 (by exact_mod_cast r.bound_nonneg)))
change
((((intervalExpectation c.terminal r.intervals).lo -
r.bound * stationaryErrorRadius c rho : ℚ) : ℝ) ≤
rewardExpectation π reward ∧
rewardExpectation π reward ≤
(((intervalExpectation c.terminal r.intervals).hi +
r.bound * stationaryErrorRadius c rho : ℚ) : ℝ))
norm_num only [Rat.cast_sub, Rat.cast_add, Rat.cast_mul]
rcases hbase with ⟨hbase_lo, hbase_hi⟩
rcases abs_le.mp hperturb with ⟨hperturb_lo, hperturb_hi⟩
constructor <;> linarith
structure CoordinateRecurrenceCertificate reviewed
⚑ flagged
Causalean.Mathlib.Probability.CertifiedFiniteMarkovExpectation
A coordinate recurrence certificate records, for an interval transition matrix, a current interval vector, a next interval vector, and a chunk-size bound, one chunked dot-product certificate for each output coordinate.
Definition (Lean source)
parameters
fields
Chunked certificate for the dot product producing each next coordinate.
coordinate :
∀ j, ChunkedDotCertificate current (fun i => K i j) chunkSize (next j)
structure ChunkedFiniteIterateCertificate reviewed
⚑ flagged
Causalean.Mathlib.Probability.CertifiedFiniteMarkovExpectation
A chunked finite-iterate certificate stores a recurrence trace for an interval transition matrix from an exact rational initial distribution, using a number of approximation steps, a positive chunk-size bound and its positivity proof, the interval rows, initial coordinate checks, and bounded coordinate recurrence checks.
Definition (Lean source)
parameters
fields
Number of the penultimate iterate used by stationary enclosures.
steps :
ℕ
Maximum number of scalar products checked by any chunk leaf.
chunkSize :
ℕ
A chunk must contain at least one permitted slot.
chunkSize_pos :
0 < chunkSize
Interval vectors for iterates zero through `steps + 1`.
table :
Fin (steps + 2) → IntervalVector ι
Independently checked initial coordinate inclusions.
initial_checked :
∀ i, (RatInterval.point (p0.value i)).Subinterval (table 0 i)
Every recurrence step is certified coordinatewise with bounded chunks.
recurrence :
∀ k : Fin (steps + 1),
CoordinateRecurrenceCertificate K (table k.castSucc) (table k.succ) chunkSize
def toFiniteIterateCertificate reviewed
⚑ flagged
Causalean.Mathlib.Probability.CertifiedFiniteMarkovExpectation.ChunkedFiniteIterateCertificate
Given a chunked finite-iterate certificate, the corresponding established finite-iterate certificate is the same trace with each opaque coordinate proof composed into its recurrence field.
Definition (Lean source)
parameters
ι :
def
given by
clause 1
steps := c.steps
clause 2
table := c.table
clause 3
initial_checked := c.initial_checked
clause 4
recurrence_checked := by intro k exact (c.recurrence k).sound
theorem stationaryRewardInterval_sound_of_chunked reviewed
⚑ flagged
Causalean.Mathlib.Probability.CertifiedFiniteMarkovExpectation
Given a certified real kernel, a chunked finite-iterate certificate, a bounded reward certificate, a rational contraction coefficient that is nonnegative and strictly below one, the contraction property, and a stationary distribution, the stationary-reward interval obtained through the adapter contains the stationary reward expectation.
Formal statement
hypotheses
ι :
kernel :
c :
ChunkedFiniteIterateCertificate kernel.intervals p0
r :
BoundedRewardCertificate reward
rho :
ℚ
hrho0 :
0 ≤ rho
hrho1 :
rho < 1
hcontract :
ContractsL1 P (rho : ℝ)
π :
ι → ℝ
hπ :
IsStationary P π
conclusion
(stationaryRewardInterval c.toFiniteIterateCertificate r rho hrho0 hrho1).Contains (rewardExpectation π reward)
Proof (Lean source)
theorem stationaryRewardInterval_sound_of_chunked
{ι : Type*} [Fintype ι] [DecidableEq ι]
{P : Matrix ι ι ℝ} {p0 : RationalProbabilityVector ι}
{reward : ι → ℝ} (kernel : CertifiedKernel P)
(c : ChunkedFiniteIterateCertificate kernel.intervals p0)
(r : BoundedRewardCertificate reward)
(rho : ℚ) (hrho0 : 0 ≤ rho) (hrho1 : rho < 1)
(hcontract : ContractsL1 P (rho : ℝ))
{π : ι → ℝ} (hπ : IsStationary P π) :
(stationaryRewardInterval c.toFiniteIterateCertificate r rho hrho0 hrho1).Contains
(rewardExpectation π reward) := by
exact stationaryRewardInterval_sound kernel c.toFiniteIterateCertificate r
rho hrho0 hrho1 hcontract hπ
13 supporting declarations (lemmas, instances)
-
finiteIterateResidualBound_nonnegtheorem — The exact rational finite-iterate residual bound is nonnegative.hypothesesι :c :conclusionProof (Lean source)
theorem finiteIterateResidualBound_nonneg {ι : Type*} [Fintype ι] {K : IntervalMatrix ι ι} {p0 : RationalProbabilityVector ι} (c : FiniteIterateCertificate K p0) : 0 ≤ finiteIterateResidualBound c := by exact sum_nonneg fun i _ => le_max_of_le_left (abs_nonneg ((c.terminal i).sub (c.next i)).lo) -
stationaryErrorRadius_nonnegtheorem — A nonnegative contraction coefficient strictly below one gives a nonnegative a posteriori stationary error radius.hypothesesι :c :rho :ℚhrho0 :0 ≤ rhohrho1 :rho < 1conclusion0 ≤ stationaryErrorRadius c rhoProof (Lean source)
theorem stationaryErrorRadius_nonneg {ι : Type*} [Fintype ι] {K : IntervalMatrix ι ι} {p0 : RationalProbabilityVector ι} (c : FiniteIterateCertificate K p0) (rho : ℚ) (hrho0 : 0 ≤ rho) (hrho1 : rho < 1) : 0 ≤ stationaryErrorRadius c rho := by exact div_nonneg (finiteIterateResidualBound_nonneg c) (sub_nonneg.mpr hrho1.le) -
l1Distance_le_finiteIterateResidualBoundtheorem — Two real vectors enclosed by the terminal and successor rows have ℓ¹ distance at most the exact rational residual bound.hypothesesconclusionl1Distance x y ≤ (finiteIterateResidualBound c : ℝ)Proof (Lean source)
theorem l1Distance_le_finiteIterateResidualBound {ι : Type*} [Fintype ι] {K : IntervalMatrix ι ι} {p0 : RationalProbabilityVector ι} (c : FiniteIterateCertificate K p0) {x y : ι → ℝ} (hx : ContainsVector c.terminal x) (hy : ContainsVector c.next y) : l1Distance x y ≤ (finiteIterateResidualBound c : ℝ) := by unfold l1Distance finiteIterateResidualBound rw [Rat.cast_sum] exact Finset.sum_le_sum fun i _ => RatInterval.abs_le_maxAbs_of_contains _ (RatInterval.sub_sound (hx i) (hy i)) -
l1Distance_stationary_le_residualtheorem — An a posteriori contraction estimate bounds the distance from an approximate probability vector to any stationary distribution by its one-step residual divided by 1 - rho.hypothesesrho residual :ℝhp :hπ :IsStationary P πhcontract :ContractsL1 P rhohrho0 :0 ≤ rhohrho1 :rho < 1hresidual0 :0 ≤ residualhresidual :l1Distance p (markovStep p P) ≤ residualconclusionl1Distance p π ≤ residual / (1 - rho)Proof (Lean source)
theorem l1Distance_stationary_le_residual {ι : Type*} [Fintype ι] {P : Matrix ι ι ℝ} {p π : ι → ℝ} {rho residual : ℝ} (hp : IsProbabilityVector p) (hπ : IsStationary P π) (hcontract : ContractsL1 P rho) (hrho0 : 0 ≤ rho) (hrho1 : rho < 1) (hresidual0 : 0 ≤ residual) (hresidual : l1Distance p (markovStep p P) ≤ residual) : l1Distance p π ≤ residual / (1 - rho) := by have htriangle : l1Distance p π ≤ l1Distance p (markovStep p P) + l1Distance (markovStep p P) (markovStep π P) := by unfold l1Distance rw [← Finset.sum_add_distrib] exact Finset.sum_le_sum fun i _ => by calc |p i - π i| = |(p i - markovStep p P i) + (markovStep p P i - markovStep π P i)| := by rw [hπ.2]; ring _ ≤ |p i - markovStep p P i| + |markovStep p P i - markovStep π P i| := abs_add_le _ _ have hstep := hcontract p π hp hπ.1 have hmain : l1Distance p π ≤ residual + rho * l1Distance p π := htriangle.trans (add_le_add hresidual hstep) apply (le_div_iff₀ (sub_pos.mpr hrho1)).2 nlinarith -
abs_rewardExpectation_sub_letheorem — A bounded reward changes by at most its uniform absolute bound times the ℓ¹ distance between two mass vectors.hypothesesconclusionProof (Lean source)
theorem abs_rewardExpectation_sub_le {ι : Type*} [Fintype ι] {p q reward : ι → ℝ} {B : ℝ} (hB0 : 0 ≤ B) (hreward : ∀ i, |reward i| ≤ B) : |rewardExpectation p reward - rewardExpectation q reward| ≤ B * l1Distance p q := by unfold rewardExpectation l1Distance rw [← Finset.sum_sub_distrib] calc |∑ i, (p i * reward i - q i * reward i)| = |∑ i, (p i - q i) * reward i| := by congr 2 funext i ring _ ≤ ∑ i, |(p i - q i) * reward i| := Finset.abs_sum_le_sum_abs _ _ _ ≤ ∑ i, |p i - q i| * B := by apply Finset.sum_le_sum intro i hi rw [abs_mul] exact mul_le_mul_of_nonneg_left (hreward i) (abs_nonneg _) _ = B * ∑ i, |p i - q i| := by rw [Finset.mul_sum] apply Finset.sum_congr rfl intro i hi ring -
bound_soundtheorem — The endpoint check in a bounded reward certificate implies the semantic absolute bound for every true reward coordinate.hypothesesconclusion|reward i| ≤ (r.bound : ℝ)Proof (Lean source)
theorem BoundedRewardCertificate.bound_sound {ι : Type*} [Fintype ι] {reward : ι → ℝ} (r : BoundedRewardCertificate reward) (i : ι) : |reward i| ≤ (r.bound : ℝ) := by exact (RatInterval.abs_le_maxAbs_of_contains _ (r.contains i)).trans (by exact_mod_cast r.endpoints_bounded i) -
stationaryDistributionInterval_soundtheorem — A checked finite recurrence and a strict ℓ¹ contraction enclose every stationary distribution coordinate in the computed rational expansion of the terminal interval row.hypothesesι :kernel :c :FiniteIterateCertificate kernel.intervals p0rho :ℚhrho0 :0 ≤ rhohrho1 :rho < 1hcontract :ContractsL1 P (rho : ℝ)π :ι → ℝhπ :IsStationary P πconclusionContainsVector (stationaryDistributionInterval c rho hrho0 hrho1) πProof (Lean source)
theorem stationaryDistributionInterval_sound {ι : Type*} [Fintype ι] {P : Matrix ι ι ℝ} {p0 : RationalProbabilityVector ι} (kernel : CertifiedKernel P) (c : FiniteIterateCertificate kernel.intervals p0) (rho : ℚ) (hrho0 : 0 ≤ rho) (hrho1 : rho < 1) (hcontract : ContractsL1 P (rho : ℝ)) {π : ι → ℝ} (hπ : IsStationary P π) : ContainsVector (stationaryDistributionInterval c rho hrho0 hrho1) π := by let p := markovIterate P p0.toReal c.steps have hterminal : ContainsVector c.terminal p := c.terminal_sound kernel.contains have hl1 : l1Distance p π ≤ (stationaryErrorRadius c rho : ℝ) := finiteIterate_stationary_l1_le kernel c rho hrho0 hrho1 hcontract hπ intro i have hcoord : |p i - π i| ≤ (stationaryErrorRadius c rho : ℝ) := (Finset.single_le_sum (fun j _ => abs_nonneg (p j - π j)) (Finset.mem_univ i)).trans hl1 change ((((c.terminal i).lo - stationaryErrorRadius c rho : ℚ) : ℝ) ≤ π i ∧ π i ≤ (((c.terminal i).hi + stationaryErrorRadius c rho : ℚ) : ℝ)) norm_num only [Rat.cast_sub, Rat.cast_add] rcases hterminal i with ⟨hlo, hhi⟩ rcases abs_le.mp hcoord with ⟨hcoord_lo, hcoord_hi⟩ constructor <;> linarith -
stationaryRewardInterval_sound_of_minorizationtheorem — An exact rational minorization certificate supplies the contraction needed to certify the stationary reward interval with coefficient 1 - epsilon.hypothesesι :kernel :minor :RationalMinorizationCertificate kernel.intervalsc :FiniteIterateCertificate kernel.intervals p0r :BoundedRewardCertificate rewardhepsilon_pos :0 < minor.epsilonπ :ι → ℝhπ :IsStationary P πconclusion(stationaryRewardInterval c r (1 - minor.epsilon) (sub_nonneg.mpr minor.epsilon_le_one) (by linarith)).Contains (rewardExpectation π reward)Proof (Lean source)
theorem stationaryRewardInterval_sound_of_minorization {ι : Type*} [Fintype ι] {P : Matrix ι ι ℝ} {p0 : RationalProbabilityVector ι} {reward : ι → ℝ} (kernel : CertifiedKernel P) (minor : RationalMinorizationCertificate kernel.intervals) (c : FiniteIterateCertificate kernel.intervals p0) (r : BoundedRewardCertificate reward) (hepsilon_pos : 0 < minor.epsilon) {π : ι → ℝ} (hπ : IsStationary P π) : (stationaryRewardInterval c r (1 - minor.epsilon) (sub_nonneg.mpr minor.epsilon_le_one) (by linarith)).Contains (rewardExpectation π reward) := by apply stationaryRewardInterval_sound kernel c r (1 - minor.epsilon) (sub_nonneg.mpr minor.epsilon_le_one) (by linarith) _ hπ simpa only [Rat.cast_sub, Rat.cast_one] using contractsL1_of_rationalMinorization kernel.stochastic kernel.contains minor -
existsUnique_stationary_and_reward_enclosedtheorem — For a nonempty state space, the checked recurrence and contraction both produce a unique stationary distribution and certify its reward expectation.hypothesesι :kernel :c :FiniteIterateCertificate kernel.intervals p0r :BoundedRewardCertificate rewardrho :ℚhrho0 :0 ≤ rhohrho1 :rho < 1hcontract :ContractsL1 P (rho : ℝ)conclusion∃! π : ι → ℝ,conclusion 1IsStationary P πconclusion 2(stationaryRewardInterval c r rho hrho0 hrho1).Contains (rewardExpectation π reward)Proof (Lean source)
theorem existsUnique_stationary_and_reward_enclosed {ι : Type*} [Fintype ι] [Nonempty ι] {P : Matrix ι ι ℝ} {p0 : RationalProbabilityVector ι} {reward : ι → ℝ} (kernel : CertifiedKernel P) (c : FiniteIterateCertificate kernel.intervals p0) (r : BoundedRewardCertificate reward) (rho : ℚ) (hrho0 : 0 ≤ rho) (hrho1 : rho < 1) (hcontract : ContractsL1 P (rho : ℝ)) : ∃! π : ι → ℝ, IsStationary P π ∧ (stationaryRewardInterval c r rho hrho0 hrho1).Contains (rewardExpectation π reward) := by obtain ⟨π, hπ, hunique⟩ := existsUnique_stationary_of_contractsL1 kernel.stochastic (by exact_mod_cast hrho0) (by exact_mod_cast hrho1) hcontract refine ⟨π, ⟨hπ, stationaryRewardInterval_sound kernel c r rho hrho0 hrho1 hcontract hπ⟩, ?_⟩ intro π' hπ' exact hunique π' hπ'.1 -
soundtheorem — When a coordinate recurrence certificate is supplied, the interval row-vector recurrence refines the reported next interval vector.hypothesesconclusionProof (Lean source)
theorem CoordinateRecurrenceCertificate.sound {ι : Type*} [Fintype ι] [DecidableEq ι] {K : IntervalMatrix ι ι} {current next : IntervalVector ι} {chunkSize : ℕ} (c : CoordinateRecurrenceCertificate K current next chunkSize) : VectorSubinterval (intervalVecMul current K) next := by intro j exact (c.coordinate j).sound -
table_soundtheorem — Given a chunked finite-iterate certificate, a real transition matrix enclosed by its interval matrix, and a selected trace row, that row contains the corresponding exact Markov iterate.hypothesesconclusionContainsVector (c.table k) (markovIterate P p0.toReal k)Proof (Lean source)
theorem ChunkedFiniteIterateCertificate.table_sound {ι : Type*} [Fintype ι] [DecidableEq ι] {P : Matrix ι ι ℝ} {K : IntervalMatrix ι ι} {p0 : RationalProbabilityVector ι} (c : ChunkedFiniteIterateCertificate K p0) (hK : ContainsMatrix K P) (k : Fin (c.steps + 2)) : ContainsVector (c.table k) (markovIterate P p0.toReal k) := by exact c.toFiniteIterateCertificate.table_sound hK k -
adapter_rowstheorem — When a chunked finite-iterate certificate is supplied, its adapter has exactly the same table, terminal row, and successor row.hypothesesι :Proof (Lean source)
theorem ChunkedFiniteIterateCertificate.adapter_rows {ι : Type*} [Fintype ι] [DecidableEq ι] {K : IntervalMatrix ι ι} {p0 : RationalProbabilityVector ι} (c : ChunkedFiniteIterateCertificate K p0) : c.toFiniteIterateCertificate.table = c.table ∧ c.toFiniteIterateCertificate.terminal = c.table (castSucc (last c.steps)) ∧ c.toFiniteIterateCertificate.next = c.table (last (c.steps + 1)) := by exact ⟨rfl, rfl, rfl⟩ -
stationaryRewardInterval_sound_of_minorization_chunkedtheorem — Given a certified real kernel, a rational minorization certificate, a chunked finite-iterate certificate, a bounded reward certificate, positive minorization mass, and a stationary distribution, the stationary-reward interval at coefficient one minus the minorization mass contains the stationary reward expectation.hypothesesι :kernel :minor :RationalMinorizationCertificate kernel.intervalsc :ChunkedFiniteIterateCertificate kernel.intervals p0r :BoundedRewardCertificate rewardhepsilon_pos :0 < minor.epsilonπ :ι → ℝhπ :IsStationary P πconclusion(stationaryRewardInterval c.toFiniteIterateCertificate r (1 - minor.epsilon) (sub_nonneg.mpr minor.epsilon_le_one) (by linarith)).Contains (rewardExpectation π reward)Proof (Lean source)
theorem stationaryRewardInterval_sound_of_minorization_chunked {ι : Type*} [Fintype ι] [DecidableEq ι] {P : Matrix ι ι ℝ} {p0 : RationalProbabilityVector ι} {reward : ι → ℝ} (kernel : CertifiedKernel P) (minor : RationalMinorizationCertificate kernel.intervals) (c : ChunkedFiniteIterateCertificate kernel.intervals p0) (r : BoundedRewardCertificate reward) (hepsilon_pos : 0 < minor.epsilon) {π : ι → ℝ} (hπ : IsStationary P π) : (stationaryRewardInterval c.toFiniteIterateCertificate r (1 - minor.epsilon) (sub_nonneg.mpr minor.epsilon_le_one) (by linarith)).Contains (rewardExpectation π reward) := by exact stationaryRewardInterval_sound_of_minorization kernel minor c.toFiniteIterateCertificate r hepsilon_pos hπ
Comparison 2 core · 3 supporting This module provides the final order-theoretic comparison step. ★ stationaryExpectation_lt_of_certified_intervals
Strict comparison of certified stationary expectations
This module provides the final order-theoretic comparison step. Disjoint rational enclosures for two stationary expectations certify a strict ordering, and subtracting a common benchmark turns the same ordering into a strict bias comparison between two policies.
def stationaryBias reviewed
⚑ flagged
Causalean.Mathlib.Probability.CertifiedFiniteMarkovExpectation
The stationary bias of a reward process relative to a benchmark is the reward expectation under a supplied weight vector minus that benchmark. No condition is imposed on the vector; it is the bias of the stationary reward when the vector is the stationary distribution.
Definition (Lean source)
parameters
def
stationaryBias π reward benchmark :
ℝ
given by
rewardExpectation π reward - benchmark
theorem stationaryExpectation_lt_of_certified_intervals reviewed
⚑ flagged
Causalean.Mathlib.Probability.CertifiedFiniteMarkovExpectation
Given the first certified policy kernel, the second certified policy kernel, their checked finite interval recurrences, a certified bounded reward vector, their rational contraction coefficients, the first coefficient's nonnegativity and strict upper bound, the second coefficient's nonnegativity and strict upper bound, the two contraction guarantees, their stationary distributions, and strictly separated computed reward intervals, the first stationary reward expectation is strictly smaller than the second.
Formal statement
hypotheses
ι :
kernelP :
kernelQ :
iterateP :
FiniteIterateCertificate kernelP.intervals p0P
iterateQ :
FiniteIterateCertificate kernelQ.intervals p0Q
rewardCert :
BoundedRewardCertificate reward
rhoP rhoQ :
ℚ
hrhoP0 :
0 ≤ rhoP
hrhoP1 :
rhoP < 1
hrhoQ0 :
0 ≤ rhoQ
hrhoQ1 :
rhoQ < 1
hcontractP :
ContractsL1 P (rhoP : ℝ)
hcontractQ :
ContractsL1 Q (rhoQ : ℝ)
πP πQ :
ι → ℝ
hπP :
IsStationary P πP
hπQ :
IsStationary Q πQ
hsep :
(stationaryRewardInterval iterateP rewardCert rhoP hrhoP0 hrhoP1).hi < (stationaryRewardInterval iterateQ rewardCert rhoQ hrhoQ0 hrhoQ1).lo
conclusion
rewardExpectation πP reward < rewardExpectation πQ reward
Proof (Lean source)
theorem stationaryExpectation_lt_of_certified_intervals
{ι : Type*} [Fintype ι]
{P Q : Matrix ι ι ℝ}
{p0P p0Q : RationalProbabilityVector ι}
{reward : ι → ℝ}
(kernelP : CertifiedKernel P) (kernelQ : CertifiedKernel Q)
(iterateP : FiniteIterateCertificate kernelP.intervals p0P)
(iterateQ : FiniteIterateCertificate kernelQ.intervals p0Q)
(rewardCert : BoundedRewardCertificate reward)
(rhoP rhoQ : ℚ)
(hrhoP0 : 0 ≤ rhoP) (hrhoP1 : rhoP < 1)
(hrhoQ0 : 0 ≤ rhoQ) (hrhoQ1 : rhoQ < 1)
(hcontractP : ContractsL1 P (rhoP : ℝ))
(hcontractQ : ContractsL1 Q (rhoQ : ℝ))
{πP πQ : ι → ℝ} (hπP : IsStationary P πP) (hπQ : IsStationary Q πQ)
(hsep :
(stationaryRewardInterval iterateP rewardCert rhoP hrhoP0 hrhoP1).hi <
(stationaryRewardInterval iterateQ rewardCert rhoQ hrhoQ0 hrhoQ1).lo) :
rewardExpectation πP reward < rewardExpectation πQ reward := by
-- Obtain both semantic containment facts from `stationaryRewardInterval_sound`,
-- then apply `lt_of_disjoint_enclosures` to the checked endpoint separation.
apply lt_of_disjoint_enclosures
· exact stationaryRewardInterval_sound kernelP iterateP rewardCert rhoP
hrhoP0 hrhoP1 hcontractP hπP
· exact stationaryRewardInterval_sound kernelQ iterateQ rewardCert rhoQ
hrhoQ0 hrhoQ1 hcontractQ hπQ
· exact hsep
3 supporting declarations (lemmas, instances)
-
lt_of_disjoint_enclosurestheorem — If two rational intervals contain two real values and the first upper endpoint is below the second lower endpoint, then the first value is strictly smaller.hypothesesconclusionx < yProof (Lean source)
theorem lt_of_disjoint_enclosures {I J : RatInterval} {x y : ℝ} (hx : I.Contains x) (hy : J.Contains y) (hsep : I.hi < J.lo) : x < y := by -- Cast the exact rational endpoint separation to `ℝ`, then chain the upper -- containment inequality for `x` with the lower containment inequality for `y`. have hsep_real : (I.hi : ℝ) < (J.lo : ℝ) := by exact_mod_cast hsep exact hx.2.trans_lt (hsep_real.trans_le hy.1) -
stationaryBias_lt_of_expectation_lttheorem — Strict ordering of two stationary reward expectations is preserved after subtracting the same real benchmark, yielding a strict stationary-bias comparison.hypothesesconclusionstationaryBias πP reward benchmark < stationaryBias πQ reward benchmarkProof (Lean source)
theorem stationaryBias_lt_of_expectation_lt {ι : Type*} [Fintype ι] {πP πQ reward : ι → ℝ} {benchmark : ℝ} (h : rewardExpectation πP reward < rewardExpectation πQ reward) : stationaryBias πP reward benchmark < stationaryBias πQ reward benchmark := by -- Unfold the common-benchmark subtraction and use strict-order compatibility. simpa only [stationaryBias] using sub_lt_sub_right h benchmark -
stationaryBias_lt_of_certified_intervalstheorem — For two certified policy kernels, disjoint stationary-expectation intervals imply a strict comparison of their stationary biases relative to any common benchmark.hypothesesι :kernelP :kernelQ :iterateP :FiniteIterateCertificate kernelP.intervals p0PiterateQ :FiniteIterateCertificate kernelQ.intervals p0QrewardCert :BoundedRewardCertificate rewardrhoP rhoQ :ℚhrhoP0 :0 ≤ rhoPhrhoP1 :rhoP < 1hrhoQ0 :0 ≤ rhoQhrhoQ1 :rhoQ < 1hcontractP :ContractsL1 P (rhoP : ℝ)hcontractQ :ContractsL1 Q (rhoQ : ℝ)πP πQ :ι → ℝhπP :IsStationary P πPhπQ :IsStationary Q πQbenchmark :ℝhsep :(stationaryRewardInterval iterateP rewardCert rhoP hrhoP0 hrhoP1).hi < (stationaryRewardInterval iterateQ rewardCert rhoQ hrhoQ0 hrhoQ1).loconclusionstationaryBias πP reward benchmark < stationaryBias πQ reward benchmarkProof (Lean source)
theorem stationaryBias_lt_of_certified_intervals {ι : Type*} [Fintype ι] {P Q : Matrix ι ι ℝ} {p0P p0Q : RationalProbabilityVector ι} {reward : ι → ℝ} (kernelP : CertifiedKernel P) (kernelQ : CertifiedKernel Q) (iterateP : FiniteIterateCertificate kernelP.intervals p0P) (iterateQ : FiniteIterateCertificate kernelQ.intervals p0Q) (rewardCert : BoundedRewardCertificate reward) (rhoP rhoQ : ℚ) (hrhoP0 : 0 ≤ rhoP) (hrhoP1 : rhoP < 1) (hrhoQ0 : 0 ≤ rhoQ) (hrhoQ1 : rhoQ < 1) (hcontractP : ContractsL1 P (rhoP : ℝ)) (hcontractQ : ContractsL1 Q (rhoQ : ℝ)) {πP πQ : ι → ℝ} (hπP : IsStationary P πP) (hπQ : IsStationary Q πQ) {benchmark : ℝ} (hsep : (stationaryRewardInterval iterateP rewardCert rhoP hrhoP0 hrhoP1).hi < (stationaryRewardInterval iterateQ rewardCert rhoQ hrhoQ0 hrhoQ1).lo) : stationaryBias πP reward benchmark < stationaryBias πQ reward benchmark := by -- First invoke the assembled expectation comparison above, then translate it -- through `stationaryBias_lt_of_expectation_lt`. apply stationaryBias_lt_of_expectation_lt exact stationaryExpectation_lt_of_certified_intervals kernelP kernelQ iterateP iterateQ rewardCert rhoP rhoQ hrhoP0 hrhoP1 hrhoQ0 hrhoQ1 hcontractP hcontractQ hπP hπQ hsep
Existence 1 core · 2 supporting This module isolates the topological fixed-point argument for finite stochastic kernels. ★ existsUnique_stationary_of_contractsL1
Existence and uniqueness of finite stationary distributions
This module isolates the topological fixed-point argument for finite stochastic
kernels. Existence uses compactness of the finite probability simplex, while
strict ℓ¹ contraction supplies uniqueness. It also records the bridges from this library's
probability-vector and row-stochastic predicates to Mathlib's standard simplex and
Matrix.rowStochastic.
theorem existsUnique_stationary_of_contractsL1 reviewed
⚑ flagged
Causalean.Mathlib.Probability.CertifiedFiniteMarkovExpectation
On a nonempty finite state space, given a row-stochastic transition matrix, a nonnegative contraction coefficient, the fact that the coefficient is strictly below one, and a total-variation contraction bound, there is exactly one stationary probability distribution.
Formal statement
hypotheses
conclusion
∃! π : ι → ℝ, IsStationary P π
Proof (Lean source)
theorem existsUnique_stationary_of_contractsL1 {ι : Type*}
[Fintype ι] [Nonempty ι]
{P : Matrix ι ι ℝ} {rho : ℝ}
(hP : IsStochasticMatrix P) (hrho0 : 0 ≤ rho) (hrho1 : rho < 1)
(hcontract : ContractsL1 P rho) :
∃! π : ι → ℝ, IsStationary P π := by
classical
let i₀ : ι := Classical.choice inferInstance
let p₀ : ι → ℝ := single i₀ 1
have hp₀ : IsProbabilityVector p₀ := by
change p₀ ∈ stdSimplex ℝ ι
simpa only [p₀] using single_mem_stdSimplex ℝ i₀
let p : ℕ → (ι → ℝ) := markovIterate P p₀
have hp (n : ℕ) : IsProbabilityVector (p n) := hP.iterate_probability hp₀ n
have hl1_nonneg (q r : ι → ℝ) : 0 ≤ l1Distance q r := by
exact sum_nonneg fun _ _ => abs_nonneg _
let d : ℕ → ℝ := fun n => l1Distance (p (n + 1)) (p n)
have hd_le (n : ℕ) : d n ≤ rho ^ n * d 0 := by
induction n with
| zero => simp
| succ n ih =>
calc
d (n + 1) = l1Distance (markovStep (p (n + 1)) P)
(markovStep (p n) P) := by
simp only [d, p, markovIterate]
_ ≤ rho * l1Distance (p (n + 1)) (p n) :=
hcontract _ _ (hp (n + 1)) (hp n)
_ = rho * d n := rfl
_ ≤ rho * (rho ^ n * d 0) := mul_le_mul_of_nonneg_left ih hrho0
_ = rho ^ (n + 1) * d 0 := by rw [pow_succ]; ring
have hd_tendsto : Tendsto d atTop (nhds 0) := by
have hu : Tendsto (fun n => rho ^ n * d 0) atTop (nhds 0) := by
simpa using (tendsto_pow_atTop_nhds_zero_of_lt_one hrho0 hrho1).mul_const (d 0)
apply tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds hu
· exact Filter.Eventually.of_forall fun n => hl1_nonneg _ _
· exact Filter.Eventually.of_forall hd_le
have hp_simplex (n : ℕ) : p n ∈ stdSimplex ℝ ι := hp n
obtain ⟨π, hπ_prob, φ, hφ, hφ_tendsto⟩ :=
(isCompact_stdSimplex ℝ ι).tendsto_subseq hp_simplex
have hd_subseq : Tendsto (fun n => d (φ n)) atTop (nhds 0) :=
hd_tendsto.comp hφ.tendsto_atTop
have hshift : Tendsto (fun n => p (φ n + 1)) atTop (nhds π) := by
rw [tendsto_pi_nhds]
intro i
have habs (n : ℕ) : |p (φ n + 1) i - p (φ n) i| ≤ d (φ n) := by
apply Finset.single_le_sum (fun j _ => abs_nonneg (p (φ n + 1) j - p (φ n) j))
exact Finset.mem_univ i
have hdiff : Tendsto (fun n => p (φ n + 1) i - p (φ n) i)
atTop (nhds 0) := by
have hneg : Tendsto (fun n => -d (φ n)) atTop (nhds 0) := by
simpa using hd_subseq.neg
apply tendsto_of_tendsto_of_tendsto_of_le_of_le' hneg hd_subseq
· exact Filter.Eventually.of_forall fun n => (neg_le_of_abs_le (habs n))
· exact Filter.Eventually.of_forall fun n => (le_of_abs_le (habs n))
convert (hφ_tendsto.apply_nhds i).add hdiff using 1 <;> simp
have hstep : Tendsto (fun n => markovStep (p (φ n)) P)
atTop (nhds (markovStep π P)) := by
rw [tendsto_pi_nhds]
intro j
unfold markovStep vecMul dotProduct
apply tendsto_finsetSum
intro i hi
exact (hφ_tendsto.apply_nhds i).mul tendsto_const_nhds
have hshift_step : Tendsto (fun n => p (φ n + 1))
atTop (nhds (markovStep π P)) := by
convert hstep using 1
funext n
simp only [p, markovIterate]
have hfixed : markovStep π P = π := tendsto_nhds_unique hshift_step hshift
refine ⟨π, ⟨hπ_prob, hfixed⟩, ?_⟩
intro π' hπ'
have hdist_le : l1Distance π' π ≤ rho * l1Distance π' π := by
calc
l1Distance π' π = l1Distance (markovStep π' P) (markovStep π P) := by
rw [hπ'.2, hfixed]
_ ≤ rho * l1Distance π' π := hcontract _ _ hπ'.1 hπ_prob
have hdist_zero : l1Distance π' π = 0 := by
nlinarith [hl1_nonneg π' π]
funext i
have hi : |π' i - π i| ≤ l1Distance π' π := by
apply Finset.single_le_sum (fun j _ => abs_nonneg (π' j - π j))
exact Finset.mem_univ i
rw [hdist_zero] at hi
exact sub_eq_zero.mp (abs_eq_zero.mp (le_antisymm hi (abs_nonneg _)))
2 supporting declarations (lemmas, instances)
-
isProbabilityVector_iff_mem_stdSimplextheorem — A real vector is a probability vector exactly when it lies in the standard simplex.Proof (Lean source)
theorem isProbabilityVector_iff_mem_stdSimplex {ι : Type*} [Fintype ι] (p : ι → ℝ) : IsProbabilityVector p ↔ p ∈ stdSimplex ℝ ι := Iff.rfl -
isStochasticMatrix_iff_mem_rowStochastictheorem — For a real square matrix indexed by a finite state space, being row-stochastic, with nonnegative entries and every row summing to one, is equivalent to membership in Mathlib's submonoid of row-stochastic matrices.Proof (Lean source)
theorem isStochasticMatrix_iff_mem_rowStochastic {ι : Type*} [Fintype ι] [DecidableEq ι] (P : Matrix ι ι ℝ) : IsStochasticMatrix P ↔ P ∈ rowStochastic ℝ ι := Matrix.mem_rowStochastic_iff_sum.symm
NormalCDF 9 core · 7 supporting This module gives an executable, exact-rational checker for standard-normal CDF values at rational endpoints. ★ sound
Certified rational enclosures for the standard normal CDF
This module gives an executable, exact-rational checker for standard-normal CDF values at rational endpoints. It combines Causalean's certified Machin enclosure for π, Newton square-root enclosure, exponential enclosure, and a rigorously widened trapezoidal rule. A caller may enlarge the computed result, but cannot introduce a decimal endpoint without proving an exact rational subinterval check.
Scaling limitation — read before instantiating
The trapezoidal rule here uses a UNIFORM mesh, so the node count is set by the
worst-behaved part of the interval rather than by local curvature. Away from the
origin this is severe: at endpoint 193/5 with target width 1e-12 the mesh floor
forces more than 5.7e16 exact-rational nodes, which is sound but not computable in
practice. The checker is therefore usable for narrow targets near the origin and
unusable for tight enclosures at large endpoints.
A caller needing the latter wants a symmetry + central-series + Mills-tail construction instead, which spends nodes only where the integrand is hard. Nothing here is wrong; it is a question of which regime applies.
def twoPiInterval reviewed
⚑ flagged
Causalean.Mathlib.Probability.CertifiedFiniteMarkovExpectation
The interval enclosing 2π at a chosen exact arithmetic fuel level.
Definition (Lean source)
structure NormalCDFSchedule reviewed
⚑ flagged
Causalean.Mathlib.Probability.CertifiedFiniteMarkovExpectation
A normal-CDF schedule records a positive mesh and the exact rational side conditions needed to invert the computed enclosure of sqrt (2π).
Definition (Lean source)
fields
Precision used by the π, square-root, and exponential interval evaluators.
fuel :
ℕ
Number of cells in the certified trapezoidal quadrature.
mesh :
ℕ
The quadrature mesh is nonempty.
mesh_pos :
0 < mesh
The computed lower endpoint for `2π` is nonnegative.
twoPi_nonneg :
0 ≤ (twoPiInterval fuel).lo
The computed square-root interval excludes zero, so its reciprocal is sound.
sqrt_away :
(RatInterval.sqrtInterval (twoPiInterval fuel) twoPi_nonneg fuel).AwayFromZero
def normalDensityScaleInterval reviewed
⚑ flagged
Causalean.Mathlib.Probability.CertifiedFiniteMarkovExpectation
The certified rational enclosure of the standard-normal density's scale factor 1 / sqrt (2π) for a schedule.
Definition (Lean source)
parameters
def
given by
root :
RatInterval.sqrtInterval (twoPiInterval s.fuel) s.twoPi_nonneg s.fuel
root.inv s.sqrt_away
def normalDensityNode reviewed
⚑ flagged
Causalean.Mathlib.Probability.CertifiedFiniteMarkovExpectation
For a rational endpoint q, a schedule, and a natural node index k, this interval encloses the rescaled Gaussian integrand at the point q k / mesh used for CDF quadrature. The quadrature applies it to nonnegative endpoints and node indices up to the mesh size; no such restriction is imposed here.
Definition (Lean source)
parameters
def
given by
x :
q * k / s.mesh (: ℚ)
exponent :
-(x ^ 2) / 2 (: ℚ)
((RatInterval.point q).mul (normalDensityScaleInterval s)).mul (Transcendental.expInterval (RatInterval.point exponent) s.fuel)
def normalDensityComplexNode reviewed
⚑ flagged
Causalean.Mathlib.Probability.CertifiedFiniteMarkovExpectation
The complex rectangle obtained from a real Gaussian quadrature node by adjoining the point interval at zero as imaginary coordinate.
Definition (Lean source)
parameters
def
given by
⟨normalDensityNode q s k, RatInterval.point 0⟩
def nonnegativeNormalIntegralInterval reviewed
⚑ flagged
Causalean.Mathlib.Probability.CertifiedFiniteMarkovExpectation
For a nonnegative rational endpoint, the computed interval encloses the integral of the standard-normal density from zero to that endpoint.
Definition (Lean source)
parameters
def
given by
(CircleMesh.integralEnclosure (normalDensityComplexNode q s) (q ^ 3) (pow_nonneg hq 3) s.mesh s.mesh_pos).re
def normalCDFInterval reviewed
⚑ flagged
Causalean.Mathlib.Probability.CertifiedFiniteMarkovExpectation
The internally computed rational enclosure of the standard-normal CDF at any rational endpoint, using symmetry for negative endpoints.
Definition (Lean source)
parameters
q :
ℚ
def
given by
positive :
(RatInterval.point (1 / 2)).add (nonnegativeNormalIntegralInterval |q| (abs_nonneg q) s)
if 0 ≤ q then positive else (RatInterval.point 1).sub positive
structure NormalCDFCertificate reviewed
⚑ flagged
Causalean.Mathlib.Probability.CertifiedFiniteMarkovExpectation
A standard-normal CDF certificate consists of a checked internal schedule, a caller-facing rational interval, and an exact proof that the internally computed interval refines the caller-facing one.
Definition (Lean source)
parameters
q :
ℚ
fields
Internal exact-arithmetic evaluation schedule.
schedule :
Rational interval reported in the caller's endpoint table.
enclosure :
Exact rational refinement check connecting the reported interval to the evaluator.
checked :
(normalCDFInterval q schedule).Subinterval enclosure
theorem sound reviewed
⚑ flagged
Causalean.Mathlib.Probability.CertifiedFiniteMarkovExpectation.NormalCDFCertificate
Given a checked rational certificate at a rational endpoint, the certificate's reported interval contains the true standard-normal cumulative probability at that endpoint.
Formal statement
Proof (Lean source)
theorem NormalCDFCertificate.sound {q : ℚ} (c : NormalCDFCertificate q) :
c.enclosure.Contains (stdNormalCDF (q : ℝ)) := by
exact (normalCDFInterval_sound q c.schedule).mono c.checked
7 supporting declarations (lemmas, instances)
-
normalDensityScaleInterval_soundtheorem — The executable density-scale interval contains the mathematical constant 1 / sqrt (2π).hypothesesconclusionProof (Lean source)
theorem normalDensityScaleInterval_sound (s : NormalCDFSchedule) : (normalDensityScaleInterval s).Contains (1 / sqrt (2 * pi)) := by dsimp [normalDensityScaleInterval] rw [one_div] apply RatInterval.inv_sound s.sqrt_away apply RatInterval.sqrtInterval_sound s.twoPi_nonneg simpa [twoPiInterval] using RatInterval.mul_sound (RatInterval.point_sound 2) (Complex.Transcendental.piInterval_sound s.fuel) -
normalDensityNode_soundtheorem — Every computed Gaussian quadrature node contains the corresponding value of the rescaled standard-normal density.hypothesesconclusion(normalDensityNode q s k).Contains ((q : ℝ) * stdNormalPDF ((q : ℝ) * CircleMesh.meshPoint s.mesh k))Proof (Lean source)
theorem normalDensityNode_sound (q : ℚ) (hq : 0 ≤ q) (s : NormalCDFSchedule) (k : ℕ) : (normalDensityNode q s k).Contains ((q : ℝ) * stdNormalPDF ((q : ℝ) * CircleMesh.meshPoint s.mesh k)) := by have hscale := normalDensityScaleInterval_sound s have hexp := Transcendental.expInterval_sound (RatInterval.point_sound (-(q * k / s.mesh) ^ 2 / 2)) s.fuel have h := RatInterval.mul_sound (RatInterval.mul_sound (RatInterval.point_sound q) hscale) hexp convert h using 1 all_goals simp [normalDensityNode, stdNormalPDF, gaussianPDFReal, CircleMesh.meshPoint] all_goals ring -
rescaledNormalDensity_lipschitztheorem — The rescaled standard-normal density on the unit interval is Lipschitz with the exact rational constant q³ for every nonnegative rational q.hypothesesq :ℚhq :0 ≤ qu ∈ Icc (0 : ℝ) 1 :v ∈ Icc (0 : ℝ) 1 :conclusionProof (Lean source)
theorem rescaledNormalDensity_lipschitz (q : ℚ) (hq : 0 ≤ q) : ∀ u ∈ Icc (0 : ℝ) 1, ∀ v ∈ Icc (0 : ℝ) 1, |(q : ℝ) * stdNormalPDF ((q : ℝ) * u) - (q : ℝ) * stdNormalPDF ((q : ℝ) * v)| ≤ (q ^ 3 : ℚ) * |u - v| := by let F : ℝ → ℝ := fun x => (q : ℝ) * ((sqrt (2 * pi))⁻¹ * exp (-((q : ℝ) * x) ^ 2 / 2)) have hF (x : ℝ) : F x = (q : ℝ) * stdNormalPDF ((q : ℝ) * x) := by simp [F, stdNormalPDF, gaussianPDFReal] have hqR : (0 : ℝ) ≤ q := by exact_mod_cast hq have hscale_nonneg : 0 ≤ (sqrt (2 * pi))⁻¹ := by positivity have hscale_le_one : (sqrt (2 * pi))⁻¹ ≤ 1 := by have hsqrt : 1 ≤ sqrt (2 * pi) := by rw [Real.one_le_sqrt] nlinarith [Real.pi_gt_three] exact (inv_le_one₀ (by positivity)).2 hsqrt have hderiv (x : ℝ) : HasDerivAt F (-((q : ℝ) ^ 3) * (sqrt (2 * pi))⁻¹ * x * exp (-((q : ℝ) * x) ^ 2 / 2)) x := by have hi : HasDerivAt (fun y : ℝ => -((q : ℝ) * y) ^ 2 / 2) (-((q : ℝ) ^ 2) * x) x := by convert (((hasDerivAt_id x).const_mul (q : ℝ)).pow 2).neg.div_const 2 using 1 <;> try rfl all_goals simp only [id_eq] all_goals ring dsimp [F] convert ((hi.exp.const_mul (sqrt (2 * pi))⁻¹).const_mul (q : ℝ)) using 1 <;> try rfl all_goals ring have hbound : ∀ x ∈ Icc (0 : ℝ) 1, ‖-((q : ℝ) ^ 3) * (sqrt (2 * pi))⁻¹ * x * exp (-((q : ℝ) * x) ^ 2 / 2)‖ ≤ (q : ℝ) ^ 3 := by intro x hx rcases hx with ⟨hx0, hx1⟩ rw [Real.norm_eq_abs, abs_mul, abs_mul, abs_mul, abs_neg, abs_of_nonneg (pow_nonneg hqR 3), abs_of_nonneg hscale_nonneg, abs_of_nonneg hx0, abs_of_pos (Real.exp_pos _)] have hexp : exp (-((q : ℝ) * x) ^ 2 / 2) ≤ 1 := by rw [Real.exp_le_one_iff] exact div_nonpos_of_nonpos_of_nonneg (neg_nonpos.mpr (sq_nonneg _)) (by norm_num) calc (q : ℝ) ^ 3 * (sqrt (2 * pi))⁻¹ * x * exp (-((q : ℝ) * x) ^ 2 / 2) ≤ (q : ℝ) ^ 3 * 1 * 1 * 1 := by gcongr _ = (q : ℝ) ^ 3 := by ring intro u hu v hv rw [← hF u, ← hF v] have hmv := (convex_Icc (0 : ℝ) 1).norm_image_sub_le_of_norm_hasDerivWithin_le (fun x hx => (hderiv x).hasDerivWithinAt) hbound hu hv simpa [Real.norm_eq_abs, abs_sub_comm] using hmv -
nonnegativeNormalIntegralInterval_soundtheorem — The nonnegative-endpoint quadrature interval contains the exact integral of the standard-normal density from zero to the endpoint.hypothesesconclusion(nonnegativeNormalIntegralInterval q hq s).Contains (∫ u in (0 : ℝ)..1, (q : ℝ) * stdNormalPDF ((q : ℝ) * u))Proof (Lean source)
theorem nonnegativeNormalIntegralInterval_sound (q : ℚ) (hq : 0 ≤ q) (s : NormalCDFSchedule) : (nonnegativeNormalIntegralInterval q hq s).Contains (∫ u in (0 : ℝ)..1, (q : ℝ) * stdNormalPDF ((q : ℝ) * u)) := by let f : ℝ → ℝ := fun u => (q : ℝ) * stdNormalPDF ((q : ℝ) * u) have hquad := CircleMesh.integralEnclosure_sound (g := fun u => (f u : ℂ)) (nodes := normalDensityComplexNode q s) (pow_nonneg hq 3) s.mesh_pos (fun u hu v hv => by rw [← Complex.ofReal_sub, Complex.norm_real] simpa [f] using rescaledNormalDensity_lipschitz q hq u hu v hv) (fun k hk => by constructor · simpa [normalDensityComplexNode, f] using normalDensityNode_sound q hq s k · simp [normalDensityComplexNode]) have hre := hquad.1 rw [intervalIntegral.integral_ofReal] at hre simpa [nonnegativeNormalIntegralInterval, f] using hre -
stdNormalCDF_eq_half_add_rescaled_integraltheorem — For a nonnegative real endpoint, its standard-normal CDF is one half plus the integral of the rescaled density over the unit interval.hypothesesq :ℚhq :0 ≤ qconclusionstdNormalCDF (q : ℝ)= (1 / 2 : ℝ) + ∫ u in (0 : ℝ)..1, (q : ℝ) * stdNormalPDF ((q : ℝ) * u)Proof (Lean source)
theorem stdNormalCDF_eq_half_add_rescaled_integral (q : ℚ) (hq : 0 ≤ q) : stdNormalCDF (q : ℝ) = (1 / 2 : ℝ) + ∫ u in (0 : ℝ)..1, (q : ℝ) * stdNormalPDF ((q : ℝ) * u) := by have hqR : (0 : ℝ) ≤ q := by exact_mod_cast hq have hzero : stdNormalCDF 0 = (1 / 2 : ℝ) := by have hsym := stdNormalCDF_neg 0 norm_num at hsym ⊢ linarith have hmeasure : (gaussianReal 0 1) (Ioc 0 (q : ℝ)) = ofReal (stdNormalCDF (q : ℝ) - stdNormalCDF 0) := by calc (gaussianReal 0 1) (Ioc 0 (q : ℝ)) = (cdf (gaussianReal 0 1)).measure (Ioc 0 (q : ℝ)) := by rw [ProbabilityTheory.measure_cdf] _ = ofReal (cdf (gaussianReal 0 1) (q : ℝ) - cdf (gaussianReal 0 1) 0) := by rw [StieltjesFunction.measure_Ioc] _ = ofReal (stdNormalCDF (q : ℝ) - stdNormalCDF 0) := by rfl have hgauss : (gaussianReal 0 1) (Ioc 0 (q : ℝ)) = ofReal (∫ x in (0 : ℝ)..(q : ℝ), stdNormalPDF x) := by rw [ProbabilityTheory.gaussianReal_apply_eq_integral (μ := 0) (v := 1) one_ne_zero] simp [intervalIntegral.integral_of_le hqR, stdNormalPDF] have hdiff_nonneg : 0 ≤ stdNormalCDF (q : ℝ) - stdNormalCDF 0 := sub_nonneg.mpr (stdNormalCDF_monotone hqR) have hint_nonneg : 0 ≤ ∫ x in (0 : ℝ)..(q : ℝ), stdNormalPDF x := by rw [intervalIntegral.integral_of_le hqR] exact integral_nonneg (fun x => ProbabilityTheory.gaussianPDFReal_nonneg 0 1 x) have hdiff : stdNormalCDF (q : ℝ) - stdNormalCDF 0 = ∫ x in (0 : ℝ)..(q : ℝ), stdNormalPDF x := by rw [← ENNReal.ofReal_eq_ofReal_iff hdiff_nonneg hint_nonneg] exact hmeasure.symm.trans hgauss have hsubst : (∫ u in (0 : ℝ)..1, (q : ℝ) * stdNormalPDF ((q : ℝ) * u)) = ∫ x in (0 : ℝ)..(q : ℝ), stdNormalPDF x := by rw [intervalIntegral.integral_const_mul, intervalIntegral.mul_integral_comp_mul_left] simp rw [hsubst, ← hdiff, hzero] ring -
normalCDFInterval_soundtheorem — The internally evaluated interval soundly contains the standard-normal CDF at its rational endpoint; no external numerical approximation is assumed.Proof (Lean source)
theorem normalCDFInterval_sound (q : ℚ) (s : NormalCDFSchedule) : (normalCDFInterval q s).Contains (stdNormalCDF (q : ℝ)) := by by_cases hq : 0 ≤ q · have hint := nonnegativeNormalIntegralInterval_sound q hq s have hadd := RatInterval.add_sound (RatInterval.point_sound (1 / 2)) hint simp only [normalCDFInterval, if_pos hq] rw [stdNormalCDF_eq_half_add_rescaled_integral q hq] simpa [abs_of_nonneg hq] using hadd · have hqabs : 0 ≤ |q| := abs_nonneg q have hint := nonnegativeNormalIntegralInterval_sound |q| hqabs s have hadd := RatInterval.add_sound (RatInterval.point_sound (1 / 2)) hint have hpositive : ((RatInterval.point (1 / 2)).add (nonnegativeNormalIntegralInterval |q| hqabs s)).Contains (stdNormalCDF (|q| : ℚ)) := by rw [stdNormalCDF_eq_half_add_rescaled_integral |q| hqabs] convert hadd using 1 <;> norm_num have hsub := RatInterval.sub_sound (RatInterval.point_sound 1) hpositive have hq_nonpos : q ≤ 0 := le_of_not_ge hq have hneg : (q : ℝ) = -(|q| : ℚ) := by have hnegQ : q = -|q| := by rw [abs_of_nonpos hq_nonpos]; simp exact_mod_cast hnegQ rw [hneg, stdNormalCDF_neg] simpa [normalCDFInterval, hq] using hsub -
normalCDFDifference_soundtheorem — Subtracting two checked CDF enclosures contains the corresponding difference of standard-normal CDF values, as used for threshold-cell probabilities.hypothesesa b :ℚca :NormalCDFCertificate acb :NormalCDFCertificate bconclusion(cb.enclosure.sub ca.enclosure).Contains (stdNormalCDF (b : ℝ) - stdNormalCDF (a : ℝ))Proof (Lean source)
theorem normalCDFDifference_sound {a b : ℚ} (ca : NormalCDFCertificate a) (cb : NormalCDFCertificate b) : (cb.enclosure.sub ca.enclosure).Contains (stdNormalCDF (b : ℝ) - stdNormalCDF (a : ℝ)) := by exact RatInterval.sub_sound cb.sound ca.sound