Stat.Sample

Sampling primitives: iid samples as measurable maps with their product-law identities.

Sample 3 core · 0 supporting This file provides the library's causal-agnostic model of an independent and identically distributed sample on a common ambient probability space. ★ map_eq

I.i.d. Samples

This file provides the library's causal-agnostic model of an independent and identically distributed sample on a common ambient probability space. It also defines sample means of real-valued statistics along the first $n$ sample points, supplying the base object used by the limit and inference modules.

structure IIDSample reviewed

Causalean.Stat

An independent and identically distributed sample with marginal law P, realized as a sequence of sample points given by measurable maps on a single ambient probability space: the family is mutually independent, identically distributed, and the law of each point is the population law P.

Definition (Lean source)

parameters

Ω X :

Type*

MeasurableSpace Ω

MeasurableSpace X

μ :

Measure Ω

P :

Measure X

fields

Z :

ℕ → Ω → X

meas :

∀ i, Measurable (Z i)

indep :

iIndepFun Z μ

identDist :

∀ i, IdentDistrib (Z 0) (Z i) μ μ

law :

(μ.map (Z 0)) = P

Causalean.Stat.IIDSample · Causalean/Stat/Sample.lean:32

def sampleMean reviewed

Causalean.Stat.IIDSample

Sample mean of a real-valued statistic f along the sample's first n points: (1/n) Σ_{i < n} f (Z i ω).

Definition (Lean source)

noncomputable def sampleMean (S : IIDSample Ω X μ P) (f : X → ℝ) (n : ℕ) : Ω → ℝ := fun ω => (n : ℝ)⁻¹ * ∑ i ∈ range n, f (S.Z i ω)

Causalean.Stat.IIDSample.sampleMean · Causalean/Stat/Sample.lean:57 · uses IIDSample

theorem map_eq reviewed

Causalean.Stat.IIDSample

For an i.i.d. sample S and any sample index i, the pushforward law of the i-th sample point equals the population law P.

Formal statement

hypotheses

S :

IIDSample Ω X μ P

i :

ℕ

conclusion

μ.map (S.Z i) = P

Proof (Lean source)

theorem map_eq (S : IIDSample Ω X μ P) (i : ℕ) : μ.map (S.Z i) = P := by rw [← (S.identDist i).map_eq, S.law]

Causalean.Stat.IIDSample.map_eq · Causalean/Stat/Sample.lean:63 · uses IIDSample

FiniteStratumMarkedRatioMse 31 to review 31 core · 16 supporting · 6 submodules This module collects totalized finite-stratum arm means, their fixed-set population targets and missing-arm decompositions, exact missing-count moments, and boundary-safe mean-squared-error bounds for real square-integra OccupancyWeightedMean 21 to review 21 core · 17 supporting · 5 submodules This module provides totalized occupancy-weighted differences of within-group sample means and a weak-second-moment variance bound under fixed overlap.

CollisionEstimator 4 core · 0 supporting This module defines an ordered-pair collision estimator for inverse-frequency functionals, together with cell-weighted moments and cross-sample averages for observations equipped with an explicit projection to their cell

Collision and cross-sample estimators

This module defines an ordered-pair collision estimator for inverse-frequency functionals, together with cell-weighted moments and cross-sample averages for observations equipped with an explicit projection to their cell labels.

def collisionKernel reviewed

Causalean.Stat

The collision kernel contributes the inverse mass of a cell when two observations have the same label and zero otherwise.

Definition (Lean source)

noncomputable def collisionKernel {𝒳 : Type*} (q : 𝒳 → ℝ) (x y : 𝒳) : ℝ := by classical exact if x = y then 1 / q x else 0

Causalean.Stat.collisionKernel · Causalean/Stat/Sample/CollisionEstimator.lean:22

def collisionScale reviewed

Causalean.Stat

The collision scale averages inverse-frequency collisions over distinct ordered pairs in a sample.

Definition (Lean source)

noncomputable def collisionScale {𝒳 : Type*} (q : 𝒳 → ℝ) {N : ℕ} (target : Fin N → 𝒳) : ℝ := ((N : ℝ) * (N - 1 : ℕ))⁻¹ * ∑ j, ∑ l, if j ≠ l then collisionKernel q (target j) (target l) else 0

Causalean.Stat.collisionScale · Causalean/Stat/Sample/CollisionEstimator.lean:29

def cellMoment reviewed

Causalean.Stat

A cell moment is the sample average of a statistic within one projected cell, rescaled by that cell's inverse population frequency.

Definition (Lean source)

noncomputable def cellMoment {𝒳 Ω : Type*} (q : 𝒳 → ℝ) (proj : Ω → 𝒳) {n : ℕ} (sample : Fin n → Ω) (G : Ω → ℝ) (x : 𝒳) : ℝ := by classical exact (n : ℝ)⁻¹ / q x * ∑ i, if proj (sample i) = x then G (sample i) else 0

Causalean.Stat.cellMoment · Causalean/Stat/Sample/CollisionEstimator.lean:36

def crossAverage reviewed

Causalean.Stat

A cross-sample average evaluates source-sample cell moments at every target observation and averages the resulting values over the target sample.

Definition (Lean source)

noncomputable def crossAverage {𝒳 Ω : Type*} (q : 𝒳 → ℝ) (proj : Ω → 𝒳) {n N : ℕ} (source : Fin n → Ω) (target : Fin N → 𝒳) (G : Ω → ℝ) : ℝ := (N : ℝ)⁻¹ * ∑ j, cellMoment q proj source G (target j)

Causalean.Stat.crossAverage · Causalean/Stat/Sample/CollisionEstimator.lean:45

EffectiveSampleSize 3 core · 2 supporting This module develops the empirical second-moment statistic used for weighted i.i.d. ★ empiricalKishDispersion_mean★ empiricalKishDispersion_lower_tail_le

Kish dispersion and effective sample size

