Stat.Sample

Sampling primitives: iid samples as measurable maps, coordinatewise measurable modifications of almost-everywhere measurable iid families, and their product-law identities.

OccupancyWeightedMean 45 core · 41 supporting · 6 submodules This module provides totalized occupancy-weighted differences of within-group sample means and a weak-second-moment variance bound under fixed overlap. Stratified 66 core · 62 supporting · 7 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

Sample 5 core · 6 supporting This file provides the library's causal-agnostic model of an independent and identically distributed sample relative to arbitrary ambient and population measures; probability-measure instances are supplied separately whe ★ map_eq★ ofAEMeasurable

I.i.d. Samples

This file provides the library's causal-agnostic model of an independent and identically distributed sample relative to arbitrary ambient and population measures; probability-measure instances are supplied separately when needed. 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 measured space: the family is mutually independent, identically distributed, and the law of each point is the measure P. Neither the ambient measure nor P is required by this structure to be a probability measure.

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

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

def measurableModification reviewed

Causalean.Stat.IIDSample

Each indexed family of random variables whose coordinates are almost-everywhere measurable has a coordinatewise measurable modification, chosen by the standard measurable-representative construction at every index.

Definition (Lean source)

parameters

Ω :

Type u_1

shared

E :

Type u_2

shared

μ :

Measure Ω

shared

X :

ℕ → Ω → E

hX :

∀ i, AEMeasurable (X i) μ

def

measurableModification X hX :

ℕ → Ω → E

given by

fun i => (hX i).mk (X i)

Causalean.Stat.IIDSample.measurableModification · Causalean/Stat/Sample.lean:90

def ofAEMeasurable reviewed

Causalean.Stat.IIDSample

Coordinatewise almost-everywhere measurability, mutual independence of the original coordinates, and a common coordinate law define an IID sample of measurable representatives with the original first-coordinate law, using the representatives, their measurability, their independence, their identical distributions, and their marginal law.

Definition (Lean source)

parameters

Ω :

Type u_1

shared

E :

Type u_2

shared

μ :

Measure Ω

shared

X :

ℕ → Ω → E

shared

hX :

∀ i, AEMeasurable (X i) μ

hindep :

iIndepFun X μ

hident :

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

def

ofAEMeasurable hX hindep hident :

IIDSample Ω E μ (μ.map (X 0))

given by

clause 1

Z := measurableModification X hX

clause 2

meas := measurableModification_measurable hX

clause 3

indep := hindep.congr (fun i => (measurableModification_ae_eq hX i).symm)

clause 4

identDist := fun i

=> by refine ⟨(measurableModification_measurable hX 0).aemeasurable, (measurableModification_measurable hX i).aemeasurable, ?_⟩ rw [Measure.map_congr (measurableModification_ae_eq hX 0), Measure.map_congr (measurableModification_ae_eq hX i)] exact (hident i).map_eq

clause 5

law := Measure.map_congr (measurableModification_ae_eq hX 0)

Causalean.Stat.IIDSample.ofAEMeasurable · Causalean/Stat/Sample.lean:114 · uses IIDSample

6 supporting declarations (lemmas, instances)

measurable_Z theorem — Each individual sample point of an i.i.d. sample is a measurable map from the ambient measured 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:63
measurableModification_measurable theorem — Under coordinatewise almost-everywhere measurability, the measurable modification at the specified index is measurable.

hypotheses

Ω :

Type u_1
shared

E :

Type u_2
shared

μ :

Measure Ω
shared

X :

ℕ → Ω → E
shared

hX :

∀ i, AEMeasurable (X i) μ

i :

ℕ

conclusion

Measurable (measurableModification X hX i)

Proof (Lean source)

@[fun_prop] theorem measurableModification_measurable (hX : ∀ i, AEMeasurable (X i) μ) (i : ℕ) : Measurable (measurableModification X hX i) := (hX i).measurable_mk

Causalean.Stat.IIDSample.measurableModification_measurable · Causalean/Stat/Sample.lean:98
measurableModification_ae_eq theorem — Under coordinatewise almost-everywhere measurability, the measurable modification at the specified index equals the original coordinate almost everywhere.

hypotheses

Ω :

Type u_1
shared

E :

Type u_2
shared

μ :

Measure Ω
shared

X :

ℕ → Ω → E
shared

hX :

∀ i, AEMeasurable (X i) μ

i :

ℕ

conclusion

measurableModification X hX i =ᵐ[μ] X i

