Stat
Statistical foundations: convergence modes, limit theorems, concentration inequalities, and minimax lower-bound tools.
Sample 133 core · 130 supporting · 6 submodules This file provides the library's causal-agnostic model of an independent and identically distributed sample relative to arbitrary ambient and population measures; probability-measure instances are supplied separately whe FiniteDesign 20 core · 53 supporting · 6 submodules Statistical tools for finite experimental and sampling designs. FinitePositiveTable 43 core · 50 supporting · 5 submodules This roll-up module exports graph-independent finite positive tables, their marginals and conditionals, coordinate fixing, sequential expansions, and two-row cancellation identities. OrderStatistic 44 core · 101 supporting · 8 submodules Exact distribution theory for the order statistics of n i.i.d. PolynomialTail 18 core · 35 supporting · 6 submodules Probability and moment bounds under polynomial-tail assumptions. RandomGraph 48 core · 42 supporting · 4 submodules This topic supplies a reusable spanning-parent union bound for expected counts of finite connected components meeting a designated root set under finite product measures. RecurrentEvent 111 core · 105 supporting · 14 submodules This directory packages a finite-horizon Poisson recurrent-event experiment with independent death and censoring. Weighted 33 core · 54 supporting · 10 submodules Weighted least squares as linear algebra: the geometry that underlies estimators built from nonuniform observation weights. Limit 30 core · 58 supporting · 11 submodules Modes of convergence for random sequences, and the calculus for manipulating them. CLT 290 core · 175 supporting · 18 submodules Central limit theory, including martingale extensions. UStatistic 81 core · 109 supporting · 5 submodules Asymptotic theory of U-statistics of fixed order m built from an i.i.d. SampleSplit 23 core · 29 supporting · 8 submodules Probabilistic facts behind estimators that fit nuisance functions on one part of an i.i.d. MEstimation 34 core · 27 supporting · 16 submodules Asymptotic theory for estimators defined by an estimating equation Pₙ ψ(θ̂) ≈ 0 or by maximizing a sample criterion. LinearModel 67 core · 50 supporting · 3 submodules Linear-model tools for the L² Frisch–Waugh–Lovell specialization, algebraic variance orderings for least-squares weights, and robust OLS asymptotics and inference. Minimax 1 to review
381 core · 577 supporting · 37 submodules Minimax risk: the best worst-case performance any procedure can achieve over a model class, and the standard devices for lower-bounding it. Concentration 373 core · 523 supporting · 17 submodules Concentration tools for scalar, vector, matrix, Poisson, and function-class deviations, including Hoeffding, Rademacher, VC, and entropy methods. EmpiricalProcess 76 core · 80 supporting · 6 submodules Empirical-process foundations for uniform stochastic deviations. GMM 37 core · 23 supporting · 11 submodules Large-sample theory for GMM estimators of a finite-dimensional parameter identified by moment conditions E g(θ₀, Z) = 0 with Jacobian G, weight W and moment covariance Cov. Inference 26 core · 19 supporting · 8 submodules General tools for statistical inference. FiniteRaoBlackwell 151 core · 187 supporting · 7 submodules Rao–Blackwell results for finite sampling designs, including Poisson designs. MomentProblems 78 core · 77 supporting · 10 submodules The classical moment problem: which sequences of raw moments come from a probability law, and what the moments pin down about the law. Nonparametric 134 core · 153 supporting · 8 submodules Finite-sample bias, variance and risk bounds for nonparametric estimators of a regression function under Hölder smoothness. Privacy 62 core · 72 supporting · 8 submodules Differential-privacy mechanisms and their statistical guarantees. Coupling 45 core · 49 supporting · 7 submodules This module collects coupling-based statistical primitives. Quantile 96 core · 125 supporting · 18 submodules Quantiles, empirical quantiles, and their statistical properties. Bootstrap 91 core · 55 supporting · 5 submodules Validity of Efron's nonparametric bootstrap for asymptotically linear estimators.
AttainableSet 1 core · 0 supporting This file defines the identified set of a real-valued objective as the set of values attained over its feasible parameter set; it need not be an interval. ★ IdentifiedSet
Identified sets
This file defines the identified set of a real-valued objective as the set of values attained over its feasible parameter set; it need not be an interval. The definition is shared by potential-outcome and structural-causal-model partial identification results.
def IdentifiedSet reviewed
⚑ flagged
Causalean.Stat.AttainableSet
For a parameter space, an objective function, and a feasibility condition on its parameter values, the identified set is the set of all objective values attained by feasible parameters.
ConditionalLaw 6 core · 14 supporting This module packages an explicitly supplied Markov kernel that disintegrates a full observation law given a real-valued dose. ★ integral_graph
Chosen conditional laws for real doses
This module packages an explicitly supplied Markov kernel that disintegrates a full observation law given a real-valued dose. It supplies pointwise conditional moments from that one chosen kernel, without asserting that such a kernel exists.
structure ContinuousDoseConditionalLaw reviewed
⚑ flagged
Causalean.Stat.ConditionalLaw
A measurable observation space, probability law, and measurable real-valued dose map determine a chosen continuous-dose conditional law. It consists of a proof that the dose map is measurable, a kernel assigning to each real dose value a measure on observations, a proof that every such measure is a probability measure, and the coherence identity: drawing a dose from its marginal law and then an observation from the kernel at that dose reproduces the joint law of the dose and the observation. The kernel is supplied, not constructed; nothing asserts that the kernel at a dose value is concentrated on observations with that dose beyond what the coherence identity implies.
Definition (Lean source)
parameters
fields
measurable_dose :
K :
Kernel ℝ Obs
markov :
coherence :
(letI : IsMarkovKernel K := markov (P.map A) ⊗ₘ K = P.map (fun ω ↦ (A ω, ω)))
theorem integral_graph reviewed
⚑ flagged
Causalean.Stat.ConditionalLaw.ContinuousDoseConditionalLaw
A chosen conditional law, joint real-valued quantity, and integrability under the joint dose--observation law imply that joint integration equals first averaging within each dose and then averaging over the dose distribution.
Formal statement
hypotheses
L :
ContinuousDoseConditionalLaw Obs P A
f :
ℝ × Obs → ℝ
hf :
Integrable f (P.map (fun ω ↦ (A ω, ω)))
conclusion
∫ z, f z ∂(P.map (fun ω ↦ (A ω, ω))) = ∫ a, ∫ ω, f (a, ω) ∂L.K a ∂(P.map A)
Proof (Lean source)
theorem integral_graph (L : ContinuousDoseConditionalLaw Obs P A)
(f : ℝ × Obs → ℝ)
(hf : Integrable f (P.map (fun ω ↦ (A ω, ω)))) :
∫ z, f z ∂(P.map (fun ω ↦ (A ω, ω))) =
∫ a, ∫ ω, f (a, ω) ∂L.K a ∂(P.map A) := by
haveI : IsMarkovKernel L.K := L.markov
rw [← L.coherence]
exact Measure.integral_compProd (L.coherence ▸ hf)
def mean reviewed
⚑ flagged
Causalean.Stat.ConditionalLaw.ContinuousDoseConditionalLaw
The chosen conditional law, real observation, and specified dose determine the pointwise conditional mean, given by integration against the selected kernel fiber.
Definition (Lean source)
parameters
def
mean L f a :
ℝ
given by
∫ ω, f ω ∂L.K a
def squaredRisk reviewed
⚑ flagged
Causalean.Stat.ConditionalLaw.ContinuousDoseConditionalLaw
The chosen conditional law, real observation, dose-indexed prediction, and specified dose determine the pointwise squared prediction risk, given by the kernel-fiber average of squared prediction error.
Definition (Lean source)
parameters
def
squaredRisk L f g a :
ℝ
given by
∫ ω, (f ω - g a) ^ 2 ∂L.K a
def secondMoment reviewed
⚑ flagged
Causalean.Stat.ConditionalLaw.ContinuousDoseConditionalLaw
The chosen conditional law, real observation, and specified dose determine the conditional second moment, given by the kernel-fiber average of the squared observation.
Definition (Lean source)
parameters
def
secondMoment L f a :
ℝ
given by
∫ ω, (f ω) ^ 2 ∂L.K a
def variance reviewed
⚑ flagged
Causalean.Stat.ConditionalLaw.ContinuousDoseConditionalLaw
The chosen conditional law, real observation, and specified dose determine the conditional variance, given by the squared risk of the conditional mean under the same kernel fiber.
Definition (Lean source)
parameters
def
variance L f a :
ℝ
given by
L.squaredRisk f (L.mean f) a
14 supporting declarations (lemmas, instances)
-
kernel_probabilitytheorem — The chosen conditional law assigns a probability distribution to the specified dose, so its kernel fiber has total mass one.hypothesesconclusionIsProbabilityMeasure (L.K a)Proof (Lean source)
theorem kernel_probability (L : ContinuousDoseConditionalLaw Obs P A) (a : ℝ) : IsProbabilityMeasure (L.K a) := by haveI : IsMarkovKernel L.K := L.markov infer_instance -
dose_probabilitytheorem — The chosen conditional law makes the marginal distribution of the dose a probability measure.Proof (Lean source)
theorem dose_probability (L : ContinuousDoseConditionalLaw Obs P A) : IsProbabilityMeasure (P.map A) := by exact Measure.isProbabilityMeasure_map L.measurable_dose.aemeasurable -
mean_eq_integraltheorem — A chosen conditional law, real observation, and specified dose satisfy the defining integral formula for its conditional mean.hypothesesconclusionL.mean f a = ∫ ω, f ω ∂L.K aProof (Lean source)
theorem mean_eq_integral (L : ContinuousDoseConditionalLaw Obs P A) (f : Obs → ℝ) (a : ℝ) : L.mean f a = ∫ ω, f ω ∂L.K a := rfl -
squaredRisk_eq_integraltheorem — A chosen conditional law, real observation, dose-indexed prediction, and specified dose satisfy the defining integral formula for their squared prediction risk.hypothesesconclusionL.squaredRisk f g a = ∫ ω, (f ω - g a) ^ 2 ∂L.K aProof (Lean source)
theorem squaredRisk_eq_integral (L : ContinuousDoseConditionalLaw Obs P A) (f : Obs → ℝ) (g : ℝ → ℝ) (a : ℝ) : L.squaredRisk f g a = ∫ ω, (f ω - g a) ^ 2 ∂L.K a := rfl -
secondMoment_eq_integraltheorem — A chosen conditional law, real observation, and specified dose satisfy the defining integral formula for their conditional second moment.hypothesesconclusionL.secondMoment f a = ∫ ω, (f ω) ^ 2 ∂L.K aProof (Lean source)
theorem secondMoment_eq_integral (L : ContinuousDoseConditionalLaw Obs P A) (f : Obs → ℝ) (a : ℝ) : L.secondMoment f a = ∫ ω, (f ω) ^ 2 ∂L.K a := rfl -
variance_eq_integraltheorem — A chosen conditional law, real observation, and specified dose satisfy the defining integral formula for their conditional variance.hypothesesconclusionL.variance f a = ∫ ω, (f ω - L.mean f a) ^ 2 ∂L.K aProof (Lean source)
theorem variance_eq_integral (L : ContinuousDoseConditionalLaw Obs P A) (f : Obs → ℝ) (a : ℝ) : L.variance f a = ∫ ω, (f ω - L.mean f a) ^ 2 ∂L.K a := rfl -
squaredRisk_nonnegtheorem — A chosen conditional law, real observation, dose-indexed prediction, and specified dose have a nonnegative squared prediction risk.hypothesesconclusion0 ≤ L.squaredRisk f g aProof (Lean source)
theorem squaredRisk_nonneg (L : ContinuousDoseConditionalLaw Obs P A) (f : Obs → ℝ) (g : ℝ → ℝ) (a : ℝ) : 0 ≤ L.squaredRisk f g a := by simp only [squaredRisk] exact integral_nonneg fun ω ↦ sq_nonneg _ -
secondMoment_nonnegtheorem — A chosen conditional law, real observation, and specified dose have a nonnegative conditional second moment.hypothesesconclusion0 ≤ L.secondMoment f aProof (Lean source)
theorem secondMoment_nonneg (L : ContinuousDoseConditionalLaw Obs P A) (f : Obs → ℝ) (a : ℝ) : 0 ≤ L.secondMoment f a := by simp only [secondMoment] exact integral_nonneg fun ω ↦ sq_nonneg _ -
variance_nonnegtheorem — A chosen conditional law, real observation, and specified dose have a nonnegative conditional variance.hypothesesconclusion0 ≤ L.variance f aProof (Lean source)
theorem variance_nonneg (L : ContinuousDoseConditionalLaw Obs P A) (f : Obs → ℝ) (a : ℝ) : 0 ≤ L.variance f a := L.squaredRisk_nonneg f (L.mean f) a -
measurable_meantheorem — A chosen conditional law and measurable real observation give a measurable pointwise conditional mean.hypothesesconclusionMeasurable (L.mean f)Proof (Lean source)
theorem measurable_mean (L : ContinuousDoseConditionalLaw Obs P A) {f : Obs → ℝ} (hf : Measurable f) : Measurable (L.mean f) := by haveI : IsMarkovKernel L.K := L.markov exact hf.stronglyMeasurable.integral_kernel.measurable -
measurable_squaredRisktheorem — A chosen conditional law, measurable real observation, and measurable dose-indexed prediction give a measurable pointwise squared prediction risk.hypothesesconclusionMeasurable (L.squaredRisk f g)Proof (Lean source)
theorem measurable_squaredRisk (L : ContinuousDoseConditionalLaw Obs P A) {f : Obs → ℝ} {g : ℝ → ℝ} (hf : Measurable f) (hg : Measurable g) : Measurable (L.squaredRisk f g) := by haveI : IsMarkovKernel L.K := L.markov have h : Measurable (fun p : ℝ × Obs ↦ (f p.2 - g p.1) ^ 2) := ((hf.comp measurable_snd).sub (hg.comp measurable_fst)).pow_const 2 exact (h.stronglyMeasurable.integral_kernel_prod_right').measurable -
measurable_secondMomenttheorem — A chosen conditional law and measurable real observation give a measurable conditional second moment.hypothesesconclusionMeasurable (L.secondMoment f)Proof (Lean source)
theorem measurable_secondMoment (L : ContinuousDoseConditionalLaw Obs P A) {f : Obs → ℝ} (hf : Measurable f) : Measurable (L.secondMoment f) := by haveI : IsMarkovKernel L.K := L.markov exact (hf.pow_const 2).stronglyMeasurable.integral_kernel.measurable -
measurable_variancetheorem — A chosen conditional law and measurable real observation give a measurable conditional variance.hypothesesconclusionMeasurable (L.variance f)Proof (Lean source)
theorem measurable_variance (L : ContinuousDoseConditionalLaw Obs P A) {f : Obs → ℝ} (hf : Measurable f) : Measurable (L.variance f) := by exact L.measurable_squaredRisk hf (L.measurable_mean hf) -
variance_eq_secondMoment_sub_sq_meantheorem — A chosen conditional law, real observation, specified dose, integrable observation on its kernel fiber, and integrable squared observation on that fiber imply that conditional variance equals the conditional second moment minus the squared conditional mean.hypothesesL :ContinuousDoseConditionalLaw Obs P Af :Obs → ℝa :ℝhf :Integrable f (L.K a)hf2 :Integrable (fun ω ↦ (f ω) ^ 2) (L.K a)conclusionL.variance f a = L.secondMoment f a - (L.mean f a) ^ 2Proof (Lean source)
theorem variance_eq_secondMoment_sub_sq_mean (L : ContinuousDoseConditionalLaw Obs P A) (f : Obs → ℝ) (a : ℝ) (hf : Integrable f (L.K a)) (hf2 : Integrable (fun ω ↦ (f ω) ^ 2) (L.K a)) : L.variance f a = L.secondMoment f a - (L.mean f a) ^ 2 := by haveI : IsMarkovKernel L.K := L.markov letI : IsProbabilityMeasure (L.K a) := L.kernel_probability a have hlinear : Integrable (fun ω ↦ 2 * L.mean f a * f ω) (L.K a) := hf.const_mul _ calc L.variance f a = ∫ ω, ((f ω) ^ 2 - 2 * L.mean f a * f ω + (L.mean f a) ^ 2) ∂L.K a := by rw [L.variance_eq_integral] apply integral_congr_ae filter_upwards with ω ring _ = (∫ ω, (f ω) ^ 2 - 2 * L.mean f a * f ω ∂L.K a) + (∫ _ω, (L.mean f a) ^ 2 ∂L.K a) := by simpa only [Pi.sub_apply, Pi.add_apply] using (integral_add (hf2.sub hlinear) (integrable_const (L.mean f a ^ 2))) _ = L.secondMoment f a - (L.mean f a) ^ 2 := by rw [integral_sub hf2 hlinear, integral_const, probReal_univ, one_smul, integral_const_mul] simp only [L.secondMoment_eq_integral, L.mean_eq_integral] ring
ContrastInformation 4 core · 17 supporting This module gives a finite-index interface for constrained quadratic information and generalized contrast variance of real positive-semidefinite matrices. ★ generalizedContrastVariance_eq_inv_constrainedInformation★ generalizedContrastVariance_antitone
Finite positive-semidefinite contrast information
This module gives a finite-index interface for constrained quadratic information and generalized contrast variance of real positive-semidefinite matrices. It includes the exact reciprocal identity in singular cases, range and positivity characterizations, and monotonicity under positive-semidefinite order.
def constrainedInformation reviewed
⚑ flagged
Causalean.Stat
A real finite matrix and contrast determine the constrained quadratic information, given by the infimum of the quadratic form of the matrix over all directions whose inner product with the contrast equals one.
def generalizedContrastVariance reviewed
⚑ flagged
Causalean.Stat
A real finite matrix and contrast determine the generalized contrast variance, given, when the linear system with this matrix and the contrast as right-hand side has a solution, by the infimum over solutions of the inner product of the contrast with the solution, truncated below at zero, and by infinity when no solution exists.
theorem generalizedContrastVariance_eq_inv_constrainedInformation reviewed
⚑ flagged
Causalean.Stat
A positive-semidefinite matrix and nonzero contrast have generalized contrast variance equal to the extended reciprocal of constrained information.
Formal statement
hypotheses
conclusion
Proof (Lean source)
theorem generalizedContrastVariance_eq_inv_constrainedInformation {I : Matrix ι ι ℝ}
(hI : I.PosSemidef) {c : ι → ℝ} (hc : c ≠ 0) :
generalizedContrastVariance I c = (ofReal (constrainedInformation I c))⁻¹ := by
classical
by_cases h : ∃ v : ι → ℝ, I.mulVec v = c
· obtain ⟨v, hv⟩ := h
rw [generalizedContrastVariance_eq_of_solution hI hv,
constrainedInformation_eq_inv_of_solution hI hc hv,
ENNReal.ofReal_inv_of_pos (solution_dot_pos hI hc hv), inv_inv]
· simp [generalizedContrastVariance, h, constrainedInformation_eq_zero_of_no_solution hI hc h]
theorem generalizedContrastVariance_antitone reviewed
⚑ flagged
Causalean.Stat
For two positive-semidefinite matrices I and J such that J minus I is positive semidefinite, and a nonzero contrast, the generalized contrast variance under J is at most the generalized contrast variance under I.
Formal statement
hypotheses
conclusion
Proof (Lean source)
theorem generalizedContrastVariance_antitone {I J : Matrix ι ι ℝ} (hI : I.PosSemidef)
(hJ : J.PosSemidef) (hIJ : (J - I).PosSemidef)
{c : ι → ℝ} (hc : c ≠ 0) :
generalizedContrastVariance J c ≤ generalizedContrastVariance I c := by
rw [generalizedContrastVariance_eq_inv_constrainedInformation hJ hc,
generalizedContrastVariance_eq_inv_constrainedInformation hI hc]
exact ENNReal.inv_le_inv'
(ENNReal.ofReal_le_ofReal (constrainedInformation_mono hI hIJ hc))
17 supporting declarations (lemmas, instances)
-
exists_unitContrastDirectiontheorem — A finite contrast that is nonzero has a direction with unit contrast pairing.hypothesesι :sharedType u_1c :ι → ℝhc :c ≠ 0conclusion∃ d : ι → ℝ, c ⬝ᵥ d = 1Proof (Lean source)
theorem exists_unitContrastDirection (c : ι → ℝ) (hc : c ≠ 0) : ∃ d : ι → ℝ, c ⬝ᵥ d = 1 := by classical have hi : ∃ i, c i ≠ 0 := by by_contra h push Not at h exact hc (funext h) obtain ⟨i, hi⟩ := hi refine ⟨Pi.single i (c i)⁻¹, ?_⟩ rw [dotProduct_single] exact mul_inv_cancel₀ hi -
constrainedInformation_nonnegtheorem — A positive-semidefinite matrix and a nonzero contrast have nonnegative constrained quadratic information.hypothesesconclusion0 ≤ constrainedInformation I cProof (Lean source)
theorem constrainedInformation_nonneg {I : Matrix ι ι ℝ} (hI : I.PosSemidef) {c : ι → ℝ} (hc : c ≠ 0) : 0 ≤ constrainedInformation I c := by unfold constrainedInformation apply le_csInf · obtain ⟨d, hd⟩ := exists_unitContrastDirection c hc exact ⟨d ⬝ᵥ I.mulVec d, d, hd, rfl⟩ · rintro r ⟨d, -, rfl⟩ simpa using hI.dotProduct_mulVec_nonneg d -
constrainedInformation_le_quadtheorem — A positive-semidefinite matrix and a direction with unit pairing against the contrast have constrained information no larger than that direction's quadratic energy.hypothesesconclusionconstrainedInformation I c ≤ d ⬝ᵥ I.mulVec dProof (Lean source)
theorem constrainedInformation_le_quad {I : Matrix ι ι ℝ} (hI : I.PosSemidef) {c d : ι → ℝ} (hd : c ⬝ᵥ d = 1) : constrainedInformation I c ≤ d ⬝ᵥ I.mulVec d := by unfold constrainedInformation apply csInf_le · refine ⟨0, ?_⟩ rintro r ⟨e, -, rfl⟩ simpa using hI.dotProduct_mulVec_nonneg e · exact ⟨d, hd, rfl⟩ -
constrainedInformation_monotheorem — A positive-semidefinite matrix and a second matrix whose difference in the stated order is positive semidefinite, at a nonzero contrast, have ordered constrained information.hypothesesconclusionconstrainedInformation I c ≤ constrainedInformation J cProof (Lean source)
theorem constrainedInformation_mono {I J : Matrix ι ι ℝ} (hI : I.PosSemidef) (hIJ : (J - I).PosSemidef) {c : ι → ℝ} (hc : c ≠ 0) : constrainedInformation I c ≤ constrainedInformation J c := by unfold constrainedInformation apply le_csInf · obtain ⟨d, hd⟩ := exists_unitContrastDirection c hc exact ⟨d ⬝ᵥ J.mulVec d, d, hd, rfl⟩ · rintro r ⟨d, hd, rfl⟩ calc sInf {r : ℝ | ∃ e : ι → ℝ, c ⬝ᵥ e = 1 ∧ r = e ⬝ᵥ I.mulVec e} ≤ d ⬝ᵥ I.mulVec d := by apply csInf_le · refine ⟨0, ?_⟩ rintro x ⟨e, -, rfl⟩ simpa using hI.dotProduct_mulVec_nonneg e · exact ⟨d, hd, rfl⟩ _ ≤ d ⬝ᵥ J.mulVec d := by have h := hIJ.dotProduct_mulVec_nonneg d simpa [Matrix.sub_mulVec, dotProduct_sub] using h -
generalizedContrastVariance_nonnegtheorem — A real finite matrix and contrast have nonnegative generalized contrast variance.hypothesesconclusion0 ≤ generalizedContrastVariance I cProof (Lean source)
theorem generalizedContrastVariance_nonneg (I : Matrix ι ι ℝ) (c : ι → ℝ) : 0 ≤ generalizedContrastVariance I c := bot_le -
exists_kernel_nonorthogonaltheorem — A positive-semidefinite matrix for which the contrast equation has no solution has a kernel direction with nonzero contrast pairing.hypothesesconclusion∃ k : ι → ℝ,conclusion 1I.mulVec k = 0conclusion 2c ⬝ᵥ k ≠ 0Proof (Lean source)
theorem exists_kernel_nonorthogonal {I : Matrix ι ι ℝ} (hI : I.PosSemidef) {c : ι → ℝ} (hnone : ¬ ∃ v : ι → ℝ, I.mulVec v = c) : ∃ k : ι → ℝ, I.mulVec k = 0 ∧ c ⬝ᵥ k ≠ 0 := by classical let T := I.toEuclideanLin have hT : T.IsSymmetric := Matrix.isSymmetric_toEuclideanLin_iff.mpr hI.isHermitian by_contra h push Not at h have hcorth : (toLp 2 c : EuclideanSpace ℝ ι) ∈ T.kerᗮ := by rw [Submodule.mem_orthogonal] intro x hx have hk : I.mulVec (ofLp x) = 0 := by have hx0 : T x = 0 := hx have := congrArg ofLp hx0 simpa [T, Matrix.toEuclideanLin_apply] using this have hck : c ⬝ᵥ ofLp x = 0 := h _ hk simpa [EuclideanSpace.inner_eq_star_dotProduct] using hck rw [T.orthogonal_ker, hT.adjoint_eq] at hcorth obtain ⟨v, hv⟩ := hcorth apply hnone refine ⟨WithLp.ofLp v, ?_⟩ have := congrArg ofLp hv simpa [T, Matrix.toEuclideanLin_apply] using this -
constrainedInformation_eq_zero_of_kerneltheorem — A positive-semidefinite matrix, nonzero contrast, and kernel direction with nonzero contrast pairing have zero constrained information.hypotheseshI :I.PosSemidefc k :ι → ℝhc :c ≠ 0hk :I.mulVec k = 0hck :c ⬝ᵥ k ≠ 0conclusionconstrainedInformation I c = 0Proof (Lean source)
theorem constrainedInformation_eq_zero_of_kernel {I : Matrix ι ι ℝ} (hI : I.PosSemidef) {c k : ι → ℝ} (hc : c ≠ 0) (hk : I.mulVec k = 0) (hck : c ⬝ᵥ k ≠ 0) : constrainedInformation I c = 0 := by let d : ι → ℝ := (c ⬝ᵥ k)⁻¹ • k have hd : c ⬝ᵥ d = 1 := by simp [d, dotProduct_smul, inv_mul_cancel₀ hck] have hId : I.mulVec d = 0 := by simp [d, mulVec_smul, hk] apply le_antisymm · simpa [hId] using constrainedInformation_le_quad hI hd · exact constrainedInformation_nonneg hI hc -
constrainedInformation_eq_zero_of_no_solutiontheorem — A positive-semidefinite matrix, nonzero contrast, and unsolvable contrast equation have zero constrained information.hypotheseshI :I.PosSemidefc :ι → ℝhc :c ≠ 0hnone :¬ ∃ v : ι → ℝ, I.mulVec v = cconclusionconstrainedInformation I c = 0Proof (Lean source)
theorem constrainedInformation_eq_zero_of_no_solution {I : Matrix ι ι ℝ} (hI : I.PosSemidef) {c : ι → ℝ} (hc : c ≠ 0) (hnone : ¬ ∃ v : ι → ℝ, I.mulVec v = c) : constrainedInformation I c = 0 := by obtain ⟨k, hk, hck⟩ := exists_kernel_nonorthogonal hI hnone exact constrainedInformation_eq_zero_of_kernel hI hc hk hck -
solution_dot_eqtheorem — A positive-semidefinite matrix and two solutions to its contrast equation have the same contrast pairing.hypotheseshI :I.PosSemidefc v w :ι → ℝhv :I.mulVec v = chw :I.mulVec w = cconclusionc ⬝ᵥ v = c ⬝ᵥ wProof (Lean source)
theorem solution_dot_eq {I : Matrix ι ι ℝ} (hI : I.PosSemidef) {c v w : ι → ℝ} (hv : I.mulVec v = c) (hw : I.mulVec w = c) : c ⬝ᵥ v = c ⬝ᵥ w := by have hs : Iᵀ = I := by simpa using hI.isHermitian.eq calc c ⬝ᵥ v = (I.mulVec w) ⬝ᵥ v := by rw [hw] _ = w ⬝ᵥ I.mulVec v := by rw [dotProduct_comm] simpa [hs] using (Matrix.dotProduct_transpose_mulVec I w v).symm _ = c ⬝ᵥ w := by rw [hv, dotProduct_comm] -
solution_dot_postheorem — A positive-semidefinite matrix, nonzero contrast, and solution to its contrast equation have a strictly positive contrast pairing.hypothesesconclusion0 < c ⬝ᵥ vProof (Lean source)
theorem solution_dot_pos {I : Matrix ι ι ℝ} (hI : I.PosSemidef) {c v : ι → ℝ} (hc : c ≠ 0) (hv : I.mulVec v = c) : 0 < c ⬝ᵥ v := by have hn : 0 ≤ c ⬝ᵥ v := by rw [← hv] simpa [dotProduct_comm] using hI.dotProduct_mulVec_nonneg v rcases hn.eq_or_lt with hz | hp · have hz' : v ⬝ᵥ I.mulVec v = 0 := by simpa [← hv, dotProduct_comm] using hz.symm exact False.elim (hc ((hI.dotProduct_mulVec_zero_iff v).mp hz' ▸ hv.symm)) · exact hp -
generalizedContrastVariance_eq_of_solutiontheorem — A positive-semidefinite matrix and a solution to its contrast equation have generalized contrast variance equal to that solution's contrast pairing.hypothesesconclusiongeneralizedContrastVariance I c = ofReal (c ⬝ᵥ v)Proof (Lean source)
theorem generalizedContrastVariance_eq_of_solution {I : Matrix ι ι ℝ} (hI : I.PosSemidef) {c v : ι → ℝ} (hv : I.mulVec v = c) : generalizedContrastVariance I c = ofReal (c ⬝ᵥ v) := by unfold generalizedContrastVariance rw [if_pos ⟨v, hv⟩] congr 1 have hs : {r : ℝ | ∃ w : ι → ℝ, I.mulVec w = c ∧ r = c ⬝ᵥ w} = {c ⬝ᵥ v} := by ext r simp only [Set.mem_ofPred_eq, Set.mem_singleton_iff] constructor · rintro ⟨w, hw, rfl⟩ exact (solution_dot_eq hI hv hw).symm · rintro rfl exact ⟨v, hv, rfl⟩ rw [hs, csInf_singleton] -
inv_solution_dot_le_quadtheorem — A positive-semidefinite matrix, nonzero contrast, solution to its contrast equation, and unit-contrast direction have the reciprocal solution pairing no greater than that direction's energy.hypotheseshI :I.PosSemidefc v d :ι → ℝhc :c ≠ 0hv :I.mulVec v = chd :c ⬝ᵥ d = 1conclusion(c ⬝ᵥ v)⁻¹ ≤ d ⬝ᵥ I.mulVec dProof (Lean source)
theorem inv_solution_dot_le_quad {I : Matrix ι ι ℝ} (hI : I.PosSemidef) {c v d : ι → ℝ} (hc : c ≠ 0) (hv : I.mulVec v = c) (hd : c ⬝ᵥ d = 1) : (c ⬝ᵥ v)⁻¹ ≤ d ⬝ᵥ I.mulVec d := by let a := (c ⬝ᵥ v)⁻¹ have hp := solution_dot_pos hI hc hv have ha : a * (c ⬝ᵥ v) = 1 := inv_mul_cancel₀ (ne_of_gt hp) have hs : Iᵀ = I := by simpa using hI.isHermitian.eq have hcross : v ⬝ᵥ I.mulVec d = 1 := by calc v ⬝ᵥ I.mulVec d = d ⬝ᵥ I.mulVec v := by simpa [hs] using Matrix.dotProduct_transpose_mulVec I v d _ = 1 := by rw [hv, dotProduct_comm, hd] have hsq : 0 ≤ (d - a • v) ⬝ᵥ I.mulVec (d - a • v) := by simpa only [TrivialStar.star_trivial] using hI.dotProduct_mulVec_nonneg (d - a • v) simp only [Matrix.mulVec_sub, Matrix.mulVec_smul, dotProduct_sub, dotProduct_smul, smul_eq_mul] at hsq simp only [sub_dotProduct, smul_dotProduct, smul_eq_mul] at hsq have hdc : d ⬝ᵥ c = 1 := by simpa [dotProduct_comm] using hd rw [hv, hcross, hdc, dotProduct_comm v c] at hsq dsimp [a] at * nlinarith -
exists_unitContrastDirection_energy_invtheorem — A positive-semidefinite matrix, nonzero contrast, and solution to its contrast equation have a unit-contrast direction attaining reciprocal solution energy.hypothesesconclusion∃ d : ι → ℝ,conclusion 1c ⬝ᵥ d = 1conclusion 2d ⬝ᵥ I.mulVec d = (c ⬝ᵥ v)⁻¹Proof (Lean source)
theorem exists_unitContrastDirection_energy_inv {I : Matrix ι ι ℝ} (hI : I.PosSemidef) {c v : ι → ℝ} (hc : c ≠ 0) (hv : I.mulVec v = c) : ∃ d : ι → ℝ, c ⬝ᵥ d = 1 ∧ d ⬝ᵥ I.mulVec d = (c ⬝ᵥ v)⁻¹ := by let a := (c ⬝ᵥ v)⁻¹ have hp := solution_dot_pos hI hc hv have ha : a * (c ⬝ᵥ v) = 1 := inv_mul_cancel₀ (ne_of_gt hp) refine ⟨a • v, ?_, ?_⟩ · rw [dotProduct_smul, smul_eq_mul] exact ha · rw [Matrix.mulVec_smul, dotProduct_smul, smul_dotProduct, smul_eq_mul, smul_eq_mul, hv, dotProduct_comm] change a * (a * (c ⬝ᵥ v)) = a rw [ha, mul_one] -
constrainedInformation_eq_inv_of_solutiontheorem — A positive-semidefinite matrix, nonzero contrast, and solution to its contrast equation have constrained information equal to the reciprocal solution pairing.hypothesesconclusionconstrainedInformation I c = (c ⬝ᵥ v)⁻¹Proof (Lean source)
theorem constrainedInformation_eq_inv_of_solution {I : Matrix ι ι ℝ} (hI : I.PosSemidef) {c v : ι → ℝ} (hc : c ≠ 0) (hv : I.mulVec v = c) : constrainedInformation I c = (c ⬝ᵥ v)⁻¹ := by apply le_antisymm · obtain ⟨d, hd, he⟩ := exists_unitContrastDirection_energy_inv hI hc hv rw [← he] exact constrainedInformation_le_quad hI hd · unfold constrainedInformation apply le_csInf · obtain ⟨d, hd⟩ := exists_unitContrastDirection c hc exact ⟨d ⬝ᵥ I.mulVec d, d, hd, rfl⟩ · rintro r ⟨d, hd, rfl⟩ exact inv_solution_dot_le_quad hI hc hv hd -
constrainedInformation_pos_iff_solutiontheorem — A positive-semidefinite matrix and nonzero contrast have strictly positive constrained information exactly when their contrast equation is solvable.hypothesesconclusion0 < constrainedInformation I c ↔ ∃ v : ι → ℝ, I.mulVec v = cProof (Lean source)
theorem constrainedInformation_pos_iff_solution {I : Matrix ι ι ℝ} (hI : I.PosSemidef) {c : ι → ℝ} (hc : c ≠ 0) : 0 < constrainedInformation I c ↔ ∃ v : ι → ℝ, I.mulVec v = c := by constructor · intro hq by_contra h exact (ne_of_gt hq) (constrainedInformation_eq_zero_of_no_solution hI hc h) · rintro ⟨v, hv⟩ rw [constrainedInformation_eq_inv_of_solution hI hc hv] exact inv_pos.mpr (solution_dot_pos hI hc hv) -
generalizedContrastVariance_eq_top_iff_no_solutiontheorem — A positive-semidefinite matrix and a contrast have infinite generalized contrast variance exactly when their contrast equation has no solution.hypothesesconclusiongeneralizedContrastVariance I c = ⊤ ↔ ¬ ∃ v : ι → ℝ, I.mulVec v = cProof (Lean source)
theorem generalizedContrastVariance_eq_top_iff_no_solution {I : Matrix ι ι ℝ} (hI : I.PosSemidef) {c : ι → ℝ} : generalizedContrastVariance I c = ⊤ ↔ ¬ ∃ v : ι → ℝ, I.mulVec v = c := by classical constructor · intro htop h obtain ⟨v, hv⟩ := h rw [generalizedContrastVariance_eq_of_solution hI hv] at htop exact ENNReal.ofReal_ne_top htop · intro h simp [generalizedContrastVariance, h] -
generalizedContrastVariance_eq_ofReal_inv_of_constrainedInformation_postheorem — A positive-semidefinite matrix, nonzero contrast, and strictly positive constrained information have generalized contrast variance equal to the extended-real reciprocal.Proof (Lean source)
theorem generalizedContrastVariance_eq_ofReal_inv_of_constrainedInformation_pos {I : Matrix ι ι ℝ} (hI : I.PosSemidef) {c : ι → ℝ} (hc : c ≠ 0) (hq : 0 < constrainedInformation I c) : generalizedContrastVariance I c = ofReal (constrainedInformation I c)⁻¹ := by rw [generalizedContrastVariance_eq_inv_constrainedInformation hI hc, ENNReal.ofReal_inv_of_pos hq]
FiniteFiberConditioning 1 core · 0 supporting This file turns elementary probability-mass factorization within every fiber of a finite-valued conditioning map into conditional independence given that map. ★ condIndepFun_finite_of_measureReal_fibers
Conditional Independence from Finite Fibers
This file turns elementary probability-mass factorization within every fiber of a finite-valued conditioning map into conditional independence given that map. The proof computes conditional expectations of event indicators by finite-fiber probability ratios.
theorem condIndepFun_finite_of_measureReal_fibers reviewed
⚑ flagged
Causalean.Stat
For a finite measure, a finite-valued conditioning map, two random elements, measurability of all three maps, and factorization of their ordinary real masses on every measurable pair of events inside every conditioning fiber, the two random elements are conditionally independent given the sigma-algebra generated by the conditioning map.
Formal statement
hypotheses
Omega T A B :
mu :
Measure Omega
X :
Omega → T
hX :
f :
Omega → A
hf :
g :
Omega → B
hg :
hfactor :
if
and
then
mu.real (((f ⁻¹' s) ∩ (g ⁻¹' t)) ∩ X ⁻¹' {x}) * mu.real (X ⁻¹' {x})
= mu.real ((f ⁻¹' s) ∩ X ⁻¹' {x}) * mu.real ((g ⁻¹' t) ∩ X ⁻¹' {x})
conclusion
Proof (Lean source)
theorem condIndepFun_finite_of_measureReal_fibers
{Omega T A B : Type*} [MeasurableSpace Omega] [StandardBorelSpace Omega]
[Finite T] [MeasurableSpace T] [MeasurableSingletonClass T]
[MeasurableSpace A] [MeasurableSpace B]
(mu : Measure Omega) [IsFiniteMeasure mu]
(X : Omega → T) (hX : Measurable X)
(f : Omega → A) (hf : Measurable f)
(g : Omega → B) (hg : Measurable g)
(hfactor :
∀ (x : T) (s : Set A) (t : Set B),
MeasurableSet s → MeasurableSet t →
mu.real (((f ⁻¹' s) ∩ (g ⁻¹' t)) ∩ X ⁻¹' {x}) *
mu.real (X ⁻¹' {x}) =
mu.real ((f ⁻¹' s) ∩ X ⁻¹' {x}) *
mu.real ((g ⁻¹' t) ∩ X ⁻¹' {x})) :
CondIndepFun (comap X inferInstance)
hX.comap_le f g mu := by
rw [condIndepFun_iff_condExp_inter_preimage_eq_mul hf hg]
intro s t hs ht
have hfg : MeasurableSet (f ⁻¹' s ∩ g ⁻¹' t) :=
(hf hs).inter (hg ht)
have hleft := condExp_indicator_finite_comap mu X hX _ hfg
have hfiber := condExp_indicator_finite_comap mu X hX _ (hf hs)
have hgiber := condExp_indicator_finite_comap mu X hX _ (hg ht)
filter_upwards [hleft, hfiber, hgiber] with omega hleftomega hfomega hgomega
rw [hleftomega, hfomega, hgomega]
unfold finiteCondProb
let m := mu.real (X ⁻¹' {X omega})
by_cases hm : m = 0
· simp only [m] at hm
simp [hm]
· have hfac := hfactor (X omega) s t hs ht
simp only [Set.inter_assoc] at hfac
change m⁻¹ *
mu.real (X ⁻¹' {X omega} ∩ (f ⁻¹' s ∩ g ⁻¹' t)) =
(m⁻¹ * mu.real (X ⁻¹' {X omega} ∩ f ⁻¹' s)) *
(m⁻¹ * mu.real (X ⁻¹' {X omega} ∩ g ⁻¹' t))
have hfac' :
mu.real (X ⁻¹' {X omega} ∩ (f ⁻¹' s ∩ g ⁻¹' t)) * m =
mu.real (X ⁻¹' {X omega} ∩ f ⁻¹' s) *
mu.real (X ⁻¹' {X omega} ∩ g ⁻¹' t) := by
simpa [m, Set.inter_comm, Set.inter_left_comm, Set.inter_assoc] using
hfac
field_simp
simpa [mul_comm] using hfac'
ScoreProjection 3 core · 6 supporting This module develops guarded likelihood scores for dominated laws and proves that pushing a law through any measurable statistic projects its score onto the statistic's σ-algebra, provided the derivative density on the s ★ condExp_guardedScore_eq_statistic_score★ statistic_score_memLp_and_secondMoment_le
Likelihood-score projection through measurable statistics
This module develops guarded likelihood scores for dominated laws and proves that pushing a law through any measurable statistic projects its score onto the statistic's σ-algebra, provided the derivative density on the statistic's space is assumed to be the pushforward of the source derivative density. It also gives the corresponding L² contraction, without conditional distributions or regularity assumptions on the sample spaces.
def guardedScore reviewed
⚑ flagged
Causalean.Stat.ScoreProjection
A density, signed derivative density, and observation determine the guarded likelihood score, given by their quotient away from a zero density and by zero at a zero density.
Definition (Lean source)
parameters
α :
Type u_1
q qdot :
α → ℝ
x :
α
def
guardedScore q qdot x :
ℝ
given by
if q x = 0 then 0 else qdot x / q x
theorem condExp_guardedScore_eq_statistic_score reviewed
⚑ flagged
Causalean.Stat.ScoreProjection
Take finite reference measures on the source space and on the statistic's space, a source probability law and a statistic law, a measurable statistic, and real densities and derivative densities on both spaces, all measurable except possibly the source derivative density. Suppose the densities are nonnegative almost everywhere under their reference measures, each derivative density vanishes almost everywhere where its density vanishes, the source law has the source density with respect to its reference measure, the statistic law is the law of the statistic under the source law, and it has the statistic density with respect to its reference measure, both guarded scores are integrable under their laws, and the derivative densities are linked by the same pushforward: for every measurable set of statistic values, the source derivative density integrated over the set's preimage equals the statistic derivative density integrated over the set. Then the conditional expectation, under the source law, of the source guarded score given the statistic equals the statistic's guarded score evaluated at the statistic, almost everywhere.
Formal statement
hypotheses
Ω :
Type u_2
Y :
Type u_3
T :
Ω → Y
qΩ :
Ω → ℝ
qdotΩ :
Ω → ℝ
qY :
Y → ℝ
qdotY :
Y → ℝ
hT :
hqΩ :
Measurable qΩ
hqY :
Measurable qY
hqdotY :
Measurable qdotY
hqΩnonneg :
∀ᵐ ω ∂νΩ, 0 ≤ qΩ ω
hqYnonneg :
∀ᵐ y ∂νY, 0 ≤ qY y
hzeroΩ :
∀ᵐ ω ∂νΩ, qΩ ω = 0 → qdotΩ ω = 0
hzeroY :
∀ᵐ y ∂νY, qY y = 0 → qdotY y = 0
hμΩ :
μΩ = νΩ.withDensity (fun ω => ofReal (qΩ ω))
hμYmap :
μY = μΩ.map T
hμYdensity :
μY = νY.withDensity (fun y => ofReal (qY y))
hscoreΩInt :
Integrable (guardedScore qΩ qdotΩ) μΩ
hscoreYInt :
Integrable (guardedScore qY qdotY) μY
hderivMap :
∀ A : Set Y
if
then
∫ ω in T ⁻¹' A, qdotΩ ω ∂νΩ = ∫ y in A, qdotY y ∂νY
conclusion
=ᵐ[μΩ] fun ω => guardedScore qY qdotY (T ω)
Proof (Lean source)
theorem condExp_guardedScore_eq_statistic_score
(hT : Measurable T)
(hqΩ : Measurable qΩ)
(hqY : Measurable qY) (hqdotY : Measurable qdotY)
(hqΩnonneg : ∀ᵐ ω ∂νΩ, 0 ≤ qΩ ω)
(hqYnonneg : ∀ᵐ y ∂νY, 0 ≤ qY y)
(hzeroΩ : ∀ᵐ ω ∂νΩ, qΩ ω = 0 → qdotΩ ω = 0)
(hzeroY : ∀ᵐ y ∂νY, qY y = 0 → qdotY y = 0)
(hμΩ : μΩ = νΩ.withDensity (fun ω => ofReal (qΩ ω)))
(hμYmap : μY = μΩ.map T)
(hμYdensity : μY = νY.withDensity (fun y => ofReal (qY y)))
(hscoreΩInt : Integrable (guardedScore qΩ qdotΩ) μΩ)
(hscoreYInt : Integrable (guardedScore qY qdotY) μY)
(hderivMap : ∀ A : Set Y, MeasurableSet A →
∫ ω in T ⁻¹' A, qdotΩ ω ∂νΩ = ∫ y in A, qdotY y ∂νY) :
μΩ[guardedScore qΩ qdotΩ | comap T inferInstance] =ᵐ[μΩ]
fun ω => guardedScore qY qdotY (T ω) := by
apply (condExp_eq_statistic_iff_integral_preimage_eq μΩ μY T hT hμYmap
(guardedScore qΩ qdotΩ) (guardedScore qY qdotY)
hscoreΩInt hscoreYInt (measurable_guardedScore hqY hqdotY)).2
intro A hA
calc
∫ ω in T ⁻¹' A, guardedScore qΩ qdotΩ ω ∂μΩ =
∫ ω in T ⁻¹' A, guardedScore qY qdotY (T ω) ∂μΩ :=
score_integral_preimage_eq νΩ νY μΩ μY T qΩ qdotΩ qY qdotY
hT hqΩ hqY hqdotY hqΩnonneg hqYnonneg
hzeroΩ hzeroY hμΩ hμYmap hμYdensity hderivMap A hA
_ = ∫ y in A, guardedScore qY qdotY y ∂μY := by
rw [hμYmap]
exact (setIntegral_map hA
(measurable_guardedScore hqY hqdotY).aestronglyMeasurable
hT.aemeasurable).symm
theorem statistic_score_memLp_and_secondMoment_le reviewed
⚑ flagged
Causalean.Stat.ScoreProjection
Take finite reference measures on the source space and on the statistic's space, a source probability law and a statistic law, a measurable statistic, and real densities and derivative densities on both spaces, all measurable except possibly the source derivative density. Suppose the densities are nonnegative almost everywhere under their reference measures, each derivative density vanishes almost everywhere where its density vanishes, the source law has the source density with respect to its reference measure, the statistic law is the law of the statistic under the source law, and it has the statistic density with respect to its reference measure, the statistic derivative density is integrable under its reference measure, for every measurable set of statistic values, the source derivative density integrated over the set's preimage equals the statistic derivative density integrated over the set, and the source guarded score is square-integrable under the source law. Then the statistic's guarded score is square-integrable under the statistic law, and its second moment is at most the second moment of the source guarded score under the source law.
Formal statement
hypotheses
Ω :
Type u_2
Y :
Type u_3
T :
Ω → Y
qΩ :
Ω → ℝ
qdotΩ :
Ω → ℝ
qY :
Y → ℝ
qdotY :
Y → ℝ
hT :
hqΩ :
Measurable qΩ
hqY :
Measurable qY
hqdotY :
Measurable qdotY
hqΩnonneg :
∀ᵐ ω ∂νΩ, 0 ≤ qΩ ω
hqYnonneg :
∀ᵐ y ∂νY, 0 ≤ qY y
hzeroΩ :
∀ᵐ ω ∂νΩ, qΩ ω = 0 → qdotΩ ω = 0
hzeroY :
∀ᵐ y ∂νY, qY y = 0 → qdotY y = 0
hμΩ :
μΩ = νΩ.withDensity (fun ω => ofReal (qΩ ω))
hμYmap :
μY = μΩ.map T
hμYdensity :
μY = νY.withDensity (fun y => ofReal (qY y))
hderivYInt :
Integrable qdotY νY
hderivMap :
∀ A : Set Y
if
then
∫ ω in T ⁻¹' A, qdotΩ ω ∂νΩ = ∫ y in A, qdotY y ∂νY
hscoreΩL2 :
MemLp (guardedScore qΩ qdotΩ) 2 μΩ
conclusion
conclusion 1
MemLp (guardedScore qY qdotY) 2 μY
conclusion 2
(∫ y, guardedScore qY qdotY y ^ 2 ∂μY) ≤ ∫ ω, guardedScore qΩ qdotΩ ω ^ 2 ∂μΩ
Proof (Lean source)
theorem statistic_score_memLp_and_secondMoment_le
(hT : Measurable T)
(hqΩ : Measurable qΩ)
(hqY : Measurable qY) (hqdotY : Measurable qdotY)
(hqΩnonneg : ∀ᵐ ω ∂νΩ, 0 ≤ qΩ ω)
(hqYnonneg : ∀ᵐ y ∂νY, 0 ≤ qY y)
(hzeroΩ : ∀ᵐ ω ∂νΩ, qΩ ω = 0 → qdotΩ ω = 0)
(hzeroY : ∀ᵐ y ∂νY, qY y = 0 → qdotY y = 0)
(hμΩ : μΩ = νΩ.withDensity (fun ω => ofReal (qΩ ω)))
(hμYmap : μY = μΩ.map T)
(hμYdensity : μY = νY.withDensity (fun y => ofReal (qY y)))
(hderivYInt : Integrable qdotY νY)
(hderivMap : ∀ A : Set Y, MeasurableSet A →
∫ ω in T ⁻¹' A, qdotΩ ω ∂νΩ = ∫ y in A, qdotY y ∂νY)
(hscoreΩL2 : MemLp (guardedScore qΩ qdotΩ) 2 μΩ) :
MemLp (guardedScore qY qdotY) 2 μY ∧
(∫ y, guardedScore qY qdotY y ^ 2 ∂μY) ≤
∫ ω, guardedScore qΩ qdotΩ ω ^ 2 ∂μΩ := by
have hscoreΩInt : Integrable (guardedScore qΩ qdotΩ) μΩ :=
hscoreΩL2.integrable (by norm_num)
have hscoreYInt : Integrable (guardedScore qY qdotY) μY :=
integrable_guardedScore_of_derivative_integrable νY μY qY qdotY
hqY hqYnonneg hzeroY hμYdensity hderivYInt
have hprojection := condExp_guardedScore_eq_statistic_score
νΩ νY μΩ μY T qΩ qdotΩ qY qdotY hT hqΩ hqY hqdotY
hqΩnonneg hqYnonneg hzeroΩ hzeroY hμΩ hμYmap hμYdensity
hscoreΩInt hscoreYInt hderivMap
have hpull : MemLp (fun ω => guardedScore qY qdotY (T ω)) 2 μΩ :=
(memLp_congr_ae hprojection).mp
(MemLp.condExp (m := comap T inferInstance)
(by norm_num) hscoreΩL2)
have hscoreY : MemLp (guardedScore qY qdotY) 2 μY := by
rw [hμYmap]
exact (memLp_map_measure_iff
(measurable_guardedScore hqY hqdotY).aestronglyMeasurable
hT.aemeasurable).2 hpull
refine ⟨hscoreY, ?_⟩
have hbound := integral_norm_condExp_rpow_le
(m := comap T inferInstance) (μ := μΩ)
(f := guardedScore qΩ qdotΩ) (p := (2 : ℝ)) (by norm_num)
(by
convert hscoreΩL2.integrable_norm_pow (p := 2) (by norm_num) using 1
ext x
rw [← @Nat.cast_two ℝ, Real.rpow_natCast])
have hmap :
(∫ y, guardedScore qY qdotY y ^ 2 ∂μY) =
∫ ω, guardedScore qY qdotY (T ω) ^ 2 ∂μΩ := by
rw [hμYmap]
exact integral_map hT.aemeasurable
((measurable_guardedScore hqY hqdotY).pow_const 2).aestronglyMeasurable
rw [hmap]
have hprojSq :
(∫ ω, guardedScore qY qdotY (T ω) ^ 2 ∂μΩ) =
∫ ω, (μΩ[guardedScore qΩ qdotΩ |
comap T inferInstance]) ω ^ 2 ∂μΩ := by
apply integral_congr_ae
filter_upwards [hprojection] with ω hω
rw [hω]
rw [hprojSq]
have hsq (x : ℝ) : ‖x‖ ^ (2 : ℝ) = x ^ 2 := by
rw [← @Nat.cast_two ℝ, Real.rpow_natCast, Real.norm_eq_abs, sq_abs]
simpa only [hsq] using hbound
6 supporting declarations (lemmas, instances)
-
measurable_guardedScoretheorem — Measurable density and derivative functions give a measurable guarded likelihood score.hypothesesconclusionMeasurable (guardedScore q qdot)Proof (Lean source)
@[fun_prop] theorem measurable_guardedScore {q qdot : α → ℝ} (hq : Measurable q) (hqdot : Measurable qdot) : Measurable (guardedScore q qdot) := by unfold guardedScore exact Measurable.ite (hq (measurableSet_singleton 0)) measurable_const (hqdot.div hq) -
derivative_eq_density_mul_guardedScoretheorem — A reference measure, density, and derivative density whose derivative vanishes wherever the density vanishes satisfy the almost-everywhere identity between the derivative density and density times its guarded score.hypotheseshzero :∀ᵐ x ∂ν, q x = 0 → qdot x = 0conclusion∀ᵐ x ∂ν, qdot x = q x * guardedScore q qdot xProof (Lean source)
theorem derivative_eq_density_mul_guardedScore {ν : Measure α} {q qdot : α → ℝ} (hzero : ∀ᵐ x ∂ν, q x = 0 → qdot x = 0) : ∀ᵐ x ∂ν, qdot x = q x * guardedScore q qdot x := by filter_upwards [hzero] with x hx by_cases hq : q x = 0 · simp [guardedScore, hq, hx hq] · simp [guardedScore, hq, mul_div_cancel₀ _ hq] -
integrable_guardedScore_of_derivative_integrabletheorem — A reference measure and law, measurable density and derivative density, nonnegative density, zero-set derivative control, density representation of the law, and integrable derivative density give an integrable guarded likelihood score under the law.hypothesesα :sharedType u_1ν μ :Measure αq qdot :α → ℝhq :hqnonneg :∀ᵐ x ∂ν, 0 ≤ q xhzero :∀ᵐ x ∂ν, q x = 0 → qdot x = 0hμ :μ = ν.withDensity (fun x => ofReal (q x))hderivInt :Integrable qdot νconclusionIntegrable (guardedScore q qdot) μProof (Lean source)
theorem integrable_guardedScore_of_derivative_integrable (ν μ : Measure α) (q qdot : α → ℝ) (hq : Measurable q) (hqnonneg : ∀ᵐ x ∂ν, 0 ≤ q x) (hzero : ∀ᵐ x ∂ν, q x = 0 → qdot x = 0) (hμ : μ = ν.withDensity (fun x => ofReal (q x))) (hderivInt : Integrable qdot ν) : Integrable (guardedScore q qdot) μ := by rw [hμ, integrable_withDensity_iff_integrable_smul' hq.ennreal_ofReal (by simp)] apply hderivInt.congr filter_upwards [hqnonneg, derivative_eq_density_mul_guardedScore hzero] with x hx hxeq rw [ENNReal.toReal_ofReal hx, smul_eq_mul] exact hxeq -
setIntegral_guardedScore_eq_derivativetheorem — A finite reference measure and law, measurable density and derivative density, nonnegative density, zero-set derivative control, density representation, and measurable event make the guarded-score integral on that event equal the derivative-density integral.hypothesesα :sharedType u_1ν μ :q qdot :α → ℝhq :hqnonneg :∀ᵐ x ∂ν, 0 ≤ q xhzero :∀ᵐ x ∂ν, q x = 0 → qdot x = 0hμ :μ = ν.withDensity (fun x => ofReal (q x))A :Set αhA :conclusion∫ x in A, guardedScore q qdot x ∂μ = ∫ x in A, qdot x ∂νProof (Lean source)
theorem setIntegral_guardedScore_eq_derivative (ν μ : Measure α) [IsFiniteMeasure ν] (q qdot : α → ℝ) (hq : Measurable q) (hqnonneg : ∀ᵐ x ∂ν, 0 ≤ q x) (hzero : ∀ᵐ x ∂ν, q x = 0 → qdot x = 0) (hμ : μ = ν.withDensity (fun x => ofReal (q x))) {A : Set α} (hA : MeasurableSet A) : ∫ x in A, guardedScore q qdot x ∂μ = ∫ x in A, qdot x ∂ν := by rw [hμ, restrict_withDensity hA, integral_withDensity_eq_integral_toReal_smul hq.ennreal_ofReal (by simp)] apply integral_congr_ae filter_upwards [ae_restrict_of_ae hqnonneg, ae_restrict_of_ae (derivative_eq_density_mul_guardedScore hzero)] with x hxq hxeq rw [ENNReal.toReal_ofReal hxq, smul_eq_mul, ← hxeq] -
condExp_eq_statistic_iff_integral_preimage_eqtheorem — A measurable statistic with its pushed-forward law, integrable source and statistic functions, and a measurable statistic function has its conditional expectation equal to the pulled-back statistic function exactly when their integrals agree on every measurable statistic event.hypothesesΩ :sharedType u_2Y :sharedType u_3T :sharedΩ → YhT :hμYmap :μY = μΩ.map Tf :Ω → ℝg :Y → ℝhf :Integrable f μΩhg :Integrable g μYhgmeas :conclusion(μΩ[f | comap T inferInstance] =ᵐ[μΩ] fun ω => g (T ω))↔ ∀ A : Set Y, MeasurableSet A → ∫ ω in T ⁻¹' A, f ω ∂μΩ = ∫ y in A, g y ∂μYProof (Lean source)
theorem condExp_eq_statistic_iff_integral_preimage_eq (hT : Measurable T) (hμYmap : μY = μΩ.map T) (f : Ω → ℝ) (g : Y → ℝ) (hf : Integrable f μΩ) (hg : Integrable g μY) (hgmeas : Measurable g) : (μΩ[f | comap T inferInstance] =ᵐ[μΩ] fun ω => g (T ω)) ↔ ∀ A : Set Y, MeasurableSet A → ∫ ω in T ⁻¹' A, f ω ∂μΩ = ∫ y in A, g y ∂μY := by have hmap (A : Set Y) (hA : MeasurableSet A) : ∫ ω in T ⁻¹' A, g (T ω) ∂μΩ = ∫ y in A, g y ∂μY := by rw [hμYmap] exact (setIntegral_map hA hgmeas.aestronglyMeasurable hT.aemeasurable).symm constructor · intro hcond A hA calc ∫ ω in T ⁻¹' A, f ω ∂μΩ = ∫ ω in T ⁻¹' A, (μΩ[f | comap T inferInstance]) ω ∂μΩ := (setIntegral_condExp hT.comap_le hf ⟨A, hA, rfl⟩).symm _ = ∫ ω in T ⁻¹' A, g (T ω) ∂μΩ := setIntegral_congr_ae (hT hA) (hcond.mono fun ω hω _ => hω) _ = ∫ y in A, g y ∂μY := hmap A hA · intro hintegral have hgmap : Integrable g (μΩ.map T) := by simpa only [hμYmap] using hg have hgcomp : Integrable (fun ω => g (T ω)) μΩ := by simpa only [Function.comp_def] using hgmap.comp_measurable hT have hTcomap : Measurable[comap T inferInstance] T := comap_measurable T have hgstrong : StronglyMeasurable[comap T inferInstance] (fun ω => g (T ω)) := hgmeas.stronglyMeasurable.comp_measurable hTcomap exact condExp_eq_of_integral_preimage_eq μΩ T hT f (fun ω => g (T ω)) hf hgcomp hgstrong.aestronglyMeasurable (by intro A hA exact (hintegral A hA).trans (hmap A hA).symm) -
score_integral_preimage_eqtheorem — Finite source and statistic reference measures, source and statistic laws, a measurable statistic, densities and derivative densities, all measurable except possibly the source derivative density, nonnegative densities, zero-set derivative controls, the source and statistic density laws, an exact derivative pushforward identity, and a measurable statistic event give equal source-score and pulled-back statistic-score integrals on that event.hypothesesΩ :sharedType u_2Y :sharedType u_3T :sharedΩ → YqΩ :sharedΩ → ℝqdotΩ :sharedΩ → ℝqY :sharedY → ℝqdotY :sharedY → ℝhT :hqΩ :Measurable qΩhqY :Measurable qYhqdotY :Measurable qdotYhqΩnonneg :∀ᵐ ω ∂νΩ, 0 ≤ qΩ ωhqYnonneg :∀ᵐ y ∂νY, 0 ≤ qY yhzeroΩ :∀ᵐ ω ∂νΩ, qΩ ω = 0 → qdotΩ ω = 0hzeroY :∀ᵐ y ∂νY, qY y = 0 → qdotY y = 0hμΩ :μΩ = νΩ.withDensity (fun ω => ofReal (qΩ ω))hμYmap :μY = μΩ.map ThμYdensity :μY = νY.withDensity (fun y => ofReal (qY y))hderivMap :∀ A : Set Yifthen∫ ω in T ⁻¹' A, qdotΩ ω ∂νΩ = ∫ y in A, qdotY y ∂νYA :Set YhA :conclusion∫ ω in T ⁻¹' A, guardedScore qΩ qdotΩ ω ∂μΩ= ∫ ω in T ⁻¹' A, guardedScore qY qdotY (T ω) ∂μΩProof (Lean source)
theorem score_integral_preimage_eq (hT : Measurable T) (hqΩ : Measurable qΩ) (hqY : Measurable qY) (hqdotY : Measurable qdotY) (hqΩnonneg : ∀ᵐ ω ∂νΩ, 0 ≤ qΩ ω) (hqYnonneg : ∀ᵐ y ∂νY, 0 ≤ qY y) (hzeroΩ : ∀ᵐ ω ∂νΩ, qΩ ω = 0 → qdotΩ ω = 0) (hzeroY : ∀ᵐ y ∂νY, qY y = 0 → qdotY y = 0) (hμΩ : μΩ = νΩ.withDensity (fun ω => ofReal (qΩ ω))) (hμYmap : μY = μΩ.map T) (hμYdensity : μY = νY.withDensity (fun y => ofReal (qY y))) (hderivMap : ∀ A : Set Y, MeasurableSet A → ∫ ω in T ⁻¹' A, qdotΩ ω ∂νΩ = ∫ y in A, qdotY y ∂νY) (A : Set Y) (hA : MeasurableSet A) : ∫ ω in T ⁻¹' A, guardedScore qΩ qdotΩ ω ∂μΩ = ∫ ω in T ⁻¹' A, guardedScore qY qdotY (T ω) ∂μΩ := by have hmap : ∫ ω in T ⁻¹' A, guardedScore qY qdotY (T ω) ∂μΩ = ∫ y in A, guardedScore qY qdotY y ∂μY := by rw [hμYmap] exact (setIntegral_map hA (measurable_guardedScore hqY hqdotY).aestronglyMeasurable hT.aemeasurable).symm calc ∫ ω in T ⁻¹' A, guardedScore qΩ qdotΩ ω ∂μΩ = ∫ ω in T ⁻¹' A, qdotΩ ω ∂νΩ := setIntegral_guardedScore_eq_derivative νΩ μΩ qΩ qdotΩ hqΩ hqΩnonneg hzeroΩ hμΩ (hT hA) _ = ∫ y in A, qdotY y ∂νY := hderivMap A hA _ = ∫ y in A, guardedScore qY qdotY y ∂μY := (setIntegral_guardedScore_eq_derivative νY μY qY qdotY hqY hqYnonneg hzeroY hμYdensity hA).symm _ = ∫ ω in T ⁻¹' A, guardedScore qY qdotY (T ω) ∂μΩ := hmap.symm
SupportTransfer 2 core · 0 supporting This file defines a real-valued event indicator and proves a measure-theoretic support-transfer theorem under a normalized restriction to a positive-mass cell. ★ ae_abs_target_le_of_indep_positive_event
Support Transfer Across an Independent Event
This file defines a real-valued event indicator and proves a measure-theoretic support-transfer theorem under a normalized restriction to a positive-mass cell. Independence from a positive-probability event and almost-everywhere agreement on that event transfer an absolute bound from a reference quantity to the target quantity throughout the cell.
def eventIndicator reviewed
⚑ flagged
Causalean.Stat
Given a sample space and an event in it, the real-valued event indicator equals one for sample points in the event and zero for all other sample points.
Definition (Lean source)
parameters
Omega :
Type*
A :
Set Omega
def
eventIndicator A :
Omega → ℝ
given by
A.indicator (fun _ => 1)
theorem ae_abs_target_le_of_indep_positive_event reviewed
⚑ flagged
Causalean.Stat
Within a measurable positive-mass cell, for a measurable event, if a target quantity is measurable, the event has positive normalized cell probability, the target is independent of the event indicator under the normalized cell law, a reference quantity agrees almost surely with the target on that event, and the reference obeys an absolute bound there, then the target obeys the same absolute bound almost surely throughout the cell.
Formal statement
hypotheses
Omega :
C A :
Set Omega
_hC :
hCpos :
0 < P C
_hA :
target reference :
Omega → ℝ
hTarget :
Measurable target
hEventPos :
0 < normalizedRestrict P C A
hInd :
IndepFun target (eventIndicator A) (normalizedRestrict P C)
hAgreement :
reference =ᵐ[(normalizedRestrict P C).restrict A] target
R :
ℝ
hReferenceBound :
∀ᵐ omega ∂(normalizedRestrict P C).restrict A, |reference omega| ≤ R
conclusion
∀ᵐ omega ∂P.restrict C, |target omega| ≤ R
Proof (Lean source)
theorem ae_abs_target_le_of_indep_positive_event
{Omega : Type*} [MeasurableSpace Omega]
{P : Measure Omega} [IsProbabilityMeasure P]
{C A : Set Omega} (_hC : MeasurableSet C) (hCpos : 0 < P C)
(_hA : MeasurableSet A)
{target reference : Omega → ℝ} (hTarget : Measurable target)
(hEventPos : 0 < normalizedRestrict P C A)
(hInd : IndepFun target (eventIndicator A) (normalizedRestrict P C))
(hAgreement :
reference =ᵐ[(normalizedRestrict P C).restrict A] target)
{R : ℝ}
(hReferenceBound :
∀ᵐ omega ∂(normalizedRestrict P C).restrict A,
|reference omega| ≤ R) :
∀ᵐ omega ∂P.restrict C, |target omega| ≤ R := by
let B : Set Omega := {omega | R < |target omega|}
have hBadRange : MeasurableSet {y : ℝ | R < |y|} := by
rw [show {y : ℝ | R < |y|} = {y : ℝ | R < ‖y‖} by
ext y
simp only [Real.norm_eq_abs]]
exact measurableSet_lt measurable_const (by fun_prop)
have hB : MeasurableSet B := hTarget hBadRange
have hTargetBoundEvent :
∀ᵐ omega ∂(normalizedRestrict P C).restrict A,
|target omega| ≤ R := by
filter_upwards [hAgreement, hReferenceBound] with omega hEq hBound
rw [← hEq]
exact hBound
have hBAzero : normalizedRestrict P C (B ∩ A) = 0 := by
rw [measure_eq_zero_iff_ae_notMem]
filter_upwards [ae_imp_of_ae_restrict hTargetBoundEvent] with omega homega
intro hmem
exact (not_lt_of_ge (homega hmem.2)) hmem.1
have hEventPreimage : eventIndicator A ⁻¹' ({1} : Set ℝ) = A := by
ext omega
simp [eventIndicator]
have hFactor :
normalizedRestrict P C (B ∩ A) =
normalizedRestrict P C B * normalizedRestrict P C A := by
simpa [B, hEventPreimage] using
hInd.measure_inter_preimage_eq_mul
{y : ℝ | R < |y|} ({1} : Set ℝ)
hBadRange (measurableSet_singleton (1 : ℝ))
have hBzero : normalizedRestrict P C B = 0 := by
have hprod :
normalizedRestrict P C B * normalizedRestrict P C A = 0 := by
rw [← hFactor, hBAzero]
exact (mul_eq_zero.mp hprod).resolve_right hEventPos.ne'
apply (ae_normalizedRestrict_iff hCpos).mp
filter_upwards [(measure_eq_zero_iff_ae_notMem.mp hBzero)] with omega homega
exact le_of_not_gt (by simpa [B] using homega)
DoobInformation 4 core · 8 supporting For a square-integrable score under one probability law, this module develops the finite-horizon decomposition into conditional-expectation increments along an arbitrary filtration. ★ fisher_eq_sum★ guarded_density_fisher_eq_doob_sum
Finite-horizon Doob information decomposition
For a square-integrable score under one probability law, this module develops the finite-horizon decomposition into conditional-expectation increments along an arbitrary filtration. It supplies centering, orthogonality, information additivity, a uniform increment-budget bound, and a density-facing Fisher-information corollary without disintegration or stagewise Radon–Nikodym derivatives.
def increment reviewed
⚑ flagged
Causalean.Stat.DoobInformation
A probability law, filtration, terminal score, and stage determine the Doob score increment, given by the change in the score's conditional expectation between the two adjacent prefix σ-algebras.
Definition (Lean source)
parameters
def
increment μ F S k :
Ω → ℝ
given by
fun ω => μ[S | F (k + 1)] ω - μ[S | F k] ω
def doobArray reviewed
⚑ flagged
Causalean.Stat.DoobInformation
A probability law, filtration, terminal score, square-integrability certificate, and horizon determine the constant-row Doob martingale-difference array, given by the Doob construction in which every row uses this same law, filtration, and score, has length equal to the horizon, and has as its entry at each stage the change in the score's conditional expectation between the two adjacent prefix σ-algebras.
Definition (Lean source)
parameters
def
given by
doobMartingaleDifferenceArray (μ := fun _ => μ) (fun _ => n) (fun _ => F) (fun _ => S) (fun _ => hS)
theorem fisher_eq_sum reviewed
⚑ flagged
Causalean.Stat.DoobInformation
Under a probability law and filtration, if a square-integrable terminal score is its terminal conditional expectation and has zero initial conditional expectation, then its Fisher-information second moment, the expectation of the squared score, equals the sum over the stages before the horizon of the increment second moments at the given horizon.
Formal statement
Proof (Lean source)
theorem fisher_eq_sum (hS : MemLp S 2 μ) (n : ℕ)
(hterminal : μ[S | F n] =ᵐ[μ] S)
(hinitial : μ[S | F 0] =ᵐ[μ] (0 : Ω → ℝ)) :
∫ ω, S ω ^ 2 ∂μ =
∑ k ∈ range n, ∫ ω, increment μ F S k ω ^ 2 ∂μ := by
let d : ℕ → Ω → ℝ := increment μ F S
let t : ℕ → Ω → ℝ := fun r ω => ∑ k ∈ range r, d k ω
have hd (k : ℕ) : MemLp (d k) 2 μ := increment_memLp (μ := μ) F S hS k
have ht (r : ℕ) : MemLp (t r) 2 μ := by
induction r with
| zero => simp [t]
| succ r ihr =>
convert ihr.add (hd r) using 1
funext ω
simp [t, Finset.sum_range_succ]
have hsq (r : ℕ) :
∫ ω, t r ω ^ 2 ∂μ = ∑ k ∈ range r, ∫ ω, d k ω ^ 2 ∂μ := by
induction r with
| zero => simp [t]
| succ r ihr =>
have hcross : ∫ ω, t r ω * d r ω ∂μ = 0 := by
calc
_ = ∫ ω, ∑ k ∈ range r, d k ω * d r ω ∂μ := by
congr 1
funext ω
simp [t, Finset.sum_mul]
_ = ∑ k ∈ range r, ∫ ω, d k ω * d r ω ∂μ := by
exact integral_finsetSum _ (by
intro k hk
exact (hd k).integrable_mul (hd r))
_ = 0 := by
apply Finset.sum_eq_zero
intro k hk
exact increment_orthogonal (μ := μ) F S hS
(Nat.ne_of_lt (Finset.mem_range.mp hk))
have hrr : Integrable (fun ω => t r ω * t r ω) μ :=
(ht r).integrable_mul (ht r)
have hrd : Integrable (fun ω => t r ω * d r ω) μ :=
(ht r).integrable_mul (hd r)
have hdr : Integrable (fun ω => d r ω * t r ω) μ :=
(hd r).integrable_mul (ht r)
have hdd : Integrable (fun ω => d r ω * d r ω) μ :=
(hd r).integrable_mul (hd r)
calc
∫ ω, t (r + 1) ω ^ 2 ∂μ =
∫ ω, (t r ω * t r ω + t r ω * d r ω) +
(d r ω * t r ω + d r ω * d r ω) ∂μ := by
congr 1
funext ω
simp only [t, Finset.sum_range_succ]
ring
_ = (∫ ω, t r ω * t r ω ∂μ) +
(∫ ω, t r ω * d r ω ∂μ) +
(∫ ω, d r ω * t r ω ∂μ) +
(∫ ω, d r ω * d r ω ∂μ) := by
have houter := integral_add (hrr.add hrd) (hdr.add hdd)
have hleft := integral_add hrr hrd
have hright := integral_add hdr hdd
simpa only [Pi.add_apply, hleft, hright, add_assoc] using houter
_ = ∑ k ∈ range (r + 1), ∫ ω, d k ω ^ 2 ∂μ := by
rw [hcross]
have hcross' : ∫ ω, d r ω * t r ω ∂μ = 0 := by
convert hcross using 1
congr 1
funext ω
ring
rw [hcross']
simp only [← pow_two, add_zero, Finset.sum_range_succ]
exact congrArg (· + ∫ ω, d r ω ^ 2 ∂μ) ihr
have hae : t n =ᵐ[μ] S := by
filter_upwards [increment_sum (μ := μ) F S hS n, hterminal, hinitial] with
ω hsum hterm hinit
dsimp [t, d] at hsum ⊢
rw [hsum, hterm, hinit]
simp
calc
∫ ω, S ω ^ 2 ∂μ = ∫ ω, t n ω ^ 2 ∂μ :=
integral_congr_ae (by
filter_upwards [hae] with ω hw
rw [hw])
_ = ∑ k ∈ range n, ∫ ω, increment μ F S k ω ^ 2 ∂μ := hsq n
theorem guarded_density_fisher_eq_doob_sum reviewed
⚑ flagged
Causalean.Stat.DoobInformation
A finite reference measure, probability law, filtration, horizon, density, density derivative, and score with a measurable density, the law having density q with respect to the reference measure, almost-everywhere nonnegative density, the score identity that the density derivative equals the density times the score almost everywhere under the reference measure, square-integrable score under the law, and the score agreeing almost surely with its conditional expectation at the horizon while its conditional expectation at stage zero vanishes almost surely have a guarded density Fisher integral, the reference-measure integral of the squared density derivative divided by the density with the integrand set to zero where the density vanishes, equal to the sum over the stages before the horizon of the second moments of the Doob score increments.
Formal statement
hypotheses
F :
Filtration ℕ mΩ
n :
ℕ
q qdot S :
Ω → ℝ
hq :
hμ :
μ = ν.withDensity (fun ω => ofReal (q ω))
hqnonneg :
∀ᵐ ω ∂ν, 0 ≤ q ω
hscore :
∀ᵐ ω ∂ν, qdot ω = q ω * S ω
hS :
MemLp S 2 μ
hterminal :
μ[S | F n] =ᵐ[μ] S
hinitial :
μ[S | F 0] =ᵐ[μ] (0 : Ω → ℝ)
conclusion
(∫ ω, (if q ω = 0 then 0 else qdot ω ^ 2 / q ω) ∂ν)
= ∑ k ∈ range n, ∫ ω, increment μ F S k ω ^ 2 ∂μ
Proof (Lean source)
theorem guarded_density_fisher_eq_doob_sum
(F : Filtration ℕ mΩ) (n : ℕ) (q qdot S : Ω → ℝ)
(hq : Measurable q)
(hμ : μ = ν.withDensity (fun ω => ofReal (q ω)))
(hqnonneg : ∀ᵐ ω ∂ν, 0 ≤ q ω)
(hscore : ∀ᵐ ω ∂ν, qdot ω = q ω * S ω)
(hS : MemLp S 2 μ)
(hterminal : μ[S | F n] =ᵐ[μ] S)
(hinitial : μ[S | F 0] =ᵐ[μ] (0 : Ω → ℝ)) :
(∫ ω, (if q ω = 0 then 0 else qdot ω ^ 2 / q ω) ∂ν) =
∑ k ∈ range n, ∫ ω, increment μ F S k ω ^ 2 ∂μ := by
rw [guarded_density_fisher_eq q qdot S hq hμ hqnonneg hscore]
exact fisher_eq_sum F S hS n hterminal hinitial
8 supporting declarations (lemmas, instances)
-
increment_eq_doobArraytheorem — Given a probability law, filtration, square-integrable terminal score, horizon, and stage, the score increment agrees with the matching entry of its constant-row Doob array.hypothesesconclusionincrement μ F S k = (doobArray μ F S hS n).increment 0 kProof (Lean source)
theorem increment_eq_doobArray (hS : MemLp S 2 μ) (n k : ℕ) : increment μ F S k = (doobArray μ F S hS n).increment 0 k := by rfl -
increment_memLptheorem — Under a probability law and filtration, a square-integrable terminal score has a square-integrable score increment at every stage, including the specified stage.Proof (Lean source)
theorem increment_memLp (hS : MemLp S 2 μ) (k : ℕ) : MemLp (increment μ F S k) 2 μ := by rw [increment_eq_doobArray (μ := μ) F S hS (k + 1) k] exact (doobArray μ F S hS (k + 1)).squareIntegrable 0 k (by simpa [doobArray, doobMartingaleDifferenceArray] using lt_succ_self k) -
increment_stronglyMeasurabletheorem — Under a probability law and filtration, a square-integrable terminal score has an increment measurable at the next prefix σ-algebra for the given stage.hypothesesconclusionStronglyMeasurable[F (k + 1)] (increment μ F S k)Proof (Lean source)
theorem increment_stronglyMeasurable (hS : MemLp S 2 μ) (k : ℕ) : StronglyMeasurable[F (k + 1)] (increment μ F S k) := by rw [increment_eq_doobArray (μ := μ) F S hS (k + 1) k] exact (doobArray μ F S hS (k + 1)).adapted 0 k (by simpa [doobArray, doobMartingaleDifferenceArray] using lt_succ_self k) -
increment_condExp_zerotheorem — Under a probability law and filtration, the increment of a square-integrable terminal score has conditional mean zero at the preceding prefix σ-algebra for the given stage.hypothesesconclusionμ[increment μ F S k | F k] =ᵐ[μ] (0 : Ω → ℝ)Proof (Lean source)
theorem increment_condExp_zero (hS : MemLp S 2 μ) (k : ℕ) : μ[increment μ F S k | F k] =ᵐ[μ] (0 : Ω → ℝ) := by rw [increment_eq_doobArray (μ := μ) F S hS (k + 1) k] exact (doobArray μ F S hS (k + 1)).condExp_zero 0 k (by simpa [doobArray, doobMartingaleDifferenceArray] using lt_succ_self k) -
increment_sumtheorem — Under a probability law and filtration, the increments of a square-integrable terminal score have a finite sum equal almost everywhere to the difference between terminal and initial conditional expectations at the given horizon.hypothesesconclusion(fun ω => ∑ k ∈ range n, increment μ F S k ω)=ᵐ[μ] (fun ω => μ[S | F n] ω - μ[S | F 0] ω)Proof (Lean source)
theorem increment_sum (hS : MemLp S 2 μ) (n : ℕ) : (fun ω => ∑ k ∈ range n, increment μ F S k ω) =ᵐ[μ] (fun ω => μ[S | F n] ω - μ[S | F 0] ω) := by have hsum : (fun ω => ∑ k ∈ range n, increment μ F S k ω) = (doobArray μ F S hS n).rowSum 0 := by funext ω simp only [MartingaleDifferenceArray.rowSum, Finset.sum_apply] change (∑ k ∈ range n, increment μ F S k ω) = ∑ k ∈ range n, (doobArray μ F S hS n).increment 0 k ω apply Finset.sum_congr rfl intro k _ exact congrFun (increment_eq_doobArray (μ := μ) F S hS n k) ω have hrow := doobMartingaleDifferenceArray_rowSum (μ := fun _ => μ) (fun _ => n) (fun _ => F) (fun _ => S) (fun _ => hS) 0 change (doobArray μ F S hS n).rowSum 0 = (fun ω => μ[S | F n] ω - μ[S | F 0] ω) at hrow exact Filter.Eventually.of_forall (fun ω => congrFun (hsum.trans hrow) ω) -
increment_orthogonaltheorem — Under a probability law and filtration, distinct stages of the Doob increments for a square-integrable terminal score are orthogonal in the squared-integrable sense, whenever the two stages differ.hypothesesconclusion∫ ω, increment μ F S i ω * increment μ F S j ω ∂μ = 0Proof (Lean source)
theorem increment_orthogonal (hS : MemLp S 2 μ) {i j : ℕ} (hij : i ≠ j) : ∫ ω, increment μ F S i ω * increment μ F S j ω ∂μ = 0 := by have hforward {a b : ℕ} (hab : a < b) : ∫ ω, increment μ F S a ω * increment μ F S b ω ∂μ = 0 := by have hm : F (a + 1) ≤ F b := F.mono (succ_le_of_lt hab) have hmeas : StronglyMeasurable[F b] (increment μ F S a) := (increment_stronglyMeasurable (μ := μ) F S hS a).mono hm have ha := increment_memLp (μ := μ) F S hS a have hb := increment_memLp (μ := μ) F S hS b have hprod : Integrable (increment μ F S a * increment μ F S b) μ := ha.integrable_mul hb have hpull := condExp_mul_of_stronglyMeasurable_left hmeas hprod (hb.integrable (by norm_num)) calc ∫ ω, increment μ F S a ω * increment μ F S b ω ∂μ = ∫ ω, μ[increment μ F S a * increment μ F S b | F b] ω ∂μ := by exact (integral_condExp (F.le b)).symm _ = ∫ ω, increment μ F S a ω * μ[increment μ F S b | F b] ω ∂μ := integral_congr_ae hpull _ = 0 := by have hz : (fun ω => increment μ F S a ω * μ[increment μ F S b | F b] ω) =ᵐ[μ] (0 : Ω → ℝ) := by filter_upwards [increment_condExp_zero (μ := μ) F S hS b] with ω hω simp only [Pi.zero_apply] at hω simp [hω] rw [integral_congr_ae hz] simp rcases lt_or_gt_of_ne hij with h | h · exact hforward h · rw [show (fun ω => increment μ F S i ω * increment μ F S j ω) = (fun ω => increment μ F S j ω * increment μ F S i ω) from funext (fun ω => mul_comm _ _)] exact hforward h -
fisher_le_multheorem — Under a probability law and filtration, if a square-integrable terminal score has the terminal and initial conditional-expectation identities and each active increment's second moment is bounded, then the score's Fisher information is at most the horizon times the common bound for the given horizon and bound.hypothesesS :sharedΩ → ℝhS :MemLp S 2 μn :ℕB :ℝhterminal :μ[S | F n] =ᵐ[μ] Shinitial :μ[S | F 0] =ᵐ[μ] (0 : Ω → ℝ)hbound :∀ k < n, ∫ ω, increment μ F S k ω ^ 2 ∂μ ≤ Bconclusion∫ ω, S ω ^ 2 ∂μ ≤ (n : ℝ) * BProof (Lean source)
theorem fisher_le_mul (hS : MemLp S 2 μ) (n : ℕ) (B : ℝ) (hterminal : μ[S | F n] =ᵐ[μ] S) (hinitial : μ[S | F 0] =ᵐ[μ] (0 : Ω → ℝ)) (hbound : ∀ k < n, ∫ ω, increment μ F S k ω ^ 2 ∂μ ≤ B) : ∫ ω, S ω ^ 2 ∂μ ≤ (n : ℝ) * B := by rw [fisher_eq_sum (μ := μ) F S hS n hterminal hinitial] calc ∑ k ∈ range n, ∫ ω, increment μ F S k ω ^ 2 ∂μ ≤ ∑ _k ∈ range n, B := by apply Finset.sum_le_sum intro k hk exact hbound k (Finset.mem_range.mp hk) _ = (n : ℝ) * B := by simp -
guarded_density_fisher_eqtheorem — A finite reference measure, probability law, density, density derivative, and score with a measurable density, the stated density representation, almost-everywhere nonnegative density, and almost-everywhere score identity have a guarded density Fisher integral equal to the score second moment.hypothesesq qdot S :Ω → ℝhq :hμ :μ = ν.withDensity (fun ω => ofReal (q ω))hqnonneg :∀ᵐ ω ∂ν, 0 ≤ q ωhscore :∀ᵐ ω ∂ν, qdot ω = q ω * S ωconclusion(∫ ω, (if q ω = 0 then 0 else qdot ω ^ 2 / q ω) ∂ν) = ∫ ω, S ω ^ 2 ∂μProof (Lean source)
theorem guarded_density_fisher_eq (q qdot S : Ω → ℝ) (hq : Measurable q) (hμ : μ = ν.withDensity (fun ω => ofReal (q ω))) (hqnonneg : ∀ᵐ ω ∂ν, 0 ≤ q ω) (hscore : ∀ᵐ ω ∂ν, qdot ω = q ω * S ω) : (∫ ω, (if q ω = 0 then 0 else qdot ω ^ 2 / q ω) ∂ν) = ∫ ω, S ω ^ 2 ∂μ := by have hquot : (fun ω => if q ω = 0 then 0 else qdot ω ^ 2 / q ω) =ᵐ[ν] (fun ω => q ω * S ω ^ 2) := by filter_upwards [hscore] with ω hs by_cases hq0 : q ω = 0 · simp [hq0] · rw [hs] simp only [hq0, ↓reduceIte] field_simp calc (∫ ω, (if q ω = 0 then 0 else qdot ω ^ 2 / q ω) ∂ν) = ∫ ω, q ω * S ω ^ 2 ∂ν := integral_congr_ae hquot _ = ∫ ω, S ω ^ 2 ∂μ := by rw [hμ, integral_withDensity_eq_integral_toReal_smul hq.ennreal_ofReal (by simp)] apply integral_congr_ae filter_upwards [hqnonneg] with ω hn simp [ENNReal.toReal_ofReal hn, smul_eq_mul]
GaussianCovariance 7 core · 13 supporting This module defines the Gaussian covariance discrepancy on finite positive-definite matrices and derives its compact-model attainment, strict separation, perturbation stability, and finite-model-selection interfaces. ★ finiteCovarianceModel_populationGap
Gaussian covariance discrepancy and finite model selection
This module defines the Gaussian covariance discrepancy on finite positive-definite matrices and derives its compact-model attainment, strict separation, perturbation stability, and finite-model-selection interfaces. The model assumptions are stated separately from the matrix inequality, so the results can be reused for any finite family of covariance models.
abbrev PositiveCovariance reviewed
⚑ flagged
Causalean.Stat
For a finite coordinate type, the positive covariance matrices are real square matrices equipped with a proof of positive definiteness.
def gaussianCovarianceDiscrepancy reviewed
⚑ flagged
Causalean.Stat
For a candidate covariance matrix and target second-moment matrix, the Gaussian covariance discrepancy is log determinant plus inverse-weighted trace.
Definition (Lean source)
def normalizedCovarianceDiscrepancy reviewed
⚑ flagged
Causalean.Stat
For positive-definite candidate and target covariances, the normalized Gaussian covariance discrepancy subtracts the criterion's value at the target.
Definition (Lean source)
parameters
K T :
def
normalizedCovarianceDiscrepancy K T :
ℝ
given by
gaussianCovarianceDiscrepancy (K : Matrix V V ℝ) T
- gaussianCovarianceDiscrepancy (T : Matrix V V ℝ) T
def IsDiscrepancyAttainedOn reviewed
⚑ flagged
Causalean.Stat
For a covariance model and target matrix, discrepancy attainment means that one model member has no larger Gaussian discrepancy than every other member.
Definition (Lean source)
parameters
def
IsDiscrepancyAttainedOn M T :
Prop
given by
∃ K ∈ M,
∀ L ∈ M,
gaussianCovarianceDiscrepancy (K : Matrix V V ℝ) T
≤ gaussianCovarianceDiscrepancy (L : Matrix V V ℝ) T
def HasCompactDiscrepancySublevel reviewed
⚑ flagged
Causalean.Stat
For a covariance model and target matrix, a compact discrepancy sublevel is a nonempty compact cut of the model below some criterion value.
Definition (Lean source)
parameters
def
HasCompactDiscrepancySublevel M T :
Prop
given by
∃ c : ℝ,
clause 1
(M ∩ {K | gaussianCovarianceDiscrepancy (K : Matrix V V ℝ) T ≤ c}).Nonempty
clause 2
def covarianceModelLoss reviewed
⚑ flagged
Causalean.Stat
For a covariance model and target matrix, the population loss is the infimum Gaussian discrepancy over positive-definite model covariances.
Definition (Lean source)
parameters
def
covarianceModelLoss M T :
ℝ
given by
theorem finiteCovarianceModel_populationGap reviewed
⚑ flagged
Causalean.Stat
Given a finite family of covariance models whose members are compact and nonempty, and a positive-definite true covariance contained in at least one model, the population losses have the positive gap required by finite penalized model selection.
Formal statement
hypotheses
V :
Type u_2
I :
Type u_3
Fintype V
Fintype I
Nonempty I
models :
I → Set (PositiveCovariance V)
hcompact :
∀ i, IsCompact (models i)
hne :
∀ i, (models i).Nonempty
T :
hcontains :
∃ i, T ∈ models i
conclusion
∃ gap : ℝ,
0 < gap
conclusion 1
i ∈ Causalean.Stat.populationMinimizers
(fun j => covarianceModelLoss (models j) T) :
j ∉ Causalean.Stat.populationMinimizers
(fun k => covarianceModelLoss (models k) T) :
covarianceModelLoss (models i) T + gap ≤ covarianceModelLoss (models j) T
Proof (Lean source)
theorem finiteCovarianceModel_populationGap [Fintype V] [DecidableEq V]
[Fintype I] [Nonempty I]
(models : I → Set (PositiveCovariance V))
(hcompact : ∀ i, IsCompact (models i)) (hne : ∀ i, (models i).Nonempty)
(T : PositiveCovariance V) (hcontains : ∃ i, T ∈ models i) :
∃ gap : ℝ, 0 < gap ∧
∀ i ∈ populationMinimizers
(fun j => covarianceModelLoss (models j) T),
∀ j ∉ populationMinimizers
(fun k => covarianceModelLoss (models k) T),
covarianceModelLoss (models i) T + gap ≤
covarianceModelLoss (models j) T := by
classical
let minimizers := populationMinimizers
(fun j => covarianceModelLoss (models j) T)
let bad : Finset I := Finset.univ.filter fun j => j ∉ minimizers
by_cases hbad : bad.Nonempty
· obtain ⟨j0, hj0bad, hj0min⟩ := Finset.exists_min_image bad
(fun j => covarianceModelLoss (models j) T) hbad
have hj0not : j0 ∉ minimizers := (Finset.mem_filter.mp hj0bad).2
have hj0T : T ∉ models j0 := by
simpa [minimizers, populationMinimizers_covarianceModelLoss_iff
models hcompact hne T hcontains j0] using hj0not
have hbase_lt : gaussianCovarianceDiscrepancy (T : Matrix V V ℝ) T <
covarianceModelLoss (models j0) T :=
lt_of_le_of_ne (covarianceModelLoss_ge_truth (hcompact j0) (hne j0) T)
(fun h => hj0T ((covarianceModelLoss_eq_truth_iff
(hcompact j0) (hne j0) T).mp h.symm))
refine ⟨covarianceModelLoss (models j0) T -
gaussianCovarianceDiscrepancy (T : Matrix V V ℝ) T, sub_pos.mpr hbase_lt, ?_⟩
intro i hi j hj
have hiT : T ∈ models i := by
exact (populationMinimizers_covarianceModelLoss_iff
models hcompact hne T hcontains i).mp hi
have hjbad : j ∈ bad := Finset.mem_filter.mpr ⟨Finset.mem_univ _, hj⟩
rw [(covarianceModelLoss_eq_truth_iff (hcompact i) (hne i) T).2 hiT]
linarith [hj0min j hjbad]
· refine ⟨1, zero_lt_one, ?_⟩
intro i hi j hj
exfalso
exact hbad ⟨j, Finset.mem_filter.mpr ⟨Finset.mem_univ _, hj⟩⟩
13 supporting declarations (lemmas, instances)
-
continuous_gaussianCovarianceDiscrepancytheorem — The Gaussian covariance discrepancy varies continuously with its positive-definite candidate and target matrix.hypothesesconclusionContinuous (fun p : PositiveCovariance V × Matrix V V ℝ => gaussianCovarianceDiscrepancy (p.1 : Matrix V V ℝ) p.2)Proof (Lean source)
theorem continuous_gaussianCovarianceDiscrepancy [Fintype V] [DecidableEq V] : Continuous (fun p : PositiveCovariance V × Matrix V V ℝ => gaussianCovarianceDiscrepancy (p.1 : Matrix V V ℝ) p.2) := by rw [continuous_iff_continuousAt] intro p unfold gaussianCovarianceDiscrepancy apply ContinuousAt.add · apply ContinuousAt.log · fun_prop · exact ne_of_gt p.1.property.det_pos · apply (continuous_id.matrix_trace.continuousAt.comp) apply ContinuousAt.mul · have hinv : ContinuousAt (fun x : ℝ => Ring.inverse x) (p.1.1.det) := by simpa [Ring.inverse_eq_inv] using continuousAt_inv₀ (ne_of_gt p.1.property.det_pos) simpa [Function.comp_def] using (continuousAt_matrix_inv _ hinv).comp (x := p) ((continuous_subtype_val.comp continuous_fst).continuousAt) · fun_prop -
continuous_normalizedCovarianceDiscrepancytheorem — The normalized Gaussian covariance discrepancy varies continuously with both positive-definite covariances.hypothesesconclusionContinuous (fun p : PositiveCovariance V × PositiveCovariance V => normalizedCovarianceDiscrepancy p.1 p.2)Proof (Lean source)
theorem continuous_normalizedCovarianceDiscrepancy [Fintype V] [DecidableEq V] : Continuous (fun p : PositiveCovariance V × PositiveCovariance V => normalizedCovarianceDiscrepancy p.1 p.2) := by unfold normalizedCovarianceDiscrepancy apply Continuous.sub · have h : Continuous (fun p : PositiveCovariance V × PositiveCovariance V => (p.1, (p.2 : Matrix V V ℝ))) := by fun_prop exact continuous_gaussianCovarianceDiscrepancy.comp h · have h : Continuous (fun p : PositiveCovariance V × PositiveCovariance V => (p.2, (p.2 : Matrix V V ℝ))) := by fun_prop exact continuous_gaussianCovarianceDiscrepancy.comp h -
normalizedCovarianceDiscrepancy_nonnegtheorem — For positive-definite candidate and target covariances, the normalized Gaussian covariance discrepancy is nonnegative.Proof (Lean source)
theorem normalizedCovarianceDiscrepancy_nonneg [Fintype V] [DecidableEq V] (K T : PositiveCovariance V) : 0 ≤ normalizedCovarianceDiscrepancy K T := by let S := CFC.sqrt ((K : Matrix V V ℝ)⁻¹) let A := S * (T : Matrix V V ℝ) * S obtain ⟨hA, hgap, -⟩ := normalizedCovarianceDiscrepancy_whiten K T rw [hgap] exact posDef_logdet_trace_gap_nonneg A hA -
normalizedCovarianceDiscrepancy_eq_zero_ifftheorem — For positive-definite candidate and target covariances, the normalized Gaussian covariance discrepancy is zero exactly when the two covariances agree.Proof (Lean source)
theorem normalizedCovarianceDiscrepancy_eq_zero_iff [Fintype V] [DecidableEq V] (K T : PositiveCovariance V) : normalizedCovarianceDiscrepancy K T = 0 ↔ K = T := by let S := CFC.sqrt ((K : Matrix V V ℝ)⁻¹) let A := S * (T : Matrix V V ℝ) * S obtain ⟨hA, hgap, hAone⟩ := normalizedCovarianceDiscrepancy_whiten K T rw [hgap, posDef_logdet_trace_gap_eq_zero_iff A hA, hAone] -
gaussianCovarianceDiscrepancy_le_truth_ifftheorem — For positive-definite candidate and target covariances, the candidate has no larger Gaussian discrepancy than the truth exactly when it is the truth.hypothesesK T :conclusiongaussianCovarianceDiscrepancy (K : Matrix V V ℝ) T≤ gaussianCovarianceDiscrepancy (T : Matrix V V ℝ) T ↔ K = TProof (Lean source)
theorem gaussianCovarianceDiscrepancy_le_truth_iff [Fintype V] [DecidableEq V] (K T : PositiveCovariance V) : gaussianCovarianceDiscrepancy (K : Matrix V V ℝ) T ≤ gaussianCovarianceDiscrepancy (T : Matrix V V ℝ) T ↔ K = T := by constructor · intro hle apply (normalizedCovarianceDiscrepancy_eq_zero_iff K T).mp have hnonneg := normalizedCovarianceDiscrepancy_nonneg K T unfold normalizedCovarianceDiscrepancy at hnonneg ⊢ linarith · rintro rfl exact le_rfl -
discrepancyAttainedOn_of_isCompacttheorem — Given a compact covariance model, a nonempty model, and a target matrix, the Gaussian discrepancy minimum is attained.Proof (Lean source)
theorem discrepancyAttainedOn_of_isCompact [Fintype V] [DecidableEq V] {M : Set (PositiveCovariance V)} (hM : IsCompact M) (hne : M.Nonempty) (T : Matrix V V ℝ) : IsDiscrepancyAttainedOn M T := by have hcont : Continuous (fun K : PositiveCovariance V => gaussianCovarianceDiscrepancy (K : Matrix V V ℝ) T) := continuous_gaussianCovarianceDiscrepancy.comp (continuous_id.prodMk continuous_const) obtain ⟨K, hKM, _, hKmin⟩ := hM.exists_sInf_image_eq_and_le hne hcont.continuousOn exact ⟨K, hKM, hKmin⟩ -
discrepancyAttainedOn_of_compactSubleveltheorem — Given a covariance model with a nonempty compact discrepancy sublevel, the global Gaussian discrepancy minimum is attained.hypotheseshM :conclusionProof (Lean source)
theorem discrepancyAttainedOn_of_compactSublevel [Fintype V] [DecidableEq V] {M : Set (PositiveCovariance V)} {T : Matrix V V ℝ} (hM : HasCompactDiscrepancySublevel M T) : IsDiscrepancyAttainedOn M T := by rcases hM with ⟨c, hne, hcompact⟩ let S : Set (PositiveCovariance V) := M ∩ {K | gaussianCovarianceDiscrepancy (K : Matrix V V ℝ) T ≤ c} have hatt := discrepancyAttainedOn_of_isCompact (M := S) hcompact hne T rcases hatt with ⟨K, hKS, hKmin⟩ refine ⟨K, hKS.1, ?_⟩ intro L hLM by_cases hLc : gaussianCovarianceDiscrepancy (L : Matrix V V ℝ) T ≤ c · exact hKmin L ⟨hLM, hLc⟩ · exact hKS.2.trans (le_of_lt (lt_of_not_ge hLc)) -
exists_positive_gap_of_attainedtheorem — Given an attained covariance-model discrepancy that omits the positive-definite truth, every model covariance has a common strictly positive normalized gap.hypotheseshatt :hT :T ∉ MProof (Lean source)
theorem exists_positive_gap_of_attained [Fintype V] [DecidableEq V] {M : Set (PositiveCovariance V)} {T : PositiveCovariance V} (hatt : IsDiscrepancyAttainedOn M T) (hT : T ∉ M) : ∃ gap : ℝ, 0 < gap ∧ ∀ K ∈ M, gap ≤ normalizedCovarianceDiscrepancy K T := by rcases hatt with ⟨K, hKM, hKmin⟩ refine ⟨normalizedCovarianceDiscrepancy K T, ?_, ?_⟩ · have hKT : K ≠ T := fun h => hT (h ▸ hKM) have hzero : normalizedCovarianceDiscrepancy K T ≠ 0 := fun h => hKT ((normalizedCovarianceDiscrepancy_eq_zero_iff K T).mp h) exact lt_of_le_of_ne (normalizedCovarianceDiscrepancy_nonneg K T) hzero.symm · intro L hLM unfold normalizedCovarianceDiscrepancy linarith [hKmin L hLM] -
exists_positive_gap_of_isCompacttheorem — Given a compact covariance model, a nonempty model, and a truth outside the model, the model is separated from the truth by a strictly positive population gap.hypotheseshM :hne :M.NonemptyT :hT :T ∉ MProof (Lean source)
theorem exists_positive_gap_of_isCompact [Fintype V] [DecidableEq V] {M : Set (PositiveCovariance V)} (hM : IsCompact M) (hne : M.Nonempty) {T : PositiveCovariance V} (hT : T ∉ M) : ∃ gap : ℝ, 0 < gap ∧ ∀ K ∈ M, gap ≤ normalizedCovarianceDiscrepancy K T := by exact exists_positive_gap_of_attained (discrepancyAttainedOn_of_isCompact hM hne T) hT -
exists_stable_positive_gaptheorem — Given a compact covariance model, a nonempty model, and a truth outside the model, the strict positive population gap persists for nearby positive-definite truths.hypotheseshM :hne :M.NonemptyT :hT :T ∉ Mconclusion∃ gap : ℝ,conclusion 10 < gapconclusion 2∃ U ∈ nhds T, ∀ T' ∈ U, ∀ K ∈ M, gap ≤ normalizedCovarianceDiscrepancy K T'Proof (Lean source)
theorem exists_stable_positive_gap [Fintype V] [DecidableEq V] {M : Set (PositiveCovariance V)} (hM : IsCompact M) (hne : M.Nonempty) {T : PositiveCovariance V} (hT : T ∉ M) : ∃ gap : ℝ, 0 < gap ∧ ∃ U ∈ nhds T, ∀ T' ∈ U, ∀ K ∈ M, gap ≤ normalizedCovarianceDiscrepancy K T' := by let m : PositiveCovariance V → ℝ := fun T' => sInf ((fun K : PositiveCovariance V => normalizedCovarianceDiscrepancy K T') '' M) have hjoint : Continuous (fun p : PositiveCovariance V × PositiveCovariance V => normalizedCovarianceDiscrepancy p.2 p.1) := continuous_normalizedCovarianceDiscrepancy.comp continuous_swap have hm : Continuous m := hM.continuous_sInf hjoint obtain ⟨delta, hdelta, hdelta_le⟩ := exists_positive_gap_of_isCompact hM hne hT have hcontT : Continuous (fun K : PositiveCovariance V => normalizedCovarianceDiscrepancy K T) := continuous_normalizedCovarianceDiscrepancy.comp (continuous_id.prodMk (continuous_const : Continuous fun _ : PositiveCovariance V => T)) obtain ⟨K0, hK0M, hm_eq, _⟩ := hM.exists_sInf_image_eq_and_le hne hcontT.continuousOn have hhalf : 0 < delta / 2 := half_pos hdelta have hhalf_m : delta / 2 < m T := by dsimp [m] rw [hm_eq] exact lt_of_lt_of_le (half_lt_self hdelta) (hdelta_le K0 hK0M) refine ⟨delta / 2, hhalf, {T' | delta / 2 < m T'}, ?_, ?_⟩ · exact (isOpen_lt continuous_const hm).mem_nhds hhalf_m · intro T' hT' K hKM exact hT'.le.trans (csInf_le (hM.image_of_continuousOn ((continuous_normalizedCovarianceDiscrepancy.comp (continuous_id.prodMk continuous_const)).continuousOn)).bddBelow (mem_image_of_mem _ hKM)) -
continuous_covarianceModelLosstheorem — Given a compact covariance model, the population loss is continuous in the target second-moment matrix.hypotheseshM :conclusionProof (Lean source)
theorem continuous_covarianceModelLoss [Fintype V] [DecidableEq V] {M : Set (PositiveCovariance V)} (hM : IsCompact M) : Continuous (covarianceModelLoss M) := by unfold covarianceModelLoss have hjoint : Continuous (fun p : Matrix V V ℝ × PositiveCovariance V => gaussianCovarianceDiscrepancy (p.2 : Matrix V V ℝ) p.1) := continuous_gaussianCovarianceDiscrepancy.comp continuous_swap exact hM.continuous_sInf hjoint -
populationMinimizers_covarianceModelLoss_ifftheorem — Given covariance models that are compact and nonempty, a positive-definite truth contained in some model, and a model index, the population minimizers are exactly the indices whose models contain the truth.hypothesesV :sharedType u_2I :sharedType u_3Fintype VFintype INonempty Imodels :I → Set (PositiveCovariance V)hcompact :∀ i, IsCompact (models i)hne :∀ i, (models i).NonemptyT :hcontains :∃ i, T ∈ models ii :Iconclusioni ∈ populationMinimizers (fun j => covarianceModelLoss (models j) T)↔ T ∈ models iProof (Lean source)
theorem populationMinimizers_covarianceModelLoss_iff [Fintype V] [DecidableEq V] [Fintype I] [Nonempty I] (models : I → Set (PositiveCovariance V)) (hcompact : ∀ i, IsCompact (models i)) (hne : ∀ i, (models i).Nonempty) (T : PositiveCovariance V) (hcontains : ∃ i, T ∈ models i) (i : I) : i ∈ populationMinimizers (fun j => covarianceModelLoss (models j) T) ↔ T ∈ models i := by rcases hcontains with ⟨j0, hj0⟩ rw [populationMinimizers] constructor · intro hi apply (covarianceModelLoss_eq_truth_iff (hcompact i) (hne i) T).mp apply le_antisymm · calc covarianceModelLoss (models i) T ≤ covarianceModelLoss (models j0) T := hi j0 _ = gaussianCovarianceDiscrepancy (T : Matrix V V ℝ) T := (covarianceModelLoss_eq_truth_iff (hcompact j0) (hne j0) T).2 hj0 · exact covarianceModelLoss_ge_truth (hcompact i) (hne i) T · intro hi j rw [(covarianceModelLoss_eq_truth_iff (hcompact i) (hne i) T).2 hi] exact covarianceModelLoss_ge_truth (hcompact j) (hne j) T -
tendstoInProb_covarianceModelLosstheorem — Given covariance models that are compact and nonempty, an empirical covariance sequence, a target matrix, a sampling measure, and entrywise convergence in probability, the model losses converge coordinatewise in probability.hypothesesV :sharedType u_2I :sharedType u_3Fintype VFintype Imodels :I → Set (PositiveCovariance V)hcompact :∀ i, IsCompact (models i)hne :∀ i, (models i).NonemptySn :ℕ → Ω → Matrix V V ℝT :Matrix V V ℝP :Measure ΩhSn :∀ a b,TendstoInProbability (fun _ : ℕ => P) (fun n ω => Sn n ω a b) atTop (fun _ _ => T a b)i :conclusionTendstoInProbability (fun _ : ℕ => P) (fun n ω => covarianceModelLoss (models i) (Sn n ω)) atTop (fun _ _ => covarianceModelLoss (models i) T)Proof (Lean source)
theorem tendstoInProb_covarianceModelLoss [MeasurableSpace Ω] [Fintype V] [DecidableEq V] [Fintype I] (models : I → Set (PositiveCovariance V)) (hcompact : ∀ i, IsCompact (models i)) (hne : ∀ i, (models i).Nonempty) (Sn : ℕ → Ω → Matrix V V ℝ) (T : Matrix V V ℝ) (P : Measure Ω) (hSn : ∀ a b, TendstoInProbability (fun _ : ℕ => P) (fun n ω => Sn n ω a b) atTop (fun _ _ => T a b)) : ∀ i, TendstoInProbability (fun _ : ℕ => P) (fun n ω => covarianceModelLoss (models i) (Sn n ω)) atTop (fun _ _ => covarianceModelLoss (models i) T) := by classical intro i let uncurryMatrix : ((V × V) → ℝ) → Matrix V V ℝ := fun x a b => x (a, b) let Yn : ℕ → Ω → ((V × V) → ℝ) := fun n ω ab => Sn n ω ab.1 ab.2 let c : (V × V) → ℝ := fun ab => T ab.1 ab.2 let g : ((V × V) → ℝ) → ℝ := fun x => covarianceModelLoss (models i) (uncurryMatrix x) have huncurry : Continuous uncurryMatrix := by fun_prop have hg : ContinuousAt g c := ((continuous_covarianceModelLoss (hcompact i)).comp huncurry).continuousAt have hcoord : ∀ ab, TendstoInProbability (fun _ : ℕ => P) (fun n ω => Yn n ω ab) atTop (fun _ _ => c ab) := by rintro ⟨a, b⟩ exact hSn a b simpa [Yn, c, g, uncurryMatrix] using pi_comp_continuousAt hg hcoord