This module develops the empirical second-moment statistic used for weighted i.i.d. samples. When weights have population mean one, their second moment is the Kish design effect; dividing the nominal sample size by this design effect gives the effective sample size. The results below establish its mean, a variance bound under a fourth-moment envelope, and a lower-tail bound.

def empiricalKishDispersion reviewed

Causalean.Stat

Empirical Kish dispersion is the sample average of the squared observation-level weights.

Definition (Lean source)

def empiricalKishDispersion {Ω : Type*} (g : Ω → ℝ) (n : ℕ) (sample : Fin n → Ω) : ℝ := (n : ℝ)⁻¹ * ∑ i, g (sample i) ^ 2

Causalean.Stat.empiricalKishDispersion · Causalean/Stat/Sample/EffectiveSampleSize.lean:26

lemma empiricalKishDispersion_mean reviewed

Causalean.Stat

Expected empirical Kish dispersion. Given a positive sample size $n$ and an integrable squared weight statistic $g^2$ under the population measure, the expectation of the empirical Kish dispersion — the sample average of the squared observation-level weights — under the $n$ -fold product sampling measure equals the population second moment $\int g^2\,d\mu$ .

Formal statement

hypotheses

Ω :

Type*

MeasurableSpace Ω

μ :

Measure Ω

IsProbabilityMeasure μ

g :

Ω → ℝ

n :

ℕ

hn :

0 < n

hF :

Integrable (fun o => g o ^ 2) μ

conclusion

(∫ sample : Fin n → Ω, empiricalKishDispersion g n sample ∂Measure.pi (fun _ : Fin n => μ))

= ∫ o, g o ^ 2 ∂μ

Proof (Lean source)

lemma empiricalKishDispersion_mean {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] (g : Ω → ℝ) (n : ℕ) (hn : 0 < n) (hF : Integrable (fun o => g o ^ 2) μ) : (∫ sample : Fin n → Ω, empiricalKishDispersion g n sample ∂Measure.pi (fun _ : Fin n => μ)) = ∫ o, g o ^ 2 ∂μ := by simpa [empiricalKishDispersion] using iid_average_integral μ n hn (fun o => g o ^ 2) hF

Causalean.Stat.empiricalKishDispersion_mean · Causalean/Stat/Sample/EffectiveSampleSize.lean:43 · uses empiricalKishDispersion

lemma empiricalKishDispersion_lower_tail_le reviewed

Causalean.Stat

Lower-tail bound for empirical Kish dispersion. Given a positive sample size $n$ , a positive population Kish dispersion $\kappa$ , the empirical Kish dispersion is square-integrable under the sampling measure Q, its expectation under Q equals $\kappa$ , and its variance under Q is at most $4k^2\kappa/n$ for a weight envelope $k$ , then the probability that the empirical Kish dispersion falls below half its mean $\kappa/2$ is at most $16k^2/(n\kappa)$ .

Formal statement

hypotheses

Ω :

Type*

MeasurableSpace Ω

n :

ℕ

Q :

Measure (Fin n → Ω)

IsProbabilityMeasure Q

g :

Ω → ℝ

k kappa :

ℝ

hn :

0 < n

hkappa :

0 < kappa

hF :

MemLp (empiricalKishDispersion g n) 2 Q

hmean :

(∫ sample, empiricalKishDispersion g n sample ∂Q) = kappa

hvar :

variance (empiricalKishDispersion g n) Q ≤ 4 * k ^ 2 * kappa / n

conclusion

(Q {sample | empiricalKishDispersion g n sample < kappa / 2}).toReal

≤ 16 * k ^ 2 / ((n : ℝ) * kappa)

Proof (Lean source)

lemma empiricalKishDispersion_lower_tail_le {Ω : Type*} [MeasurableSpace Ω] (n : ℕ) (Q : Measure (Fin n → Ω)) [IsProbabilityMeasure Q] (g : Ω → ℝ) (k kappa : ℝ) (hn : 0 < n) (hkappa : 0 < kappa) (hF : MemLp (empiricalKishDispersion g n) 2 Q) (hmean : (∫ sample, empiricalKishDispersion g n sample ∂Q) = kappa) (hvar : variance (empiricalKishDispersion g n) Q ≤ 4 * k ^ 2 * kappa / n) : (Q {sample | empiricalKishDispersion g n sample < kappa / 2}).toReal ≤ 16 * k ^ 2 / ((n : ℝ) * kappa) := by have hcheb := probability_abs_sub_mean_gt_le Q (empiricalKishDispersion g n) kappa (4 * k ^ 2 * kappa / n) (kappa / 2) hF (half_pos hkappa) hmean hvar have hsub : {sample | empiricalKishDispersion g n sample < kappa / 2} ⊆ {sample | kappa / 2 < |empiricalKishDispersion g n sample - kappa|} := by intro sample hs simp only [Set.mem_setOf_eq] at hs ⊢ rw [abs_of_neg (by linarith)] linarith calc (Q {sample | empiricalKishDispersion g n sample < kappa / 2}).toReal ≤ (Q {sample | kappa / 2 < |empiricalKishDispersion g n sample - kappa|}).toReal := measureReal_mono hsub _ ≤ (4 * k ^ 2 * kappa / n) / (kappa / 2) ^ 2 := hcheb _ = 16 * k ^ 2 / ((n : ℝ) * kappa) := by have hnR : (0 : ℝ) < n := by exact_mod_cast hn field_simp [hnR.ne', hkappa.ne'] ring

Causalean.Stat.empiricalKishDispersion_lower_tail_le · Causalean/Stat/Sample/EffectiveSampleSize.lean:108 · uses empiricalKishDispersion

2 supporting declarations (lemmas, instances)

one_le_secondMoment_of_mean_one lemma — A mean-one square-integrable weight has second moment at least one, so its Kish design effect cannot improve on an equally weighted sample.

hypotheses

𝒳 :

Type*
MeasurableSpace 𝒳

μ :

Measure 𝒳
IsProbabilityMeasure μ

w :

𝒳 → ℝ

hw :

MemLp w 2 μ

hmean :

(∫ x, w x ∂μ) = 1