Proof (Lean source)

theorem measurableModification_ae_eq (hX : ∀ i, AEMeasurable (X i) μ) (i : ℕ) : measurableModification X hX i =ᵐ[μ] X i := (hX i).ae_eq_mk.symm

Causalean.Stat.IIDSample.measurableModification_ae_eq · Causalean/Stat/Sample.lean:106
ofAEMeasurable_ae_eq theorem — Coordinatewise almost-everywhere measurability, mutual independence, a common coordinate law, and a specified index imply that the corresponding constructed sample coordinate equals the original coordinate almost everywhere.

hypotheses

Ω :

Type u_1
shared

E :

Type u_2
shared

μ :

Measure Ω
shared

X :

ℕ → Ω → E
shared

hX :

∀ i, AEMeasurable (X i) μ

hindep :

iIndepFun X μ

hident :

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

i :

ℕ

conclusion

(ofAEMeasurable hX hindep hident).Z i =ᵐ[μ] X i

Proof (Lean source)

theorem ofAEMeasurable_ae_eq (hX : ∀ i, AEMeasurable (X i) μ) (hindep : iIndepFun X μ) (hident : ∀ i, IdentDistrib (X 0) (X i) μ μ) (i : ℕ) : (ofAEMeasurable hX hindep hident).Z i =ᵐ[μ] X i := measurableModification_ae_eq hX i

Causalean.Stat.IIDSample.ofAEMeasurable_ae_eq · Causalean/Stat/Sample.lean:136
finite_sum_ae_eq theorem — Coordinatewise almost-everywhere measurability, a real-valued statistic, and a finite set of indices imply that the sum of the statistic over the measurable modifications equals the original-coordinate sum almost everywhere.

hypotheses

Ω :

Type u_1
shared

E :

Type u_2
shared

μ :

Measure Ω
shared

X :

ℕ → Ω → E
shared

hX :

∀ i, AEMeasurable (X i) μ

ψ :

E → ℝ

s :

Finset ℕ

conclusion

(fun ω => ∑ i ∈ s, ψ (measurableModification X hX i ω))
=ᵐ[μ] (fun ω => ∑ i ∈ s, ψ (X i ω))

Proof (Lean source)

theorem finite_sum_ae_eq (hX : ∀ i, AEMeasurable (X i) μ) (ψ : E → ℝ) (s : Finset ℕ) : (fun ω => ∑ i ∈ s, ψ (measurableModification X hX i ω)) =ᵐ[μ] (fun ω => ∑ i ∈ s, ψ (X i ω)) := by induction s using Finset.induction_on with | empty => simp | @insert i s his ih => filter_upwards [ih, measurableModification_ae_eq hX i] with ω hsum hi simp [Finset.sum_insert his, hsum, hi]

Causalean.Stat.IIDSample.finite_sum_ae_eq · Causalean/Stat/Sample.lean:147
sampleMean_ae_eq theorem — Coordinatewise almost-everywhere measurability, mutual independence, a common coordinate law, a real-valued statistic, and a sample size imply that the measurable sample mean equals the original-coordinate sample mean almost everywhere.

hypotheses

Ω :

Type u_1
shared

E :

Type u_2
shared

μ :

Measure Ω
shared

X :

ℕ → Ω → E
shared

hX :

∀ i, AEMeasurable (X i) μ

hindep :

iIndepFun X μ

hident :

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

ψ :

E → ℝ

n :

ℕ

conclusion

(ofAEMeasurable hX hindep hident).sampleMean ψ n
=ᵐ[μ] (fun ω => (n : ℝ)⁻¹ * ∑ i ∈ range n, ψ (X i ω))

Proof (Lean source)

theorem sampleMean_ae_eq (hX : ∀ i, AEMeasurable (X i) μ) (hindep : iIndepFun X μ) (hident : ∀ i, IdentDistrib (X 0) (X i) μ μ) (ψ : E → ℝ) (n : ℕ) : (ofAEMeasurable hX hindep hident).sampleMean ψ n =ᵐ[μ] (fun ω => (n : ℝ)⁻¹ * ∑ i ∈ range n, ψ (X i ω)) := by change (fun ω => (n : ℝ)⁻¹ * ∑ i ∈ range n, ψ (measurableModification X hX i ω)) =ᵐ[μ] (fun ω => (n : ℝ)⁻¹ * ∑ i ∈ range n, ψ (X i ω)) filter_upwards [finite_sum_ae_eq hX ψ (range n)] with ω hω exact congrArg ((n : ℝ)⁻¹ * ·) hω

