Stat

Statistical foundations: convergence modes, limit theorems, concentration inequalities, and minimax lower-bound tools.

Sample 69 core · 53 supporting · 6 submodules This file provides the library's causal-agnostic model of an independent and identically distributed sample on a common ambient probability space. Limit 37 core · 55 supporting · 7 submodules Convergence concepts: convergence in probability and distribution, continuous mapping, and Slutsky-style composition rules. CLT 58 core · 52 supporting · 10 submodules Central limit theory: iid and triangular-array CLTs, Lindeberg conditions, and vector-valued versions used by the estimation layer. Minimax 10 to review 197 core · 329 supporting · 26 submodules Minimax lower-bound machinery: risk definitions, maximal couplings, coordinatewise overlap, Le Cam two-point methods, Pinsker/KL bridges, and rate statements for estimation problems. EmpiricalProcess 20 core · 13 supporting · 5 submodules Empirical-process theory: Rademacher complexities, maximal inequalities, moduli of continuity, and uniform laws for function classes. MEstimation 21 core · 16 supporting · 11 submodules M- and Z-estimation: consistency, asymptotic normality, and influence-function representations. Quantile 51 core · 66 supporting · 7 submodules Quantile processes: empirical quantiles, Bahadur representations, and joint sample-quantile asymptotics. UStatistic 2 to review 66 core · 87 supporting · 4 submodules Collects the U-statistic library: order-2 Hoeffding and variance tools, fixed-order m infrastructure, Hájek expansions, remainder negligibility, and the fixed-order CLT. Bootstrap 9 core · 2 supporting · 3 submodules Bootstrap foundations: resampling distributions and consistency of bootstrap approximations. Concentration 199 core · 303 supporting · 15 submodules Vendored concentration-of-measure library (a port of auto-res/lean-rademacher; see UPSTREAM.md). Coupling 26 core · 36 supporting · 1 submodule This module collects coupling-based statistical primitives. FiniteRaoBlackwell 52 core · 77 supporting · 7 submodules Guarded finite conditional laws and Rao–Blackwell reductions for arbitrary finite-design pushforwards and uniform allocation experiments, with exact disintegration, finite-prior posteriors, factorization sufficiency, and real-valued minimax bridges. GMM 15 core · 9 supporting · 4 submodules Generalized method of moments: identification, consistency, and asymptotic normality of GMM estimators. Inference 22 core · 39 supporting · 9 submodules Inferential tooling: delta methods (scalar, functional, Hadamard), Wald/chi-squared statistics, and Slutsky ingredients. Nonparametric 144 core · 147 supporting · 7 submodules Top barrel for reusable nonparametric statistical methods: approximation theory, weighted least squares, local-polynomial and series/sieve estimators, and higher-order influence-function tools. Orthogonality 4 core · 5 supporting · 2 submodules Neyman orthogonality as a statistical property: definitions and the second-order remainder characterization. PolynomialTail 23 core · 33 supporting · 7 submodules Polynomial lower-tail moment analysis: the polynomial small-value tail law for a bounded positive variable, truncated inverse first/second moment asymptotics, the trimming-bias bound, and the bias-variance rate-balancing algebra. Privacy 9 core · 9 supporting · 1 submodule Differential privacy via the Laplace mechanism: the centered Laplace distribution and its density-ratio bound, scalar and finite-dimensional additive-noise release, pure and approximate ε-differential-privacy guarantees, post-processing closure, and Laplace-noise moment bounds. SampleSplit 23 core · 24 supporting · 7 submodules This module is the public import point for sample-splitting infrastructure used by cross-fitting and fold-based estimation arguments.

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

Causalean.Stat

For a finite coordinate type, the positive covariance matrices are real square matrices equipped with a proof of positive definiteness.

Definition (Lean source)

parameters

V :

Type*

Fintype V

def

PositiveCovariance V :

Type (max 0 u_2)

given by

{K : Matrix V V ℝ // PosDef K}

Causalean.Stat.PositiveCovariance · Causalean/Stat/GaussianCovariance.lean:23

def gaussianCovarianceDiscrepancy reviewed

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)

parameters

V :

Type u_1

Fintype V

DecidableEq V

shared

K T :

Matrix V V ℝ

def

gaussianCovarianceDiscrepancy K T :

ℝ

given by

log K.det + trace (K⁻¹ * T)

Causalean.Stat.gaussianCovarianceDiscrepancy · Causalean/Stat/GaussianCovariance.lean:28

def normalizedCovarianceDiscrepancy reviewed

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

V :

Type u_1

Fintype V

DecidableEq V

shared

K T :

PositiveCovariance V

def

normalizedCovarianceDiscrepancy K T :

ℝ

given by

gaussianCovarianceDiscrepancy (K : Matrix V V ℝ) T

- gaussianCovarianceDiscrepancy (T : Matrix V V ℝ) T

Causalean.Stat.normalizedCovarianceDiscrepancy · Causalean/Stat/GaussianCovariance.lean:34 · uses PositiveCovariance