conclusion

1 ≤ ∫ x, w x ^ 2 ∂μ

Proof (Lean source)

lemma one_le_secondMoment_of_mean_one {𝒳 : Type*} [MeasurableSpace 𝒳] (μ : Measure 𝒳) [IsProbabilityMeasure μ] (w : 𝒳 → ℝ) (hw : MemLp w 2 μ) (hmean : (∫ x, w x ∂μ) = 1) : 1 ≤ ∫ x, w x ^ 2 ∂μ := by have hv := variance_nonneg w μ rw [variance_eq_sub hw, hmean] at hv norm_num at hv ⊢ linarith

Causalean.Stat.one_le_secondMoment_of_mean_one · Causalean/Stat/Sample/EffectiveSampleSize.lean:31
empiricalKishDispersion_variance_le lemma — If the fourth power of a weight is bounded by four times a squared envelope times its second power, empirical Kish dispersion has variance at most four times the squared envelope and the population second moment, divided by sample size.

hypotheses

Ω :

Type*
MeasurableSpace Ω

μ :

Measure Ω
IsProbabilityMeasure μ

g :

Ω → ℝ

n :

ℕ

k kappa :

ℝ

hn :

0 < n

hF :

MemLp (fun o => g o ^ 2) 2 μ

hkappa :

(∫ o, g o ^ 2 ∂μ) = kappa

hfourth :

∀ᵐ o ∂μ, g o ^ 4 ≤ 4 * k ^ 2 * g o ^ 2

conclusion

variance (fun sample : Fin n → Ω => empiricalKishDispersion g n sample) (Measure.pi (fun _ : Fin n => μ))
≤ 4 * k ^ 2 * kappa / n

Proof (Lean source)

lemma empiricalKishDispersion_variance_le {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] (g : Ω → ℝ) (n : ℕ) (k kappa : ℝ) (hn : 0 < n) (hF : MemLp (fun o => g o ^ 2) 2 μ) (hkappa : (∫ o, g o ^ 2 ∂μ) = kappa) (hfourth : ∀ᵐ o ∂μ, g o ^ 4 ≤ 4 * k ^ 2 * g o ^ 2) : variance (fun sample : Fin n → Ω => empiricalKishDispersion g n sample) (Measure.pi (fun _ : Fin n => μ)) ≤ 4 * k ^ 2 * kappa / n := by have hvar := iid_average_variance μ n (fun o => g o ^ 2) hF have hsingle : variance (fun o => g o ^ 2) μ ≤ 4 * k ^ 2 * kappa := by calc variance (fun o => g o ^ 2) μ ≤ ∫ o, (g o ^ 2) ^ 2 ∂μ := variance_le_expectation_sq hF.aestronglyMeasurable _ = ∫ o, g o ^ 4 ∂μ := by apply integral_congr_ae filter_upwards with o ring _ ≤ ∫ o, 4 * k ^ 2 * g o ^ 2 ∂μ := by have hleft : Integrable (fun o => g o ^ 4) μ := by have hpow : (fun o => g o ^ 4) = fun o => (g o ^ 2) ^ 2 := by funext o ring rw [hpow] exact hF.integrable_sq exact integral_mono_ae hleft (hF.integrable (by norm_num) |>.const_mul _) hfourth _ = 4 * k ^ 2 * kappa := by rw [integral_const_mul, hkappa] change variance (fun sample : Fin n → Ω => (n : ℝ)⁻¹ * ∑ i, g (sample i) ^ 2) (Measure.pi (fun _ : Fin n => μ)) ≤ _ rw [hvar] calc (n : ℝ)⁻¹ * variance (fun o => g o ^ 2) μ ≤ (n : ℝ)⁻¹ * (4 * k ^ 2 * kappa) := by gcongr _ = 4 * k ^ 2 * kappa / n := by ring

Causalean.Stat.empiricalKishDispersion_variance_le · Causalean/Stat/Sample/EffectiveSampleSize.lean:60

EmpiricalMass 3 core · 1 supporting This module defines the empirical frequency of one point in a finite i.i.d. ★ integral_empiricalMass★ integral_empiricalMass_sq

Empirical mass of a point

This module defines the empirical frequency of one point in a finite i.i.d. sample and establishes its range, expectation, and second moment.

def empiricalMass reviewed

Causalean.Stat

The empirical mass of a point is the fraction of sample observations equal to that point.

Definition (Lean source)

def empiricalMass {N : ℕ} (sample : Fin N → 𝒳) (x : 𝒳) : ℝ := by classical exact (N : ℝ)⁻¹ * ∑ j, if sample j = x then 1 else 0

Causalean.Stat.empiricalMass · Causalean/Stat/Sample/EmpiricalMass.lean:24

lemma integral_empiricalMass reviewed

Causalean.Stat

Expected empirical mass. Given a positive sample size $m$ and a measurable singleton {a}, the expectation, under the $m$ -fold product sampling measure, of the empirical mass of the point a — the fraction of sample observations equal to a — equals the population probability of {a}.

Formal statement

hypotheses

MeasurableSpace 𝒳

μ :

Measure 𝒳

IsProbabilityMeasure μ

m :

ℕ

hm :

0 < m

a :

𝒳

ha :

MeasurableSet {a}

conclusion

(∫ sample : Fin m → 𝒳, empiricalMass sample a ∂Measure.pi (fun _ : Fin m => μ))

= μ.real {a}

Proof (Lean source)