Causalean.Stat.IIDSample.sampleMean_ae_eq · Causalean/Stat/Sample.lean:161

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

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

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

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

EffectiveSampleSize 6 core · 7 supporting This module distinguishes the sample average of squared weights from the scale-invariant Kish design effect and effective sample size. ★ empiricalWeightSecondMoment_mean★ empiricalWeightSecondMoment_lower_tail_le_of_mean_variance

Empirical weight second moments and Kish effective sample size

This module distinguishes the sample average of squared weights from the scale-invariant Kish design effect and effective sample size. It proves agreement under realized mean-one normalization, then gives mean, variance, and product-law lower-tail results for the empirical weight second moment.

def empiricalWeightSecondMoment reviewed

Causalean.Stat

Given a real-valued weight function, a sample size, and an indexed sample, the empirical weight second moment is the sample average of the squared weights.

Definition (Lean source)

parameters

Ω :

Type*

g :

Ω → ℝ

n :

ℕ

sample :

Fin n → Ω

def

empiricalWeightSecondMoment g n sample :

ℝ

given by

(n : ℝ)⁻¹ * ∑ i, g (sample i) ^ 2

Causalean.Stat.empiricalWeightSecondMoment · Causalean/Stat/Sample/EffectiveSampleSize.lean:29

abbrev empiricalKishDispersion reviewed

Causalean.Stat

Given a real-valued weight function, a sample size, and an indexed sample, this legacy compatibility name denotes the empirical weight second moment, not a scale-invariant finite-sample Kish design effect.

Definition (Lean source)

parameters

Ω :

Type*

g :

Ω → ℝ

n :

ℕ

sample :

Fin n → Ω

def

empiricalKishDispersion g n sample :

ℝ

given by

empiricalWeightSecondMoment g n sample

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

def kishDesignEffect reviewed

Causalean.Stat

Given a finite vector of realized weights, the Kish design effect is zero when their sum is zero; otherwise it is the number of weights times their squared-weight sum, divided by the square of their total weight.

Definition (Lean source)

parameters

n :

ℕ

w :

Fin n → ℝ

def

kishDesignEffect w :

ℝ

given by

if ∑ i, w i = 0 then 0 else ((n : ℝ) * ∑ i, w i ^ 2) / (∑ i, w i) ^ 2

Causalean.Stat.kishDesignEffect · Causalean/Stat/Sample/EffectiveSampleSize.lean:43

def kishEffectiveSampleSize reviewed

Causalean.Stat

Given a finite vector of realized weights, the Kish effective sample size is zero when their squared-weight sum is zero, and otherwise uses squared total weight divided by the squared-weight sum.

Definition (Lean source)

parameters

n :

ℕ

w :

Fin n → ℝ

def

kishEffectiveSampleSize w :

ℝ

given by

if ∑ i, w i ^ 2 = 0 then 0 else (∑ i, w i) ^ 2 / ∑ i, w i ^ 2

Causalean.Stat.kishEffectiveSampleSize · Causalean/Stat/Sample/EffectiveSampleSize.lean:50

lemma empiricalWeightSecondMoment_mean reviewed

Causalean.Stat

For a probability measure, a weight function, a sample size, positivity of that size, and integrability of the squared weight, the expected empirical weight second moment equals its population counterpart.

Formal statement

hypotheses

Ω :

Type*

MeasurableSpace Ω

μ :

Measure Ω

IsProbabilityMeasure μ

g :

Ω → ℝ

n :

ℕ

hn :

0 < n

hF :

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

conclusion

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

= ∫ o, g o ^ 2 ∂μ

Proof (Lean source)

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

Causalean.Stat.empiricalWeightSecondMoment_mean · Causalean/Stat/Sample/EffectiveSampleSize.lean:87 · uses empiricalWeightSecondMoment

lemma empiricalWeightSecondMoment_lower_tail_le_of_mean_variance reviewed

Causalean.Stat

Given a sample size, a sampling probability measure, a weight function, a weight envelope, a positive reference mean, positivity of the sample size, positivity of the reference mean, square-integrability of the empirical second moment, its assumed exact mean, and its assumed variance bound, Chebyshev's inequality bounds the probability of falling below half the reference mean.

Formal statement

hypotheses

Ω :

Type*

MeasurableSpace Ω

n :

ℕ

Q :

