Stat.Sample · Causalean Library

Sample 3 core · 1 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

For a measurable sample space carrying a measure, a measurable observation space carrying a population measure, an independent and identically distributed sample from that population, a real-valued statistic of one observation, and a nonnegative integer sample size, the sample mean is the function that assigns each sample-space outcome the average $n^{-1}\sum_{i<n} f(Z_i)$ , with the reciprocal convention also applying when $n=0$ .

Definition (Lean source)

parameters

Ω :

Type u_1

shared

X :

Type u_2

shared

μ :

Measure Ω

shared

P :

Measure X

shared

S :

IIDSample Ω X μ P

f :

X → ℝ

n :

ℕ

def

sampleMean S f n :

Ω → ℝ

given by

fun ω => (n : ℝ)⁻¹ * ∑ i ∈ range n, f (S.Z i ω)

Causalean.Stat.IIDSample.sampleMean · Causalean/Stat/Sample.lean:66 · 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

Ω :

Type u_1

shared

X :

Type u_2

shared

μ :

Measure Ω

shared

P :

Measure X

shared

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:73 · uses IIDSample

1 supporting declaration (lemmas, instances)

measurable_Z theorem — Each individual sample point of an i.i.d. sample is a measurable map from the ambient probability space to the observation space.

hypotheses

Ω :

Type u_1
shared

X :

Type u_2
shared

μ :

Measure Ω
shared

P :

Measure X
shared

S :

IIDSample Ω X μ P

i :

ℕ

conclusion

Measurable (S.Z i)

Proof (Lean source)

@[fun_prop] theorem measurable_Z (S : IIDSample Ω X μ P) (i : ℕ) : Measurable (S.Z i) := S.meas i

Causalean.Stat.IIDSample.measurable_Z · Causalean/Stat/Sample.lean:57

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

Given a finite or infinite cell-label space, a real-valued cell-mass function, and two cell labels, the collision kernel equals the reciprocal mass of the first label when the labels coincide and equals zero otherwise.

Definition (Lean source)

parameters

𝒳 :

Type*

q :

𝒳 → ℝ

x y :

𝒳

def

collisionKernel q x y :

ℝ

given by

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

Given a cell-label space, a real-valued cell-mass function, a nonnegative integer target-sample size, and a target sample of that size, the collision scale is the average collision-kernel value over all ordered pairs of distinct target indices, with the displayed reciprocal convention also applying at sample sizes zero and one.

Definition (Lean source)

parameters

𝒳 :

Type*

q :

𝒳 → ℝ

N :

ℕ

target :

Fin N → 𝒳

def

collisionScale q target :

ℝ

given by