lemma integral_empiricalMass [MeasurableSpace 𝒳] (μ : Measure 𝒳) [IsProbabilityMeasure μ] {m : ℕ} (hm : 0 < m) (a : 𝒳) (ha : MeasurableSet {a}) : (∫ sample : Fin m → 𝒳, empiricalMass sample a ∂Measure.pi (fun _ : Fin m => μ)) = μ.real {a} := by classical let F : 𝒳 → ℝ := fun x => if x = a then 1 else 0 have hFMeas : Measurable F := by exact Measurable.ite ha measurable_const measurable_const have hFMem : MemLp F 2 μ := MemLp.of_bound hFMeas.aestronglyMeasurable 1 (Filter.Eventually.of_forall fun x => by by_cases hx : x = a <;> simp [F, hx]) have hstat : (fun sample : Fin m → 𝒳 => empiricalMass sample a) = fun sample => (m : ℝ)⁻¹ * ∑ j, F (sample j) := by funext sample unfold empiricalMass apply congrArg ((m : ℝ)⁻¹ * ·) apply Finset.sum_congr rfl intro j hj by_cases hx : sample j = a <;> simp [F, hx] rw [hstat, iid_average_integral μ m hm F (hFMem.integrable (by norm_num))] change (∫ x, ({a} : Set 𝒳).indicator (fun _ => (1 : ℝ)) x ∂μ) = μ.real {a} rw [integral_indicator_const (μ := μ) (1 : ℝ) ha] simp

Causalean.Stat.integral_empiricalMass · Causalean/Stat/Sample/EmpiricalMass.lean:58 · uses empiricalMass

lemma integral_empiricalMass_sq reviewed

Causalean.Stat

Second moment of the empirical mass. Given a positive sample size $m$ and a measurable singleton {a}, the second moment, under the $m$ -fold product sampling measure, of the empirical mass of the point a equals the squared population probability of {a} plus the usual binomial sampling correction $(1/m)(\mu(\{a\})-\mu(\{a\})^2)$ .

Formal statement

hypotheses

MeasurableSpace 𝒳

μ :

Measure 𝒳

IsProbabilityMeasure μ

m :

ℕ

hm :

0 < m

a :

𝒳

ha :

MeasurableSet {a}

conclusion

(∫ sample : Fin m → 𝒳, empiricalMass sample a ^ 2 ∂Measure.pi (fun _ : Fin m => μ))

= μ.real {a} ^ 2 + (m : ℝ)⁻¹ * (μ.real {a} - μ.real {a} ^ 2)

Proof (Lean source)

lemma integral_empiricalMass_sq [MeasurableSpace 𝒳] (μ : Measure 𝒳) [IsProbabilityMeasure μ] {m : ℕ} (hm : 0 < m) (a : 𝒳) (ha : MeasurableSet {a}) : (∫ sample : Fin m → 𝒳, empiricalMass sample a ^ 2 ∂Measure.pi (fun _ : Fin m => μ)) = μ.real {a} ^ 2 + (m : ℝ)⁻¹ * (μ.real {a} - μ.real {a} ^ 2) := by classical let F : 𝒳 → ℝ := fun x => if x = a then 1 else 0 have hFMeas : Measurable F := by dsimp [F] exact Measurable.ite (ha.preimage measurable_id) measurable_const measurable_const have hFBound : ∀ x, |F x| ≤ 1 := by intro x by_cases hx : x = a <;> simp [F, hx] have hFMem : MemLp F 2 μ := MemLp.of_bound hFMeas.aestronglyMeasurable 1 (Filter.Eventually.of_forall fun x => by simpa [Real.norm_eq_abs] using hFBound x) have hmeanF : (∫ x, F x ∂μ) = μ.real {a} := by change (∫ x, ({a} : Set 𝒳).indicator (fun _ => (1 : ℝ)) x ∂μ) = _ rw [integral_indicator_const (μ := μ) (1 : ℝ) ha] simp have hsquareF : (∫ x, F x ^ 2 ∂μ) = μ.real {a} := by have hpoint : (fun x => F x ^ 2) = F := by funext x by_cases hx : x = a <;> simp [F, hx] rw [hpoint, hmeanF] have hstat : (fun sample : Fin m → 𝒳 => empiricalMass sample a) = fun sample => (m : ℝ)⁻¹ * ∑ j, F (sample j) := by funext sample unfold empiricalMass apply congrArg ((m : ℝ)⁻¹ * ·) apply Finset.sum_congr rfl intro j hj by_cases hx : sample j = a <;> simp [F, hx] have hAvgMem : MemLp (fun sample : Fin m → 𝒳 => (m : ℝ)⁻¹ * ∑ j, F (sample j)) 2 (Measure.pi (fun _ : Fin m => μ)) := by apply MemLp.const_mul apply memLp_finset_sum intro j hj exact hFMem.comp_measurePreserving (measurePreserving_eval _ j) have hvar := iid_average_variance μ m F hFMem rw [ProbabilityTheory.variance_eq_sub hAvgMem, ProbabilityTheory.variance_eq_sub hFMem] at hvar have hmean := iid_average_integral μ m hm F (hFMem.integrable (by norm_num)) rw [hmeanF] at hmean have hstat' (sample : Fin m → 𝒳) : empiricalMass sample a = (m : ℝ)⁻¹ * ∑ j, F (sample j) := congrFun hstat sample simp_rw [hstat'] simp only [Pi.pow_apply] at hvar rw [hmean, hmeanF, hsquareF] at hvar linarith

Causalean.Stat.integral_empiricalMass_sq · Causalean/Stat/Sample/EmpiricalMass.lean:94 · uses empiricalMass

1 supporting declaration (lemmas, instances)

abs_empiricalMass_le_one lemma — The absolute empirical mass of any point is at most one, including for the empty sample.

hypotheses

N :

ℕ

sample :

Fin N → 𝒳

x :

𝒳

conclusion

|empiricalMass sample x| ≤ 1

Proof (Lean source)

lemma abs_empiricalMass_le_one {N : ℕ} (sample : Fin N → 𝒳) (x : 𝒳) : |empiricalMass sample x| ≤ 1 := by by_cases hN : 0 < N · classical unfold empiricalMass have hcount_nonneg : 0 ≤ ∑ j : Fin N, if sample j = x then (1 : ℝ) else 0 := by positivity have hcount_le : ∑ j : Fin N, (if sample j = x then (1 : ℝ) else 0) ≤ N := by calc _ ≤ ∑ _j : Fin N, (1 : ℝ) := by apply Finset.sum_le_sum intro j hj split_ifs <;> norm_num _ = N := by simp have hNreal : 0 < (N : ℝ) := by exact_mod_cast hN rw [abs_of_nonneg (mul_nonneg (inv_nonneg.mpr hNreal.le) hcount_nonneg)] calc (N : ℝ)⁻¹ * ∑ j : Fin N, (if sample j = x then 1 else 0) ≤ (N : ℝ)⁻¹ * N := by gcongr _ = 1 := by field_simp · have hzero : N = 0 := Nat.eq_zero_of_not_pos hN subst N simp [empiricalMass]

