Mathlib.Probability.Certified
This directory provides exact-rational interval certificates for finite kernels and stationary expectations, together with certified standard-normal CDF enclosures.
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 Finset.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 :
ℚ
hrho1 :
rho < 1
def
given by
fun i
=> (c.terminal i).expand (stationaryErrorRadius c rho) (stationaryErrorRadius_nonneg c rho 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 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 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
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 Finset.sum_nonneg fun i _ => le_max_of_le_left (abs_nonneg ((c.terminal i).sub (c.next i)).lo) -
stationaryErrorRadius_nonnegtheorem — A contraction coefficient strictly below one gives a nonnegative a posteriori stationary error radius.Proof (Lean source)
theorem stationaryErrorRadius_nonneg {ι : Type*} [Fintype ι] {K : IntervalMatrix ι ι} {p0 : RationalProbabilityVector ι} (c : FiniteIterateCertificate K p0) (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 rhohrho1 :rho < 1hresidual :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) (hrho1 : rho < 1) (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 : ℝ} (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 :ℚhrho1 :rho < 1hcontract :ContractsL1 P (rho : ℝ)π :ι → ℝhπ :IsStationary P πconclusionContainsVector (stationaryDistributionInterval c rho hrho1) πProof (Lean source)
theorem stationaryDistributionInterval_sound {ι : Type*} [Fintype ι] {P : Matrix ι ι ℝ} {p0 : RationalProbabilityVector ι} (kernel : CertifiedKernel P) (c : FiniteIterateCertificate kernel.intervals p0) (rho : ℚ) (hrho1 : rho < 1) (hcontract : ContractsL1 P (rho : ℝ)) {π : ι → ℝ} (hπ : IsStationary P π) : ContainsVector (stationaryDistributionInterval c rho 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 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 finite Markov reward processes.
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 two certified Markov kernels, their checked finite interval recurrences, a certified bounded reward vector, their rational contraction coefficients, the first coefficient's admissible bounds, the second coefficient's admissible bounds, 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 — Given two certified Markov kernels, their checked finite interval recurrences, a certified bounded reward vector, their rational contraction coefficients, the first coefficient's admissible bounds, the second coefficient's admissible bounds, the two contraction guarantees, their stationary distributions, a common benchmark, and strictly separated computed reward intervals, the first stationary bias is strictly smaller than the second.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 Finset.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
NormalCDFInterval 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) (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 : ℚ) (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 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