Measure (Fin n → Ω)

IsProbabilityMeasure Q

g :

Ω → ℝ

k kappa :

ℝ

hn :

0 < n

hkappa :

0 < kappa

hF :

MemLp (empiricalWeightSecondMoment g n) 2 Q

hmean :

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

hvar :

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

conclusion

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

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

Proof (Lean source)

lemma empiricalWeightSecondMoment_lower_tail_le_of_mean_variance {Ω : Type*} [MeasurableSpace Ω] (n : ℕ) (Q : Measure (Fin n → Ω)) [IsProbabilityMeasure Q] (g : Ω → ℝ) (k kappa : ℝ) (hn : 0 < n) (hkappa : 0 < kappa) (hF : MemLp (empiricalWeightSecondMoment g n) 2 Q) (hmean : (∫ sample, empiricalWeightSecondMoment g n sample ∂Q) = kappa) (hvar : variance (empiricalWeightSecondMoment g n) Q ≤ 4 * k ^ 2 * kappa / n) : (Q {sample | empiricalWeightSecondMoment g n sample < kappa / 2}).toReal ≤ 16 * k ^ 2 / ((n : ℝ) * kappa) := by have hcheb := probability_abs_sub_mean_gt_le Q (empiricalWeightSecondMoment g n) kappa (4 * k ^ 2 * kappa / n) (kappa / 2) hF (half_pos hkappa) hmean hvar have hsub : {sample | empiricalWeightSecondMoment g n sample < kappa / 2} ⊆ {sample | kappa / 2 < |empiricalWeightSecondMoment g n sample - kappa|} := by intro sample hs simp only [Set.mem_ofPred_eq] at hs ⊢ rw [abs_of_neg (by linarith)] linarith calc (Q {sample | empiricalWeightSecondMoment g n sample < kappa / 2}).toReal ≤ (Q {sample | kappa / 2 < |empiricalWeightSecondMoment 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.empiricalWeightSecondMoment_lower_tail_le_of_mean_variance · Causalean/Stat/Sample/EffectiveSampleSize.lean:188 · uses empiricalWeightSecondMoment

7 supporting declarations (lemmas, instances)

kishDesignEffect_eq_empiricalWeightSecondMoment_of_sum_eq lemma — Given realized weights, a positive sample size, and realized mean-one normalization, the two quantities agree.

hypotheses

n :

ℕ

w :

Fin n → ℝ

hn :

0 < n

hsum :

∑ i, w i = (n : ℝ)

conclusion

kishDesignEffect w = empiricalWeightSecondMoment id n w

Proof (Lean source)

lemma kishDesignEffect_eq_empiricalWeightSecondMoment_of_sum_eq {n : ℕ} (w : Fin n → ℝ) (hn : 0 < n) (hsum : ∑ i, w i = (n : ℝ)) : kishDesignEffect w = empiricalWeightSecondMoment id n w := by have hnR : (n : ℝ) ≠ 0 := by exact_mod_cast hn.ne' rw [kishDesignEffect, if_neg] · simp only [empiricalWeightSecondMoment, id_eq, hsum, inv_eq_one_div] calc (n : ℝ) * (∑ x, w x ^ 2) / (n : ℝ) ^ 2 = ((n : ℝ) / (n : ℝ) ^ 2) * ∑ x, w x ^ 2 := by ring _ = 1 / (n : ℝ) * ∑ x, w x ^ 2 := by congr 1 field_simp [hnR] · simpa [hsum] using hnR

Causalean.Stat.kishDesignEffect_eq_empiricalWeightSecondMoment_of_sum_eq · Causalean/Stat/Sample/EffectiveSampleSize.lean:57
one_le_secondMoment_of_mean_one lemma — For a probability measure, a real-valued weight, square-integrability of the weight, and population mean one, the weight's population second moment is at least one.

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:74
empiricalKishDispersion_mean lemma — For a probability measure, a weight function, a sample size, positivity of that size, and integrability of the squared weight, this legacy compatibility theorem gives the mean of the empirical weight second moment.

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 exact empiricalWeightSecondMoment_mean μ g n hn hF

Causalean.Stat.empiricalKishDispersion_mean · Causalean/Stat/Sample/EffectiveSampleSize.lean:103
empiricalWeightSecondMoment_variance_le lemma — For a probability measure, a weight function, a sample size, a weight envelope, a population second-moment value, positivity of the sample size, square-integrability of the squared weight, the population second-moment identity, and the fourth-moment envelope, the stated variance bound holds.

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 → Ω => empiricalWeightSecondMoment g n sample) (Measure.pi (fun _ : Fin n => μ))
≤ 4 * k ^ 2 * kappa / n

Proof (Lean source)

lemma empiricalWeightSecondMoment_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 → Ω => empiricalWeightSecondMoment 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.empiricalWeightSecondMoment_variance_le · Causalean/Stat/Sample/EffectiveSampleSize.lean:117
empiricalKishDispersion_variance_le lemma — For a probability measure, a weight function, a sample size, a weight envelope, a population second-moment value, positivity of the sample size, square-integrability of the squared weight, the population second-moment identity, and the fourth-moment envelope, this legacy compatibility theorem gives the variance bound for the empirical weight second moment.

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 exact empiricalWeightSecondMoment_variance_le μ g n k kappa hn hF hkappa hfourth

Causalean.Stat.empiricalKishDispersion_variance_le · Causalean/Stat/Sample/EffectiveSampleSize.lean:168
empiricalKishDispersion_lower_tail_le lemma — Given a sample size, a sampling probability measure, a weight function, a weight envelope, a positive reference mean, positivity of the sample size, positivity of the reference mean, square-integrability of the empirical second moment, its assumed exact mean, and its assumed variance bound, this legacy compatibility theorem is the Chebyshev specialization now named empiricalWeightSecondMoment_lower_tail_le_of_mean_variance.

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 exact empiricalWeightSecondMoment_lower_tail_le_of_mean_variance n Q g k kappa hn hkappa hF hmean hvar

Causalean.Stat.empiricalKishDispersion_lower_tail_le · Causalean/Stat/Sample/EffectiveSampleSize.lean:228
empiricalWeightSecondMoment_lower_tail_le lemma — For a population probability measure, a weight function, a sample size, a weight envelope, a positive population second-moment value, positivity of the sample size, positivity of that moment, square-integrability of the squared weight, the population second-moment identity, and the fourth-moment envelope, the stated product-law lower-tail bound holds.

hypotheses

Ω :

Type*
MeasurableSpace Ω

μ :

Measure Ω
IsProbabilityMeasure μ

g :

Ω → ℝ

n :

ℕ

k kappa :

ℝ

hn :

0 < n

hkappa :

0 < kappa

hF :

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

hmoment :

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

hfourth :

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

conclusion

((Measure.pi (fun _ : Fin n => μ)) {sample | empiricalWeightSecondMoment g n sample < kappa / 2}).toReal
≤ 16 * k ^ 2 / ((n : ℝ) * kappa)

Proof (Lean source)

lemma empiricalWeightSecondMoment_lower_tail_le {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] (g : Ω → ℝ) (n : ℕ) (k kappa : ℝ) (hn : 0 < n) (hkappa : 0 < kappa) (hF : MemLp (fun o => g o ^ 2) 2 μ) (hmoment : (∫ o, g o ^ 2 ∂μ) = kappa) (hfourth : ∀ᵐ o ∂μ, g o ^ 4 ≤ 4 * k ^ 2 * g o ^ 2) : ((Measure.pi (fun _ : Fin n => μ)) {sample | empiricalWeightSecondMoment g n sample < kappa / 2}).toReal ≤ 16 * k ^ 2 / ((n : ℝ) * kappa) := by have hsample : MemLp (empiricalWeightSecondMoment g n) 2 (Measure.pi (fun _ : Fin n => μ)) := by unfold empiricalWeightSecondMoment apply MemLp.const_mul simpa using memLp_finsetSum univ fun i _ => hF.comp_measurePreserving (measurePreserving_eval (fun _ : Fin n => μ) i) exact empiricalWeightSecondMoment_lower_tail_le_of_mean_variance n (Measure.pi (fun _ : Fin n => μ)) g k kappa hn hkappa hsample ((empiricalWeightSecondMoment_mean μ g n hn (hF.integrable (by norm_num))).trans hmoment) (empiricalWeightSecondMoment_variance_le μ g n k kappa hn hF hmoment hfourth)

Causalean.Stat.empiricalWeightSecondMoment_lower_tail_le · Causalean/Stat/Sample/EffectiveSampleSize.lean:250

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

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:64 · 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:100 · 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:36

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:55 · 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:70 · 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:94 · 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:238

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:88
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:133
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:150
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:158
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:166
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:201
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:210
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:218
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:246
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:253
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:286
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:293
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:305