Causalean.Stat.abs_empiricalMass_le_one · Causalean/Stat/Sample/EmpiricalMass.lean:30

PiTransport 4 core · 13 supporting This file proves that the joint observable of a finite independent identically distributed sample pushes the underlying probability measure forward to the corresponding finite product measure. ★ iidSample_finN_pushforward★ event_pullback_along_iidSample

Transport to Product Samples

This file proves that the joint observable of a finite independent identically distributed sample pushes the underlying probability measure forward to the corresponding finite product measure. It also transports high-probability events on product samples back to events on the original sample space.

Two further transports live here. First, forgetting part of an i.i.d. sample: restricting a product sample to a sub-index (a cross-fitting fold, a sample split, a Finset of coordinates) is measure preserving onto the product measure over the sub-index, so integrals and pushforwards transport verbatim. Second, the existence of an i.i.d. sample with a prescribed marginal, which is shown to be equivalent to that marginal being a probability measure — i.e. to carry no information at all.

def iidSample_infinitePi reviewed

Causalean.Stat

The coordinate projections on an infinite product probability space form an i.i.d. sample with the common marginal law.

Definition (Lean source)

noncomputable def iidSample_infinitePi (P : Measure X) [IsProbabilityMeasure P] : IIDSample (ℕ → X) X (Measure.infinitePi (fun _ : ℕ => P)) P where Z i ω := ω i meas _ := measurable_pi_apply _ indep := ProbabilityTheory.iIndepFun_infinitePi (P := fun _ : ℕ => P) (X := fun _ : ℕ => id) (fun _ => measurable_id) identDist i := by refine ⟨(measurable_pi_apply 0).aemeasurable, (measurable_pi_apply i).aemeasurable, ?_⟩ rw [Measure.infinitePi_map_eval, Measure.infinitePi_map_eval] law := Measure.infinitePi_map_eval _ _

Causalean.Stat.iidSample_infinitePi · Causalean/Stat/Sample/PiTransport.lean:52 · uses IIDSample

lemma iidSample_finN_pushforward reviewed

Causalean.Stat

For an i.i.d. sample S and a fixed horizon n, the joint map of the first n sample points pushes μ forward to the product measure on Fin n → X.

Formal statement

hypotheses

S :

IIDSample Ω X μ P

n :

ℕ

conclusion

μ.map (fun ω : Ω => fun k : Fin n => S.Z k ω) = Measure.pi (fun _ : Fin n => P)

Proof (Lean source)

lemma iidSample_finN_pushforward (S : IIDSample Ω X μ P) (n : ℕ) : μ.map (fun ω : Ω => fun k : Fin n => S.Z k ω) = Measure.pi (fun _ : Fin n => P) := by haveI : IsProbabilityMeasure μ := S.indep.isProbabilityMeasure have hindep_s : iIndepFun (fun k : Fin n => S.Z (k : ℕ)) μ := S.indep.precomp Fin.val_injective have hmap := (ProbabilityTheory.iIndepFun_iff_map_fun_eq_pi_map (fun k : Fin n => (S.meas k).aemeasurable)).mp hindep_s calc μ.map (fun ω : Ω => fun k : Fin n => S.Z k ω) = Measure.pi (fun k : Fin n => μ.map (S.Z k)) := hmap _ = Measure.pi (fun _ : Fin n => P) := by congr with k rw [← (S.identDist k).map_eq, S.law]

Causalean.Stat.iidSample_finN_pushforward · Causalean/Stat/Sample/PiTransport.lean:66 · uses IIDSample

lemma event_pullback_along_iidSample reviewed

Causalean.Stat

Event transport along an IID sample (Fin n version). Given a measurable event E in the space of length-n outcome tuples whose product-measure probability under n independent copies of the population law is at least $1-\delta$ , the pullback of E along the joint observable built from the first n coordinates of the i.i.d. sample is a measurable event on the underlying sample space, with probability at least $1-\delta$ .

Formal statement

hypotheses

S :

IIDSample Ω X μ P

n :

ℕ

Set (Fin n → X)

hE_meas :

MeasurableSet E

δ :

ℝ

hE_prob :

Measure.pi (fun _ : Fin n => P) E ≥ 1 - ofReal δ

conclusion

let Ψ : Ω → (Fin n → X) := fun ω k => S.Z k ω let E' : Set Ω := Ψ ⁻¹' E MeasurableSet E' ∧

μ E' ≥ 1 - ofReal δ

Proof (Lean source)

lemma event_pullback_along_iidSample (S : IIDSample Ω X μ P) (n : ℕ) {E : Set (Fin n → X)} (hE_meas : MeasurableSet E) {δ : ℝ} (hE_prob : Measure.pi (fun _ : Fin n => P) E ≥ 1 - ofReal δ) : let Ψ : Ω → (Fin n → X) := fun ω k => S.Z k ω let E' : Set Ω := Ψ ⁻¹' E MeasurableSet E' ∧ μ E' ≥ 1 - ofReal δ := by haveI : IsProbabilityMeasure μ := S.indep.isProbabilityMeasure have hΨ_meas := iidSample_finN_measurable S n refine ⟨hΨ_meas hE_meas, ?_⟩ have hpush : μ.map (fun ω : Ω => fun k : Fin n => S.Z k ω) = Measure.pi (fun _ : Fin n => P) := iidSample_finN_pushforward S n have hmap : μ ((fun ω : Ω => fun k : Fin n => S.Z k ω) ⁻¹' E) = Measure.pi (fun _ : Fin n => P) E := by rw [← hpush, Measure.map_apply hΨ_meas hE_meas] change μ ((fun ω : Ω => fun k : Fin n => S.Z k ω) ⁻¹' E) ≥ 1 - ofReal δ rw [hmap] exact hE_prob