((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:30

def cellMoment reviewed

Causalean.Stat

Given a cell-label space and an observation space, a real-valued cell-mass function, a map assigning each observation to a cell, a nonnegative integer source-sample size, a source sample, a real-valued observation statistic, and a cell label, the cell moment is the inverse source-sample size and inverse cell mass times the sum of the statistic over source observations projected to that cell.

Definition (Lean source)

parameters

𝒳 Ω :

Type*

q :

𝒳 → ℝ

proj :

Ω → 𝒳

n :

ℕ

sample :

Fin n → Ω

G :

Ω → ℝ

x :

𝒳

def

cellMoment q proj sample G x :

ℝ

given by

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:39

def crossAverage reviewed

Causalean.Stat

Given a cell-label space and an observation space, a real-valued cell-mass function, an observation-to-cell map, nonnegative integer source and target sample sizes, a source sample, a target sample of cell labels, and a real-valued observation statistic, the cross-sample average is the average, over target observations, of the corresponding source-sample cell moments.

Definition (Lean source)

parameters

𝒳 Ω :

Type*

q :

𝒳 → ℝ

proj :

Ω → 𝒳

n N :

ℕ

source :

Fin n → Ω

target :

Fin N → 𝒳

G :

Ω → ℝ

def

crossAverage q proj source target G :

ℝ

given by

(N : ℝ)⁻¹ * ∑ j, cellMoment q proj source G (target j)

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

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

Given an observation space, a real-valued weight function on that space, a nonnegative sample size, and a sample indexed by the integers from zero through one less than that size, the empirical Kish dispersion is the reciprocal of the sample size multiplied by the sum of the squared weights of the sampled observations.

Definition (Lean source)

parameters

Ω :

Type*

g :

Ω → ℝ

n :

ℕ

sample :

Fin n → Ω

def

empiricalKishDispersion g n sample :

ℝ

given by

(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:45 · 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:110 · 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:33
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:62

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

Given an observation space, a nonnegative sample size, a sample indexed by the integers from zero through one less than that size, and a point in the observation space, the empirical mass of that point is the reciprocal of the sample size multiplied by the number of sampled observations equal to that point.

Definition (Lean source)

parameters

𝒳 :

Type u_1

shared

N :

ℕ

sample :

Fin N → 𝒳

x :

𝒳

def

empiricalMass sample x :

ℝ

given by

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

𝒳 :

Type u_1

MeasurableSpace 𝒳

shared

μ :

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:60 · 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

𝒳 :

Type u_1

MeasurableSpace 𝒳

shared

μ :

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:96 · 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

𝒳 :

Type u_1
shared

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:32

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

Given a measurable observation space and a probability measure on it, the independent, identically distributed sample on the infinite product space is formed by coordinate projections, and every coordinate has the given probability measure as its marginal law.

Definition (Lean source)

parameters

X :

Type u_2

shared

P :

Measure X

IsProbabilityMeasure P

def

iidSample_infinitePi P :

IIDSample (ℕ → X) X (Measure.infinitePi (fun _ : ℕ => P)) P

given by

clause 1

Z i ω := ω i

clause 2

meas _ := measurable_pi_apply _

clause 3

indep := ProbabilityTheory.iIndepFun_infinitePi (P := fun _ : ℕ => P) (X := fun _ : ℕ => id) (fun _ => measurable_id)

clause 4

identDist i := by refine ⟨(measurable_pi_apply 0).aemeasurable, (measurable_pi_apply i).aemeasurable, ?_⟩ rw [Measure.infinitePi_map_eval, Measure.infinitePi_map_eval]

clause 5

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

Ω :

Type u_1

shared

X :

Type u_2

shared

μ :

Measure Ω

shared

P :

Measure X

shared

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:67 · 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

Ω :

Type u_1

shared

X :

Type u_2

shared

μ :

Measure Ω

shared

P :

Measure X

shared

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

Ψ :

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

E' :

Ψ ⁻¹' E (: Set Ω)

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:91 · uses IIDSample

def HasIIDSample reviewed

Causalean.Stat

Given a measurable observation space and a measure on it, the existence-of-an-independent, identically distributed-sample assertion states that there is a sample space with a measurable structure and a measure carrying a nonempty collection of independent, identically distributed samples whose common marginal law is the given measure.

Definition (Lean source)

parameters

X :

Type u

MeasurableSpace X

P :

Measure X

def

HasIIDSample P :

Prop

given by

∃ (Ω : Type u) (mΩ : MeasurableSpace Ω) (μ : @Measure Ω mΩ),

Nonempty (@IIDSample Ω X mΩ _ μ P)

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

13 supporting declarations (lemmas, instances)

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

hypotheses

Ω :

Type u_1
shared

X :

Type u_2
shared

μ :

Measure Ω
shared

P :

Measure X
shared

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:85
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

ι :

Type u_3
ι → Type*
shared

∀ 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:130
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

ι :

Type u_3
shared

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:147
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

ι :

Type u_3
shared

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:155
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

ι :

Type u_3
shared

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) := by fun_prop 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:163
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

ι :

Type u_3
shared

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:198
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

ι :

Type u_3
shared

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:207
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

ι :

Type u_3
shared

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:215
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:243
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:250
measurable_finCoordinatewise theorem — Applying a measurable observation rule separately to every position of a finite sample produces a measurable recoded sample.

hypotheses

X :

Type uX
shared

Y :

Type uY
shared

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:283
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

X :

Type uX
shared

Y :

Type uY
shared

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:290
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

X :

Type uX
shared

Y :

Type uY
shared

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:302