def IsDiscrepancyAttainedOn reviewed

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

V :

Type u_2

Fintype V

DecidableEq V

shared

M :

Set (PositiveCovariance V)

T :

Matrix V V ℝ

def

IsDiscrepancyAttainedOn M T :

Prop

given by

∃ K ∈ M,

∀ L ∈ M,

gaussianCovarianceDiscrepancy (K : Matrix V V ℝ) T

≤ gaussianCovarianceDiscrepancy (L : Matrix V V ℝ) T

Causalean.Stat.IsDiscrepancyAttainedOn · Causalean/Stat/GaussianCovariance.lean:257 · uses PositiveCovariance

def HasCompactDiscrepancySublevel reviewed

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

V :

Type u_2

Fintype V

DecidableEq V

shared

M :

Set (PositiveCovariance V)

T :

Matrix V V ℝ

def

HasCompactDiscrepancySublevel M T :

Prop

given by

∃ c : ℝ,

clause 1

(M ∩ {K | gaussianCovarianceDiscrepancy (K : Matrix V V ℝ) T ≤ c}).Nonempty

clause 2

IsCompact (M ∩ {K | gaussianCovarianceDiscrepancy (K : Matrix V V ℝ) T ≤ c})

Causalean.Stat.HasCompactDiscrepancySublevel · Causalean/Stat/GaussianCovariance.lean:265 · uses PositiveCovariance

def covarianceModelLoss reviewed

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

V :

Type u_2

Fintype V

DecidableEq V

shared

M :

Set (PositiveCovariance V)

T :

Matrix V V ℝ

def

covarianceModelLoss M T :

ℝ

given by

sInf ((fun K : PositiveCovariance V => gaussianCovarianceDiscrepancy (K : Matrix V V ℝ) T) '' M)

Causalean.Stat.covarianceModelLoss · Causalean/Stat/GaussianCovariance.lean:369 · uses PositiveCovariance

theorem finiteCovarianceModel_populationGap reviewed

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

shared

I :

Type u_3

shared

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

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⟩⟩

Causalean.Stat.finiteCovarianceModel_populationGap · Causalean/Stat/GaussianCovariance.lean:456 · uses PositiveCovariance , covarianceModelLoss , populationMinimizers

13 supporting declarations (lemmas, instances)

continuous_gaussianCovarianceDiscrepancy theorem — The Gaussian covariance discrepancy varies continuously with its positive-definite candidate and target matrix.

hypotheses

V :

Type u_1
Fintype V
DecidableEq V
shared

conclusion