Causalean.Stat.event_pullback_along_iidSample · Causalean/Stat/Sample/PiTransport.lean:90 · uses IIDSample

def HasIIDSample reviewed

Causalean.Stat

Existence of an i.i.d. sample with a given law: the assertion that some probability space carries an independent, identically distributed sample whose common marginal law is a given measure.

Definition (Lean source)

def HasIIDSample {X : Type u} [MeasurableSpace X] (P : Measure X) : Prop := ∃ (Ω : Type u) (mΩ : MeasurableSpace Ω) (μ : @Measure Ω mΩ), Nonempty (@IIDSample Ω X mΩ _ μ P)

Causalean.Stat.HasIIDSample · Causalean/Stat/Sample/PiTransport.lean:234

13 supporting declarations (lemmas, instances)

iidSample_finN_measurable lemma — The joint observable Ψ ω k = S.Z k ω is measurable Ω → (Fin n → X).

hypotheses

S :

IIDSample Ω X μ P

n :

ℕ

conclusion

Measurable (fun ω : Ω => fun k : Fin n => S.Z k ω)

Proof (Lean source)

lemma iidSample_finN_measurable (S : IIDSample Ω X μ P) (n : ℕ) : Measurable (fun ω : Ω => fun k : Fin n => S.Z k ω) := measurable_pi_lambda _ (fun k => S.meas k)

Causalean.Stat.iidSample_finN_measurable · Causalean/Stat/Sample/PiTransport.lean:84
measurePreserving_pi_restrict_dep theorem — Dropping the coordinates outside a decidable sub-index of a product of probability measures leaves the product measure over that sub-index: the retained coordinates carry exactly their own product law, with no trace of the discarded ones.

hypotheses

X :

ι → Type*
∀ i, MeasurableSpace (X i)

μ :

∀ i, Measure (X i)
∀ i, IsProbabilityMeasure (μ i)

p :

ι → Prop
DecidablePred p

conclusion

MeasurePreserving (fun (s : ∀ i, X i) (i : Subtype p) => s i.1) (Measure.pi μ) (Measure.pi fun i : Subtype p => μ i.1)

Proof (Lean source)

theorem measurePreserving_pi_restrict_dep {X : ι → Type*} [∀ i, MeasurableSpace (X i)] (μ : ∀ i, Measure (X i)) [∀ i, IsProbabilityMeasure (μ i)] (p : ι → Prop) [DecidablePred p] : MeasurePreserving (fun (s : ∀ i, X i) (i : Subtype p) => s i.1) (Measure.pi μ) (Measure.pi fun i : Subtype p => μ i.1) := by have hsplit := MeasureTheory.measurePreserving_piEquivPiSubtypeProd (μ := μ) p have hfst : MeasurePreserving fst ((Measure.pi fun i : Subtype p => μ i.1).prod (Measure.pi fun i : Subtype (fun i => ¬ p i) => μ i.1)) (Measure.pi fun i : Subtype p => μ i.1) := measurePreserving_fst simpa [MeasurableEquiv.piEquivPiSubtypeProd, Function.comp_def] using hfst.comp hsplit

Causalean.Stat.measurePreserving_pi_restrict_dep · Causalean/Stat/Sample/PiTransport.lean:129
measurePreserving_pi_restrict theorem — Dropping the coordinates outside a decidable sub-index of an i.i.d. product sample leaves the i.i.d. product sample over that sub-index.

hypotheses

X :

Type*
MeasurableSpace X

μ :

Measure X
IsProbabilityMeasure μ

p :

ι → Prop
DecidablePred p

conclusion

MeasurePreserving (fun (s : ι → X) (i : Subtype p) => s i.1) (Measure.pi fun _ : ι => μ) (Measure.pi fun _ : Subtype p => μ)

Proof (Lean source)

theorem measurePreserving_pi_restrict {X : Type*} [MeasurableSpace X] (μ : Measure X) [IsProbabilityMeasure μ] (p : ι → Prop) [DecidablePred p] : MeasurePreserving (fun (s : ι → X) (i : Subtype p) => s i.1) (Measure.pi fun _ : ι => μ) (Measure.pi fun _ : Subtype p => μ) := measurePreserving_pi_restrict_dep (fun _ : ι => μ) p

Causalean.Stat.measurePreserving_pi_restrict · Causalean/Stat/Sample/PiTransport.lean:146
map_pi_restrict theorem — The law of the sub-index coordinates of an i.i.d. product sample is the product law over that sub-index; this is the pushforward packaging of the measure-preserving statement.

hypotheses

X :

Type*
MeasurableSpace X

μ :

Measure X
IsProbabilityMeasure μ

p :

ι → Prop
DecidablePred p

conclusion

(Measure.pi fun _ : ι => μ).map (fun (s : ι → X) (i : Subtype p) => s i.1)
= Measure.pi fun _ : Subtype p => μ

Proof (Lean source)

theorem map_pi_restrict {X : Type*} [MeasurableSpace X] (μ : Measure X) [IsProbabilityMeasure μ] (p : ι → Prop) [DecidablePred p] : (Measure.pi fun _ : ι => μ).map (fun (s : ι → X) (i : Subtype p) => s i.1) = Measure.pi fun _ : Subtype p => μ := (measurePreserving_pi_restrict μ p).map_eq

Causalean.Stat.map_pi_restrict · Causalean/Stat/Sample/PiTransport.lean:154
integral_comp_pi_restrict theorem — Averaging a function of the sub-index coordinates over the whole i.i.d. product sample is the same as averaging it over an i.i.d. product sample indexed by the sub-index alone.

hypotheses

X E :

Type*
MeasurableSpace X
NormedAddCommGroup E
NormedSpace ℝ E

μ :

