Stat.UStatistic.OrderM
Fixed- and mixed-order U-statistics: ordered injective tuples, partial-matching product and covariance expansions, normalization bounds, Hájek projections, variance identities, degeneracy conditions, remainder negligibility, CLTs, and the order-2 bridge.
Basic 15 core · 13 supporting 4 to review This module defines fixed-order U-statistics over ordered injective tuples. ★ uStatisticOrder★ hoeffding_decomp_order
Fixed-order U-statistics
This module defines fixed-order U-statistics over ordered injective tuples. The
core objects are injectiveTuples, injectiveTupleCount, uStatisticOrder,
uMeanOrder, the coordinatewise first projections uProjOrderAt and
uProjOrder, and the residual kernel uDegenOrder.
The main structural results are the falling-factorial tuple counts
injectiveTuples_card_eq_descFactorial and
injectiveTupleCount_eq_descFactorial, the pointwise Hoeffding decomposition
hoeffding_decomp_order, centering and integrability lemmas for the first-order
influence function, and uDegenOrder_integral_tail_eq_zero, which proves
coordinatewise first-order degeneracy of the residual under the stated
finite-product/Fubini hypotheses. The order-2 compatibility layer is supplied
by pairKernel, sum_injectiveTuples_two_eq_offDiag, and
uStatisticOrder_two_eq_uStatistic.
def injectiveTuples reviewed
⚑ flagged
Causalean.Stat
Ordered injective m-tuples from the first n sample indices.
Definition (Lean source)
noncomputable def injectiveTuples (m n : ℕ) : Finset (Fin m → Fin n) := by
classical
exact Finset.univ.filter Injective
def injectiveTupleCount reviewed
⚑ flagged
Causalean.Stat
The number of ordered injective m-tuples from the first n sample indices.
Definition (Lean source)
noncomputable def injectiveTupleCount (m n : ℕ) : ℝ :=
((injectiveTuples m n).card : ℝ)
def injectiveSubtypeEquivEmbedding reviewed
⚑ flagged
Causalean.Stat
Injective functions Fin m → Fin n as elements of the finite embedding type.
def uStatisticOrder reviewed
⚑ flagged
Causalean.Stat
The fixed-order U-statistic averages a kernel over ordered injective sample tuples from the first n observations.
Definition (Lean source)
noncomputable def uStatisticOrder (S : IIDSample Ω X μ P) {m : ℕ}
(h : (Fin m → X) → ℝ) (n : ℕ) : Ω → ℝ :=
fun ω => (injectiveTupleCount m n)⁻¹ *
∑ t ∈ injectiveTuples m n, h (fun j => S.Z (t j : ℕ) ω)
def uMeanOrder reviewed
⚑ flagged
Causalean.Stat
Population mean of an order-m kernel under the product law.
Definition (Lean source)
noncomputable def uMeanOrder {m : ℕ} (h : (Fin m → X) → ℝ) (P : Measure X) : ℝ :=
∫ z, h z ∂(Measure.pi fun _ : Fin m => P)
def insertCoord reviewed
⚑ flagged
Causalean.Stat
Insert one distinguished coordinate into the remaining coordinates.
Definition (Lean source)
def insertCoord {m : ℕ} (j : Fin m) (x : X) (tail : ({k : Fin m // k ≠ j}) → X) :
Fin m → X :=
fun k => if hkj : k = j then x else tail ⟨k, hkj⟩
def uProjOrderAt reviewed
⚑ flagged
Causalean.Stat
First Hoeffding projection of an order-m kernel, centred at its population mean. The distinguished coordinate is supplied explicitly; for symmetric kernels all choices agree.
Definition (Lean source)
noncomputable def uProjOrderAt {m : ℕ} (j : Fin m) (h : (Fin m → X) → ℝ)
(P : Measure X) : X → ℝ :=
fun x =>
(∫ tail : ({k : Fin m // k ≠ j}) → X,
h (insertCoord j x tail) ∂(Measure.pi fun _ : {k : Fin m // k ≠ j} => P))
- uMeanOrder h P
def uProjOrder reviewed
⚑ flagged
Causalean.Stat
First Hoeffding projection of a positive-order kernel, using coordinate 0 as the distinguished coordinate.
Definition (Lean source)
noncomputable def uProjOrder {m : ℕ} [NeZero m] (h : (Fin m → X) → ℝ)
(P : Measure X) : X → ℝ :=
uProjOrderAt (⟨0, Nat.pos_of_ne_zero (NeZero.ne m)⟩ : Fin m) h P
def uDegenOrder reviewed
⚑ flagged
Causalean.Stat
Higher-order residual kernel after removing the mean and all first Hoeffding projection terms.
Definition (Lean source)
noncomputable def uDegenOrder {m : ℕ} [NeZero m] (h : (Fin m → X) → ℝ)
(P : Measure X) : (Fin m → X) → ℝ :=
fun z => h z - uMeanOrder h P - ∑ j : Fin m, uProjOrderAt j h P (z j)
theorem hoeffding_decomp_order reviewed
⚑ flagged
Causalean.Stat
For an order-m kernel h, population law P, and an m-tuple of points z, the kernel value decomposes as the population mean plus the sum of the m coordinatewise first Hoeffding projections plus the degenerate higher-order residual kernel evaluated at z.
Formal statement
hypotheses
conclusion
Proof (Lean source)
theorem hoeffding_decomp_order {m : ℕ} [NeZero m] (h : (Fin m → X) → ℝ)
(P : Measure X) (z : Fin m → X) :
h z = uMeanOrder h P + (∑ j : Fin m, uProjOrderAt j h P (z j)) +
uDegenOrder h P z := by
simp only [uDegenOrder]
ring
def pairKernel reviewed
⚑ flagged
Causalean.Stat
Encode a binary kernel as a kernel on Fin 2 → X.
Definition (Lean source)
def pairKernel (h : X → X → ℝ) : (Fin 2 → X) → ℝ :=
fun z => h (z 0) (z 1)
def finiteInjectiveTuples unreviewed
⚑ flagged
Causalean.Stat
The injective assignments send each coordinate in a finite family to a distinct observation among the first n sample positions.
Definition (Lean source)
noncomputable def finiteInjectiveTuples (ι : Type*) [Fintype ι] (n : ℕ) :
Finset (ι → Fin n) := by
classical
exact Finset.univ.filter Injective
def normalizedFiniteKernelStatistic unreviewed
⚑ flagged
Causalean.Stat
The normalized finite-kernel statistic averages a kernel over every injective assignment of its finite coordinate family to sample positions.
Definition (Lean source)
noncomputable def normalizedFiniteKernelStatistic (S : IIDSample Ω X μ P)
{ι : Type*} [Fintype ι] (k : (ι → X) → ℝ) (n : ℕ) : Ω → ℝ :=
fun ω => ((n.descFactorial (card ι) : ℝ)⁻¹) *
∑ t ∈ finiteInjectiveTuples ι n, k (fun i => S.Z (t i : ℕ) ω)
def orderedProductKernel unreviewed
⚑ flagged
Causalean.Stat
The ordered-product kernel multiplies one real-valued coordinate function for every position in an ordered tuple.
Definition (Lean source)
def normalizedOrderedProductStatistic unreviewed
⚑ flagged
Causalean.Stat
The normalized ordered-product statistic averages coordinatewise products over injective ordered tuples and divides by the corresponding falling factorial.
Definition (Lean source)
noncomputable def normalizedOrderedProductStatistic
(S : IIDSample Ω X μ P) {r : ℕ}
(f : Fin r → X → ℝ) (n : ℕ) : Ω → ℝ :=
normalizedFiniteKernelStatistic S (orderedProductKernel f) n
13 supporting declarations (lemmas, instances)
-
injectiveTuples_card_eq_descFactorialtheorem — The ordered injective tuple count is the falling factorial n (n-1) ....Proof (Lean source)
theorem injectiveTuples_card_eq_descFactorial (m n : ℕ) : (injectiveTuples m n).card = n.descFactorial m := by classical have hsub : card {t : Fin m → Fin n // Injective t} = (injectiveTuples m n).card := by unfold injectiveTuples exact Fintype.card_of_subtype _ (by intro t; simp) rw [← hsub] rw [Fintype.card_congr (injectiveSubtypeEquivEmbedding m n)] simp [Fintype.card_embedding_eq] -
injectiveTupleCount_eq_descFactorialtheorem — The real-valued ordered injective tuple count is the falling factorial.Proof (Lean source)
theorem injectiveTupleCount_eq_descFactorial (m n : ℕ) : injectiveTupleCount m n = (n.descFactorial m : ℝ) := by rw [injectiveTupleCount, injectiveTuples_card_eq_descFactorial] -
uProjOrderAt_integrabletheorem — The coordinatewise first projection is integrable whenever the corresponding slice-averaged kernel is integrable.hypothesesm :ℕj :Fin mh :(Fin m → X) → ℝhint :Integrable (fun x => ∫ tail : ({k : Fin m // k ≠ j}) → X, h (insertCoord j x tail) ∂(Measure.pi fun _ : {k : Fin m // k ≠ j} => P)) PconclusionIntegrable (uProjOrderAt j h P) PProof (Lean source)
theorem uProjOrderAt_integrable [IsFiniteMeasure P] {m : ℕ} (j : Fin m) {h : (Fin m → X) → ℝ} (hint : Integrable (fun x => ∫ tail : ({k : Fin m // k ≠ j}) → X, h (insertCoord j x tail) ∂(Measure.pi fun _ : {k : Fin m // k ≠ j} => P)) P) : Integrable (uProjOrderAt j h P) P := by unfold uProjOrderAt exact hint.sub (integrable_const _) -
uProjOrderAt_integral_eq_zerotheorem — The coordinatewise first projection integrates to zero once the slice-averaged representation of the population mean is available. The additional equality is the standard finite-product/Fubini identity for the chosen coordinate.hypothesesm :ℕj :Fin mh :(Fin m → X) → ℝhint :Integrable (fun x => ∫ tail : ({k : Fin m // k ≠ j}) → X, h (insertCoord j x tail) ∂(Measure.pi fun _ : {k : Fin m // k ≠ j} => P)) Phmean :∫ x, (∫ tail : ({k : Fin m // k ≠ j}) → X, h (insertCoord j x tail) ∂(Measure.pi fun _ : {k : Fin m // k ≠ j} => P)) ∂P= uMeanOrder h Pconclusion∫ x, uProjOrderAt j h P x ∂P = 0Proof (Lean source)
theorem uProjOrderAt_integral_eq_zero [IsProbabilityMeasure P] {m : ℕ} (j : Fin m) {h : (Fin m → X) → ℝ} (hint : Integrable (fun x => ∫ tail : ({k : Fin m // k ≠ j}) → X, h (insertCoord j x tail) ∂(Measure.pi fun _ : {k : Fin m // k ≠ j} => P)) P) (hmean : ∫ x, (∫ tail : ({k : Fin m // k ≠ j}) → X, h (insertCoord j x tail) ∂(Measure.pi fun _ : {k : Fin m // k ≠ j} => P)) ∂P = uMeanOrder h P) : ∫ x, uProjOrderAt j h P x ∂P = 0 := by unfold uProjOrderAt rw [integral_sub hint (integrable_const _), integral_const, probReal_univ, one_smul, hmean] ring -
uInfluenceOrder_integrabletheorem — The summed first-order influence function is integrable if every coordinatewise first projection is integrable.Proof (Lean source)
theorem uInfluenceOrder_integrable {m : ℕ} {h : (Fin m → X) → ℝ} (hint : ∀ j : Fin m, Integrable (uProjOrderAt j h P) P) : Integrable (fun x => ∑ j : Fin m, uProjOrderAt j h P x) P := by exact integrable_finset_sum _ (fun j _ => hint j) -
uInfluenceOrder_integral_eq_zerotheorem — The summed first-order influence function is centered if every coordinatewise first projection is centered.hypothesesconclusion∫ x, (∑ j : Fin m, uProjOrderAt j h P x) ∂P = 0Proof (Lean source)
theorem uInfluenceOrder_integral_eq_zero {m : ℕ} {h : (Fin m → X) → ℝ} (hint : ∀ j : Fin m, Integrable (uProjOrderAt j h P) P) (hzero : ∀ j : Fin m, ∫ x, uProjOrderAt j h P x ∂P = 0) : ∫ x, (∑ j : Fin m, uProjOrderAt j h P x) ∂P = 0 := by rw [integral_finset_sum _ (fun j _ => hint j)] simp [hzero] -
integral_pi_eval_eqtheorem — Integrating a function of one coordinate under a finite product law recovers the one-dimensional integral.hypothesesconclusion∫ z : ι → X, f (z i) ∂(Measure.pi fun _ : ι => P) = ∫ x, f x ∂PProof (Lean source)
theorem integral_pi_eval_eq [IsProbabilityMeasure P] {ι : Type*} [Fintype ι] {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E] (i : ι) {f : X → E} (hf : Integrable f P) : ∫ z : ι → X, f (z i) ∂(Measure.pi fun _ : ι => P) = ∫ x, f x ∂P := by have hmp := measurePreserving_eval (fun _ : ι => P) i have hsm : AEStronglyMeasurable f (Measure.map (Function.eval i) (Measure.pi fun _ : ι => P)) := by rw [hmp.map_eq] exact hf.aestronglyMeasurable have hmap := integral_map hmp.aemeasurable hsm rw [hmp.map_eq] at hmap exact hmap.symm -
uDegenOrder_integral_tail_eq_zerotheorem — The first-order Hoeffding residual has zero conditional mean in each coordinate after integrating over all other coordinates, provided the usual finite-product/Fubini identities and slice integrability assumptions hold.hypotheseshslice_int :∀ j : Fin m,Integrable (fun x => ∫ tail : ({k : Fin m // k ≠ j}) → X, h (insertCoord j x tail) ∂(Measure.pi fun _ : {k : Fin m // k ≠ j} => P)) Phmean :∀ j : Fin m,∫ x, (∫ tail : ({k : Fin m // k ≠ j}) → X, h (insertCoord j x tail) ∂(Measure.pi fun _ : {k : Fin m // k ≠ j} => P)) ∂P= uMeanOrder h Phrow :∀ (j : Fin m) (x : X),Integrable (fun tail : ({k : Fin m // k ≠ j}) → X => h (insertCoord j x tail)) (Measure.pi fun _ : {k : Fin m // k ≠ j} => P)j :Fin mx :Xconclusion∫ tail : ({k : Fin m // k ≠ j}) → X, uDegenOrder h P (insertCoord j x tail) ∂(Measure.pi fun _ : {k : Fin m // k ≠ j} => P)= 0Proof (Lean source)
theorem uDegenOrder_integral_tail_eq_zero [IsProbabilityMeasure P] {m : ℕ} [NeZero m] {h : (Fin m → X) → ℝ} (hslice_int : ∀ j : Fin m, Integrable (fun x => ∫ tail : ({k : Fin m // k ≠ j}) → X, h (insertCoord j x tail) ∂(Measure.pi fun _ : {k : Fin m // k ≠ j} => P)) P) (hmean : ∀ j : Fin m, ∫ x, (∫ tail : ({k : Fin m // k ≠ j}) → X, h (insertCoord j x tail) ∂(Measure.pi fun _ : {k : Fin m // k ≠ j} => P)) ∂P = uMeanOrder h P) (hrow : ∀ (j : Fin m) (x : X), Integrable (fun tail : ({k : Fin m // k ≠ j}) → X => h (insertCoord j x tail)) (Measure.pi fun _ : {k : Fin m // k ≠ j} => P)) (j : Fin m) (x : X) : ∫ tail : ({k : Fin m // k ≠ j}) → X, uDegenOrder h P (insertCoord j x tail) ∂(Measure.pi fun _ : {k : Fin m // k ≠ j} => P) = 0 := by classical let ν : Measure (({k : Fin m // k ≠ j}) → X) := Measure.pi fun _ : {k : Fin m // k ≠ j} => P have hproj_int : ∀ l : Fin m, Integrable (uProjOrderAt l h P) P := fun l => uProjOrderAt_integrable l (hslice_int l) have hproj_zero : ∀ l : Fin m, ∫ y, uProjOrderAt l h P y ∂P = 0 := fun l => uProjOrderAt_integral_eq_zero l (hslice_int l) (hmean l) have hterm_int : ∀ l : Fin m, Integrable (fun tail : ({k : Fin m // k ≠ j}) → X => uProjOrderAt l h P ((insertCoord j x tail) l)) ν := by intro l by_cases hlj : l = j · subst l simp [ν, insertCoord] · have hcomp : Integrable (fun tail : ({k : Fin m // k ≠ j}) → X => uProjOrderAt l h P (tail ⟨l, hlj⟩)) ν := by change Integrable (fun tail : ({k : Fin m // k ≠ j}) → X => uProjOrderAt l h P (tail ⟨l, hlj⟩)) (Measure.pi fun _ : {k : Fin m // k ≠ j} => P) have := integral_pi_eval_eq (P := P) (i := (⟨l, hlj⟩ : {k : Fin m // k ≠ j})) (f := uProjOrderAt l h P) (hproj_int l) -- The integral identity above also supplies the needed map-law; use -- `Integrable.comp_measurePreserving` for the actual integrability. have hmp := measurePreserving_eval (fun _ : {k : Fin m // k ≠ j} => P) (⟨l, hlj⟩ : {k : Fin m // k ≠ j}) simpa [Function.comp_def] using hmp.integrable_comp_of_integrable (hproj_int l) simpa [insertCoord, hlj, ν] using hcomp have hsum_int : Integrable (fun tail : ({k : Fin m // k ≠ j}) → X => ∑ l : Fin m, uProjOrderAt l h P ((insertCoord j x tail) l)) ν := integrable_finset_sum _ (fun l _ => hterm_int l) have hconst_int : Integrable (fun _ : ({k : Fin m // k ≠ j}) → X => uMeanOrder h P) ν := integrable_const _ have hleft_int : Integrable (fun tail : ({k : Fin m // k ≠ j}) → X => h (insertCoord j x tail) - uMeanOrder h P) ν := (hrow j x).sub hconst_int have hkey : ∫ tail : ({k : Fin m // k ≠ j}) → X, uDegenOrder h P (insertCoord j x tail) ∂ν = (∫ tail : ({k : Fin m // k ≠ j}) → X, h (insertCoord j x tail) ∂ν) - uMeanOrder h P - ∑ l : Fin m, ∫ tail : ({k : Fin m // k ≠ j}) → X, uProjOrderAt l h P ((insertCoord j x tail) l) ∂ν := by rw [show (fun tail : ({k : Fin m // k ≠ j}) → X => uDegenOrder h P (insertCoord j x tail)) = (fun tail => (h (insertCoord j x tail) - uMeanOrder h P) - ∑ l : Fin m, uProjOrderAt l h P ((insertCoord j x tail) l)) from by funext tail simp only [uDegenOrder]] rw [integral_sub hleft_int hsum_int, integral_sub (hrow j x) hconst_int, integral_const, probReal_univ, one_smul, integral_finset_sum _ (fun l _ => hterm_int l)] have hsum_eval : (∑ l : Fin m, ∫ tail : ({k : Fin m // k ≠ j}) → X, uProjOrderAt l h P ((insertCoord j x tail) l) ∂ν) = uProjOrderAt j h P x := by rw [Finset.sum_eq_single j] · simp [ν, insertCoord] · intro l _ hlj have hmp := measurePreserving_eval (fun _ : {k : Fin m // k ≠ j} => P) (⟨l, hlj⟩ : {k : Fin m // k ≠ j}) have hsm : AEStronglyMeasurable (uProjOrderAt l h P) (Measure.map (Function.eval (⟨l, hlj⟩ : {k : Fin m // k ≠ j})) ν) := by change AEStronglyMeasurable (uProjOrderAt l h P) (Measure.map (Function.eval (⟨l, hlj⟩ : {k : Fin m // k ≠ j})) (Measure.pi fun _ : {k : Fin m // k ≠ j} => P)) rw [hmp.map_eq] exact (hproj_int l).aestronglyMeasurable have hmap := integral_map hmp.aemeasurable hsm change (∫ (a : X), uProjOrderAt l h P a ∂Measure.map (Function.eval (⟨l, hlj⟩ : {k : Fin m // k ≠ j})) (Measure.pi fun _ : {k : Fin m // k ≠ j} => P)) = ∫ (a : ({k : Fin m // k ≠ j}) → X), uProjOrderAt l h P (Function.eval (⟨l, hlj⟩ : {k : Fin m // k ≠ j}) a) ∂Measure.pi fun _ : {k : Fin m // k ≠ j} => P at hmap rw [hmp.map_eq] at hmap rw [show (fun tail : ({k : Fin m // k ≠ j}) → X => uProjOrderAt l h P ((insertCoord j x tail) l)) = fun tail => uProjOrderAt l h P (tail ⟨l, hlj⟩) by funext tail simp [insertCoord, hlj]] rw [← hmap, hproj_zero l] · intro hjnot exact elim (hjnot (Finset.mem_univ j)) rw [hkey, hsum_eval] unfold uProjOrderAt ring -
sum_injectiveTuples_two_eq_offDiagtheorem — Ordered injective Fin 2 tuples are the same data as off-diagonal ordered pairs.hypothesesconclusion∑ t ∈ injectiveTuples 2 n, pairKernel h (fun j => S.Z (t j : ℕ) ω)Proof (Lean source)
theorem sum_injectiveTuples_two_eq_offDiag (S : IIDSample Ω X μ P) (h : X → X → ℝ) (n : ℕ) (ω : Ω) : ∑ t ∈ injectiveTuples 2 n, pairKernel h (fun j => S.Z (t j : ℕ) ω) = ∑ p ∈ (range n).offDiag, h (S.Z p.1 ω) (S.Z p.2 ω) := by classical refine Finset.sum_bij' (fun t _ => ((t 0 : ℕ), (t 1 : ℕ))) (fun p _ => Fin.cases ⟨p.1, by exact (Finset.mem_range.mp (Finset.mem_offDiag.mp ‹p ∈ (range n).offDiag›).1)⟩ (fun _ : Fin 1 => ⟨p.2, by exact (Finset.mem_range.mp (Finset.mem_offDiag.mp ‹p ∈ (range n).offDiag›).2.1)⟩)) ?_ ?_ ?_ ?_ ?_ · intro t ht rw [Finset.mem_offDiag] have htinj : Injective t := (Finset.mem_filter.mp ht).2 refine ⟨Finset.mem_range.mpr (t 0).isLt, Finset.mem_range.mpr (t 1).isLt, ?_⟩ intro h01 have : (0 : Fin 2) = 1 := htinj (Fin.ext h01) norm_num at this · intro p hp rw [injectiveTuples, mem_filter] refine ⟨Finset.mem_univ _, ?_⟩ intro a b hab fin_cases a <;> fin_cases b · rfl · exact elim ((Finset.mem_offDiag.mp hp).2.2 (congrArg val hab)) · exact elim ((Finset.mem_offDiag.mp hp).2.2 (congrArg val hab.symm)) · rfl · intro t ht funext j fin_cases j <;> rfl · intro p hp exact Prod.ext rfl rfl · intro t ht rfl -
uStatisticOrder_two_eq_uStatistictheorem — The order-2 fixed-order statistic agrees with the existing ordered off-diagonal U-statistic for the corresponding pair kernel.hypothesesconclusionProof (Lean source)
theorem uStatisticOrder_two_eq_uStatistic (S : IIDSample Ω X μ P) (h : X → X → ℝ) (n : ℕ) : uStatisticOrder S (pairKernel h) n = uStatistic S h n := by funext ω simp only [uStatisticOrder, uStatistic, injectiveTupleCount] rw [sum_injectiveTuples_two_eq_offDiag S h n ω] congr 1 have hcard : (injectiveTuples 2 n).card = (range n).offDiag.card := Finset.card_bij (fun t _ => ((t 0 : ℕ), (t 1 : ℕ))) (by intro t ht rw [Finset.mem_offDiag] have htinj : Injective t := (Finset.mem_filter.mp ht).2 refine ⟨Finset.mem_range.mpr (t 0).isLt, Finset.mem_range.mpr (t 1).isLt, ?_⟩ intro h01 have : (0 : Fin 2) = 1 := htinj (Fin.ext h01) norm_num at this) (by intro t₁ ht₁ t₂ ht₂ hpair funext j fin_cases j · exact Fin.ext (congrArg fst hpair) · exact Fin.ext (congrArg snd hpair)) (by intro p hp refine ⟨Fin.cases ⟨p.1, Finset.mem_range.mp (Finset.mem_offDiag.mp hp).1⟩ (fun _ : Fin 1 => ⟨p.2, Finset.mem_range.mp (Finset.mem_offDiag.mp hp).2.1⟩), ?_, ?_⟩ · rw [injectiveTuples, mem_filter] refine ⟨Finset.mem_univ _, ?_⟩ intro a b hab fin_cases a <;> fin_cases b · rfl · exact elim ((Finset.mem_offDiag.mp hp).2.2 (congrArg val hab)) · exact elim ((Finset.mem_offDiag.mp hp).2.2 (congrArg val hab.symm)) · rfl · exact Prod.ext rfl rfl) have hoff : ((range n).offDiag.card : ℝ) = (n : ℝ) * ((n : ℝ) - 1) := by rw [Finset.offDiag_card, Finset.card_range] have hle : n ≤ n * n := by by_cases hn0 : n = 0 · subst n simp · exact Nat.le_mul_of_pos_right n (Nat.pos_of_ne_zero hn0) rw [Nat.cast_sub hle, Nat.cast_mul] ring rw [show ((injectiveTuples 2 n).card : ℝ) = (n : ℝ) * ((n : ℝ) - 1) by rw [hcard, hoff]] -
finiteInjectiveTuples_cardtheorem — For a finite coordinate family and sample size n, the number of injective sample assignments is the falling factorial of n with length equal to the number of coordinates.hypothesesι :Type*Fintype ιn :ℕconclusion(finiteInjectiveTuples ι n).card = n.descFactorial (card ι)Proof (Lean source)
theorem finiteInjectiveTuples_card (ι : Type*) [Fintype ι] (n : ℕ) : (finiteInjectiveTuples ι n).card = n.descFactorial (card ι) := by classical have hsub : card {t : ι → Fin n // Injective t} = (finiteInjectiveTuples ι n).card := by unfold finiteInjectiveTuples exact Fintype.card_of_subtype _ (by intro t; simp) let e : {t : ι → Fin n // Injective t} ≃ (ι ↪ Fin n) := { toFun := fun t => ⟨t.1, t.2⟩ invFun := fun f => ⟨f, f.2⟩ left_inv := fun t => by cases t; rfl right_inv := fun f => by cases f; rfl } rw [← hsub, Fintype.card_congr e] simp [Fintype.card_embedding_eq] -
normalizedFiniteKernelStatistic_fin_eq_uStatisticOrdertheorem — For an i.i.d. sample, an order-r kernel, and sample size n, the normalized finite-kernel statistic agrees with the existing fixed-order U-statistic.hypothesesconclusionnormalizedFiniteKernelStatistic S k n = uStatisticOrder S k nProof (Lean source)
theorem normalizedFiniteKernelStatistic_fin_eq_uStatisticOrder (S : IIDSample Ω X μ P) {r : ℕ} (k : (Fin r → X) → ℝ) (n : ℕ) : normalizedFiniteKernelStatistic S k n = uStatisticOrder S k n := by classical have htuples : finiteInjectiveTuples (Fin r) n = injectiveTuples r n := by ext t simp [finiteInjectiveTuples, injectiveTuples] unfold normalizedFiniteKernelStatistic uStatisticOrder rw [injectiveTupleCount_eq_descFactorial] rw [htuples] simp -
normalizedOrderedProductStatistic_eq_uStatisticOrdertheorem — For an i.i.d. sample, a family of order-r coordinate functions, and sample size n, the normalized ordered-product statistic is the existing fixed-order U-statistic applied to their product kernel.hypothesesconclusion= uStatisticOrder S (orderedProductKernel f) nProof (Lean source)
theorem normalizedOrderedProductStatistic_eq_uStatisticOrder (S : IIDSample Ω X μ P) {r : ℕ} (f : Fin r → X → ℝ) (n : ℕ) : normalizedOrderedProductStatistic S f n = uStatisticOrder S (orderedProductKernel f) n := by exact normalizedFiniteKernelStatistic_fin_eq_uStatisticOrder S (orderedProductKernel f) n
Hajek 6 core · 5 supporting Develops the fixed-order Hájek decomposition for U-statistics indexed by injective ordered m-tuples. ★ uStatisticOrder_sub_uMean_eq★ uStatisticOrder_isAsymLinear
Develops the fixed-order Hájek decomposition for U-statistics indexed by
injective ordered m-tuples.
The main objects are uInfluenceOrder, the sum of the coordinatewise first
Hoeffding projections; uRemainderOrder, the U-statistic formed from the
higher-order residual kernel; and OrderDegenerateNegligible, the √n-scale
negligibility hypothesis consumed by the fixed-order CLT. The theorem
uStatisticOrder_sub_uMean_eq proves the exact finite-sample decomposition, and
uStatisticOrder_isAsymLinear packages it as asymptotic linearity once the
residual term is negligible.
def uInfluenceOrder reviewed
⚑ flagged
Causalean.Stat
The first-order influence function of an ordered fixed-order kernel: the sum of its coordinatewise first Hoeffding projections. For a symmetric kernel this is m times the usual first projection.
Definition (Lean source)
noncomputable def uInfluenceOrder {m : ℕ} (h : (Fin m → X) → ℝ)
(P : Measure X) : X → ℝ :=
fun x => ∑ j : Fin m, uProjOrderAt j h P x
def uRemainderOrder reviewed
⚑ flagged
Causalean.Stat
The higher-order remainder statistic for an order-m U-statistic.
Definition (Lean source)
noncomputable def uRemainderOrder (S : IIDSample Ω X μ P) {m : ℕ} [NeZero m]
(h : (Fin m → X) → ℝ) (n : ℕ) : Ω → ℝ :=
uStatisticOrder S (uDegenOrder h P) n
structure OrderDegenKernel reviewed
⚑ flagged
Causalean.Stat
Fully degenerate order-m kernel. A kernel g on m-tuples over X is completely degenerate under the product measure when g is measurable, g is invariant under permuting its m coordinates, integrating g over any one coordinate against P gives zero, whichever coordinate and values are held fixed for the rest, and g is square-integrable under .
Definition (Lean source)
parameters
fields
meas :
deg :
∀ j (tail : ({k : Fin m // k ≠ j}) → X), ∫ x, g (insertCoord j x tail) ∂P = 0
sq :
Integrable (fun z => (g z) ^ 2) (Measure.pi fun _ : Fin m => P)
def OrderDegenerateNegligible reviewed
⚑ flagged
Causalean.Stat
The higher-order order-m Hájek remainder is negligible at the √n scale.
Definition (Lean source)
def OrderDegenerateNegligible (S : IIDSample Ω X μ P) {m : ℕ} [NeZero m]
(h : (Fin m → X) → ℝ) : Prop :=
IsLittleOp
(fun n ω => sqrt (n : ℝ) * uRemainderOrder S h n ω)
(fun _ => (1 : ℝ)) μ
theorem uStatisticOrder_sub_uMean_eq reviewed
⚑ flagged
Causalean.Stat
Hájek decomposition for a fixed-order U-statistic. For an i.i.d. sample S, order-m kernel h, and sample outcome ω, if the sample size is at least m, then the order-m U-statistic centered at its population mean decomposes exactly as the average of the first-order influence function over the first n sample points plus the higher-order Hájek remainder statistic.
Formal statement
hypotheses
conclusion
uStatisticOrder S h n ω - uMeanOrder h P
= (n : ℝ)⁻¹ * (∑ i ∈ range n, uInfluenceOrder h P (S.Z i ω))
+ uRemainderOrder S h n ω
Proof (Lean source)
theorem uStatisticOrder_sub_uMean_eq (S : IIDSample Ω X μ P)
{m : ℕ} [NeZero m] (h : (Fin m → X) → ℝ)
{n : ℕ} (hmn : m ≤ n) (ω : Ω) :
uStatisticOrder S h n ω - uMeanOrder h P
= (n : ℝ)⁻¹ * (∑ i ∈ range n, uInfluenceOrder h P (S.Z i ω))
+ uRemainderOrder S h n ω := by
classical
have hmpos : 0 < m := Nat.pos_of_ne_zero (NeZero.ne m)
have hnpos_nat : 0 < n := lt_of_lt_of_le hmpos hmn
have hnne : (n : ℝ) ≠ 0 := by exact_mod_cast (Nat.ne_of_gt hnpos_nat)
have hcount_ne : injectiveTupleCount m n ≠ 0 := injectiveTupleCount_ne_zero hmn
have hterm : ∀ t ∈ injectiveTuples m n,
h (fun j => S.Z (t j : ℕ) ω)
= uMeanOrder h P
+ (∑ j : Fin m, uProjOrderAt j h P (S.Z (t j : ℕ) ω))
+ uDegenOrder h P (fun j => S.Z (t j : ℕ) ω) :=
fun t _ => hoeffding_decomp_order h P _
have hproj :
(∑ t ∈ injectiveTuples m n,
∑ j : Fin m, uProjOrderAt j h P (S.Z (t j : ℕ) ω))
= (injectiveTupleCount m n / (n : ℝ))
* (∑ i ∈ range n, uInfluenceOrder h P (S.Z i ω)) := by
rw [Finset.sum_comm]
rw [show (∑ j : Fin m, ∑ t ∈ injectiveTuples m n,
uProjOrderAt j h P (S.Z (t j : ℕ) ω))
= ∑ j : Fin m, (injectiveTupleCount m n / (n : ℝ))
* ∑ i ∈ range n, uProjOrderAt j h P (S.Z i ω) from by
apply Finset.sum_congr rfl
intro j _
exact sum_injectiveTuples_apply_eq_range hmn j
(fun i => uProjOrderAt j h P (S.Z i ω))]
rw [← Finset.mul_sum]
congr 1
rw [Finset.sum_comm]
simp [uInfluenceOrder]
have hsum : (∑ t ∈ injectiveTuples m n, h (fun j => S.Z (t j : ℕ) ω))
= injectiveTupleCount m n * uMeanOrder h P
+ (injectiveTupleCount m n / (n : ℝ))
* (∑ i ∈ range n, uInfluenceOrder h P (S.Z i ω))
+ ∑ t ∈ injectiveTuples m n,
uDegenOrder h P (fun j => S.Z (t j : ℕ) ω) := by
rw [Finset.sum_congr rfl hterm]
rw [Finset.sum_add_distrib, Finset.sum_add_distrib]
rw [Finset.sum_const, nsmul_eq_mul]
rw [hproj]
simp only [injectiveTupleCount]
simp only [uStatisticOrder, uRemainderOrder, hsum]
field_simp [hcount_ne, hnne]
ring
theorem uStatisticOrder_isAsymLinear reviewed
⚑ flagged
Causalean.Stat
Fixed-order U-statistic asymptotic linearity. For an i.i.d. sample S and an order-m kernel h, write ψ for the summed coordinatewise first Hoeffding projection of h. If ψ has population mean zero and is square-integrable, and if the higher-order Hájek remainder of the order-m U-statistic is negligible at the √n scale, then the order-m U-statistic is asymptotically linear toward its population mean uMeanOrder h P, with influence function ψ.
Formal statement
hypotheses
S :
IIDSample Ω X μ P
m :
ℕ
NeZero m
h :
(Fin m → X) → ℝ
hψ_mean :
∫ x, uInfluenceOrder h P x ∂P = 0
hψ_sq :
Integrable (fun x => (uInfluenceOrder h P x) ^ 2) P
hneg :
conclusion
Proof (Lean source)
theorem uStatisticOrder_isAsymLinear (S : IIDSample Ω X μ P)
{m : ℕ} [NeZero m] (h : (Fin m → X) → ℝ)
(hψ_mean : ∫ x, uInfluenceOrder h P x ∂P = 0)
(hψ_sq : Integrable (fun x => (uInfluenceOrder h P x) ^ 2) P)
(hneg : OrderDegenerateNegligible S h) :
IsAsymLinear (uStatisticOrder S h) (uMeanOrder h P)
(uInfluenceOrder h P) S (fun r => range r) := by
refine ⟨hψ_mean, hψ_sq, ?_⟩
refine isLittleOp_of_eventuallyEq hneg ?_
filter_upwards [eventually_ge_atTop m] with n hn
exact uStatisticOrder_remainder_eq S h hn
5 supporting declarations (lemmas, instances)
-
uInfluenceOrder_eq_card_mul_of_common_projectiontheorem — If all coordinatewise first projections agree with a common projection, then the order-m influence function is m times that projection.hypothesesconclusionuInfluenceOrder h P = fun x => (m : ℝ) * φ xProof (Lean source)
theorem uInfluenceOrder_eq_card_mul_of_common_projection {m : ℕ} {h : (Fin m → X) → ℝ} {φ : X → ℝ} (hproj : ∀ j : Fin m, ∀ x, uProjOrderAt j h P x = φ x) : uInfluenceOrder h P = fun x => (m : ℝ) * φ x := by funext x simp [uInfluenceOrder, hproj, Finset.sum_const, nsmul_eq_mul] -
injectiveTupleCount_ne_zerotheorem — If m ≤ n, there is at least one ordered injective m-tuple in Fin n.Proof (Lean source)
theorem injectiveTupleCount_ne_zero {m n : ℕ} (hmn : m ≤ n) : injectiveTupleCount m n ≠ 0 := by classical have hmem : (fun j : Fin m => (⟨j.1, lt_of_lt_of_le j.2 hmn⟩ : Fin n)) ∈ injectiveTuples m n := by rw [injectiveTuples, mem_filter] refine ⟨Finset.mem_univ _, ?_⟩ intro a b hab exact Fin.ext (congrArg (fun x : Fin n => x.val) hab) have hpos : 0 < (injectiveTuples m n).card := Finset.card_pos.mpr ⟨_, hmem⟩ rw [injectiveTupleCount] exact_mod_cast (Nat.ne_of_gt hpos) -
injectiveTuples_fiber_card_eqtheorem — Fibres of a fixed coordinate map on ordered injective tuples have the same cardinality. The bijection composes tuples with the codomain transposition swapping the two fibre values.hypothesesconclusion((injectiveTuples m n).filter (fun t => t j = y)).card= ((injectiveTuples m n).filter (fun t => t j = y')).cardProof (Lean source)
theorem injectiveTuples_fiber_card_eq {m n : ℕ} (j : Fin m) (y y' : Fin n) : ((injectiveTuples m n).filter (fun t => t j = y)).card = ((injectiveTuples m n).filter (fun t => t j = y')).card := by classical refine Finset.card_bij (fun t _ => (Equiv.swap y y') ∘ t) ?hmem ?hinj ?hsurj · intro t ht rw [mem_filter] at ht ⊢ rcases ht with ⟨htuple, hj⟩ have htinj : Injective t := by simpa [injectiveTuples] using htuple refine ⟨?_, ?_⟩ · simp [injectiveTuples, (Equiv.swap y y').injective.comp htinj] · simp [comp, hj, Equiv.swap_apply_left] · intro t₁ _ t₂ _ h funext k exact (Equiv.swap y y').injective (congrFun h k) · intro t ht refine ⟨(Equiv.swap y y') ∘ t, ?_, ?_⟩ · rw [mem_filter] at ht ⊢ rcases ht with ⟨htuple, hj⟩ have htinj : Injective t := by simpa [injectiveTuples] using htuple refine ⟨?_, ?_⟩ · simp [injectiveTuples, (Equiv.swap y y').injective.comp htinj] · simp [comp, hj, Equiv.swap_apply_right] · funext k simp [comp] -
sum_injectiveTuples_apply_eq_rangetheorem — For each coordinate of an ordered injective tuple, every sample index appears equally often.hypothesesconclusion∑ t ∈ injectiveTuples m n, f (t j : ℕ)= (injectiveTupleCount m n / (n : ℝ)) * ∑ i ∈ range n, f iProof (Lean source)
theorem sum_injectiveTuples_apply_eq_range {m n : ℕ} (hmn : m ≤ n) (j : Fin m) (f : ℕ → ℝ) : ∑ t ∈ injectiveTuples m n, f (t j : ℕ) = (injectiveTupleCount m n / (n : ℝ)) * ∑ i ∈ range n, f i := by classical have hmpos : 0 < m := lt_of_le_of_lt (zero_le _) j.isLt have hnpos_nat : 0 < n := lt_of_lt_of_le hmpos hmn have hnne : (n : ℝ) ≠ 0 := by exact_mod_cast (Nat.ne_of_gt hnpos_nat) let y0 : Fin n := ⟨0, hnpos_nat⟩ let c : ℕ := ((injectiveTuples m n).filter (fun t => t j = y0)).card have hfiber_card : ∀ y : Fin n, ((injectiveTuples m n).filter (fun t => t j = y)).card = c := by intro y exact injectiveTuples_fiber_card_eq j y y0 have hcard : (injectiveTuples m n).card = n * c := by have hmaps : Set.MapsTo (fun t : Fin m → Fin n => t j) (↑(injectiveTuples m n)) (↑(Finset.univ : Finset (Fin n))) := by intro t ht simp rw [Finset.card_eq_sum_card_fiberwise (f := fun t : Fin m → Fin n => t j) (s := injectiveTuples m n) (t := (Finset.univ : Finset (Fin n))) hmaps] simp [hfiber_card, c] have hcoeff : injectiveTupleCount m n / (n : ℝ) = (c : ℝ) := by rw [injectiveTupleCount, hcard, Nat.cast_mul] field_simp [hnne] rw [← Finset.sum_fiberwise_of_maps_to (s := injectiveTuples m n) (t := (Finset.univ : Finset (Fin n))) (g := fun t : Fin m → Fin n => t j) (f := fun t : Fin m → Fin n => f (t j : ℕ))] · have hinner : ∀ y : Fin n, (∑ t ∈ injectiveTuples m n with t j = y, f (t j : ℕ)) = (c : ℝ) * f (y : ℕ) := by intro y calc ∑ t ∈ injectiveTuples m n with t j = y, f (t j : ℕ) = ∑ t ∈ injectiveTuples m n with t j = y, f (y : ℕ) := by apply Finset.sum_congr rfl intro t ht have htj : t j = y := (Finset.mem_filter.mp ht).2 simp [htj] _ = (c : ℝ) * f (y : ℕ) := by rw [Finset.sum_const, nsmul_eq_mul, hfiber_card y] simp_rw [hinner] rw [← Finset.mul_sum] rw [Fin.sum_univ_eq_sum_range] rw [hcoeff] · intro t ht simp -
uStatisticOrder_remainder_eqtheorem — The Hájek remainder in IsAsymLinear form is the rescaled higher-order residual U-statistic.hypothesesconclusion(fun ω => sqrt ((range n).card : ℝ) * (uStatisticOrder S h n ω - uMeanOrder h P) - (sqrt ((range n).card : ℝ))⁻¹ * ∑ i ∈ range n, uInfluenceOrder h P (S.Z i ω))= fun ω => sqrt (n : ℝ) * uRemainderOrder S h n ωProof (Lean source)
theorem uStatisticOrder_remainder_eq (S : IIDSample Ω X μ P) {m : ℕ} [NeZero m] (h : (Fin m → X) → ℝ) {n : ℕ} (hmn : m ≤ n) : (fun ω => sqrt ((range n).card : ℝ) * (uStatisticOrder S h n ω - uMeanOrder h P) - (sqrt ((range n).card : ℝ))⁻¹ * ∑ i ∈ range n, uInfluenceOrder h P (S.Z i ω)) = fun ω => sqrt (n : ℝ) * uRemainderOrder S h n ω := by funext ω rw [Finset.card_range] have hmpos : 0 < m := Nat.pos_of_ne_zero (NeZero.ne m) have hnpos_nat : 0 < n := lt_of_lt_of_le hmpos hmn have hnpos : (0 : ℝ) < (n : ℝ) := by exact_mod_cast hnpos_nat set s : ℝ := sqrt (n : ℝ) with hsdef have hsne : s ≠ 0 := ne_of_gt (Real.sqrt_pos.mpr hnpos) have hs2 : s * s = (n : ℝ) := Real.mul_self_sqrt (le_of_lt hnpos) rw [uStatisticOrder_sub_uMean_eq S h hmn ω] set B : ℝ := ∑ i ∈ range n, uInfluenceOrder h P (S.Z i ω) with hBdef set G : ℝ := uRemainderOrder S h n ω with hGdef rw [show (n : ℝ) = s * s from hs2.symm] field_simp ring
FirstDegenKernel 2 core · 1 supporting This module introduces OrderFirstDegenKernel, a measurable square-integrable order-m kernel whose conditional mean is zero after integrating out all coordinates except any chosen one. ★ integral_eq_zero
First-order degenerate fixed-order kernels
This module introduces OrderFirstDegenKernel, a measurable square-integrable
order-m kernel whose conditional mean is zero after integrating out all
coordinates except any chosen one. This is the degeneracy notion satisfied by
the first-order Hoeffding residual in the fixed-order U-statistic CLT.
The namespace results show that such kernels are integrable and have product-law
mean zero (OrderFirstDegenKernel.integrable and
OrderFirstDegenKernel.integral_eq_zero). Generic IIDSample transport lemmas
from OrderM.Variance supply the downstream L² bounds.
structure OrderFirstDegenKernel reviewed
⚑ flagged
Causalean.Stat
First-order degenerate order-m kernel. A kernel g on m-tuples over X, together with the population measure P, is first-order degenerate when g is measurable, its first Hoeffding projection vanishes in every coordinate — integrating g over the other coordinates against the product measure leaves zero, whichever coordinate and value are held fixed, and g is square-integrable under the product measure .
Definition (Lean source)
parameters
fields
meas :
The first Hoeffding projection in every coordinate vanishes: integrating
out the `m − 1` tail coordinates leaves `0`.
firstDeg :
∀ (j : Fin m) (x : X)
if
∫ tail : ({k : Fin m // k ≠ j})
then
X, g (insertCoord j x tail) ∂(Measure.pi fun _ : {k : Fin m // k ≠ j} => P) = 0
sq :
Integrable (fun z => (g z) ^ 2) (Measure.pi fun _ : Fin m => P)
theorem integral_eq_zero reviewed
⚑ flagged
Causalean.Stat.OrderFirstDegenKernel
Population mean of a first-order degenerate kernel is zero. If the order-m kernel g is first-order degenerate: measurable, square-integrable under the m-fold product law, and with zero mean after integrating out all but any single coordinate, then the population mean of g under the m-fold product law is zero.
Formal statement
Proof (Lean source)
theorem integral_eq_zero [IsFiniteMeasure P] (hg : OrderFirstDegenKernel P g) :
uMeanOrder g P = 0 := by
classical
let j : Fin m := ⟨0, Nat.pos_of_ne_zero (NeZero.ne m)⟩
let p : Fin m → Prop := fun k => k = j
let π : Measure (Fin m → X) := Measure.pi fun _ : Fin m => P
let πhead : Measure ({k : Fin m // p k} → X) :=
@Measure.pi {k : Fin m // p k} (fun _ => X) (fintype p)
(fun _ => inferInstance) (fun _ => P)
let πtail : Measure ({k : Fin m // ¬ p k} → X) :=
@Measure.pi {k : Fin m // ¬ p k} (fun _ => X) (fintype fun k => ¬ p k)
(fun _ => inferInstance) (fun _ => P)
let e := MeasurableEquiv.piEquivPiSubtypeProd (fun _ : Fin m => X) p
let F : (({k : Fin m // p k} → X) × ({k : Fin m // ¬ p k} → X)) → ℝ :=
fun q => g (e.symm q)
have hmp : MeasurePreserving e π (πhead.prod πtail) := by
simpa [π, πhead, πtail, e] using
(measurePreserving_piEquivPiSubtypeProd (μ := fun _ : Fin m => P)
(α := fun _ : Fin m => X) p)
have hπhead_eval : πhead =
@Measure.pi {k : Fin m // p k} (fun _ => X) (Fintype.subtypeEq j)
(fun _ => inferInstance) (fun _ => P) := by
dsimp [πhead]
letI : Fintype {k : Fin m // p k} := fintype p
refine Measure.pi_eq (μ := fun _ : {k : Fin m // p k} => P)
(μ' := @Measure.pi {k : Fin m // p k} (fun _ => X) (Fintype.subtypeEq j)
(fun _ => inferInstance) (fun _ => P)) ?_
intro s hs
letI : Fintype {k : Fin m // p k} := Fintype.subtypeEq j
rw [Measure.pi_pi]
simp
have hFsm : AEStronglyMeasurable F (πhead.prod πtail) := by
exact (hg.meas.comp e.symm.measurable).aestronglyMeasurable
have hFint : Integrable F (πhead.prod πtail) := by
have hcomp : Integrable (fun z : Fin m → X => F (e z)) π := by
simpa [F, e, π] using hg.integrable
exact (hmp.integrable_comp hFsm).mp hcomp
have hsplit : ∫ z, g z ∂π = ∫ q, F q ∂(πhead.prod πtail) := by
have h := hmp.integral_comp' F
simpa [F, e, π] using h
rw [uMeanOrder]
change ∫ z, g z ∂π = 0
rw [hsplit, integral_prod F hFint]
have hinner : ∀ head : {k : Fin m // p k} → X,
(∫ tail : {k : Fin m // ¬ p k} → X, F (head, tail) ∂πtail) = 0 := by
intro head
let a0 : {k : Fin m // p k} := ⟨j, rfl⟩
have hhead :
(fun tail : {k : Fin m // ¬ p k} → X => F (head, tail))
= fun tail => F ((fun _ : {k : Fin m // p k} => head a0), tail) := by
funext tail
congr 2
ext a
have ha : a = a0 := by
cases a with
| mk val property =>
simp only [p] at property
subst val
rfl
rw [ha]
rw [hhead]
have hfun : (fun tail : {k : Fin m // ¬ p k} → X =>
F ((fun _ : {k : Fin m // p k} => head a0), tail))
= fun tail : ({k : Fin m // k ≠ j}) → X => g (insertCoord j (head a0) tail) := by
funext tail
change g (fun k : Fin m => if h : k = j then head a0 else tail ⟨k, h⟩)
= g (insertCoord j (head a0) tail)
rfl
rw [hfun]
exact hg.firstDeg j (head a0)
rw [show (fun head : {k : Fin m // p k} → X =>
∫ tail : {k : Fin m // ¬ p k} → X, F (head, tail) ∂πtail)
= fun _ => 0 by
funext head
exact hinner head]
simp
1 supporting declaration (lemmas, instances)
-
integrabletheorem — A first-order degenerate square-integrable kernel is integrable under the product law.Proof (Lean source)
theorem integrable [IsFiniteMeasure P] (hg : OrderFirstDegenKernel P g) : Integrable g (Measure.pi fun _ : Fin m => P) := ((memLp_two_iff_integrable_sq hg.meas.aestronglyMeasurable).mpr hg.sq).integrable (by norm_num)
PartialMatching 11 core · 8 supporting 11 to review This module packages a partial matching between two finite coordinate sets as an equivalence between selected subsets. ★ card_partialMatchingsOfSize
Finite partial matchings
This module packages a partial matching between two finite coordinate sets as an equivalence between selected subsets. It provides the fixed-cardinality families used to classify collisions between two ordered injective tuples.
structure PartialMatching unreviewed
⚑ flagged
Causalean.Stat
A partial matching between ordered coordinate sets of sizes r and s selects a subset from each side and pairs the selected coordinates bijectively.
def size unreviewed
⚑ flagged
Causalean.Stat.PartialMatching
The size of a partial matching is its number of paired coordinates.
Definition (Lean source)
def size (M : PartialMatching r s) : ℕ := M.left.card
def empty unreviewed
⚑ flagged
Causalean.Stat.PartialMatching
The empty partial matching between two coordinate sets pairs no coordinates.
Definition (Lean source)
abbrev MergedIndex unreviewed
⚑ flagged
Causalean.Stat.PartialMatching
The merged coordinate set retains every left coordinate and only the unmatched right coordinates.
Definition (Lean source)
def leftInjection unreviewed
⚑ flagged
Causalean.Stat.PartialMatching
A left coordinate occupies its own position in the merged coordinate set.
Definition (Lean source)
def rightInjection unreviewed
⚑ flagged
Causalean.Stat.PartialMatching
A right coordinate shares the position of its matched left coordinate, or occupies a separate position when it is unmatched.
Definition (Lean source)
noncomputable def rightInjection (M : PartialMatching r s) (j : Fin s) : M.MergedIndex := by
classical
by_cases hj : j ∈ M.right
· exact inl (M.equiv.symm ⟨j, hj⟩).1
· exact inr ⟨j, hj⟩
def partialMatchingEquivSigma unreviewed
⚑ flagged
Causalean.Stat
Partial matchings are represented exactly by a selected subset on each side together with a bijection between those subsets.
Definition (Lean source)
def equivFintype unreviewed
⚑ flagged
Causalean.Stat
The equivalences between two finite sets form a finite collection.
Definition (Lean source)
noncomputable local instance equivFintype {α β : Type*} [Fintype α] [Fintype β] :
Fintype (α ≃ β) := by
classical
let e : (α ≃ β) ≃ {f : α → β // Bijective f} :=
{ toFun := fun f => ⟨f, f.bijective⟩
invFun := fun f => Equiv.ofBijective f.1 f.2
left_inv := fun f => Equiv.ext (fun x => rfl)
right_inv := fun f => Subtype.ext (funext (fun x => rfl)) }
exact Fintype.ofEquiv {f : α → β // Bijective f} e.symm
def finsetFintype unreviewed
⚑ flagged
Causalean.Stat
The finite subsets of a finite set form a finite collection.
Definition (Lean source)
noncomputable local instance finsetFintype {α : Type*} [Fintype α] :
Fintype (Finset α) where
elems := Finset.univ.powerset
complete := by simp
def partialMatchingsOfSize unreviewed
⚑ flagged
Causalean.Stat
The fixed-size matching family consists of all partial matchings with exactly the prescribed number of pairs.
Definition (Lean source)
noncomputable def partialMatchingsOfSize (r s h : ℕ) : Finset (PartialMatching r s) := by
classical
exact Finset.univ.filter (fun M => M.size = h)
theorem card_partialMatchingsOfSize unreviewed
⚑ flagged
Causalean.Stat
For coordinate-set sizes r and s and matching size h, the number of partial matchings is the product of the two subset counts and the number of permutations of h objects.
Formal statement
hypotheses
r s h :
ℕ
conclusion
Proof (Lean source)
theorem card_partialMatchingsOfSize (r s h : ℕ) :
(partialMatchingsOfSize r s h).card =
choose r h * choose s h * h.factorial := by
/- Count the left and right `h`-subsets, then identify equivalences between
two `h`-element subtypes with permutations of `Fin h`. -/
classical
let e : {M : PartialMatching r s // M.size = h} ≃
Σ left : {L : Finset (Fin r) // L.card = h},
Σ right : {R : Finset (Fin s) // R.card = h},
(left.1 : Set (Fin r)) ≃ (right.1 : Set (Fin s)) :=
{ toFun := fun M =>
⟨⟨M.1.left, M.2⟩,
⟨⟨M.1.right, by simpa [M.2] using M.1.right_card⟩, M.1.equiv⟩⟩
invFun := fun M =>
⟨⟨M.1.1, M.2.1.1, M.2.2⟩, M.1.2⟩
left_inv := by
rintro ⟨⟨left, right, equiv⟩, hsize⟩
rfl
right_inv := by
rintro ⟨⟨left, hleft⟩, ⟨⟨right, hright⟩, equiv⟩⟩
rfl }
rw [← Fintype.card_of_subtype (partialMatchingsOfSize r s h)
(fun M => mem_partialMatchingsOfSize M)]
rw [Fintype.card_congr e, Fintype.card_sigma]
simp_rw [Fintype.card_sigma]
have hequiv : ∀ (left : {L : Finset (Fin r) // L.card = h})
(right : {R : Finset (Fin s) // R.card = h}),
card ((left.1 : Set (Fin r)) ≃ (right.1 : Set (Fin s))) = h.factorial := by
intro left right
have hcard : card (left.1 : Set (Fin r)) =
card (right.1 : Set (Fin s)) := by
simp [left.2, right.2]
let f := Classical.choice (Fintype.card_eq.mp hcard)
exact (@Fintype.card_congr
((left.1 : Set (Fin r)) ≃ (right.1 : Set (Fin s)))
((left.1 : Set (Fin r)) ≃ (right.1 : Set (Fin s)))
equivFintype Equiv.instFintype (Equiv.refl _)).trans (by
simpa [left.2] using Fintype.card_equiv f)
simp_rw [hequiv]
simp [Fintype.card_finset_len, Nat.mul_assoc]
8 supporting declarations (lemmas, instances)
-
right_cardtheorem — Given a partial matching, its selected right subset has the same number of coordinates as the matching.Proof (Lean source)
theorem right_card (M : PartialMatching r s) : M.right.card = M.size := by simpa [size] using (Fintype.card_congr M.equiv).symm -
empty_sizetheorem — For coordinate-set sizes r and s, the empty partial matching has no pairs.Proof (Lean source)
-
eq_empty_of_size_eq_zerotheorem — A partial matching with no pairs is the empty partial matching.Proof (Lean source)
theorem eq_empty_of_size_eq_zero (M : PartialMatching r s) (hM : M.size = 0) : M = empty r s := by have hleft : M.left = ∅ := Finset.card_eq_zero.mp (by simpa [size] using hM) have hright : M.right = ∅ := Finset.card_eq_zero.mp (by simpa [right_card] using hM) cases M with | mk left right equiv => simp only at hleft hright subst left subst right congr apply Equiv.ext intro x exact elim (by simpa using x.property) -
mergedIndex_cardtheorem — For a partial matching between coordinate sets of sizes r and s, the merged coordinate set contains r + s minus the matching size coordinates.Proof (Lean source)
theorem mergedIndex_card (M : PartialMatching r s) : card M.MergedIndex = r + s - M.size := by rw [Fintype.card_sum] simp only [Fintype.card_fin, Fintype.card_subtype_compl, Fintype.card_coe, right_card] have hs : M.size ≤ s := by rw [← M.right_card] simpa using M.right.card_le_univ omega -
partialMatchingFintypeinstance — The collection of partial matchings between two finite coordinate sets is finite.noncomputable instance partialMatchingFintype (r s : ℕ) : Fintype (PartialMatching r s) := by classical exact Fintype.ofEquiv _ (partialMatchingEquivSigma r s).symm -
mem_partialMatchingsOfSizetheorem — A partial matching belongs to the family with h pairs exactly when its matching size is h.hypothesesr s h :ℕM :PartialMatching r sconclusionM ∈ partialMatchingsOfSize r s h ↔ M.size = hProof (Lean source)
@[simp] theorem mem_partialMatchingsOfSize {r s h : ℕ} (M : PartialMatching r s) : M ∈ partialMatchingsOfSize r s h ↔ M.size = h := by simp [partialMatchingsOfSize] -
size_le_mintheorem — A partial matching has at most the smaller coordinate-set size many pairs.Proof (Lean source)
theorem PartialMatching.size_le_min (M : PartialMatching r s) : M.size ≤ min r s := by apply le_min · simpa [PartialMatching.size] using M.left.card_le_univ · simpa [PartialMatching.right_card] using M.right.card_le_univ -
sum_partialMatchingsOfSizetheorem — Given a quantity assigned to each partial matching, summing it over all matchings equals summing first by matching size through the smaller coordinate-set size.Proof (Lean source)
theorem sum_partialMatchingsOfSize {α : Type*} [AddCommMonoid α] (F : PartialMatching r s → α) : (∑ M : PartialMatching r s, F M) = ∑ h ∈ range (min r s + 1), ∑ M ∈ partialMatchingsOfSize r s h, F M := by /- Partition `univ` by `M.size`; `size_le_min` supplies the range bound. -/ classical simp only [partialMatchingsOfSize, Finset.sum_filter] rw [Finset.sum_comm] apply Finset.sum_congr rfl intro M _ rw [Finset.sum_eq_single M.size] · simp · intro h hh hne simp [hne.symm] · exact fun hnotmem => elim (hnotmem (Finset.mem_range.mpr (Nat.lt_succ_of_le M.size_le_min)))
Variance 4 core · 24 supporting Provides the product-law and L² infrastructure for fixed-order U-statistics. ★ map_tuple_eq★ orderTerm_diag★ memLp_rescaled_order
Provides the product-law and L² infrastructure for fixed-order U-statistics.
For injectively indexed sample tuples, map_fintype_tuple_eq and
map_tuple_eq identify the joint law with the product measure. The remaining
public lemmas transfer integrability, unbiasedness, mean-zero, and diagonal
second-moment facts from an order-m kernel under P^m to the corresponding
sample terms and U-statistics. The declaration zetaOrder names the kernel
second moment used by the exact and upper-bound variance arguments.
theorem map_tuple_eq reviewed
⚑ flagged
Causalean.Stat.IIDSample
For an i.i.d. sample S, sample size n, and order m, if the index map t : Fin m → Fin n is injective, then the joint law of the sample coordinates selected by t is the m-fold product measure P^m.
Formal statement
def zetaOrder reviewed
⚑ flagged
Causalean.Stat.IIDSample
ζ_m = E[g(Z₁,…,Z_m)^2], the second moment of an order-m kernel under the product law P^m.
theorem orderTerm_diag reviewed
⚑ flagged
Causalean.Stat.IIDSample
For an i.i.d. sample S and order-m kernel g that is measurable, if the index map t is injective, then the second moment of the kernel term evaluated along the sample coordinates selected by t equals the kernel's second moment ζ_m under the m-fold product law.
Formal statement
hypotheses
conclusion
∫ ω, (g (fun j => S.Z (t j : ℕ) ω)) ^ 2 ∂μ = zetaOrder P g
Proof (Lean source)
theorem orderTerm_diag (hmeas : Measurable g)
{t : Fin m → Fin n} (ht : Injective t) :
∫ ω, (g (fun j => S.Z (t j : ℕ) ω)) ^ 2 ∂μ = zetaOrder P g := by
rw [zetaOrder]
rw [← S.map_tuple_eq ht]
rw [integral_map
(measurable_pi_lambda _ (fun j : Fin m => S.meas (t j : ℕ))).aemeasurable
(hmeas.pow_const 2).aestronglyMeasurable]
theorem memLp_rescaled_order reviewed
⚑ flagged
Causalean.Stat.IIDSample
For an i.i.d. sample S, order-m kernel g that is measurable and square-integrable under the m-fold product law, and sample size n, the √n-rescaled order-m U-statistic of g is square-integrable.
Formal statement
hypotheses
conclusion
Proof (Lean source)
theorem memLp_rescaled_order (hmeas : Measurable g)
(hsq : Integrable (fun z => (g z) ^ 2) (Measure.pi fun _ : Fin m => P)) (n : ℕ) :
MemLp (fun ω => sqrt (n : ℝ) * uStatisticOrder S g n ω) 2 μ := by
have hsum : MemLp (fun ω => ∑ t ∈ injectiveTuples m n,
g (fun j => S.Z (t j : ℕ) ω)) 2 μ :=
S.memLp_injectiveTuples_sum hmeas hsq n
have : (fun ω => sqrt (n : ℝ) * uStatisticOrder S g n ω)
= (fun ω => (sqrt (n : ℝ) * (injectiveTupleCount m n)⁻¹)
* ∑ t ∈ injectiveTuples m n, g (fun j => S.Z (t j : ℕ) ω)) := by
funext ω
simp only [uStatisticOrder]
ring
rw [this]
exact hsum.const_mul _
24 supporting declarations (lemmas, instances)
-
map_fintype_tuple_eqtheorem — The joint law of any finite collection of distinct sample coordinates is the corresponding product law.hypothesesconclusionμ.map (fun ω : Ω => fun i : ι => S.Z (r i : ℕ) ω) = Measure.pi (fun _ : ι => P)Proof (Lean source)
theorem map_fintype_tuple_eq (S : IIDSample Ω X μ P) {ι : Type*} [Fintype ι] {n : ℕ} {r : ι → Fin n} (hr : Injective r) : μ.map (fun ω : Ω => fun i : ι => S.Z (r i : ℕ) ω) = Measure.pi (fun _ : ι => P) := by letI : IsProbabilityMeasure μ := S.indep.isProbabilityMeasure have hrNat : Injective (fun i : ι => (r i : ℕ)) := by intro a b hab exact hr (Fin.ext hab) have hindep : iIndepFun (fun i : ι => S.Z (r i : ℕ)) μ := S.indep.precomp hrNat have hmap := (ProbabilityTheory.iIndepFun_iff_map_fun_eq_pi_map (fun i : ι => (S.meas (r i : ℕ)).aemeasurable)).mp hindep calc μ.map (fun ω : Ω => fun i : ι => S.Z (r i : ℕ) ω) = Measure.pi (fun i : ι => μ.map (S.Z (r i : ℕ))) := hmap _ = Measure.pi (fun _ : ι => P) := by congr with i rw [S.map_eq (r i : ℕ)] -
integrabletheorem — A square-integrable order-m degenerate kernel is integrable under the product law.Proof (Lean source)
theorem integrable [IsFiniteMeasure P] (hg : OrderDegenKernel P g) : Integrable g (Measure.pi fun _ : Fin m => P) := ((memLp_two_iff_integrable_sq hg.meas.aestronglyMeasurable).mpr hg.sq).integrable (by norm_num) -
integral_eq_zerotheorem — A fully degenerate order-m kernel has zero product-law mean.Proof (Lean source)
theorem integral_eq_zero (hg : OrderDegenKernel P g) : uMeanOrder g P = 0 := by classical let j : Fin m := ⟨0, Nat.pos_of_ne_zero (NeZero.ne m)⟩ let p : Fin m → Prop := fun k => k = j let π : Measure (Fin m → X) := Measure.pi fun _ : Fin m => P let πhead : Measure ({k : Fin m // p k} → X) := @Measure.pi {k : Fin m // p k} (fun _ => X) (fintype p) (fun _ => inferInstance) (fun _ => P) let πtail : Measure ({k : Fin m // ¬ p k} → X) := @Measure.pi {k : Fin m // ¬ p k} (fun _ => X) (fintype fun k => ¬ p k) (fun _ => inferInstance) (fun _ => P) let e := MeasurableEquiv.piEquivPiSubtypeProd (fun _ : Fin m => X) p let F : (({k : Fin m // p k} → X) × ({k : Fin m // ¬ p k} → X)) → ℝ := fun q => g (e.symm q) have hmp : MeasurePreserving e π (πhead.prod πtail) := by simpa [π, πhead, πtail, e] using (measurePreserving_piEquivPiSubtypeProd (μ := fun _ : Fin m => P) (α := fun _ : Fin m => X) p) have hπhead_eval : πhead = @Measure.pi {k : Fin m // p k} (fun _ => X) (Fintype.subtypeEq j) (fun _ => inferInstance) (fun _ => P) := by dsimp [πhead] letI : Fintype {k : Fin m // p k} := fintype p refine Measure.pi_eq (μ := fun _ : {k : Fin m // p k} => P) (μ' := @Measure.pi {k : Fin m // p k} (fun _ => X) (Fintype.subtypeEq j) (fun _ => inferInstance) (fun _ => P)) ?_ intro s hs letI : Fintype {k : Fin m // p k} := Fintype.subtypeEq j rw [Measure.pi_pi] simp have hFsm : AEStronglyMeasurable F (πhead.prod πtail) := by exact (hg.meas.comp e.symm.measurable).aestronglyMeasurable have hFint : Integrable F (πhead.prod πtail) := by have hcomp : Integrable (fun z : Fin m → X => F (e z)) π := by simpa [F, e, π] using hg.integrable exact (hmp.integrable_comp hFsm).mp hcomp have hsplit : ∫ z, g z ∂π = ∫ q, F q ∂(πhead.prod πtail) := by have h := hmp.integral_comp' F simpa [F, e, π] using h rw [uMeanOrder] change ∫ z, g z ∂π = 0 rw [hsplit, integral_prod_symm F hFint] have hinner : ∀ tail : {k : Fin m // ¬ p k} → X, (∫ head : {k : Fin m // p k} → X, F (head, tail) ∂πhead) = 0 := by intro tail let a0 : {k : Fin m // p k} := ⟨j, rfl⟩ have hmpu : MeasurePreserving (Function.eval a0) πhead P := by rw [hπhead_eval] simpa [p, a0] using (measurePreserving_eval (fun _ : {k : Fin m // p k} => P) a0) have hpoint : (fun head : {k : Fin m // p k} → X => F (head, tail)) = fun head => F ((fun _ : {k : Fin m // p k} => head a0), tail) := by funext head congr 2 ext a have ha : a = a0 := by cases a with | mk val property => simp only [p] at property subst val rfl rw [ha] have hchange : (∫ head : {k : Fin m // p k} → X, F (head, tail) ∂πhead) = ∫ x : X, F ((fun _ : {k : Fin m // p k} => x), tail) ∂P := by rw [hpoint] have hsm : AEStronglyMeasurable (fun x : X => F ((fun _ : {k : Fin m // p k} => x), tail)) (Measure.map (Function.eval a0) πhead) := by rw [hmpu.map_eq] exact (hg.meas.comp (by change Measurable (fun x : X => e.symm ((fun _ : {k : Fin m // p k} => x), tail)) measurability)).aestronglyMeasurable have hmap := integral_map hmpu.measurable.aemeasurable hsm rw [hmpu.map_eq] at hmap exact hmap.symm rw [hchange] have hfun : (fun x : X => F ((fun _ : {k : Fin m // p k} => x), tail)) = fun x : X => g (insertCoord j x tail) := by funext x change g (fun k : Fin m => if h : k = j then x else tail ⟨k, h⟩) = g (insertCoord j x tail) rfl rw [hfun] exact hg.deg j tail rw [show (fun tail : {k : Fin m // ¬ p k} → X => ∫ head : {k : Fin m // p k} → X, F (head, tail) ∂πhead) = fun _ => 0 by funext tail exact hinner tail] simp -
integrable_orderKernelTermtheorem — An order-m kernel term along an injective tuple is integrable whenever the kernel is integrable under the product law.hypothesesconclusionIntegrable (fun ω => h (fun j => S.Z (t j : ℕ) ω)) μProof (Lean source)
theorem integrable_orderKernelTerm {h : (Fin m → X) → ℝ} (hmeas : Measurable h) (hint : Integrable h (Measure.pi fun _ : Fin m => P)) {t : Fin m → Fin n} (ht : Injective t) : Integrable (fun ω => h (fun j => S.Z (t j : ℕ) ω)) μ := by have hmap : Integrable h (μ.map (fun ω : Ω => fun j : Fin m => S.Z (t j : ℕ) ω)) := by rw [S.map_tuple_eq ht] exact hint exact (integrable_map_measure hmeas.aestronglyMeasurable (measurable_pi_lambda _ (fun j : Fin m => S.meas (t j : ℕ))).aemeasurable).mp hmap -
integral_orderKernelTerm_eqtheorem — The expectation of an injectively indexed order-m kernel term equals the kernel's product-law mean.hypothesesconclusion∫ ω, h (fun j => S.Z (t j : ℕ) ω) ∂μ = ∫ z, h z ∂(Measure.pi fun _ : Fin m => P)Proof (Lean source)
theorem integral_orderKernelTerm_eq {h : (Fin m → X) → ℝ} (hmeas : Measurable h) {t : Fin m → Fin n} (ht : Injective t) : ∫ ω, h (fun j => S.Z (t j : ℕ) ω) ∂μ = ∫ z, h z ∂(Measure.pi fun _ : Fin m => P) := by rw [← S.map_tuple_eq ht] rw [integral_map (measurable_pi_lambda _ (fun j : Fin m => S.meas (t j : ℕ))).aemeasurable hmeas.aestronglyMeasurable] -
integral_orderKernelTerm_eq_zero_of_uMean_zerotheorem — An injectively indexed order-m kernel term has mean zero whenever the kernel has zero product-law mean.hypothesesconclusion∫ ω, h (fun j => S.Z (t j : ℕ) ω) ∂μ = 0Proof (Lean source)
theorem integral_orderKernelTerm_eq_zero_of_uMean_zero {h : (Fin m → X) → ℝ} (hmeas : Measurable h) {t : Fin m → Fin n} (ht : Injective t) (hmean_zero : uMeanOrder h P = 0) : ∫ ω, h (fun j => S.Z (t j : ℕ) ω) ∂μ = 0 := by rw [S.integral_orderKernelTerm_eq hmeas ht, ← uMeanOrder, hmean_zero] -
integral_uStatisticOrder_eq_uMeantheorem — The fixed-order U-statistic is unbiased: its expectation is the product-law kernel mean.hypothesesconclusion∫ ω, uStatisticOrder S h n ω ∂μ = uMeanOrder h PProof (Lean source)
theorem integral_uStatisticOrder_eq_uMean {m n : ℕ} {h : (Fin m → X) → ℝ} (hmeas : Measurable h) (hint : Integrable h (Measure.pi fun _ : Fin m => P)) (hmn : m ≤ n) : ∫ ω, uStatisticOrder S h n ω ∂μ = uMeanOrder h P := by classical have hcount_ne : injectiveTupleCount m n ≠ 0 := injectiveTupleCount_ne_zero hmn have hcard_ne : ((injectiveTuples m n).card : ℝ) ≠ 0 := by simpa [injectiveTupleCount] using hcount_ne have hterm_int : ∀ t ∈ injectiveTuples m n, Integrable (fun ω => h (fun j => S.Z (t j : ℕ) ω)) μ := by intro t ht exact S.integrable_orderKernelTerm hmeas hint ((Finset.mem_filter.mp ht).2) simp only [uStatisticOrder] rw [integral_const_mul, integral_finset_sum _ (fun t ht => hterm_int t ht)] have hsum_eval : (∑ t ∈ injectiveTuples m n, ∫ ω, h (fun j => S.Z (t j : ℕ) ω) ∂μ) = ∑ _t ∈ injectiveTuples m n, ∫ z, h z ∂(Measure.pi fun _ : Fin m => P) := by apply Finset.sum_congr rfl intro t ht exact S.integral_orderKernelTerm_eq hmeas ((Finset.mem_filter.mp ht).2) rw [hsum_eval] rw [Finset.sum_const, nsmul_eq_mul, uMeanOrder] rw [injectiveTupleCount] field_simp [hcard_ne] -
integral_uStatisticOrder_eq_zero_of_uMean_zerotheorem — A fixed-order U-statistic with product-law mean zero has expectation zero.hypothesesm n :ℕ(Fin m → X) → ℝhmeas :hint :Integrable h (Measure.pi fun _ : Fin m => P)hmn :m ≤ nhmean_zero :uMeanOrder h P = 0conclusion∫ ω, uStatisticOrder S h n ω ∂μ = 0Proof (Lean source)
theorem integral_uStatisticOrder_eq_zero_of_uMean_zero {m n : ℕ} {h : (Fin m → X) → ℝ} (hmeas : Measurable h) (hint : Integrable h (Measure.pi fun _ : Fin m => P)) (hmn : m ≤ n) (hmean_zero : uMeanOrder h P = 0) : ∫ ω, uStatisticOrder S h n ω ∂μ = 0 := by rw [S.integral_uStatisticOrder_eq_uMean hmeas hint hmn, hmean_zero] -
integral_rescaled_uStatisticOrder_eq_sqrt_mul_uMeantheorem — The rescaled fixed-order U-statistic has mean equal to the same rescaling of the product-law kernel mean.hypothesesconclusionProof (Lean source)
theorem integral_rescaled_uStatisticOrder_eq_sqrt_mul_uMean {m n : ℕ} {h : (Fin m → X) → ℝ} (hmeas : Measurable h) (hint : Integrable h (Measure.pi fun _ : Fin m => P)) (hmn : m ≤ n) : ∫ ω, sqrt (n : ℝ) * uStatisticOrder S h n ω ∂μ = sqrt (n : ℝ) * uMeanOrder h P := by rw [integral_const_mul, S.integral_uStatisticOrder_eq_uMean hmeas hint hmn] -
integral_rescaled_uStatisticOrder_eq_zero_of_uMean_zerotheorem — If an order-m kernel has product-law mean zero, then the rescaled fixed-order U-statistic has mean zero.hypothesesm n :ℕ(Fin m → X) → ℝhmeas :hint :Integrable h (Measure.pi fun _ : Fin m => P)hmn :m ≤ nhmean_zero :uMeanOrder h P = 0conclusion∫ ω, sqrt (n : ℝ) * uStatisticOrder S h n ω ∂μ = 0Proof (Lean source)
theorem integral_rescaled_uStatisticOrder_eq_zero_of_uMean_zero {m n : ℕ} {h : (Fin m → X) → ℝ} (hmeas : Measurable h) (hint : Integrable h (Measure.pi fun _ : Fin m => P)) (hmn : m ≤ n) (hmean_zero : uMeanOrder h P = 0) : ∫ ω, sqrt (n : ℝ) * uStatisticOrder S h n ω ∂μ = 0 := by rw [S.integral_rescaled_uStatisticOrder_eq_sqrt_mul_uMean hmeas hint hmn, hmean_zero, mul_zero] -
integral_uStatisticOrder_eq_zero_of_degenKernel_uMean_zerotheorem — A fully degenerate order-m kernel whose product-law mean is zero gives a mean-zero fixed-order U-statistic. The product-law mean-zero assumption is kept explicit here rather than inferred from coordinatewise degeneracy.hypothesesconclusion∫ ω, uStatisticOrder S g n ω ∂μ = 0Proof (Lean source)
theorem integral_uStatisticOrder_eq_zero_of_degenKernel_uMean_zero [IsFiniteMeasure P] [NeZero m] (hg : OrderDegenKernel P g) (hmn : m ≤ n) (hmean_zero : uMeanOrder g P = 0) : ∫ ω, uStatisticOrder S g n ω ∂μ = 0 := S.integral_uStatisticOrder_eq_zero_of_uMean_zero hg.meas hg.integrable hmn hmean_zero -
integral_uStatisticOrder_eq_zero_of_degenKerneltheorem — A fully degenerate order-m kernel gives a mean-zero fixed-order U-statistic in the nonempty sampling regime m ≤ n.hypothesesconclusion∫ ω, uStatisticOrder S g n ω ∂μ = 0Proof (Lean source)
theorem integral_uStatisticOrder_eq_zero_of_degenKernel [NeZero m] (hg : OrderDegenKernel P g) (hmn : m ≤ n) : ∫ ω, uStatisticOrder S g n ω ∂μ = 0 := by letI : IsProbabilityMeasure P := by rw [← S.law] exact Measure.isProbabilityMeasure_map (S.meas 0).aemeasurable exact S.integral_uStatisticOrder_eq_zero_of_degenKernel_uMean_zero hg hmn hg.integral_eq_zero -
integral_orderTerm_eq_zero_of_degenKernel_uMean_zerotheorem — An injectively indexed fully degenerate order-m kernel term has mean zero when its product-law mean is zero.hypothesesconclusion∫ ω, g (fun j => S.Z (t j : ℕ) ω) ∂μ = 0Proof (Lean source)
theorem integral_orderTerm_eq_zero_of_degenKernel_uMean_zero [NeZero m] (hg : OrderDegenKernel P g) {t : Fin m → Fin n} (ht : Injective t) (hmean_zero : uMeanOrder g P = 0) : ∫ ω, g (fun j => S.Z (t j : ℕ) ω) ∂μ = 0 := S.integral_orderKernelTerm_eq_zero_of_uMean_zero hg.meas ht hmean_zero -
integral_orderTerm_eq_zerotheorem — An injectively indexed fully degenerate order-m kernel term has mean zero.hypothesesconclusion∫ ω, g (fun j => S.Z (t j : ℕ) ω) ∂μ = 0Proof (Lean source)
theorem integral_orderTerm_eq_zero [NeZero m] (hg : OrderDegenKernel P g) {t : Fin m → Fin n} (ht : Injective t) : ∫ ω, g (fun j => S.Z (t j : ℕ) ω) ∂μ = 0 := S.integral_orderTerm_eq_zero_of_degenKernel_uMean_zero hg ht hg.integral_eq_zero -
integral_rescaled_uStatisticOrder_eq_zero_of_degenKernel_uMean_zerotheorem — A fully degenerate order-m kernel whose product-law mean is zero gives a mean-zero rescaled fixed-order U-statistic. This is a mean statement only; it does not assert the variance bound or negligibility.hypothesesconclusion∫ ω, sqrt (n : ℝ) * uStatisticOrder S g n ω ∂μ = 0Proof (Lean source)
theorem integral_rescaled_uStatisticOrder_eq_zero_of_degenKernel_uMean_zero [IsFiniteMeasure P] [NeZero m] (hg : OrderDegenKernel P g) (hmn : m ≤ n) (hmean_zero : uMeanOrder g P = 0) : ∫ ω, sqrt (n : ℝ) * uStatisticOrder S g n ω ∂μ = 0 := S.integral_rescaled_uStatisticOrder_eq_zero_of_uMean_zero hg.meas hg.integrable hmn hmean_zero -
integral_rescaled_uStatisticOrder_eq_zero_of_degenKerneltheorem — A fully degenerate order-m kernel gives a mean-zero rescaled fixed-order U-statistic in the nonempty sampling regime m ≤ n. This is a mean statement only; it does not assert the variance bound or negligibility.hypothesesconclusion∫ ω, sqrt (n : ℝ) * uStatisticOrder S g n ω ∂μ = 0Proof (Lean source)
theorem integral_rescaled_uStatisticOrder_eq_zero_of_degenKernel [NeZero m] (hg : OrderDegenKernel P g) (hmn : m ≤ n) : ∫ ω, sqrt (n : ℝ) * uStatisticOrder S g n ω ∂μ = 0 := by letI : IsProbabilityMeasure P := by rw [← S.law] exact Measure.isProbabilityMeasure_map (S.meas 0).aemeasurable exact S.integral_rescaled_uStatisticOrder_eq_zero_of_degenKernel_uMean_zero hg hmn hg.integral_eq_zero -
integrable_orderTermtheorem — An order-m kernel term along an injective tuple is integrable.hypothesesconclusionIntegrable (fun ω => g (fun j => S.Z (t j : ℕ) ω)) μProof (Lean source)
theorem integrable_orderTerm (hmeas : Measurable g) (hint : Integrable g (Measure.pi fun _ : Fin m => P)) {t : Fin m → Fin n} (ht : Injective t) : Integrable (fun ω => g (fun j => S.Z (t j : ℕ) ω)) μ := S.integrable_orderKernelTerm hmeas hint ht -
integrable_orderTerm_sqtheorem — The square of an order-m kernel term along an injective tuple is integrable.hypothesesconclusionIntegrable (fun ω => (g (fun j => S.Z (t j : ℕ) ω)) ^ 2) μProof (Lean source)
theorem integrable_orderTerm_sq (hmeas : Measurable g) (hsq : Integrable (fun z => (g z) ^ 2) (Measure.pi fun _ : Fin m => P)) {t : Fin m → Fin n} (ht : Injective t) : Integrable (fun ω => (g (fun j => S.Z (t j : ℕ) ω)) ^ 2) μ := by have hmap : Integrable (fun z => (g z) ^ 2) (μ.map (fun ω : Ω => fun j : Fin m => S.Z (t j : ℕ) ω)) := by rw [S.map_tuple_eq ht] exact hsq exact (integrable_map_measure (hmeas.pow_const 2).aestronglyMeasurable (measurable_pi_lambda _ (fun j : Fin m => S.meas (t j : ℕ))).aemeasurable).mp hmap -
memLp_orderTermtheorem — Each injective order-m kernel term is in L².hypothesesconclusionMemLp (fun ω => g (fun j => S.Z (t j : ℕ) ω)) 2 μProof (Lean source)
theorem memLp_orderTerm (hmeas : Measurable g) (hsq : Integrable (fun z => (g z) ^ 2) (Measure.pi fun _ : Fin m => P)) {t : Fin m → Fin n} (ht : Injective t) : MemLp (fun ω => g (fun j => S.Z (t j : ℕ) ω)) 2 μ := by have hm : AEStronglyMeasurable (fun ω => g (fun j => S.Z (t j : ℕ) ω)) μ := (hmeas.comp (measurable_pi_lambda _ (fun j : Fin m => S.meas (t j : ℕ)))).aestronglyMeasurable exact (memLp_two_iff_integrable_sq hm).mpr (S.integrable_orderTerm_sq hmeas hsq ht) -
integrable_orderTerm_multheorem — The product of two injective order-m kernel terms is integrable.hypothesesconclusionIntegrable (fun ω => g (fun j => S.Z (t j : ℕ) ω) * g (fun j => S.Z (q j : ℕ) ω)) μProof (Lean source)
theorem integrable_orderTerm_mul (hmeas : Measurable g) (hsq : Integrable (fun z => (g z) ^ 2) (Measure.pi fun _ : Fin m => P)) {t q : Fin m → Fin n} (ht : Injective t) (hq : Injective q) : Integrable (fun ω => g (fun j => S.Z (t j : ℕ) ω) * g (fun j => S.Z (q j : ℕ) ω)) μ := (S.memLp_orderTerm hmeas hsq ht).integrable_mul (S.memLp_orderTerm hmeas hsq hq) -
integrable_injectiveTuples_sumtheorem — The injective-tuple sum of an order-m kernel is integrable.hypothesesconclusionIntegrable (fun ω => ∑ t ∈ injectiveTuples m n, g (fun j => S.Z (t j : ℕ) ω)) μProof (Lean source)
theorem integrable_injectiveTuples_sum (hmeas : Measurable g) (hint : Integrable g (Measure.pi fun _ : Fin m => P)) (n : ℕ) : Integrable (fun ω => ∑ t ∈ injectiveTuples m n, g (fun j => S.Z (t j : ℕ) ω)) μ := by apply integrable_finset_sum intro t ht exact S.integrable_orderTerm hmeas hint ((Finset.mem_filter.mp ht).2) -
memLp_injectiveTuples_sumtheorem — The injective-tuple sum of an order-m kernel is in L².hypothesesconclusionMemLp (fun ω => ∑ t ∈ injectiveTuples m n, g (fun j => S.Z (t j : ℕ) ω)) 2 μProof (Lean source)
theorem memLp_injectiveTuples_sum (hmeas : Measurable g) (hsq : Integrable (fun z => (g z) ^ 2) (Measure.pi fun _ : Fin m => P)) (n : ℕ) : MemLp (fun ω => ∑ t ∈ injectiveTuples m n, g (fun j => S.Z (t j : ℕ) ω)) 2 μ := by have hsum := memLp_finset_sum (μ := μ) (p := 2) (injectiveTuples m n) (f := fun t ω => g (fun j => S.Z (t j : ℕ) ω)) (fun t ht => S.memLp_orderTerm hmeas hsq ((Finset.mem_filter.mp ht).2)) simpa using hsum -
integral_normalizedFiniteKernelStatistictheorem — For an i.i.d. sample, a finite coordinate family, a kernel, and sample size n, if the number of coordinates does not exceed the sample size, the kernel is measurable, and the kernel is integrable under the product law, the expected normalized statistic equals the kernel's product-law mean.hypothesesS :IIDSample Ω X μ Pι :n :ℕhcard :card ι ≤ nhkmeas :hkint :Integrable k (Measure.pi fun _ : ι => P)conclusion∫ ω, normalizedFiniteKernelStatistic S k n ω ∂μ = ∫ z, k z ∂(Measure.pi fun _ : ι => P)Proof (Lean source)
theorem integral_normalizedFiniteKernelStatistic (S : IIDSample Ω X μ P) {ι : Type*} [Fintype ι] {k : (ι → X) → ℝ} {n : ℕ} (hcard : card ι ≤ n) (hkmeas : Measurable k) (hkint : Integrable k (Measure.pi fun _ : ι => P)) : ∫ ω, normalizedFiniteKernelStatistic S k n ω ∂μ = ∫ z, k z ∂(Measure.pi fun _ : ι => P) := by /- Expand the finite sum, transport each injective assignment with `IIDSample.map_fintype_tuple_eq`, and cancel the positive tuple count. -/ classical have hdesc_ne : (n.descFactorial (card ι) : ℝ) ≠ 0 := by exact_mod_cast (Nat.descFactorial_pos.mpr hcard).ne' have hterm_int : ∀ t ∈ finiteInjectiveTuples ι n, Integrable (fun ω => k (fun i => S.Z (t i : ℕ) ω)) μ := by intro t ht have htinj : Injective t := (Finset.mem_filter.mp ht).2 have hmap : Integrable k (μ.map (fun ω : Ω => fun i : ι => S.Z (t i : ℕ) ω)) := by rw [S.map_fintype_tuple_eq htinj] exact hkint exact (integrable_map_measure hkmeas.aestronglyMeasurable (measurable_pi_lambda _ (fun i : ι => S.meas (t i : ℕ))).aemeasurable).mp hmap simp only [normalizedFiniteKernelStatistic] rw [integral_const_mul, integral_finsetSum _ (fun t ht => hterm_int t ht)] have hsum_eval : (∑ t ∈ finiteInjectiveTuples ι n, ∫ ω, k (fun i => S.Z (t i : ℕ) ω) ∂μ) = ∑ _t ∈ finiteInjectiveTuples ι n, ∫ z, k z ∂(Measure.pi fun _ : ι => P) := by apply Finset.sum_congr rfl intro t ht have htinj : Injective t := (Finset.mem_filter.mp ht).2 rw [← S.map_fintype_tuple_eq htinj] rw [integral_map (measurable_pi_lambda _ (fun i : ι => S.meas (t i : ℕ))).aemeasurable hkmeas.aestronglyMeasurable] rw [hsum_eval, Finset.sum_const, nsmul_eq_mul] rw [finiteInjectiveTuples_card] field_simp [hdesc_ne]
MixedOrderCovariance 6 core · 4 supporting 6 to review This module classifies pairs of injective tuples by their cross-tuple collision matching. ★ centeredCrossMoment_normalizedOrderedProductStatistic
Mixed-order partial-matching expansion
This module classifies pairs of injective tuples by their cross-tuple collision matching. It gives pointwise product and product-law expectation expansions, then exposes the size-zero normalization correction in the centered identity.
def mergedProductKernel unreviewed
⚑ flagged
Causalean.Stat
The merged product kernel evaluates matched left and right factors on the same observation and unmatched factors on separate observations.
Definition (Lean source)
noncomputable def mergedProductKernel {r s : ℕ} (f : Fin r → X → ℝ)
(g : Fin s → X → ℝ) (M : PartialMatching r s) :
(M.MergedIndex → X) → ℝ :=
fun z =>
(∏ i : Fin r, f i (z (M.leftInjection i))) *
∏ j : Fin s, g j (z (M.rightInjection j))
def mergedProductMoment unreviewed
⚑ flagged
Causalean.Stat
The merged product moment is the expectation of a merged product kernel under independent copies indexed by its merged coordinates.
Definition (Lean source)
noncomputable def mergedProductMoment {r s : ℕ} (P : Measure X)
(f : Fin r → X → ℝ) (g : Fin s → X → ℝ) (M : PartialMatching r s) : ℝ :=
∫ z, mergedProductKernel f g M z ∂(Measure.pi fun _ : M.MergedIndex => P)
def matchingNormalization unreviewed
⚑ flagged
Causalean.Stat
The normalization of a partial matching is the falling factorial for its number of distinct observations divided by the two marginal falling factorials.
Definition (Lean source)
noncomputable def matchingNormalization (n : ℕ) {r s : ℕ}
(M : PartialMatching r s) : ℝ :=
(n.descFactorial (r + s - M.size) : ℝ) /
((n.descFactorial r : ℝ) * (n.descFactorial s : ℝ))
def orderedProductMean unreviewed
⚑ flagged
Causalean.Stat
The ordered-product mean is the expectation of a coordinatewise product under independent draws from the population law.
Definition (Lean source)
noncomputable def orderedProductMean {r : ℕ} (P : Measure X)
(f : Fin r → X → ℝ) : ℝ :=
∫ z, orderedProductKernel f z ∂(Measure.pi fun _ : Fin r => P)
def centeredCrossMoment unreviewed
⚑ flagged
Causalean.Stat
The centered cross moment subtracts the product of two means from the mean of their product.
Definition (Lean source)
noncomputable def centeredCrossMoment (μ : Measure Ω) (A B : Ω → ℝ) : ℝ :=
(∫ ω, A ω * B ω ∂μ) - (∫ ω, A ω ∂μ) * (∫ ω, B ω ∂μ)
theorem centeredCrossMoment_normalizedOrderedProductStatistic unreviewed
⚑ flagged
Causalean.Stat
Under a probability population law, for an i.i.d. sample, statistic orders and a sample size, if the first order and the second order do not exceed the sample size, then for two coordinate-function families, when their product kernels are measurable, their product kernels are integrable, every merged kernel is measurable, and every merged kernel is integrable, their centered cross moment equals an explicit disjoint normalization correction plus the merged moments from every positive-size partial matching.
Formal statement
hypotheses
S :
IIDSample Ω X μ P
r s n :
ℕ
hrn :
r ≤ n
hsn :
s ≤ n
f :
Fin r → X → ℝ
g :
Fin s → X → ℝ
hmeasF :
hmeasG :
hintF :
hintG :
hmeas :
hint :
∀ M : PartialMatching r s,
Integrable (mergedProductKernel f g M) (Measure.pi fun _ : M.MergedIndex => P)
conclusion
centeredCrossMoment μ (normalizedOrderedProductStatistic S f n) (normalizedOrderedProductStatistic S g n)
= (matchingNormalization n (PartialMatching.empty r s) - 1) * orderedProductMean P f * orderedProductMean P g
+ ∑ h ∈ (range (min r s + 1)).filter (fun h => 0 < h), ∑ M ∈ partialMatchingsOfSize r s h, matchingNormalization n M * mergedProductMoment P f g M
Proof (Lean source)
theorem centeredCrossMoment_normalizedOrderedProductStatistic
[IsProbabilityMeasure P]
(S : IIDSample Ω X μ P) {r s n : ℕ}
(hrn : r ≤ n) (hsn : s ≤ n) (f : Fin r → X → ℝ) (g : Fin s → X → ℝ)
(hmeasF : Measurable (orderedProductKernel f))
(hmeasG : Measurable (orderedProductKernel g))
(hintF : Integrable (orderedProductKernel f) (Measure.pi fun _ : Fin r => P))
(hintG : Integrable (orderedProductKernel g) (Measure.pi fun _ : Fin s => P))
(hmeas : ∀ M : PartialMatching r s, Measurable (mergedProductKernel f g M))
(hint : ∀ M : PartialMatching r s,
Integrable (mergedProductKernel f g M)
(Measure.pi fun _ : M.MergedIndex => P)) :
centeredCrossMoment μ (normalizedOrderedProductStatistic S f n)
(normalizedOrderedProductStatistic S g n) =
(matchingNormalization n (PartialMatching.empty r s) - 1) *
orderedProductMean P f * orderedProductMean P g +
∑ h ∈ (range (min r s + 1)).filter (fun h => 0 < h),
∑ M ∈ partialMatchingsOfSize r s h,
matchingNormalization n M * mergedProductMoment P f g M := by
/- Combine the product-moment expansion with unbiasedness of each marginal.
Use `eq_empty_of_size_eq_zero` and `mergedProductMoment_empty` to rewrite the
unique size-zero term, then partition the remaining sizes by `0 < h`. -/
classical
have hfmean : ∫ ω, normalizedOrderedProductStatistic S f n ω ∂μ =
orderedProductMean P f := by
unfold normalizedOrderedProductStatistic orderedProductMean
exact integral_normalizedFiniteKernelStatistic S (by simpa using hrn) hmeasF hintF
have hgmean : ∫ ω, normalizedOrderedProductStatistic S g n ω ∂μ =
orderedProductMean P g := by
unfold normalizedOrderedProductStatistic orderedProductMean
exact integral_normalizedFiniteKernelStatistic S (by simpa using hsn) hmeasG hintG
let F : ℕ → ℝ := fun h =>
∑ M ∈ partialMatchingsOfSize r s h,
matchingNormalization n M * mergedProductMoment P f g M
have hzero : F 0 = matchingNormalization n (PartialMatching.empty r s) *
(orderedProductMean P f * orderedProductMean P g) := by
dsimp only [F]
rw [Finset.sum_eq_single (PartialMatching.empty r s)]
· rw [mergedProductMoment_empty f g hmeasF hmeasG hintF hintG]
· intro M hM hne
exact elim (hne (PartialMatching.eq_empty_of_size_eq_zero M
((mem_partialMatchingsOfSize M).mp hM)))
· intro hnot
exact elim (hnot (by simp))
let H := range (min r s + 1)
have hnonpos : H.filter (fun h => ¬0 < h) = {0} := by
ext h
simp [H]
have hsplit : (∑ h ∈ H, F h) = F 0 +
∑ h ∈ H.filter (fun h => 0 < h), F h := by
have hpart := Finset.sum_filter_add_sum_filter_not H (fun h => 0 < h) F
rw [hnonpos] at hpart
simpa [add_comm] using hpart.symm
unfold centeredCrossMoment
rw [integral_normalizedOrderedProductStatistic_mul S hrn hsn f g hmeas hint,
hfmean, hgmean]
change (∑ h ∈ H, F h) - orderedProductMean P f * orderedProductMean P g = _
rw [hsplit, hzero]
ring
4 supporting declarations (lemmas, instances)
-
matchingNormalization_of_memtheorem — Given sample size n, statistic orders r and s, and overlap size h, a partial matching belonging to the size-h family, its normalization has the falling factorial of length r + s - h in the numerator.hypothesesn r s h :ℕPartialMatching r shM :M ∈ partialMatchingsOfSize r s hconclusion= (n.descFactorial (r + s - h) : ℝ) / ((n.descFactorial r : ℝ) * (n.descFactorial s : ℝ))Proof (Lean source)
theorem matchingNormalization_of_mem {n r s h : ℕ} {M : PartialMatching r s} (hM : M ∈ partialMatchingsOfSize r s h) : matchingNormalization n M = (n.descFactorial (r + s - h) : ℝ) / ((n.descFactorial r : ℝ) * (n.descFactorial s : ℝ)) := by rw [matchingNormalization] rw [(mem_partialMatchingsOfSize M).mp hM] -
normalizedOrderedProductStatistic_mul_expansiontheorem — For an i.i.d. sample, statistic orders and a sample size, if the first order does not exceed the sample size and the second order does not exceed the sample size, then the pointwise product of the statistics built from two coordinate-function families equals the sum of normalized merged-kernel statistics over all partial matchings, grouped by overlap size.hypothesesconclusion(fun ω => normalizedOrderedProductStatistic S f n ω * normalizedOrderedProductStatistic S g n ω)= fun ω => ∑ h ∈ range (min r s + 1), ∑ M ∈ partialMatchingsOfSize r s h, matchingNormalization n M * normalizedFiniteKernelStatistic S (mergedProductKernel f g M) n ωProof (Lean source)
theorem normalizedOrderedProductStatistic_mul_expansion (S : IIDSample Ω X μ P) {r s n : ℕ} (hrn : r ≤ n) (hsn : s ≤ n) (f : Fin r → X → ℝ) (g : Fin s → X → ℝ) : (fun ω => normalizedOrderedProductStatistic S f n ω * normalizedOrderedProductStatistic S g n ω) = fun ω => ∑ h ∈ range (min r s + 1), ∑ M ∈ partialMatchingsOfSize r s h, matchingNormalization n M * normalizedFiniteKernelStatistic S (mergedProductKernel f g M) n ω := by /- Expand both tuple sums. Send a pair `(t,q)` to the matching of coordinates satisfying `t i = q j`; injectivity makes this a partial bijection. The induced map on `MergedIndex` is injective, and this construction is a bijection with `(M,u)` where `u` is an injective merged assignment. -/ classical funext ω rw [← sum_partialMatchingsOfSize] simp_rw [matchingNormalization_mul_normalizedFiniteKernelStatistic S hrn hsn] rw [← Finset.mul_sum] rw [← unnormalized_product_sum_expansion S f g ω] unfold normalizedOrderedProductStatistic normalizedFiniteKernelStatistic simp only [Fintype.card_fin] ring -
integral_normalizedOrderedProductStatistic_multheorem — For an i.i.d. sample, statistic orders and a sample size, if the first order and the second order do not exceed the sample size, then for two coordinate-function families, when every merged kernel is measurable and integrable under its product law, the expected product of their normalized statistics is the partial-matching sum of merged product-law moments.hypothesesS :IIDSample Ω X μ Pr s n :ℕhrn :r ≤ nhsn :s ≤ nf :Fin r → X → ℝg :Fin s → X → ℝhmeas :hint :∀ M : PartialMatching r s,Integrable (mergedProductKernel f g M) (Measure.pi fun _ : M.MergedIndex => P)conclusion∫ ω, normalizedOrderedProductStatistic S f n ω * normalizedOrderedProductStatistic S g n ω ∂μ= ∑ h ∈ range (min r s + 1), ∑ M ∈ partialMatchingsOfSize r s h, matchingNormalization n M * mergedProductMoment P f g MProof (Lean source)
theorem integral_normalizedOrderedProductStatistic_mul (S : IIDSample Ω X μ P) {r s n : ℕ} (hrn : r ≤ n) (hsn : s ≤ n) (f : Fin r → X → ℝ) (g : Fin s → X → ℝ) (hmeas : ∀ M : PartialMatching r s, Measurable (mergedProductKernel f g M)) (hint : ∀ M : PartialMatching r s, Integrable (mergedProductKernel f g M) (Measure.pi fun _ : M.MergedIndex => P)) : ∫ ω, normalizedOrderedProductStatistic S f n ω * normalizedOrderedProductStatistic S g n ω ∂μ = ∑ h ∈ range (min r s + 1), ∑ M ∈ partialMatchingsOfSize r s h, matchingNormalization n M * mergedProductMoment P f g M := by classical rw [normalizedOrderedProductStatistic_mul_expansion S hrn hsn f g] have hterm : ∀ h ∈ range (min r s + 1), Integrable (fun ω => ∑ M ∈ partialMatchingsOfSize r s h, matchingNormalization n M * normalizedFiniteKernelStatistic S (mergedProductKernel f g M) n ω) μ := by intro h hh apply integrable_finset_sum intro M hM by_cases hc : card M.MergedIndex ≤ n · exact (integrable_normalizedFiniteKernelStatistic S (hmeas M) (hint M)).const_mul _ · rw [matchingNormalization_eq_zero_of_card_gt M hc] simp rw [integral_finset_sum _ hterm] apply Finset.sum_congr rfl intro h hh rw [integral_finset_sum] · apply Finset.sum_congr rfl intro M hM rw [integral_const_mul] by_cases hc : card M.MergedIndex ≤ n · rw [integral_normalizedFiniteKernelStatistic S hc (hmeas M) (hint M)] rfl · rw [matchingNormalization_eq_zero_of_card_gt M hc] simp · intro M hM by_cases hc : card M.MergedIndex ≤ n · exact (integrable_normalizedFiniteKernelStatistic S (hmeas M) (hint M)).const_mul _ · rw [matchingNormalization_eq_zero_of_card_gt M hc] simp -
mergedProductMoment_emptytheorem — Under a probability law, for two coordinate-function families of orders r and s, if the first product kernel is measurable, the second product kernel is measurable, the first product kernel is integrable, and the second product kernel is integrable, the empty matching's merged moment factors into the two separate product-law means.hypothesesconclusionmergedProductMoment P f g (PartialMatching.empty r s)= orderedProductMean P f * orderedProductMean P gProof (Lean source)
theorem mergedProductMoment_empty [IsProbabilityMeasure P] {r s : ℕ} (f : Fin r → X → ℝ) (g : Fin s → X → ℝ) (hmeasF : Measurable (orderedProductKernel f)) (hmeasG : Measurable (orderedProductKernel g)) (hintF : Integrable (orderedProductKernel f) (Measure.pi fun _ : Fin r => P)) (hintG : Integrable (orderedProductKernel g) (Measure.pi fun _ : Fin s => P)) : mergedProductMoment P f g (PartialMatching.empty r s) = orderedProductMean P f * orderedProductMean P g := by classical let J := {j : Fin s // j ∉ (PartialMatching.empty r s).right} let e : J ≃ Fin s := Equiv.subtypeUnivEquiv (by intro j simp [J, PartialMatching.empty]) let split := MeasurableEquiv.sumPiEquivProdPi (fun _ : Fin r ⊕ J => X) let reindex := MeasurableEquiv.piCongrLeft (fun _ : Fin s => X) e have hsplit := measurePreserving_sumPiEquivProdPi (fun _ : Fin r ⊕ J => P) have hreindex : Measure.map reindex (Measure.pi fun _ : J => P) = Measure.pi fun _ : Fin s => P := by simpa [reindex] using (Measure.pi_map_piCongrLeft e (fun _ : Fin s => P)) let gJ : (J → X) → ℝ := fun z => ∏ j : Fin s, g j (z (e.symm j)) have hgJ : ∫ z, gJ z ∂(Measure.pi fun _ : J => P) = orderedProductMean P g := by unfold orderedProductMean rw [← hreindex, integral_map_equiv] rfl unfold mergedProductMoment change (∫ z, mergedProductKernel f g (PartialMatching.empty r s) z ∂(Measure.pi fun _ : Fin r ⊕ J => P)) = _ calc _ = ∫ z : (Fin r → X) × (J → X), orderedProductKernel f z.1 * gJ z.2 ∂((Measure.pi fun _ : Fin r => P).prod (Measure.pi fun _ : J => P)) := by rw [← hsplit.map_eq, integral_map_equiv] rfl _ = _ := by rw [integral_prod_mul, hgJ] rfl
CLT 2 core · 0 supporting This module states the asymptotic-normality interface for fixed-order U-statistics. ★ uStatisticOrder_clt★ uStatisticOrder_clt_of_regular
Fixed-order U-statistic CLTs
This module states the asymptotic-normality interface for fixed-order
U-statistics. uStatisticOrder_clt converts a centered, square-integrable
summed first projection and an explicit higher-order remainder-negligibility
hypothesis into the Gaussian limit of the √n-rescaled statistic.
The end-to-end theorem uStatisticOrder_clt_of_regular discharges the
negligibility hypothesis from regularity of the residual kernel via
orderDegenerateNegligible_of_residual. Together these declarations are the
public CLT endpoint for the OrderM U-statistic development.
theorem uStatisticOrder_clt reviewed
⚑ flagged
Causalean.Stat
Fixed-order U-statistic CLT. For an i.i.d. sample S and an order-m kernel h, write ψ for the summed coordinatewise first Hoeffding projection of h. If ψ is measurable, has population mean zero, and is square-integrable, if the higher-order Hájek remainder of the order-m U-statistic is negligible at the √n scale, and if the √n-rescaled U-statistic is almost-everywhere measurable at every sample size, then the √n-rescaled U-statistic converges in distribution to the centered Gaussian law with variance ∫ψ²dP.
Formal statement
hypotheses
S :
IIDSample Ω X μ P
m :
ℕ
NeZero m
h :
(Fin m → X) → ℝ
hψ_meas :
Measurable (uInfluenceOrder h P)
hψ_mean :
∫ x, uInfluenceOrder h P x ∂P = 0
hψ_sq :
Integrable (fun x => (uInfluenceOrder h P x) ^ 2) P
hneg :
hθn_meas :
∀ n : ℕ,
AEMeasurable (IsAsymLinear.rescaledEstimator (uStatisticOrder S h) (uMeanOrder h P) (fun r => range r) n) μ
conclusion
Tendsto_dist (IsAsymLinear.rescaledEstimator (uStatisticOrder S h) (uMeanOrder h P) (fun r => range r)) (gaussianMeasure 0 (∫ x, (uInfluenceOrder h P x) ^ 2 ∂P)) μ hθn_meas
Proof (Lean source)
theorem uStatisticOrder_clt (S : IIDSample Ω X μ P)
{m : ℕ} [NeZero m] (h : (Fin m → X) → ℝ)
(hψ_meas : Measurable (uInfluenceOrder h P))
(hψ_mean : ∫ x, uInfluenceOrder h P x ∂P = 0)
(hψ_sq : Integrable (fun x => (uInfluenceOrder h P x) ^ 2) P)
(hneg : OrderDegenerateNegligible S h)
(hθn_meas : ∀ n : ℕ, AEMeasurable
(IsAsymLinear.rescaledEstimator (uStatisticOrder S h) (uMeanOrder h P)
(fun r => range r) n) μ) :
Tendsto_dist
(IsAsymLinear.rescaledEstimator (uStatisticOrder S h) (uMeanOrder h P)
(fun r => range r))
(gaussianMeasure 0 (∫ x, (uInfluenceOrder h P x) ^ 2 ∂P))
μ
hθn_meas := by
have hAL : IsAsymLinear (uStatisticOrder S h) (uMeanOrder h P)
(uInfluenceOrder h P) S (fun r => range r) :=
uStatisticOrder_isAsymLinear S h hψ_mean hψ_sq hneg
exact hAL.tendsto_normal hψ_meas hθn_meas
theorem uStatisticOrder_clt_of_regular reviewed
⚑ flagged
Causalean.Stat
Fixed-order U-statistic CLT (end-to-end). For an i.i.d. sample S and an order-m kernel h, write g for the higher-order Hájek residual of h and ψ for the summed coordinatewise first Hoeffding projection of h. If the residual g is measurable and square-integrable under the m-fold product law, if for every coordinate integrating h over the remaining m − 1 coordinates yields an integrable function of that coordinate with the same population mean uMeanOrder h P in every coordinate and h remains integrable in the remaining coordinates for every fixed value of that coordinate, and if ψ is measurable, mean zero, square-integrable, and the √n-rescaled U-statistic is almost-everywhere measurable at every sample size, then the √n-rescaled order-m U-statistic converges in distribution to the centered Gaussian law with variance ∫ψ²dP.
Formal statement
hypotheses
Ω X :
S :
IIDSample Ω X μ P
m :
ℕ
NeZero m
h :
(Fin m → X) → ℝ
hmeas :
Measurable (uDegenOrder h P)
hL2 :
hslice_int :
∀ j : Fin m,
Integrable (fun x => ∫ tail : ({k : Fin m // k ≠ j}) → X, h (insertCoord j x tail) ∂(Measure.pi fun _ : {k : Fin m // k ≠ j} => P)) P
hmean :
∀ j : Fin m,
∫ x, (∫ tail : ({k : Fin m // k ≠ j}) → X, h (insertCoord j x tail) ∂(Measure.pi fun _ : {k : Fin m // k ≠ j} => P)) ∂P
= uMeanOrder h P
hrow :
∀ (j : Fin m) (x : X),
Integrable (fun tail : ({k : Fin m // k ≠ j}) → X => h (insertCoord j x tail)) (Measure.pi fun _ : {k : Fin m // k ≠ j} => P)
hψ_meas :
Measurable (uInfluenceOrder h P)
hψ_mean :
∫ x, uInfluenceOrder h P x ∂P = 0
hψ_sq :
Integrable (fun x => (uInfluenceOrder h P x) ^ 2) P
hθn_meas :
∀ n : ℕ,
AEMeasurable (IsAsymLinear.rescaledEstimator (uStatisticOrder S h) (uMeanOrder h P) (fun r => range r) n) μ
conclusion
Tendsto_dist (IsAsymLinear.rescaledEstimator (uStatisticOrder S h) (uMeanOrder h P) (fun r => range r)) (gaussianMeasure 0 (∫ x, (uInfluenceOrder h P x) ^ 2 ∂P)) μ hθn_meas
Proof (Lean source)
theorem uStatisticOrder_clt_of_regular
{Ω X : Type*} [MeasurableSpace Ω] [MeasurableSpace X]
{μ : Measure Ω} {P : Measure X} [IsProbabilityMeasure μ]
(S : IIDSample Ω X μ P) {m : ℕ} [NeZero m] (h : (Fin m → X) → ℝ)
(hmeas : Measurable (uDegenOrder h P))
(hL2 : Integrable (fun z => (uDegenOrder h P z) ^ 2)
(Measure.pi fun _ : Fin m => P))
(hslice_int : ∀ j : Fin m, Integrable
(fun x => ∫ tail : ({k : Fin m // k ≠ j}) → X,
h (insertCoord j x tail) ∂(Measure.pi fun _ : {k : Fin m // k ≠ j} => P)) P)
(hmean : ∀ j : Fin m,
∫ x, (∫ tail : ({k : Fin m // k ≠ j}) → X,
h (insertCoord j x tail) ∂(Measure.pi fun _ : {k : Fin m // k ≠ j} => P)) ∂P
= uMeanOrder h P)
(hrow : ∀ (j : Fin m) (x : X),
Integrable (fun tail : ({k : Fin m // k ≠ j}) → X =>
h (insertCoord j x tail))
(Measure.pi fun _ : {k : Fin m // k ≠ j} => P))
(hψ_meas : Measurable (uInfluenceOrder h P))
(hψ_mean : ∫ x, uInfluenceOrder h P x ∂P = 0)
(hψ_sq : Integrable (fun x => (uInfluenceOrder h P x) ^ 2) P)
(hθn_meas : ∀ n : ℕ, AEMeasurable
(IsAsymLinear.rescaledEstimator (uStatisticOrder S h) (uMeanOrder h P)
(fun r => range r) n) μ) :
Tendsto_dist
(IsAsymLinear.rescaledEstimator (uStatisticOrder S h) (uMeanOrder h P)
(fun r => range r))
(gaussianMeasure 0 (∫ x, (uInfluenceOrder h P x) ^ 2 ∂P))
μ
hθn_meas := by
letI : IsProbabilityMeasure P := by
rw [← S.law]
exact Measure.isProbabilityMeasure_map (S.meas 0).aemeasurable
have hneg : OrderDegenerateNegligible S h :=
orderDegenerateNegligible_of_residual S h hmeas hL2 hslice_int hmean hrow
exact uStatisticOrder_clt S h hψ_meas hψ_mean hψ_sq hneg hθn_meas
ExactVariance 3 core · 3 supporting This module proves the exact second-moment calculation for a completely degenerate fixed-order kernel. ★ integral_injectiveTuples_sum_sq_degen★ integral_rescaled_order_sq_degen
Exact variance for completely degenerate fixed-order U-statistics
This module proves the exact second-moment calculation for a completely
degenerate fixed-order kernel. The cross-term lemmas
IIDSample.crossterm_eq_zeta_of_image_eq and
IIDSample.crossterm_eq_zero_of_image_ne classify pairs of injective tuples by
whether their images agree; card_injectiveTuples_image_eq counts the
same-image reorderings.
The headline variance identities are
IIDSample.integral_injectiveTuples_sum_sq_degen for the raw injective-tuple
sum and IIDSample.integral_rescaled_order_sq_degen for the √n-rescaled
degenerate U-statistic. These sharpen the general rate bound to an exact
formula in the completely degenerate case.
def permOfImageEq reviewed
⚑ flagged
Causalean.Stat.IIDSample
Two injective maps from a finite index set with the same image determine a permutation of that index set which reorders the first map into the second.
Definition (Lean source)
noncomputable def permOfImageEq {n : ℕ} {t q : Fin m → Fin n}
(ht : Injective t) (hq : Injective q)
(himg : Finset.univ.image t = Finset.univ.image q) : Perm (Fin m) := by
classical
let f : Fin m → Fin m := fun j =>
choose ((Finset.mem_image.mp (by
have hqmem : q j ∈ Finset.univ.image q :=
Finset.mem_image.mpr ⟨j, Finset.mem_univ j, rfl⟩
simp [himg])) : ∃ i, i ∈ univ ∧ t i = q j)
let r : Fin m → Fin m := fun i =>
choose ((Finset.mem_image.mp (by
have htmem : t i ∈ Finset.univ.image t :=
Finset.mem_image.mpr ⟨i, Finset.mem_univ i, rfl⟩
simp [← himg])) : ∃ j, j ∈ univ ∧ q j = t i)
have hf : ∀ j, t (f j) = q j := by
intro j
exact (Classical.choose_spec ((Finset.mem_image.mp (by
have hqmem : q j ∈ Finset.univ.image q :=
Finset.mem_image.mpr ⟨j, Finset.mem_univ j, rfl⟩
simp [himg])) : ∃ i, i ∈ univ ∧ t i = q j)).2
have hr : ∀ i, q (r i) = t i := by
intro i
exact (Classical.choose_spec ((Finset.mem_image.mp (by
have htmem : t i ∈ Finset.univ.image t :=
Finset.mem_image.mpr ⟨i, Finset.mem_univ i, rfl⟩
simp [← himg])) : ∃ j, j ∈ univ ∧ q j = t i)).2
exact
{ toFun := f
invFun := r
left_inv := by
intro j
apply hq
rw [hr (f j), hf j]
right_inv := by
intro i
apply ht
rw [hf (r i), hr i] }
theorem integral_injectiveTuples_sum_sq_degen reviewed
⚑ flagged
Causalean.Stat.IIDSample
Exact second moment of the injective-tuple sum. For an i.i.d. sample S and sample size n, if the order-m kernel g is completely degenerate: symmetric, square-integrable, and with zero conditional mean after integrating out any single coordinate, then the second moment of the sum of g over all ordered injective m-tuples drawn from the first n sample indices equals m! · n^{(m)} · ζ_m, where n^{(m)} is the number of such tuples and ζ_m is the kernel's second moment under the m-fold product law.
Formal statement
hypotheses
hg :
OrderDegenKernel P g
n :
ℕ
conclusion
∫ ω, (∑ t ∈ injectiveTuples m n, g (fun j => S.Z (t j : ℕ) ω)) ^ 2 ∂μ
= (m.factorial : ℝ) * injectiveTupleCount m n * zetaOrder P g
Proof (Lean source)
theorem integral_injectiveTuples_sum_sq_degen
(hg : OrderDegenKernel P g) (n : ℕ) :
∫ ω, (∑ t ∈ injectiveTuples m n, g (fun j => S.Z (t j : ℕ) ω)) ^ 2 ∂μ
= (m.factorial : ℝ) * injectiveTupleCount m n * zetaOrder P g := by
letI : IsProbabilityMeasure μ := ⟨by
calc
μ univ = μ (S.Z 0 ⁻¹' univ) := by simp
_ = (μ.map (S.Z 0)) univ := (Measure.map_apply (S.meas 0) MeasurableSet.univ).symm
_ = P univ := by rw [S.law]
_ = 1 := measure_univ⟩
letI : IsProbabilityMeasure P := by
rw [← S.law]
exact Measure.isProbabilityMeasure_map (S.meas 0).aemeasurable
classical
let T : Finset (Fin m → Fin n) := injectiveTuples m n
let F : (Fin m → Fin n) → (Fin m → Fin n) → ℝ := fun t q =>
∫ ω, g (fun j => S.Z (t j : ℕ) ω) *
g (fun j => S.Z (q j : ℕ) ω) ∂μ
have hinj_of_mem_T : ∀ t ∈ T, Injective t := by
intro t ht
have ht' : t ∈ injectiveTuples m n := by simpa [T] using ht
exact (Finset.mem_filter.mp ht').2
have hexpand :
(fun ω => (∑ t ∈ T, g (fun j => S.Z (t j : ℕ) ω)) ^ 2)
= (fun ω => ∑ t ∈ T, ∑ q ∈ T,
g (fun j => S.Z (t j : ℕ) ω) * g (fun j => S.Z (q j : ℕ) ω)) := by
funext ω
rw [sq, Finset.sum_mul_sum]
rw [show (∫ ω, (∑ t ∈ injectiveTuples m n,
g (fun j => S.Z (t j : ℕ) ω)) ^ 2 ∂μ)
= ∫ ω, (∑ t ∈ T, g (fun j => S.Z (t j : ℕ) ω)) ^ 2 ∂μ by rfl]
rw [hexpand]
rw [integral_finset_sum _ (fun t ht => by
apply integrable_finset_sum
intro q hq
exact S.integrable_orderTerm_mul hg.meas hg.sq
(hinj_of_mem_T t ht) (hinj_of_mem_T q hq))]
have hpush : ∀ t ∈ T,
∫ ω, ∑ q ∈ T,
g (fun j => S.Z (t j : ℕ) ω) * g (fun j => S.Z (q j : ℕ) ω) ∂μ
= ∑ q ∈ T, F t q := by
intro t ht
exact integral_finset_sum _ (fun q hq =>
S.integrable_orderTerm_mul hg.meas hg.sq
(hinj_of_mem_T t ht) (hinj_of_mem_T q hq))
rw [Finset.sum_congr rfl hpush]
have hinner : ∀ t ∈ T, ∑ q ∈ T, F t q = (m.factorial : ℝ) * zetaOrder P g := by
intro t ht
let SAME : Finset (Fin m → Fin n) :=
T.filter (fun q => Finset.univ.image q = Finset.univ.image t)
have hsub : SAME ⊆ T := Finset.filter_subset _ _
have hzero : ∀ q ∈ T, q ∉ SAME → F t q = 0 := by
intro q hq hqnot
have htinj := hinj_of_mem_T t ht
have hqinj := hinj_of_mem_T q hq
have hne : Finset.univ.image t ≠ Finset.univ.image q := by
intro h
exact hqnot (Finset.mem_filter.mpr ⟨hq, h.symm⟩)
simpa [F] using S.crossterm_eq_zero_of_image_ne hg.meas hg.sq hg.deg htinj hqinj hne
rw [← Finset.sum_subset hsub hzero]
have hsame : ∀ q ∈ SAME, F t q = zetaOrder P g := by
intro q hq
have htinj := hinj_of_mem_T t ht
have hqT : q ∈ T := (Finset.mem_filter.mp hq).1
have hqinj := hinj_of_mem_T q hqT
have himg : Finset.univ.image t = Finset.univ.image q :=
(Finset.mem_filter.mp hq).2.symm
simpa [F] using S.crossterm_eq_zeta_of_image_eq hg.meas hg.symm htinj hqinj himg
rw [Finset.sum_congr rfl hsame]
rw [Finset.sum_const, nsmul_eq_mul]
have htinj := hinj_of_mem_T t ht
have hcard : SAME.card = m.factorial := by
simpa [SAME, T] using card_injectiveTuples_image_eq (m := m) (n := n) htinj
rw [hcard]
rw [Finset.sum_congr rfl hinner]
rw [Finset.sum_const, nsmul_eq_mul]
simp only [T, injectiveTupleCount]
ring
theorem integral_rescaled_order_sq_degen reviewed
⚑ flagged
Causalean.Stat.IIDSample
Exact variance of the rescaled degenerate fixed-order U-statistic. For an i.i.d. sample S, if the order-m kernel g is completely degenerate and the sample size is at least m, then the second moment of the √n-rescaled order-m U-statistic of g equals n · m! · ζ_m / n^{(m)}, which specializes to 2ζ/(n−1) when m = 2.
Formal statement
hypotheses
conclusion
∫ ω, (sqrt (n : ℝ) * uStatisticOrder S g n ω) ^ 2 ∂μ
= (n : ℝ) * (m.factorial : ℝ) * zetaOrder P g / injectiveTupleCount m n
Proof (Lean source)
theorem integral_rescaled_order_sq_degen (hg : OrderDegenKernel P g)
{n : ℕ} (hmn : m ≤ n) :
∫ ω, (sqrt (n : ℝ) * uStatisticOrder S g n ω) ^ 2 ∂μ
= (n : ℝ) * (m.factorial : ℝ) * zetaOrder P g / injectiveTupleCount m n := by
letI : IsProbabilityMeasure μ := ⟨by
calc
μ univ = μ (S.Z 0 ⁻¹' univ) := by simp
_ = (μ.map (S.Z 0)) univ := (Measure.map_apply (S.meas 0) MeasurableSet.univ).symm
_ = P univ := by rw [S.law]
_ = 1 := measure_univ⟩
letI : IsProbabilityMeasure P := by
rw [← S.law]
exact Measure.isProbabilityMeasure_map (S.meas 0).aemeasurable
classical
let K : Ω → ℝ := fun ω => ∑ t ∈ injectiveTuples m n,
g (fun j => S.Z (t j : ℕ) ω)
have hcount_ne : injectiveTupleCount m n ≠ 0 := injectiveTupleCount_ne_zero hmn
have hnnonneg : 0 ≤ (n : ℝ) := by positivity
have hpoint :
(fun ω => (sqrt (n : ℝ) * uStatisticOrder S g n ω) ^ 2)
=
(fun ω => ((n : ℝ) * (injectiveTupleCount m n)⁻¹ ^ 2) * (K ω) ^ 2) := by
funext ω
simp only [uStatisticOrder, K]
rw [mul_pow, Real.sq_sqrt hnnonneg]
ring
rw [hpoint, integral_const_mul]
rw [show (∫ ω, (K ω) ^ 2 ∂μ)
= ∫ ω, (∑ t ∈ injectiveTuples m n,
g (fun j => S.Z (t j : ℕ) ω)) ^ 2 ∂μ by rfl]
rw [S.integral_injectiveTuples_sum_sq_degen hg n]
field_simp [hcount_ne]
3 supporting declarations (lemmas, instances)
-
crossterm_eq_zeta_of_image_eqtheorem — Equal-image cross term. If two ordered injective m-tuples have the same image, then q is a reordering of t, so by symmetry g(Z_q) = g(Z_t) and the cross expectation is ζ_m = zetaOrder P g.hypotheseshmeas :ht :hq :himg :Finset.univ.image t = Finset.univ.image qconclusion∫ ω, g (fun j => S.Z (t j : ℕ) ω) * g (fun j => S.Z (q j : ℕ) ω) ∂μ = zetaOrder P gProof (Lean source)
theorem crossterm_eq_zeta_of_image_eq (hmeas : Measurable g) (hsymm : ∀ σ : Perm (Fin m), ∀ z, g (z ∘ σ) = g z) {n : ℕ} {t q : Fin m → Fin n} (ht : Injective t) (hq : Injective q) (himg : Finset.univ.image t = Finset.univ.image q) : ∫ ω, g (fun j => S.Z (t j : ℕ) ω) * g (fun j => S.Z (q j : ℕ) ω) ∂μ = zetaOrder P g := by classical let σ : Perm (Fin m) := permOfImageEq (m := m) ht hq himg have hq_rewrite : ∀ ω, (fun j => S.Z (q j : ℕ) ω) = (fun j => S.Z (t j : ℕ) ω) ∘ σ := by intro ω funext j rw [Function.comp_apply] have hσ := permOfImageEq_apply (m := m) ht hq himg j rw [← hσ] have hcongr : (fun ω => g (fun j => S.Z (t j : ℕ) ω) * g (fun j => S.Z (q j : ℕ) ω)) = (fun ω => (g (fun j => S.Z (t j : ℕ) ω)) ^ 2) := by funext ω rw [hq_rewrite ω, hsymm σ] ring rw [hcongr] rw [zetaOrder, ← S.map_tuple_eq ht] rw [integral_map (measurable_pi_lambda _ (fun j : Fin m => S.meas (t j : ℕ))).aemeasurable (hmeas.pow_const 2).aestronglyMeasurable] -
crossterm_eq_zero_of_image_netheorem — Distinct-image cross term. If two ordered injective m-tuples have different images, complete degeneracy kills the cross expectation: some index of t is absent from q, and integrating that coordinate out gives 0.hypotheseshmeas :hsq :Integrable (fun z => (g z) ^ 2) (Measure.pi fun _ : Fin m => P)hdeg :ht :hq :himg :Finset.univ.image t ≠ Finset.univ.image qconclusion∫ ω, g (fun j => S.Z (t j : ℕ) ω) * g (fun j => S.Z (q j : ℕ) ω) ∂μ = 0Proof (Lean source)
theorem crossterm_eq_zero_of_image_ne (hmeas : Measurable g) (hsq : Integrable (fun z => (g z) ^ 2) (Measure.pi fun _ : Fin m => P)) (hdeg : ∀ (j : Fin m) (tail : ({k : Fin m // k ≠ j}) → X), ∫ x, g (insertCoord j x tail) ∂P = 0) {n : ℕ} {t q : Fin m → Fin n} (ht : Injective t) (hq : Injective q) (himg : Finset.univ.image t ≠ Finset.univ.image q) : ∫ ω, g (fun j => S.Z (t j : ℕ) ω) * g (fun j => S.Z (q j : ℕ) ω) ∂μ = 0 := by letI : IsProbabilityMeasure μ := ⟨by calc μ univ = μ (S.Z 0 ⁻¹' univ) := by simp _ = (μ.map (S.Z 0)) univ := (Measure.map_apply (S.meas 0) MeasurableSet.univ).symm _ = P univ := by rw [S.law] _ = 1 := measure_univ⟩ classical let A : Finset (Fin n) := Finset.univ.image t let B : Finset (Fin n) := Finset.univ.image q have hAcard : A.card = m := by simpa [A] using (Finset.card_image_of_injective (s := (Finset.univ : Finset (Fin m))) ht) have hBcard : B.card = m := by simpa [B] using (Finset.card_image_of_injective (s := (Finset.univ : Finset (Fin m))) hq) have hnot_subset : ¬ A ⊆ B := by intro hsub apply himg have hcard_le : B.card ≤ A.card := by rw [hAcard, hBcard] simpa [A, B] using (Finset.eq_of_subset_of_card_le hsub hcard_le) rcases Finset.not_subset.mp hnot_subset with ⟨a, haA, haB⟩ rcases Finset.mem_image.mp haA with ⟨p, _hp, htp⟩ subst a let R : Finset (Fin n) := (A ∪ B).erase (t p) let XR : Ω → (R → X) := fun ω i => S.Z (i.1 : ℕ) ω let πR : Measure (R → X) := Measure.pi fun _ : R => P let tailOf : (R → X) → ({k : Fin m // k ≠ p} → X) := fun xr k => xr ⟨t k.1, by have hmemA : t k.1 ∈ A := Finset.mem_image.mpr ⟨k.1, Finset.mem_univ k.1, rfl⟩ have hne : t k.1 ≠ t p := fun h => k.2 (ht h) simp [R, hmemA, hne]⟩ let Ψ : (R → X) → ℝ := fun xr => g (fun j => xr ⟨q j, by have hmemB : q j ∈ B := Finset.mem_image.mpr ⟨j, Finset.mem_univ j, rfl⟩ have hne : q j ≠ t p := by intro h exact haB (by simpa [B, h] using hmemB) simp [R, hmemB, hne]⟩) let F : X × (R → X) → ℝ := fun z => g (insertCoord p z.1 (tailOf z.2)) * Ψ z.2 have hXRmeas : Measurable XR := by exact measurable_pi_lambda _ (fun i : R => S.meas (i.1 : ℕ)) have hX0meas : Measurable (fun ω : Ω => S.Z (t p : ℕ) ω) := S.meas (t p : ℕ) have hPairMeas : Measurable (fun ω : Ω => (S.Z (t p : ℕ) ω, XR ω)) := hX0meas.prodMk hXRmeas have hXRmap : μ.map XR = πR := by have hr : Injective (fun i : R => i.1) := by intro i j hij exact Subtype.ext hij simpa [XR, πR, R] using (S.map_fintype_tuple_eq (ι := R) (r := fun i : R => i.1) hr) have hdisj : Disjoint ({t p} : Finset (Fin n)) R := by rw [Finset.disjoint_iff_inter_eq_empty] ext x constructor · intro hx rcases Finset.mem_inter.mp hx with ⟨hx0, hxR⟩ have hxeq : x = t p := by simpa using hx0 subst x simp [R] at hxR · intro hx simp at hx have hindFin : iIndepFun (fun i : Fin n => S.Z (i : ℕ)) μ := S.indep.precomp (fun _ _ h => Fin.ext h) have hindBlocks : IndepFun (fun ω : Ω => fun i : ({t p} : Finset (Fin n)) => S.Z (i.1 : ℕ) ω) XR μ := by simpa [XR] using (ProbabilityTheory.iIndepFun.indepFun_finset ({t p} : Finset (Fin n)) R hdisj hindFin (fun i : Fin n => S.meas (i : ℕ))) have hEval : Measurable (fun x : ({t p} : Finset (Fin n)) → X => x ⟨t p, by simp⟩) := measurable_pi_apply _ have hind : IndepFun (fun ω : Ω => S.Z (t p : ℕ) ω) XR μ := by have hcomp := hindBlocks.comp hEval measurable_id simpa [Function.comp_def] using hcomp have hΦ : Measurable (fun z : X × (R → X) => g (insertCoord p z.1 (tailOf z.2))) := by exact hmeas.comp (measurable_pi_lambda _ (fun j : Fin m => by by_cases hj : j = p · subst j simpa [insertCoord] using measurable_fst · simpa [tailOf, insertCoord, hj, Function.comp_def] using (measurable_pi_apply (⟨t j, by have hmemA : t j ∈ A := Finset.mem_image.mpr ⟨j, Finset.mem_univ j, rfl⟩ have hne : t j ≠ t p := fun h => hj (ht h) simp [R, hmemA, hne]⟩ : R)).comp measurable_snd)) have hΨ : Measurable Ψ := by exact hmeas.comp (measurable_pi_lambda _ (fun j : Fin m => measurable_pi_apply _)) have hFmeas : Measurable F := hΦ.mul (hΨ.comp measurable_snd) have ht_rewrite : ∀ ω, g (fun j => S.Z (t j : ℕ) ω) = g (insertCoord p (S.Z (t p : ℕ) ω) (tailOf (XR ω))) := by intro ω congr 1 funext j by_cases hj : j = p · subst j simp [insertCoord] · simp [tailOf, XR, insertCoord, hj] have hq_rewrite : ∀ ω, g (fun j => S.Z (q j : ℕ) ω) = Ψ (XR ω) := by intro ω rfl have hcomp_int : Integrable (fun ω => F (S.Z (t p : ℕ) ω, XR ω)) μ := by have hterm_mem : ∀ {r : Fin m → Fin n}, Injective r → MemLp (fun ω => g (fun j => S.Z (r j : ℕ) ω)) 2 μ := by intro r hr have hm : AEStronglyMeasurable (fun ω => g (fun j => S.Z (r j : ℕ) ω)) μ := (hmeas.comp (measurable_pi_lambda _ (fun j : Fin m => S.meas (r j : ℕ)))).aestronglyMeasurable apply (memLp_two_iff_integrable_sq hm).mpr have hmap : Integrable (fun z => (g z) ^ 2) (μ.map (fun ω : Ω => fun j : Fin m => S.Z (r j : ℕ) ω)) := by rw [S.map_tuple_eq hr] exact hsq exact (integrable_map_measure (hmeas.pow_const 2).aestronglyMeasurable (measurable_pi_lambda _ (fun j : Fin m => S.meas (r j : ℕ))).aemeasurable).mp hmap have horig := (hterm_mem ht).integrable_mul (hterm_mem hq) refine horig.congr ?_ filter_upwards with ω simp [F, ht_rewrite ω, hq_rewrite ω] have hmap_pair : μ.map (fun ω : Ω => (S.Z (t p : ℕ) ω, XR ω)) = P.prod (μ.map XR) := by have h := (indepFun_iff_map_prod_eq_prod_map_map hX0meas.aemeasurable hXRmeas.aemeasurable).mp hind simpa [S.map_eq (t p : ℕ)] using h have hFint_map : Integrable F (P.prod (μ.map XR)) := by have hmap_int : Integrable F (μ.map fun ω : Ω => (S.Z (t p : ℕ) ω, XR ω)) := (integrable_map_measure hFmeas.aestronglyMeasurable hPairMeas.aemeasurable).mpr hcomp_int simpa [hmap_pair] using hmap_int have hinner : ∀ xr : R → X, (∫ x : X, F (x, xr) ∂P) = 0 := by intro xr change (∫ x : X, g (insertCoord p x (tailOf xr)) * Ψ xr ∂P) = 0 rw [integral_mul_const, hdeg p (tailOf xr), zero_mul] calc ∫ ω, g (fun j => S.Z (t j : ℕ) ω) * g (fun j => S.Z (q j : ℕ) ω) ∂μ = ∫ ω, F (S.Z (t p : ℕ) ω, XR ω) ∂μ := by apply integral_congr_ae filter_upwards with ω simp [F, ht_rewrite ω, hq_rewrite ω] _ = ∫ z, F z ∂(μ.map fun ω : Ω => (S.Z (t p : ℕ) ω, XR ω)) := by rw [integral_map hPairMeas.aemeasurable hFmeas.aestronglyMeasurable] _ = ∫ z, F z ∂(P.prod (μ.map XR)) := by rw [hmap_pair] _ = ∫ xr, ∫ x, F (x, xr) ∂P ∂(μ.map XR) := by rw [integral_prod_symm F hFint_map] _ = 0 := by rw [show (fun xr : R → X => ∫ x, F (x, xr) ∂P) = fun _ => 0 by funext xr exact hinner xr] simp -
card_injectiveTuples_image_eqtheorem — For an ordered injective m-tuple t, the ordered injective tuples with the same image are exactly its m! reorderings.hypothesesconclusion((injectiveTuples m n).filter (fun q => Finset.univ.image q = Finset.univ.image t)).card= m.factorialProof (Lean source)
theorem card_injectiveTuples_image_eq {n : ℕ} {t : Fin m → Fin n} (ht : Injective t) : ((injectiveTuples m n).filter (fun q => Finset.univ.image q = Finset.univ.image t)).card = m.factorial := by classical have hcard_perm : (Finset.univ : Finset (Perm (Fin m))).card = m.factorial := by rw [Finset.card_univ, Fintype.card_perm, Fintype.card_fin] rw [← hcard_perm] symm refine Finset.card_bij (fun σ _ => t ∘ σ) ?hmem ?hinj ?hsurj · intro σ _hσ rw [mem_filter] refine ⟨?_, ?_⟩ · simp [injectiveTuples, ht.comp σ.injective] · ext x constructor · intro hx rcases Finset.mem_image.mp hx with ⟨j, _hj, hjx⟩ exact Finset.mem_image.mpr ⟨σ j, Finset.mem_univ _, hjx⟩ · intro hx rcases Finset.mem_image.mp hx with ⟨j, _hj, hjx⟩ exact Finset.mem_image.mpr ⟨σ.symm j, Finset.mem_univ _, by simp [comp, hjx]⟩ · intro σ₁ _ σ₂ _ hσ ext j exact congrArg val (ht (congrFun hσ j)) · intro q hq rw [mem_filter] at hq have hqinj : Injective q := by simpa [injectiveTuples] using hq.1 let σ : Perm (Fin m) := permOfImageEq (m := m) ht hqinj hq.2.symm refine ⟨σ, Finset.mem_univ σ, ?_⟩ funext j exact permOfImageEq_apply (m := m) ht hqinj hq.2.symm j
MixedOrderBounds 1 core · 3 supporting 1 to review This module supplies uniform bounds for overlap normalizations and for the size-zero disjoint correction. ★ factorialMatchingRatio_le
Mixed-order falling-factorial normalization bounds
This module supplies uniform bounds for overlap normalizations and for the
size-zero disjoint correction. The statements are symmetric in the two orders
and depend only on a common upper bound R.
theorem factorialMatchingRatio_le unreviewed
⚑ flagged
Causalean.Stat
For sample size n, orders r and s, common order bound R, and overlap size h, if the first order is at most R, the second order is at most R, the sample size is at least four times R squared, and the overlap fits inside both orders, the mixed falling-factorial ratio is at most exp(1) divided by n to the overlap size.
Formal statement
Proof (Lean source)
theorem factorialMatchingRatio_le {n r s R h : ℕ}
(hr : r ≤ R) (hs : s ≤ R) (hn : 4 * R ^ 2 ≤ n) (hh : h ≤ min r s) :
(n.descFactorial (r + s - h) : ℝ) /
((n.descFactorial r : ℝ) * (n.descFactorial s : ℝ)) ≤
exp 1 / (n : ℝ) ^ h := by
rcases le_total r s with hrs | hsr
· exact orderedFactorialMatchingRatio_le hrs (by nlinarith) (hh.trans (min_le_right _ _))
· simpa [Nat.add_comm, mul_comm] using
(orderedFactorialMatchingRatio_le hsr (by nlinarith)
(hh.trans (min_le_left _ _)))
3 supporting declarations (lemmas, instances)
-
matchingNormalization_letheorem — For sample size n, orders r and s, common order bound R, and overlap size h, a partial matching has normalization at most exp(1) divided by n to the overlap size when the first order is at most R, the second order is at most R, the sample size is at least four times R squared, and the matching has size h as claimed.hypothesesn r s R h :ℕPartialMatching r shr :r ≤ Rhs :s ≤ Rhn :4 * R ^ 2 ≤ nhM :M ∈ partialMatchingsOfSize r s hconclusionmatchingNormalization n M ≤ exp 1 / (n : ℝ) ^ hProof (Lean source)
theorem matchingNormalization_le {n r s R h : ℕ} {M : PartialMatching r s} (hr : r ≤ R) (hs : s ≤ R) (hn : 4 * R ^ 2 ≤ n) (hM : M ∈ partialMatchingsOfSize r s h) : matchingNormalization n M ≤ exp 1 / (n : ℝ) ^ h := by have hh : h ≤ min r s := by simpa [(mem_partialMatchingsOfSize M).mp hM] using M.size_le_min rw [matchingNormalization_of_mem hM] exact factorialMatchingRatio_le hr hs hn hh -
factorialDisjointCorrection_letheorem — For sample size n, orders r and s, and common order bound R, if the first order is at most R, the second order is at most R, and the sample size is at least four times R squared, the absolute disjoint normalization correction is at most twice R squared divided by n.hypothesesn r s R :ℕhr :r ≤ Rhs :s ≤ Rhn :4 * R ^ 2 ≤ nconclusion|(n.descFactorial (r + s) : ℝ) / ((n.descFactorial r : ℝ) * (n.descFactorial s : ℝ)) - 1|≤ 2 * (R : ℝ) ^ 2 / nProof (Lean source)
theorem factorialDisjointCorrection_le {n r s R : ℕ} (hr : r ≤ R) (hs : s ≤ R) (hn : 4 * R ^ 2 ≤ n) : |(n.descFactorial (r + s) : ℝ) / ((n.descFactorial r : ℝ) * (n.descFactorial s : ℝ)) - 1| ≤ 2 * (R : ℝ) ^ 2 / n := by rcases le_total r s with hrs | hsr · calc |(n.descFactorial (r + s) : ℝ) / ((n.descFactorial r : ℝ) * (n.descFactorial s : ℝ)) - 1| ≤ 2 * (s : ℝ) ^ 2 / n := orderedFactorialDisjointCorrection_le hrs (by nlinarith) _ ≤ 2 * (R : ℝ) ^ 2 / n := by have hnum : 2 * s ^ 2 ≤ 2 * R ^ 2 := Nat.mul_le_mul_left 2 (Nat.pow_le_pow_left hs 2) apply div_le_div_of_nonneg_right (by exact_mod_cast hnum) (by positivity) · calc |(n.descFactorial (r + s) : ℝ) / ((n.descFactorial r : ℝ) * (n.descFactorial s : ℝ)) - 1| = |(n.descFactorial (s + r) : ℝ) / ((n.descFactorial s : ℝ) * (n.descFactorial r : ℝ)) - 1| := by simp [Nat.add_comm, mul_comm] _ ≤ 2 * (r : ℝ) ^ 2 / n := orderedFactorialDisjointCorrection_le hsr (by nlinarith) _ ≤ 2 * (R : ℝ) ^ 2 / n := by have hnum : 2 * r ^ 2 ≤ 2 * R ^ 2 := Nat.mul_le_mul_left 2 (Nat.pow_le_pow_left hr 2) apply div_le_div_of_nonneg_right (by exact_mod_cast hnum) (by positivity) -
emptyMatchingNormalization_sub_one_letheorem — For sample size n, orders r and s, and common order bound R, if the first order is at most R, the second order is at most R, and the sample size is at least four times R squared, the empty partial matching's normalization differs from one by at most twice R squared divided by n.hypothesesn r s R :ℕhr :r ≤ Rhs :s ≤ Rhn :4 * R ^ 2 ≤ nconclusion|matchingNormalization n (PartialMatching.empty r s) - 1| ≤ 2 * (R : ℝ) ^ 2 / nProof (Lean source)
theorem emptyMatchingNormalization_sub_one_le {n r s R : ℕ} (hr : r ≤ R) (hs : s ≤ R) (hn : 4 * R ^ 2 ≤ n) : |matchingNormalization n (PartialMatching.empty r s) - 1| ≤ 2 * (R : ℝ) ^ 2 / n := by rw [matchingNormalization] simp only [PartialMatching.empty_size, Nat.sub_zero] exact factorialDisjointCorrection_le hr hs hn
OrderTwo 1 core · 4 supporting Specializes the fixed-order U-statistic CLT to the order-2 theory. ★ uStatistic_clt_of_symmetric_via_orderM
Specializes the fixed-order U-statistic CLT to the order-2 theory.
The bridge sends a two-argument kernel h : X → X → ℝ to `pairKernel h :
(Fin 2 → X) → ℝ and proves that the order-m` mean, projections, influence
function, degenerate residual, and statistic agree with their order-2
counterparts. The final theorem, uStatistic_clt_of_symmetric_via_orderM,
derives the classical symmetric-kernel order-2 CLT from
uStatisticOrder_clt_of_regular.
theorem uStatistic_clt_of_symmetric_via_orderM reviewed
⚑ flagged
Causalean.Stat
Order-2 U-statistic CLT, derived from the fixed-order-m CLT. For an i.i.d. sample S and a two-argument kernel h : X → X → ℝ that is symmetric and jointly measurable, suppose the order-2 Hájek residual of h is square-integrable under the product law P × P, the row integral x ↦ ∫h(x,y)dP(y) is integrable and each row y ↦ h(x,y) is itself integrable for every x, the first Hoeffding projection of h is square-integrable, and the √n-rescaled U-statistic is almost-everywhere measurable at every sample size. Then the √n-rescaled order-2 U-statistic converges in distribution to the centered Gaussian law with variance 4ζ₁, where ζ₁ is the variance of the first Hoeffding projection.
Formal statement
hypotheses
Ω X :
S :
IIDSample Ω X μ P
h :
X → X → ℝ
hsymm :
∀ x y, h x y = h y x
hmeas :
Measurable fun p : X × X => h p.1 p.2
hL2 :
Integrable (fun p : X × X => (uDegen h P p.1 p.2) ^ 2) (P.prod P)
hint :
Integrable (fun x => ∫ y, h x y ∂P) P
hrow :
∀ x, Integrable (fun y => h x y) P
hproj_sq :
Integrable (fun x => (uProj h P x) ^ 2) P
hθn_meas :
∀ n : ℕ,
conclusion
letI : IsProbabilityMeasure μ
Proof (Lean source)
theorem uStatistic_clt_of_symmetric_via_orderM
{Ω X : Type*} [MeasurableSpace Ω] [MeasurableSpace X]
{μ : Measure Ω} {P : Measure X}
(S : IIDSample Ω X μ P) (h : X → X → ℝ)
(hsymm : ∀ x y, h x y = h y x)
(hmeas : Measurable fun p : X × X => h p.1 p.2)
(hL2 : Integrable (fun p : X × X => (uDegen h P p.1 p.2) ^ 2) (P.prod P))
(hint : Integrable (fun x => ∫ y, h x y ∂P) P)
(hrow : ∀ x, Integrable (fun y => h x y) P)
(hproj_sq : Integrable (fun x => (uProj h P x) ^ 2) P)
(hθn_meas : ∀ n : ℕ, AEMeasurable
(IsAsymLinear.rescaledEstimator (uStatistic S h) (uMean h P)
(fun m => range m) n) μ) :
letI : IsProbabilityMeasure μ := S.indep.isProbabilityMeasure
Tendsto_dist
(IsAsymLinear.rescaledEstimator (uStatistic S h) (uMean h P)
(fun m => range m))
(gaussianMeasure 0 (∫ x, ((fun x => 2 * uProj h P x) x) ^ 2 ∂P))
μ
hθn_meas := by
letI : IsProbabilityMeasure μ := S.indep.isProbabilityMeasure
letI : IsProbabilityMeasure P := by
rw [← S.law]
exact Measure.isProbabilityMeasure_map (S.meas 0).aemeasurable
let e := MeasurableEquiv.piFinTwo (fun _ : Fin 2 => X)
have hmp : MeasurePreserving e
(Measure.pi fun _ : Fin 2 => P) (P.prod P) := by
simpa [e] using (measurePreserving_piFinTwo (fun _ : Fin 2 => P))
have hproj_meas : Measurable (uProj h P) := by
have hsm : StronglyMeasurable fun x => ∫ y, h x y ∂P :=
hmeas.stronglyMeasurable.integral_prod_right'
exact hsm.measurable.sub measurable_const
have hdeg_meas_prod : Measurable (fun p : X × X => uDegen h P p.1 p.2) := by
have h1 : Measurable fun p : X × X => uProj h P p.1 := hproj_meas.comp measurable_fst
have h2 : Measurable fun p : X × X => uProj h P p.2 := hproj_meas.comp measurable_snd
simp only [uDegen]
exact ((hmeas.sub measurable_const).sub h1).sub h2
have hproj_int : Integrable (uProj h P) P := uProj_integrable hint
have hdegen_int : Integrable (fun p : X × X => uDegen h P p.1 p.2) (P.prod P) :=
((memLp_two_iff_integrable_sq hdeg_meas_prod.aestronglyMeasurable).mpr hL2).integrable
(by norm_num)
have hh_int : Integrable (fun p : X × X => h p.1 p.2) (P.prod P) := by
have hsum_int : Integrable
(fun p : X × X =>
uMean h P + uProj h P p.1 + uProj h P p.2 + uDegen h P p.1 p.2)
(P.prod P) := by
have hfst : Integrable (fun p : X × X => uProj h P p.1) (P.prod P) :=
hproj_int.comp_fst P
have hsnd : Integrable (fun p : X × X => uProj h P p.2) (P.prod P) :=
hproj_int.comp_snd P
exact (((integrable_const (uMean h P)).add hfst).add hsnd).add hdegen_int
have hfun :
(fun p : X × X =>
uMean h P + uProj h P p.1 + uProj h P p.2 + uDegen h P p.1 p.2)
= fun p => h p.1 p.2 := by
funext p
exact (hoeffding_decomp h P p.1 p.2).symm
simpa [hfun] using hsum_int
have hmean_bridge : uMeanOrder (pairKernel h) P = uMean h P :=
uMeanOrder_pairKernel (P := P) (h := h) hh_int
have hproj_bridge :
∀ j : Fin 2, uProjOrderAt j (pairKernel h) P = uProj h P :=
fun j => uProjOrderAt_pairKernel_of_symm (P := P) (h := h) hsymm hh_int hrow j
have hψ_bridge : uInfluenceOrder (pairKernel h) P = fun x => 2 * uProj h P x :=
uInfluenceOrder_pairKernel_of_symm (P := P) (h := h) hsymm hh_int hrow
have hstat_bridge : uStatisticOrder S (pairKernel h) = uStatistic S h := by
funext n
exact uStatisticOrder_two_eq_uStatistic S h n
have hdeg_bridge :
uDegenOrder (pairKernel h) P = fun z => uDegen h P (z 0) (z 1) :=
uDegenOrder_pairKernel_of_symm (P := P) (h := h) hsymm hh_int hrow
have hmeas' : Measurable (uDegenOrder (pairKernel h) P) := by
have hraw : Measurable (fun z : Fin 2 → X => uDegen h P (z 0) (z 1)) := by
exact hdeg_meas_prod.comp e.measurable
simpa [hdeg_bridge] using hraw
have hL2' : Integrable (fun z => (uDegenOrder (pairKernel h) P z) ^ 2)
(Measure.pi fun _ : Fin 2 => P) := by
have hraw : Integrable (fun z : Fin 2 → X => (uDegen h P (z 0) (z 1)) ^ 2)
(Measure.pi fun _ : Fin 2 => P) := by
exact hmp.integrable_comp_of_integrable hL2
simpa [hdeg_bridge] using hraw
have hslice_int' : ∀ j : Fin 2, Integrable
(fun x => ∫ tail : ({k : Fin 2 // k ≠ j}) → X,
pairKernel h (insertCoord j x tail)
∂(Measure.pi fun _ : {k : Fin 2 // k ≠ j} => P)) P := by
intro j
fin_cases j
· change Integrable
(fun x => ∫ tail : ({k : Fin 2 // ¬ k = (0 : Fin 2)}) → X,
pairKernel h (insertCoord (0 : Fin 2) x tail)
∂(Measure.pi fun _ : {k : Fin 2 // ¬ k = (0 : Fin 2)} => P)) P
have hfun :
(fun x => ∫ tail : ({k : Fin 2 // ¬ k = (0 : Fin 2)}) → X,
pairKernel h (insertCoord (0 : Fin 2) x tail)
∂(Measure.pi fun _ : {k : Fin 2 // ¬ k = (0 : Fin 2)} => P))
= fun x => ∫ y, h x y ∂P := by
funext x
let a : {k : Fin 2 // ¬ k = (0 : Fin 2)} := ⟨1, by norm_num⟩
have h_eval := integral_pi_eval_eq (P := P) (i := a) (f := fun y => h x y)
(hrow x)
have htail :
(fun tail : ({k : Fin 2 // ¬ k = (0 : Fin 2)}) → X =>
pairKernel h (insertCoord (0 : Fin 2) x tail))
= fun tail => h x (tail a) := by
funext tail
simp [pairKernel, insertCoord, a]
rw [htail, h_eval]
simpa [hfun] using hint
· change Integrable
(fun x => ∫ tail : ({k : Fin 2 // ¬ k = (1 : Fin 2)}) → X,
pairKernel h (insertCoord (1 : Fin 2) x tail)
∂(Measure.pi fun _ : {k : Fin 2 // ¬ k = (1 : Fin 2)} => P)) P
have hfun :
(fun x => ∫ tail : ({k : Fin 2 // ¬ k = (1 : Fin 2)}) → X,
pairKernel h (insertCoord (1 : Fin 2) x tail)
∂(Measure.pi fun _ : {k : Fin 2 // ¬ k = (1 : Fin 2)} => P))
= fun x => ∫ y, h x y ∂P := by
funext x
let a : {k : Fin 2 // ¬ k = (1 : Fin 2)} := ⟨0, by norm_num⟩
have hcol : Integrable (fun y => h y x) P := by
have hfun_col : (fun y => h y x) = fun y => h x y := by
funext y
exact hsymm y x
rw [hfun_col]
exact hrow x
have h_eval := integral_pi_eval_eq (P := P) (i := a) (f := fun y => h y x)
hcol
have hswap : (∫ y, h y x ∂P) = ∫ y, h x y ∂P := by
congr 1
funext y
exact hsymm y x
have htail :
(fun tail : ({k : Fin 2 // ¬ k = (1 : Fin 2)}) → X =>
pairKernel h (insertCoord (1 : Fin 2) x tail))
= fun tail => h (tail a) x := by
funext tail
simp [pairKernel, insertCoord, a]
rw [htail, h_eval, hswap]
simpa [hfun] using hint
have hmean' : ∀ j : Fin 2,
∫ x, (∫ tail : ({k : Fin 2 // k ≠ j}) → X,
pairKernel h (insertCoord j x tail)
∂(Measure.pi fun _ : {k : Fin 2 // k ≠ j} => P)) ∂P
= uMeanOrder (pairKernel h) P := by
intro j
fin_cases j
· change
∫ x, (∫ tail : ({k : Fin 2 // ¬ k = (0 : Fin 2)}) → X,
pairKernel h (insertCoord (0 : Fin 2) x tail)
∂(Measure.pi fun _ : {k : Fin 2 // ¬ k = (0 : Fin 2)} => P)) ∂P
= uMeanOrder (pairKernel h) P
have hfun :
(fun x => ∫ tail : ({k : Fin 2 // ¬ k = (0 : Fin 2)}) → X,
pairKernel h (insertCoord (0 : Fin 2) x tail)
∂(Measure.pi fun _ : {k : Fin 2 // ¬ k = (0 : Fin 2)} => P))
= fun x => ∫ y, h x y ∂P := by
funext x
let a : {k : Fin 2 // ¬ k = (0 : Fin 2)} := ⟨1, by norm_num⟩
have h_eval := integral_pi_eval_eq (P := P) (i := a) (f := fun y => h x y)
(hrow x)
have htail :
(fun tail : ({k : Fin 2 // ¬ k = (0 : Fin 2)}) → X =>
pairKernel h (insertCoord (0 : Fin 2) x tail))
= fun tail => h x (tail a) := by
funext tail
simp [pairKernel, insertCoord, a]
rw [htail, h_eval]
rw [hfun, hmean_bridge]
rfl
· change
∫ x, (∫ tail : ({k : Fin 2 // ¬ k = (1 : Fin 2)}) → X,
pairKernel h (insertCoord (1 : Fin 2) x tail)
∂(Measure.pi fun _ : {k : Fin 2 // ¬ k = (1 : Fin 2)} => P)) ∂P
= uMeanOrder (pairKernel h) P
have hfun :
(fun x => ∫ tail : ({k : Fin 2 // ¬ k = (1 : Fin 2)}) → X,
pairKernel h (insertCoord (1 : Fin 2) x tail)
∂(Measure.pi fun _ : {k : Fin 2 // ¬ k = (1 : Fin 2)} => P))
= fun x => ∫ y, h x y ∂P := by
funext x
let a : {k : Fin 2 // ¬ k = (1 : Fin 2)} := ⟨0, by norm_num⟩
have hcol : Integrable (fun y => h y x) P := by
have hfun_col : (fun y => h y x) = fun y => h x y := by
funext y
exact hsymm y x
rw [hfun_col]
exact hrow x
have h_eval := integral_pi_eval_eq (P := P) (i := a) (f := fun y => h y x)
hcol
have hswap : (∫ y, h y x ∂P) = ∫ y, h x y ∂P := by
congr 1
funext y
exact hsymm y x
have htail :
(fun tail : ({k : Fin 2 // ¬ k = (1 : Fin 2)}) → X =>
pairKernel h (insertCoord (1 : Fin 2) x tail))
= fun tail => h (tail a) x := by
funext tail
simp [pairKernel, insertCoord, a]
rw [htail, h_eval, hswap]
rw [hfun, hmean_bridge]
rfl
have hrow' : ∀ (j : Fin 2) (x : X),
Integrable (fun tail : ({k : Fin 2 // k ≠ j}) → X =>
pairKernel h (insertCoord j x tail))
(Measure.pi fun _ : {k : Fin 2 // k ≠ j} => P) := by
intro j x
fin_cases j
· change Integrable
(fun tail : ({k : Fin 2 // ¬ k = (0 : Fin 2)}) → X =>
pairKernel h (insertCoord (0 : Fin 2) x tail))
(Measure.pi fun _ : {k : Fin 2 // ¬ k = (0 : Fin 2)} => P)
let a : {k : Fin 2 // ¬ k = (0 : Fin 2)} := ⟨1, by norm_num⟩
have htail :
(fun tail : ({k : Fin 2 // ¬ k = (0 : Fin 2)}) → X =>
pairKernel h (insertCoord (0 : Fin 2) x tail))
= fun tail => h x (tail a) := by
funext tail
simp [pairKernel, insertCoord, a]
rw [htail]
have hmp_eval := measurePreserving_eval
(fun _ : {k : Fin 2 // ¬ k = (0 : Fin 2)} => P) a
simpa [Function.comp_def] using hmp_eval.integrable_comp_of_integrable (hrow x)
· change Integrable
(fun tail : ({k : Fin 2 // ¬ k = (1 : Fin 2)}) → X =>
pairKernel h (insertCoord (1 : Fin 2) x tail))
(Measure.pi fun _ : {k : Fin 2 // ¬ k = (1 : Fin 2)} => P)
let a : {k : Fin 2 // ¬ k = (1 : Fin 2)} := ⟨0, by norm_num⟩
have hcol : Integrable (fun y => h y x) P := by
have hfun_col : (fun y => h y x) = fun y => h x y := by
funext y
exact hsymm y x
rw [hfun_col]
exact hrow x
-- … truncated; follow the source link for the rest …
4 supporting declarations (lemmas, instances)
-
uMeanOrder_pairKerneltheorem — The order-2 population mean of pairKernel h is the order-2 mean of h. Requires product-integrability of h so that the joint integral over Fin 2 → X agrees (via Fubini) with the iterated integral defining uMean.Proof (Lean source)
theorem uMeanOrder_pairKernel [SigmaFinite P] (hh_int : Integrable (fun p : X × X => h p.1 p.2) (P.prod P)) : uMeanOrder (pairKernel h) P = uMean h P := by let e := MeasurableEquiv.piFinTwo (fun _ : Fin 2 => X) have hmp : MeasurePreserving e (Measure.pi fun _ : Fin 2 => P) (P.prod P) := by simpa [e] using (measurePreserving_piFinTwo (fun _ : Fin 2 => P)) have hsplit : ∫ z : Fin 2 → X, h (z 0) (z 1) ∂(Measure.pi fun _ : Fin 2 => P) = ∫ p : X × X, h p.1 p.2 ∂(P.prod P) := by simpa [e] using hmp.integral_comp' (fun p : X × X => h p.1 p.2) unfold uMeanOrder pairKernel uMean rw [hsplit, integral_prod _ hh_int] -
uProjOrderAt_pairKernel_of_symmtheorem — Each coordinate first projection of pairKernel h equals the order-2 first projection of h, for a symmetric kernel. (For j = 0 no symmetry is needed; for j = 1 it is used to swap the integration coordinate.)hypotheseshsymm :∀ x y, h x y = h y xhh_int :Integrable (fun p : X × X => h p.1 p.2) (P.prod P)hrow :∀ x, Integrable (fun y => h x y) Pj :Fin 2conclusionProof (Lean source)
theorem uProjOrderAt_pairKernel_of_symm (hsymm : ∀ x y, h x y = h y x) (hh_int : Integrable (fun p : X × X => h p.1 p.2) (P.prod P)) (hrow : ∀ x, Integrable (fun y => h x y) P) (j : Fin 2) : uProjOrderAt j (pairKernel h) P = uProj h P := by funext x fin_cases j · have htail : (∫ tail : ({k : Fin 2 // ¬ k = (0 : Fin 2)}) → X, pairKernel h (insertCoord (0 : Fin 2) x tail) ∂(Measure.pi fun _ : {k : Fin 2 // ¬ k = (0 : Fin 2)} => P)) = ∫ y, h x y ∂P := by let a : {k : Fin 2 // ¬ k = (0 : Fin 2)} := ⟨1, by norm_num⟩ have h_eval := integral_pi_eval_eq (P := P) (i := a) (f := fun y => h x y) (hrow x) have hfun : (fun tail : ({k : Fin 2 // ¬ k = (0 : Fin 2)}) → X => pairKernel h (insertCoord (0 : Fin 2) x tail)) = fun tail => h x (tail a) := by funext tail simp [pairKernel, insertCoord, a] rw [hfun, h_eval] unfold uProjOrderAt uProj change (∫ tail : ({k : Fin 2 // ¬ k = (0 : Fin 2)}) → X, pairKernel h (insertCoord (0 : Fin 2) x tail) ∂(Measure.pi fun _ : {k : Fin 2 // ¬ k = (0 : Fin 2)} => P)) - uMeanOrder (pairKernel h) P = (∫ y, h x y ∂P) - uMean h P rw [htail, uMeanOrder_pairKernel (P := P) (h := h) hh_int] · have hcol : Integrable (fun y => h y x) P := by have hfun : (fun y => h y x) = fun y => h x y := by funext y exact hsymm y x rw [hfun] exact hrow x have htail : (∫ tail : ({k : Fin 2 // ¬ k = (1 : Fin 2)}) → X, pairKernel h (insertCoord (1 : Fin 2) x tail) ∂(Measure.pi fun _ : {k : Fin 2 // ¬ k = (1 : Fin 2)} => P)) = ∫ y, h x y ∂P := by let a : {k : Fin 2 // ¬ k = (1 : Fin 2)} := ⟨0, by norm_num⟩ have h_eval := integral_pi_eval_eq (P := P) (i := a) (f := fun y => h y x) hcol have hswap : (∫ y, h y x ∂P) = ∫ y, h x y ∂P := by congr 1 funext y exact hsymm y x have hfun : (fun tail : ({k : Fin 2 // ¬ k = (1 : Fin 2)}) → X => pairKernel h (insertCoord (1 : Fin 2) x tail)) = fun tail => h (tail a) x := by funext tail simp [pairKernel, insertCoord, a] rw [hfun, h_eval, hswap] unfold uProjOrderAt uProj change (∫ tail : ({k : Fin 2 // ¬ k = (1 : Fin 2)}) → X, pairKernel h (insertCoord (1 : Fin 2) x tail) ∂(Measure.pi fun _ : {k : Fin 2 // ¬ k = (1 : Fin 2)} => P)) - uMeanOrder (pairKernel h) P = (∫ y, h x y ∂P) - uMean h P rw [htail, uMeanOrder_pairKernel (P := P) (h := h) hh_int] -
uInfluenceOrder_pairKernel_of_symmtheorem — The order-2 influence function of pairKernel h is 2 · h₁, matching the order-2 CLT influence function ψ = 2 · uProj h P.hypotheseshsymm :∀ x y, h x y = h y xhh_int :Integrable (fun p : X × X => h p.1 p.2) (P.prod P)hrow :∀ x, Integrable (fun y => h x y) PconclusionProof (Lean source)
theorem uInfluenceOrder_pairKernel_of_symm (hsymm : ∀ x y, h x y = h y x) (hh_int : Integrable (fun p : X × X => h p.1 p.2) (P.prod P)) (hrow : ∀ x, Integrable (fun y => h x y) P) : uInfluenceOrder (pairKernel h) P = fun x => 2 * uProj h P x := by simpa using (uInfluenceOrder_eq_card_mul_of_common_projection (P := P) (h := pairKernel h) (φ := uProj h P) (fun j x => congrFun (uProjOrderAt_pairKernel_of_symm (P := P) (h := h) hsymm hh_int hrow j) x)) -
uDegenOrder_pairKernel_of_symmtheorem — The order-2 degenerate residual of pairKernel h is the order-2 degenerate kernel uDegen h P, evaluated at the two coordinates.hypotheseshsymm :∀ x y, h x y = h y xhh_int :Integrable (fun p : X × X => h p.1 p.2) (P.prod P)hrow :∀ x, Integrable (fun y => h x y) PconclusionProof (Lean source)
theorem uDegenOrder_pairKernel_of_symm (hsymm : ∀ x y, h x y = h y x) (hh_int : Integrable (fun p : X × X => h p.1 p.2) (P.prod P)) (hrow : ∀ x, Integrable (fun y => h x y) P) : uDegenOrder (pairKernel h) P = fun z => uDegen h P (z 0) (z 1) := by funext z have hproj0 : uProjOrderAt (0 : Fin 2) (pairKernel h) P (z 0) = uProj h P (z 0) := congrFun (uProjOrderAt_pairKernel_of_symm (P := P) (h := h) hsymm hh_int hrow 0) (z 0) have hproj1 : uProjOrderAt (1 : Fin 2) (pairKernel h) P (z 1) = uProj h P (z 1) := congrFun (uProjOrderAt_pairKernel_of_symm (P := P) (h := h) hsymm hh_int hrow 1) (z 1) simp [uDegenOrder, uDegen, pairKernel, uMeanOrder_pairKernel (P := P) (h := h) hh_int, Fin.sum_univ_two, hproj0, hproj1] ring
RemainderNegligible 2 core · 1 supporting Discharges the fixed-order Hájek remainder negligibility hypothesis. ★ orderDegenerateNegligible_of_firstDegen★ orderDegenerateNegligible_of_residual
Discharges the fixed-order Hájek remainder negligibility hypothesis.
The theorem orderDegenerateNegligible_of_firstDegen proves that a first-order
degenerate kernel has √n-rescaled U-statistic o_p(1), using the
second-moment estimate from OrderM.RemainderSecondMoment and Chebyshev's
inequality. The public wrapper orderDegenerateNegligible_of_residual applies
this result to the residual kernel uDegenOrder h P, producing the
OrderDegenerateNegligible S h hypothesis required by the fixed-order
asymptotic-linearity and CLT statements.
theorem orderDegenerateNegligible_of_firstDegen reviewed
⚑ flagged
Causalean.Stat.IIDSample
Negligibility of the higher-order remainder. For an i.i.d. sample S, if the order-m kernel g is first-order degenerate: measurable, square-integrable, and mean zero after integrating out any single coordinate, then the √n-rescaled order-m U-statistic of g converges to zero in probability, i.e. it is o_p(1).
Formal statement
hypotheses
hg :
conclusion
Proof (Lean source)
theorem orderDegenerateNegligible_of_firstDegen [IsFiniteMeasure P]
(hg : OrderFirstDegenKernel P g) :
IsLittleOp (fun n ω => sqrt (n : ℝ) * uStatisticOrder S g n ω)
(fun _ => (1 : ℝ)) μ := by
letI : IsProbabilityMeasure μ := S.indep.isProbabilityMeasure
intro ε hε
rcases S.integral_rescaled_order_sq_le hg with ⟨C, hCnn, hCbound⟩
have hb_tendsto :
Tendsto (fun n : ℕ => ofReal ((C / ε ^ 2) / (n : ℝ))) atTop (𝓝 0) := by
rw [← ENNReal.ofReal_zero]
apply ENNReal.tendsto_ofReal
have : Tendsto (fun n : ℕ => (C / ε ^ 2) * ((n : ℝ))⁻¹)
atTop (𝓝 ((C / ε ^ 2) * 0)) := by
apply Filter.Tendsto.const_mul
exact tendsto_natCast_atTop_atTop.inv_tendsto_atTop
simpa [div_eq_mul_inv, mul_zero] using this
have hbound : ∀ᶠ n : ℕ in atTop,
μ {ω | ε * (fun _ => (1 : ℝ)) n
< |sqrt (n : ℝ) * uStatisticOrder S g n ω|}
≤ ofReal ((C / ε ^ 2) / (n : ℝ)) := by
filter_upwards [eventually_ge_atTop m] with n hmn
set X : Ω → ℝ := fun ω => sqrt (n : ℝ) * uStatisticOrder S g n ω with hXdef
have hmem : MemLp X 2 μ := by
simpa [X, hXdef] using S.memLp_rescaled_order hg.meas hg.sq n
have hmean : ∫ ω, X ω ∂μ = 0 := by
simpa [X, hXdef] using S.integral_rescaled_order_eq_zero hg hmn
have hvar_le : variance X μ ≤ C / (n : ℝ) := by
rw [ProbabilityTheory.variance_eq_sub hmem, hmean]
simp only [Pi.pow_apply]
simpa [X, hXdef] using hCbound hmn
have hcheb := ProbabilityTheory.meas_ge_le_variance_div_sq hmem (c := ε) hε
simp only [hmean, sub_zero] at hcheb
have hsub :
{ω | ε * (fun _ => (1 : ℝ)) n
< |sqrt (n : ℝ) * uStatisticOrder S g n ω|}
⊆ {ω | ε ≤ |X ω|} := by
intro ω hω
simp only [Set.mem_setOf_eq, mul_one, X] at hω ⊢
exact le_of_lt hω
refine le_trans (measure_mono hsub) ?_
calc
μ {ω | ε ≤ |X ω|}
≤ ofReal (variance X μ / ε ^ 2) := hcheb
_ ≤ ofReal ((C / (n : ℝ)) / ε ^ 2) := by
apply ENNReal.ofReal_le_ofReal
gcongr
_ = ofReal ((C / ε ^ 2) / (n : ℝ)) := by
exact congrArg ofReal (by ring)
refine tendsto_of_tendsto_of_tendsto_of_le_of_le' tendsto_const_nhds hb_tendsto
(Eventually.of_forall (fun n => zero_le)) hbound
theorem orderDegenerateNegligible_of_residual reviewed
⚑ flagged
Causalean.Stat
The higher-order remainder of a fixed-order U-statistic is negligible. For an i.i.d. sample S and order-m kernel h, write g for the higher-order Hájek residual of h. If g is measurable and square-integrable under the m-fold product law, and if for every coordinate integrating h over the remaining m − 1 coordinates yields an integrable function of that coordinate with the same population mean uMeanOrder h P in every coordinate and h remains integrable in the remaining coordinates for every fixed value of that coordinate, then the √n-rescaled higher-order residual U-statistic √n · Gₙ converges to zero in probability, i.e. it is o_p(1). This discharges the OrderDegenerateNegligible hypothesis consumed by the order-m CLT uStatisticOrder_clt (Causalean.Stat.UStatistic.OrderM.CLT).
Formal statement
hypotheses
Ω X :
S :
IIDSample Ω X μ P
m :
ℕ
NeZero m
h :
(Fin m → X) → ℝ
hmeas :
Measurable (uDegenOrder h P)
hL2 :
hslice_int :
∀ j : Fin m,
Integrable (fun x => ∫ tail : ({k : Fin m // k ≠ j}) → X, h (insertCoord j x tail) ∂(Measure.pi fun _ : {k : Fin m // k ≠ j} => P)) P
hmean :
∀ j : Fin m,
∫ x, (∫ tail : ({k : Fin m // k ≠ j}) → X, h (insertCoord j x tail) ∂(Measure.pi fun _ : {k : Fin m // k ≠ j} => P)) ∂P
= uMeanOrder h P
hrow :
∀ (j : Fin m) (x : X),
Integrable (fun tail : ({k : Fin m // k ≠ j}) → X => h (insertCoord j x tail)) (Measure.pi fun _ : {k : Fin m // k ≠ j} => P)
conclusion
Proof (Lean source)
theorem orderDegenerateNegligible_of_residual
{Ω X : Type*} [MeasurableSpace Ω] [MeasurableSpace X]
{μ : Measure Ω} {P : Measure X}
(S : IIDSample Ω X μ P) {m : ℕ} [NeZero m] (h : (Fin m → X) → ℝ)
(hmeas : Measurable (uDegenOrder h P))
(hL2 : Integrable (fun z => (uDegenOrder h P z) ^ 2)
(Measure.pi fun _ : Fin m => P))
(hslice_int : ∀ j : Fin m, Integrable
(fun x => ∫ tail : ({k : Fin m // k ≠ j}) → X,
h (insertCoord j x tail) ∂(Measure.pi fun _ : {k : Fin m // k ≠ j} => P)) P)
(hmean : ∀ j : Fin m,
∫ x, (∫ tail : ({k : Fin m // k ≠ j}) → X,
h (insertCoord j x tail) ∂(Measure.pi fun _ : {k : Fin m // k ≠ j} => P)) ∂P
= uMeanOrder h P)
(hrow : ∀ (j : Fin m) (x : X),
Integrable (fun tail : ({k : Fin m // k ≠ j}) → X =>
h (insertCoord j x tail))
(Measure.pi fun _ : {k : Fin m // k ≠ j} => P)) :
OrderDegenerateNegligible S h := by
letI : IsProbabilityMeasure μ := S.indep.isProbabilityMeasure
letI : IsProbabilityMeasure P := by
rw [← S.law]
exact Measure.isProbabilityMeasure_map (S.meas 0).aemeasurable
have hg : OrderFirstDegenKernel P (uDegenOrder h P) := {
meas := hmeas
firstDeg := fun j x => uDegenOrder_integral_tail_eq_zero hslice_int hmean hrow j x
sq := hL2
}
unfold OrderDegenerateNegligible uRemainderOrder
exact S.orderDegenerateNegligible_of_firstDegen hg
1 supporting declaration (lemmas, instances)
-
integral_rescaled_order_eq_zerotheorem — The rescaled higher-order remainder has mean zero.hypothesesconclusion∫ ω, sqrt (n : ℝ) * uStatisticOrder S g n ω ∂μ = 0Proof (Lean source)
theorem integral_rescaled_order_eq_zero (hg : OrderFirstDegenKernel P g) {n : ℕ} (hmn : m ≤ n) : ∫ ω, sqrt (n : ℝ) * uStatisticOrder S g n ω ∂μ = 0 := by letI : IsProbabilityMeasure μ := S.indep.isProbabilityMeasure letI : IsProbabilityMeasure P := by rw [← S.law] exact Measure.isProbabilityMeasure_map (S.meas 0).aemeasurable exact S.integral_rescaled_uStatisticOrder_eq_zero_of_uMean_zero hg.meas hg.integrable hmn hg.integral_eq_zero
RemainderSecondMoment 2 core · 8 supporting Proves the second-moment bound for first-order degenerate fixed-order U-statistic remainders. ★ crossterm_eq_zero_of_shared_le_one★ integral_rescaled_order_sq_le
Proves the second-moment bound for first-order degenerate fixed-order U-statistic remainders.
The central public estimate is IIDSample.integral_rescaled_order_sq_le: for a
kernel satisfying OrderFirstDegenKernel, there is a finite constant C
depending only on the order and ζ_m = E[g²] such that
E[(√n * Uₙ)²] ≤ C / n whenever n ≥ m. The proof first shows
crossterm_eq_zero_of_shared_le_one, bounding the only nonzero terms by
Cauchy-Schwarz, then counts the tuple pairs sharing at least two sample indices
and normalizes by the falling factorial denominator.
theorem integral_rescaled_order_sq_le reviewed
⚑ flagged
Causalean.Stat.IIDSample
L² bound on the rescaled higher-order remainder. For an i.i.d. sample S, if the order-m kernel g is first-order degenerate, then there is a nonnegative constant C, depending only on the order m and the kernel's second moment ζ_m = E[g²], such that the second moment of the √n-rescaled order-m U-statistic of g is at most C/n for every sample size n ≥ m. This is the keystone estimate; it packages cross-term vanishing, the Cauchy–Schwarz bound |E[g_t g_q]| ≤ ζ_m, the O(n^{2m-2}) count of surviving tuple pairs, and the n · (n^{(m)})⁻² normalization.
Formal statement
hypotheses
hg :
conclusion
∃ C : ℝ
if
0 ≤ C ∧ ∀ {n : ℕ}, m ≤ n
then
∫ ω, (sqrt (n : ℝ) * uStatisticOrder S g n ω) ^ 2 ∂μ ≤ C / (n : ℝ)
Proof (Lean source)
theorem integral_rescaled_order_sq_le (hg : OrderFirstDegenKernel P g) :
∃ C : ℝ, 0 ≤ C ∧ ∀ {n : ℕ}, m ≤ n →
∫ ω, (sqrt (n : ℝ) * uStatisticOrder S g n ω) ^ 2 ∂μ ≤ C / (n : ℝ) := by
letI : IsProbabilityMeasure μ := S.indep.isProbabilityMeasure
letI : IsProbabilityMeasure P := by
rw [← S.law]
exact Measure.isProbabilityMeasure_map (S.meas 0).aemeasurable
exact S.integral_rescaled_order_sq_le_counting_normalization hg
8 supporting declarations (lemmas, instances)
-
crossterm_zero_of_disjointtheorem — For a first-order-degenerate kernel, the expected product of terms evaluated on two injective sample-index tuples with disjoint index sets is zero.hypothesesconclusion∫ ω, g (fun j => S.Z (t j : ℕ) ω) * g (fun j => S.Z (q j : ℕ) ω) ∂μ = 0Proof (Lean source)
theorem crossterm_zero_of_disjoint [IsFiniteMeasure P] (hg : OrderFirstDegenKernel P g) {n : ℕ} {t q : Fin m → Fin n} (ht : Injective t) (hq : Injective q) (hdisj : Disjoint (Finset.univ.image t) (Finset.univ.image q)) : ∫ ω, g (fun j => S.Z (t j : ℕ) ω) * g (fun j => S.Z (q j : ℕ) ω) ∂μ = 0 := by classical let A : Finset (Fin n) := Finset.univ.image t let B : Finset (Fin n) := Finset.univ.image q let Xt : Ω → (A → X) := fun ω i => S.Z (i.1 : ℕ) ω let Xq : Ω → (B → X) := fun ω i => S.Z (i.1 : ℕ) ω let φ : (A → X) → ℝ := fun x => g (fun j => x ⟨t j, Finset.mem_image.mpr ⟨j, Finset.mem_univ j, rfl⟩⟩) let ψ : (B → X) → ℝ := fun x => g (fun j => x ⟨q j, Finset.mem_image.mpr ⟨j, Finset.mem_univ j, rfl⟩⟩) have hindFin : iIndepFun (fun i : Fin n => S.Z (i : ℕ)) μ := S.indep.precomp (fun _ _ h => Fin.ext h) have hindBlocks : IndepFun Xt Xq μ := by simpa [A, B, Xt, Xq] using (ProbabilityTheory.iIndepFun.indepFun_finset A B hdisj hindFin (fun i : Fin n => S.meas (i : ℕ))) have hφ : Measurable φ := by exact hg.meas.comp (measurable_pi_lambda _ (fun j : Fin m => measurable_pi_apply _)) have hψ : Measurable ψ := by exact hg.meas.comp (measurable_pi_lambda _ (fun j : Fin m => measurable_pi_apply _)) have hind : IndepFun (φ ∘ Xt) (ψ ∘ Xq) μ := hindBlocks.comp hφ hψ have hφsm : AEStronglyMeasurable (φ ∘ Xt) μ := (hφ.comp (measurable_pi_lambda _ (fun i : A => S.meas (i.1 : ℕ)))).aestronglyMeasurable have hψsm : AEStronglyMeasurable (ψ ∘ Xq) μ := (hψ.comp (measurable_pi_lambda _ (fun i : B => S.meas (i.1 : ℕ)))).aestronglyMeasurable have hfactor : ∫ ω, (φ ∘ Xt) ω * (ψ ∘ Xq) ω ∂μ = (∫ ω, (φ ∘ Xt) ω ∂μ) * (∫ ω, (ψ ∘ Xq) ω ∂μ) := hind.integral_fun_mul_eq_mul_integral hφsm hψsm have hmean_t : ∫ ω, (φ ∘ Xt) ω ∂μ = 0 := by simpa [φ, Xt, uMeanOrder] using (S.integral_orderKernelTerm_eq_zero_of_uMean_zero hg.meas ht hg.integral_eq_zero) have hmean_q : ∫ ω, (ψ ∘ Xq) ω ∂μ = 0 := by simpa [ψ, Xq, uMeanOrder] using (S.integral_orderKernelTerm_eq_zero_of_uMean_zero hg.meas hq hg.integral_eq_zero) change ∫ ω, (φ ∘ Xt) ω * (ψ ∘ Xq) ω ∂μ = 0 rw [hfactor, hmean_t, hmean_q, zero_mul] -
crossterm_abs_le_zetatheorem — The absolute expected product of two kernel evaluations on distinct sample tuples is no larger than the kernel's second moment under the product distribution.hypothesesconclusion|∫ ω, g (fun j => S.Z (t j : ℕ) ω) * g (fun j => S.Z (q j : ℕ) ω) ∂μ| ≤ zetaOrder P gProof (Lean source)
theorem crossterm_abs_le_zeta (hmeas : Measurable g) (hsq : Integrable (fun z => (g z) ^ 2) (Measure.pi fun _ : Fin m => P)) {n : ℕ} {t q : Fin m → Fin n} (ht : Injective t) (hq : Injective q) : |∫ ω, g (fun j => S.Z (t j : ℕ) ω) * g (fun j => S.Z (q j : ℕ) ω) ∂μ| ≤ zetaOrder P g := by letI : IsProbabilityMeasure μ := S.indep.isProbabilityMeasure let ft : Ω → ℝ := fun ω => g (fun j => S.Z (t j : ℕ) ω) let fq : Ω → ℝ := fun ω => g (fun j => S.Z (q j : ℕ) ω) have hft0 : MemLp ft 2 μ := S.memLp_orderTerm hmeas hsq ht have hfq0 : MemLp fq 2 μ := S.memLp_orderTerm hmeas hsq hq have hft : MemLp ft (ofReal (2 : ℝ)) μ := by simpa using hft0 have hfq : MemLp fq (ofReal (2 : ℝ)) μ := by simpa using hfq0 have hcs := MeasureTheory.integral_mul_norm_le_Lp_mul_Lq (μ := μ) (f := ft) (g := fq) (p := (2 : ℝ)) (q := (2 : ℝ)) (Real.holderConjugate_iff.mpr (by norm_num)) hft hfq have habs : |∫ ω, ft ω * fq ω ∂μ| ≤ ∫ ω, ‖ft ω‖ * ‖fq ω‖ ∂μ := by calc |∫ ω, ft ω * fq ω ∂μ| ≤ ∫ ω, |ft ω * fq ω| ∂μ := abs_integral_le_integral_abs _ = ∫ ω, ‖ft ω‖ * ‖fq ω‖ ∂μ := by simp [Real.norm_eq_abs, abs_mul] have ht2 : ∫ ω, ‖ft ω‖ ^ (2 : ℝ) ∂μ = zetaOrder P g := by simpa [ft, sq_abs] using S.orderTerm_diag hmeas ht have hq2 : ∫ ω, ‖fq ω‖ ^ (2 : ℝ) ∂μ = zetaOrder P g := by simpa [fq, sq_abs] using S.orderTerm_diag hmeas hq have hznonneg : 0 ≤ zetaOrder P g := zetaOrder_nonneg rw [ht2, hq2] at hcs have hroot : (zetaOrder P g) ^ (1 / (2 : ℝ)) * (zetaOrder P g) ^ (1 / (2 : ℝ)) = zetaOrder P g := by rw [← Real.rpow_add' hznonneg (by norm_num : (1 / (2 : ℝ) + 1 / (2 : ℝ)) ≠ 0)] rw [show (1 / (2 : ℝ) + 1 / (2 : ℝ)) = (1 : ℝ) by norm_num] exact Real.rpow_one (zetaOrder P g) rw [hroot] at hcs exact le_trans habs hcs -
descFactorial_getheorem — When the sample size is at least the order, its falling factorial is at least the sample-size power divided by the order power.hypothesesm n :ℕhmn :m ≤ nconclusion(n : ℝ) ^ m / (m : ℝ) ^ m ≤ (n.descFactorial m : ℝ)Proof (Lean source)
theorem descFactorial_ge {m n : ℕ} (hmn : m ≤ n) : (n : ℝ) ^ m / (m : ℝ) ^ m ≤ (n.descFactorial m : ℝ) := by by_cases hmzero : m = 0 · subst m simp have hmposNat : 0 < m := Nat.pos_of_ne_zero hmzero have hmpos : 0 < (m : ℝ) := by exact_mod_cast hmposNat rw [Nat.descFactorial_eq_prod_range] norm_num [Nat.cast_prod] have hfactor : ∀ i ∈ range m, (n : ℝ) / (m : ℝ) ≤ (n - i : ℕ) := by intro i hi have him : i < m := Finset.mem_range.mp hi have hin : i ≤ n := le_trans (le_of_lt him) hmn rw [Nat.cast_sub hin] have hmnR : (m : ℝ) ≤ (n : ℝ) := by exact_mod_cast hmn have hiR : (i : ℝ) + 1 ≤ (m : ℝ) := by exact_mod_cast (Nat.succ_le_of_lt him) have hmul : (n : ℝ) ≤ ((n : ℝ) - (i : ℝ)) * (m : ℝ) := by nlinarith [mul_nonneg (sub_nonneg.mpr hmnR) (sub_nonneg.mpr (by linarith : (1 : ℝ) ≤ (m : ℝ)))] exact (div_le_iff₀ hmpos).mpr hmul have hprod := Finset.prod_le_prod (s := range m) (f := fun _i : ℕ => (n : ℝ) / (m : ℝ)) (g := fun i : ℕ => (n - i : ℕ)) (fun _i _hi => div_nonneg (Nat.cast_nonneg _) (le_of_lt hmpos)) hfactor simpa [Finset.prod_const, div_pow] using hprod -
rescaled_order_normalization_letheorem — For a nonnegative second-moment bound and a sample size at least the kernel order, the falling-factorial normalization term is bounded by a constant divided by the sample size.hypothesesn :ℕhmn :m ≤ nζ :ℝhζ :0 ≤ ζconclusion(n : ℝ) * (injectiveTupleCount m n)⁻¹ ^ 2 * ((m.choose 2 : ℝ) * (m : ℝ) ^ 2 * (n : ℝ) ^ (2 * m - 2) * ζ)≤ ((m.choose 2 : ℝ) * (m : ℝ) ^ (2 * m + 2) * ζ) / (n : ℝ)Proof (Lean source)
theorem rescaled_order_normalization_le {n : ℕ} (hmn : m ≤ n) {ζ : ℝ} (hζ : 0 ≤ ζ) : (n : ℝ) * (injectiveTupleCount m n)⁻¹ ^ 2 * ((m.choose 2 : ℝ) * (m : ℝ) ^ 2 * (n : ℝ) ^ (2 * m - 2) * ζ) ≤ ((m.choose 2 : ℝ) * (m : ℝ) ^ (2 * m + 2) * ζ) / (n : ℝ) := by have hmposNat : 0 < m := Nat.pos_of_ne_zero (NeZero.ne m) have hnposNat : 0 < n := lt_of_lt_of_le hmposNat hmn have hmpos : 0 < (m : ℝ) := by exact_mod_cast hmposNat have hnpos : 0 < (n : ℝ) := by exact_mod_cast hnposNat have hDpos : 0 < (n.descFactorial m : ℝ) := by exact_mod_cast Nat.descFactorial_pos.mpr hmn have hDlower : (n : ℝ) ^ m / (m : ℝ) ^ m ≤ (n.descFactorial m : ℝ) := descFactorial_ge (m := m) hmn have hlower_pos : 0 < (n : ℝ) ^ m / (m : ℝ) ^ m := by positivity have hinv : ((n.descFactorial m : ℝ)⁻¹) ≤ ((m : ℝ) ^ m / (n : ℝ) ^ m) := by have h := inv_anti₀ hlower_pos hDlower have hrewrite : ((n : ℝ) ^ m / (m : ℝ) ^ m)⁻¹ = (m : ℝ) ^ m / (n : ℝ) ^ m := by field_simp [pow_ne_zero _ hmpos.ne', pow_ne_zero _ hnpos.ne'] simpa [hrewrite] using h have hinv_sq : ((n.descFactorial m : ℝ)⁻¹) ^ 2 ≤ ((m : ℝ) ^ m / (n : ℝ) ^ m) ^ 2 := by exact pow_le_pow_left₀ (inv_nonneg.mpr hDpos.le) hinv 2 rw [injectiveTupleCount_eq_descFactorial] calc (n : ℝ) * ((n.descFactorial m : ℝ)⁻¹) ^ 2 * ((m.choose 2 : ℝ) * (m : ℝ) ^ 2 * (n : ℝ) ^ (2 * m - 2) * ζ) ≤ (n : ℝ) * ((m : ℝ) ^ m / (n : ℝ) ^ m) ^ 2 * ((m.choose 2 : ℝ) * (m : ℝ) ^ 2 * (n : ℝ) ^ (2 * m - 2) * ζ) := by gcongr _ = ((m.choose 2 : ℝ) * (m : ℝ) ^ (2 * m + 2) * ζ) / (n : ℝ) := by have hpow_n : (n : ℝ) ^ 2 * (n : ℝ) ^ (m * 2 - 2) = (n : ℝ) ^ (m * 2) := by rw [← pow_add] congr 1 omega have hpow_n' : (n : ℝ) ^ 2 * (n : ℝ) ^ (2 * m - 2) = (n : ℝ) ^ (2 * m) := by rw [← pow_add] congr 1 omega have hpow_m : ((m : ℝ) ^ m) ^ 2 * (m : ℝ) ^ 2 = (m : ℝ) ^ (2 * m + 2) := by rw [← pow_mul, ← pow_add] congr 1 omega have hpow_n_rhs : ((n : ℝ) ^ m) ^ 2 = (n : ℝ) ^ (2 * m) := by rw [← pow_mul] congr 1 omega field_simp [pow_ne_zero _ hnpos.ne', pow_ne_zero _ hmpos.ne'] calc (n : ℝ) ^ 2 * ((m : ℝ) ^ m) ^ 2 * (m.choose 2 : ℝ) * (m : ℝ) ^ 2 * (n : ℝ) ^ (2 * m - 2) * ζ = (m.choose 2 : ℝ) * ζ * (((m : ℝ) ^ m) ^ 2 * (m : ℝ) ^ 2) * ((n : ℝ) ^ 2 * (n : ℝ) ^ (2 * m - 2)) := by ring _ = (m.choose 2 : ℝ) * ζ * (m : ℝ) ^ (2 * m + 2) * (n : ℝ) ^ (2 * m) := by rw [hpow_m, hpow_n'] _ = ((n : ℝ) ^ m) ^ 2 * (m.choose 2 : ℝ) * ζ * (m : ℝ) ^ (2 * m + 2) := by rw [hpow_n_rhs] ring