Continuous (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

Causalean.Stat.continuous_gaussianCovarianceDiscrepancy · Causalean/Stat/GaussianCovariance.lean:41
continuous_normalizedCovarianceDiscrepancy theorem — The normalized Gaussian covariance discrepancy varies continuously with both positive-definite covariances.

hypotheses

V :

Type u_1
Fintype V
DecidableEq V
shared

conclusion

Continuous (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

Causalean.Stat.continuous_normalizedCovarianceDiscrepancy · Causalean/Stat/GaussianCovariance.lean:69
normalizedCovarianceDiscrepancy_nonneg theorem — For positive-definite candidate and target covariances, the normalized Gaussian covariance discrepancy is nonnegative.

hypotheses

V :

Type u_1
Fintype V
DecidableEq V
shared

K T :

PositiveCovariance V

conclusion

0 ≤ normalizedCovarianceDiscrepancy K T

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

Causalean.Stat.normalizedCovarianceDiscrepancy_nonneg · Causalean/Stat/GaussianCovariance.lean:218
normalizedCovarianceDiscrepancy_eq_zero_iff theorem — For positive-definite candidate and target covariances, the normalized Gaussian covariance discrepancy is zero exactly when the two covariances agree.

hypotheses

V :

Type u_1
Fintype V
DecidableEq V
shared

K T :

PositiveCovariance V

conclusion

normalizedCovarianceDiscrepancy K T = 0 ↔ K = T

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]

Causalean.Stat.normalizedCovarianceDiscrepancy_eq_zero_iff · Causalean/Stat/GaussianCovariance.lean:229
gaussianCovarianceDiscrepancy_le_truth_iff theorem — For positive-definite candidate and target covariances, the candidate has no larger Gaussian discrepancy than the truth exactly when it is the truth.

hypotheses

V :

Type u_1
Fintype V
DecidableEq V
shared

K T :

PositiveCovariance V

conclusion

gaussianCovarianceDiscrepancy (K : Matrix V V ℝ) T
≤ gaussianCovarianceDiscrepancy (T : Matrix V V ℝ) T ↔ K = T

Proof (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

Causalean.Stat.gaussianCovarianceDiscrepancy_le_truth_iff · Causalean/Stat/GaussianCovariance.lean:239
discrepancyAttainedOn_of_isCompact theorem — Given a compact covariance model, a nonempty model, and a target matrix, the Gaussian discrepancy minimum is attained.

hypotheses

V :

Type u_2
Fintype V
DecidableEq V
Set (PositiveCovariance V)
shared

hM :

IsCompact M

hne :

M.Nonempty

T :

Matrix V V ℝ

conclusion

IsDiscrepancyAttainedOn M T

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⟩

Causalean.Stat.discrepancyAttainedOn_of_isCompact · Causalean/Stat/GaussianCovariance.lean:273
discrepancyAttainedOn_of_compactSublevel theorem — Given a covariance model with a nonempty compact discrepancy sublevel, the global Gaussian discrepancy minimum is attained.

hypotheses

V :

Type u_2
Fintype V
DecidableEq V
Set (PositiveCovariance V)
Matrix V V ℝ
shared

hM :

HasCompactDiscrepancySublevel M T

conclusion

IsDiscrepancyAttainedOn M T

Proof (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))

Causalean.Stat.discrepancyAttainedOn_of_compactSublevel · Causalean/Stat/GaussianCovariance.lean:287
exists_positive_gap_of_attained theorem — Given an attained covariance-model discrepancy that omits the positive-definite truth, every model covariance has a common strictly positive normalized gap.

hypotheses

V :

Type u_2
Fintype V
DecidableEq V
Set (PositiveCovariance V)
PositiveCovariance V
shared

hatt :

IsDiscrepancyAttainedOn M T

hT :

T ∉ M

conclusion

∃ gap : ℝ,
0 < gap
conclusion 1

K ∈ M :

gap ≤ normalizedCovarianceDiscrepancy K T

Proof (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]

Causalean.Stat.exists_positive_gap_of_attained · Causalean/Stat/GaussianCovariance.lean:304
exists_positive_gap_of_isCompact theorem — 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.

hypotheses

V :

Type u_2
Fintype V
DecidableEq V
Set (PositiveCovariance V)
shared

hM :

IsCompact M

hne :

M.Nonempty

T :

PositiveCovariance V

hT :

T ∉ M

conclusion

∃ gap : ℝ,
0 < gap
conclusion 1

K ∈ M :

gap ≤ normalizedCovarianceDiscrepancy K T

Proof (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

Causalean.Stat.exists_positive_gap_of_isCompact · Causalean/Stat/GaussianCovariance.lean:321
exists_stable_positive_gap theorem — 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.

hypotheses

V :

Type u_2
Fintype V
DecidableEq V
Set (PositiveCovariance V)
shared

hM :

IsCompact M

hne :

M.Nonempty

T :

PositiveCovariance V

hT :

T ∉ M

conclusion

∃ gap : ℝ,
conclusion 1
0 < gap
conclusion 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))

Causalean.Stat.exists_stable_positive_gap · Causalean/Stat/GaussianCovariance.lean:332
continuous_covarianceModelLoss theorem — Given a compact covariance model that is nonempty, the population loss is continuous in the target second-moment matrix.

hypotheses

V :

Type u_2
Fintype V
DecidableEq V
Set (PositiveCovariance V)
shared

hM :

IsCompact M

hne :

M.Nonempty

conclusion

Continuous (covarianceModelLoss M)

Proof (Lean source)

theorem continuous_covarianceModelLoss [Fintype V] [DecidableEq V] {M : Set (PositiveCovariance V)} (hM : IsCompact M) (hne : M.Nonempty) : 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

Causalean.Stat.continuous_covarianceModelLoss · Causalean/Stat/GaussianCovariance.lean:376
populationMinimizers_covarianceModelLoss_iff theorem — 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.

hypotheses

V :

Type u_2
shared

I :

Type u_3
shared

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

conclusion

i ∈ populationMinimizers (fun j => covarianceModelLoss (models j) T)
↔ T ∈ models i

Proof (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

Causalean.Stat.populationMinimizers_covarianceModelLoss_iff · Causalean/Stat/GaussianCovariance.lean:429
tendstoInProb_covarianceModelLoss theorem — 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.

hypotheses

V :

Type u_2
shared

I :

Type u_3
shared

Ω :

Type u_4
MeasurableSpace Ω
shared

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, Tendsto_inProb (fun n ω => Sn n ω a b) (fun _ => T a b) P

i :

conclusion

Tendsto_inProb (fun n ω => covarianceModelLoss (models i) (Sn n ω)) (fun _ => covarianceModelLoss (models i) T) P

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, Tendsto_inProb (fun n ω => Sn n ω a b) (fun _ => T a b) P) : ∀ i, Tendsto_inProb (fun n ω => covarianceModelLoss (models i) (Sn n ω)) (fun _ => covarianceModelLoss (models i) T) P := 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) (hne i)).comp huncurry).continuousAt have hcoord : ∀ ab, Tendsto_inProb (fun n ω => Yn n ω ab) (fun _ => c ab) P := by rintro ⟨a, b⟩ exact hSn a b simpa [Yn, c, g, uncurryMatrix] using pi_comp_continuousAt hg hcoord

Causalean.Stat.tendstoInProb_covarianceModelLoss · Causalean/Stat/GaussianCovariance.lean:502