Measure X
IsProbabilityMeasure μ

p :

ι → Prop
DecidablePred p

g :

(Subtype p → X) → E

conclusion

∫ s : ι → X, g (fun i : Subtype p => s i.1) ∂(Measure.pi fun _ : ι => μ)
= ∫ z, g z ∂(Measure.pi fun _ : Subtype p => μ)

Proof (Lean source)

theorem integral_comp_pi_restrict {X E : Type*} [MeasurableSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E] (μ : Measure X) [IsProbabilityMeasure μ] (p : ι → Prop) [DecidablePred p] (g : (Subtype p → X) → E) : ∫ s : ι → X, g (fun i : Subtype p => s i.1) ∂(Measure.pi fun _ : ι => μ) = ∫ z, g z ∂(Measure.pi fun _ : Subtype p => μ) := by classical have hmeasf : Measurable (fun (s : ι → X) (i : Subtype p) => s i.1) := measurable_pi_lambda _ fun i => measurable_pi_apply i.1 by_cases hg : AEStronglyMeasurable g (Measure.pi fun _ : Subtype p => μ) · have hmap := integral_map (f := g) hmeasf.aemeasurable (by rwa [map_pi_restrict μ p]) rw [map_pi_restrict μ p] at hmap exact hmap.symm · rw [integral_undef (fun h => hg h.aestronglyMeasurable), integral_undef fun h => hg ?_] -- Transport `L⁰`-measurability back across the product splitting. have hsplit := MeasureTheory.measurePreserving_piEquivPiSubtypeProd (μ := fun _ : ι => μ) p have hcomp := h.aestronglyMeasurable.comp_measurePreserving (hsplit.symm (MeasurableEquiv.piEquivPiSubtypeProd (fun _ : ι => X) p)) rw [show (fun s : ι → X => g fun i : Subtype p => s i.1) ∘ ⇑(MeasurableEquiv.piEquivPiSubtypeProd (fun _ : ι => X) p).symm = fun w => g w.1 by funext w simp only [Function.comp_apply] refine congrArg g ?_ funext i simp [MeasurableEquiv.piEquivPiSubtypeProd, Equiv.piEquivPiSubtypeProd, i.2]] at hcomp exact AEStronglyMeasurable.of_comp_fst hcomp (IsProbabilityMeasure.ne_zero _)

Causalean.Stat.integral_comp_pi_restrict · Causalean/Stat/Sample/PiTransport.lean:162
measurePreserving_pi_restrict_finset theorem — Dropping the coordinates outside a finite set of indices of an i.i.d. product sample leaves the i.i.d. product sample indexed by that finite set.

hypotheses

X :

Type*
MeasurableSpace X

μ :

Measure X
IsProbabilityMeasure μ

S :

Finset ι

conclusion

MeasurePreserving (fun (s : ι → X) (i : {i : ι // i ∈ S}) => s i.1) (Measure.pi fun _ : ι => μ) (Measure.pi fun _ : {i : ι // i ∈ S} => μ)

Proof (Lean source)

theorem measurePreserving_pi_restrict_finset {X : Type*} [MeasurableSpace X] (μ : Measure X) [IsProbabilityMeasure μ] (S : Finset ι) : MeasurePreserving (fun (s : ι → X) (i : {i : ι // i ∈ S}) => s i.1) (Measure.pi fun _ : ι => μ) (Measure.pi fun _ : {i : ι // i ∈ S} => μ) := by classical convert measurePreserving_pi_restrict μ (· ∈ S) using 2

Causalean.Stat.measurePreserving_pi_restrict_finset · Causalean/Stat/Sample/PiTransport.lean:197
map_pi_restrict_finset theorem — The law of the coordinates in a finite index set of an i.i.d. product sample is the product law over that finite set; this is the pushforward packaging of the measure-preserving statement.

hypotheses

X :

Type*
MeasurableSpace X

μ :

Measure X
IsProbabilityMeasure μ

S :

Finset ι

conclusion

(Measure.pi fun _ : ι => μ).map (fun (s : ι → X) (i : {i : ι // i ∈ S}) => s i.1)
= Measure.pi fun _ : {i : ι // i ∈ S} => μ

Proof (Lean source)

theorem map_pi_restrict_finset {X : Type*} [MeasurableSpace X] (μ : Measure X) [IsProbabilityMeasure μ] (S : Finset ι) : (Measure.pi fun _ : ι => μ).map (fun (s : ι → X) (i : {i : ι // i ∈ S}) => s i.1) = Measure.pi fun _ : {i : ι // i ∈ S} => μ := (measurePreserving_pi_restrict_finset μ S).map_eq

Causalean.Stat.map_pi_restrict_finset · Causalean/Stat/Sample/PiTransport.lean:206
integral_comp_pi_restrict_finset theorem — Averaging a function of the coordinates in a finite index set over the whole i.i.d. product sample is the same as averaging it over an i.i.d. product sample indexed by that finite set.

hypotheses

X E :

Type*
MeasurableSpace X
NormedAddCommGroup E
NormedSpace ℝ E

μ :

Measure X
IsProbabilityMeasure μ

S :

Finset ι

g :

({i : ι // i ∈ S} → X) → E

conclusion

∫ s : ι → X, g (fun i : {i : ι // i ∈ S} => s i.1) ∂(Measure.pi fun _ : ι => μ)
= ∫ z, g z ∂(Measure.pi fun _ : {i : ι // i ∈ S} => μ)

Proof (Lean source)

theorem integral_comp_pi_restrict_finset {X E : Type*} [MeasurableSpace X] [NormedAddCommGroup E] [NormedSpace ℝ E] (μ : Measure X) [IsProbabilityMeasure μ] (S : Finset ι) (g : ({i : ι // i ∈ S} → X) → E) : ∫ s : ι → X, g (fun i : {i : ι // i ∈ S} => s i.1) ∂(Measure.pi fun _ : ι => μ) = ∫ z, g z ∂(Measure.pi fun _ : {i : ι // i ∈ S} => μ) := by classical convert integral_comp_pi_restrict μ (· ∈ S) g using 2 congr 1 exact Subsingleton.elim _ _

Causalean.Stat.integral_comp_pi_restrict_finset · Causalean/Stat/Sample/PiTransport.lean:214
hasIIDSample_of_isProbabilityMeasure theorem — An i.i.d. sample with a given law always exists: every probability measure is the common marginal of some independent, identically distributed sample, realised on the infinite product space by the coordinate projections.

hypotheses

X :

Type u
MeasurableSpace X

P :

Measure X
IsProbabilityMeasure P

conclusion

HasIIDSample P

Proof (Lean source)

theorem hasIIDSample_of_isProbabilityMeasure {X : Type u} [MeasurableSpace X] (P : Measure X) [IsProbabilityMeasure P] : HasIIDSample P := ⟨ℕ → X, inferInstance, Measure.infinitePi fun _ : ℕ => P, ⟨iidSample_infinitePi P⟩⟩

Causalean.Stat.hasIIDSample_of_isProbabilityMeasure · Causalean/Stat/Sample/PiTransport.lean:241
hasIIDSample_iff_isProbabilityMeasure theorem — The existence of an i.i.d. sample with a prescribed common marginal is equivalent to that marginal being a probability measure.

hypotheses

X :

Type u
MeasurableSpace X

P :

Measure X

conclusion

HasIIDSample P ↔ IsProbabilityMeasure P

Proof (Lean source)

theorem hasIIDSample_iff_isProbabilityMeasure {X : Type u} [MeasurableSpace X] (P : Measure X) : HasIIDSample P ↔ IsProbabilityMeasure P := by refine ⟨?_, fun _ => hasIIDSample_of_isProbabilityMeasure P⟩ rintro ⟨Ω, mΩ, μ, ⟨S⟩⟩ haveI : IsProbabilityMeasure μ := S.indep.isProbabilityMeasure rw [← S.map_eq 0] exact Measure.isProbabilityMeasure_map (S.meas 0).aemeasurable

Causalean.Stat.hasIIDSample_iff_isProbabilityMeasure · Causalean/Stat/Sample/PiTransport.lean:248
measurable_finCoordinatewise theorem — Applying a measurable observation rule separately to every position of a finite sample produces a measurable recoded sample.

hypotheses

n :

ℕ

phi :

X → Y

hphi :

Measurable phi

conclusion

Measurable (fun z : Fin n → X => fun i => phi (z i))

Proof (Lean source)

theorem measurable_finCoordinatewise (n : ℕ) {phi : X → Y} (hphi : Measurable phi) : Measurable (fun z : Fin n → X => fun i => phi (z i)) := by exact measurable_pi_lambda _ fun i => hphi.comp (measurable_pi_apply i)

Causalean.Stat.measurable_finCoordinatewise · Causalean/Stat/Sample/PiTransport.lean:281
map_pi_finCoordinatewise theorem — Under a common probability law, applying a measurable observation rule coordinate by coordinate turns the finite product law into the finite product of the recoded marginal law.

hypotheses

n :

ℕ

mu :

Measure X
IsProbabilityMeasure mu

phi :

X → Y

hphi :

Measurable phi

conclusion

(Measure.pi (fun _ : Fin n => mu)).map (fun z : Fin n → X => fun i => phi (z i))
= Measure.pi (fun _ : Fin n => mu.map phi)

Proof (Lean source)

theorem map_pi_finCoordinatewise (n : ℕ) (mu : Measure X) [IsProbabilityMeasure mu] {phi : X → Y} (hphi : Measurable phi) : (Measure.pi (fun _ : Fin n => mu)).map (fun z : Fin n → X => fun i => phi (z i)) = Measure.pi (fun _ : Fin n => mu.map phi) := by let _ : IsProbabilityMeasure (mu.map phi) := Measure.isProbabilityMeasure_map hphi.aemeasurable exact Measure.pi_map_pi (fun _ : Fin n => hphi.aemeasurable)

Causalean.Stat.map_pi_finCoordinatewise · Causalean/Stat/Sample/PiTransport.lean:288
integral_comp_finCoordinatewise theorem — Under a common probability law, if the observation rule is measurable and the real-valued statistic of the recoded sample is measurable, then its expectation after coordinatewise recoding equals its expectation under the product of the recoded marginal law.

hypotheses

n :

ℕ

mu :

Measure X
IsProbabilityMeasure mu

phi :

X → Y

hphi :

Measurable phi

g :

(Fin n → Y) → ℝ

hg :

Measurable g

conclusion

(∫ z : Fin n → X, g (fun i => phi (z i)) ∂Measure.pi (fun _ : Fin n => mu))
= ∫ y, g y ∂Measure.pi (fun _ : Fin n => mu.map phi)

Proof (Lean source)

theorem integral_comp_finCoordinatewise (n : ℕ) (mu : Measure X) [IsProbabilityMeasure mu] {phi : X → Y} (hphi : Measurable phi) (g : (Fin n → Y) → ℝ) (hg : Measurable g) : (∫ z : Fin n → X, g (fun i => phi (z i)) ∂Measure.pi (fun _ : Fin n => mu)) = ∫ y, g y ∂Measure.pi (fun _ : Fin n => mu.map phi) := by let coord : (Fin n → X) → (Fin n → Y) := fun z i => phi (z i) have hcoord : Measurable coord := measurable_finCoordinatewise n hphi calc (∫ z : Fin n → X, g (fun i => phi (z i)) ∂Measure.pi (fun _ : Fin n => mu)) = ∫ y, g y ∂(Measure.pi (fun _ : Fin n => mu)).map coord := (integral_map hcoord.aemeasurable hg.aestronglyMeasurable).symm _ = ∫ y, g y ∂Measure.pi (fun _ : Fin n => mu.map phi) := by rw [map_pi_finCoordinatewise n mu hphi]

Causalean.Stat.integral_comp_finCoordinatewise · Causalean/Stat/Sample/PiTransport.lean:300