Stat.EmpiricalProcess.Countable
Directory interface for atom-safe deterministic localization skeletons, countable bounded fourth-moment symmetrization, nested-chain sign maximal inequalities, and composition with second-moment energy budgets.
Basic 6 core · 0 supporting Uses the existing population-centered empirical average.
Countable empirical processes: common notation
Uses the existing population-centered empirical average. Ghost and signed sums are normalized by the sample size. Symmetrization theorems require a positive sample size; threshold measurability also covers the empty sample. The finite Boolean sign average has exactly the uniform Rademacher law.
structure BoundedClass reviewed
⚑ flagged
Causalean.Stat.EmpiricalProcess.Countable
A uniformly bounded class of real functions on a measurable sample space, indexed by an index set, consists of the indexed functions, a common bound that is nonnegative, measurability of every function, and the absolute value of every function being at most the bound at every point.
Definition (Lean source)
parameters
Ω ι :
Type*
fields
f :
ι → Ω → ℝ
bound :
ℝ
bound_nonneg :
0 ≤ bound
measurable :
∀ i, Measurable (f i)
bounded :
∀ i x, |f i x| ≤ bound
def centeredSup reviewed
⚑ flagged
Causalean.Stat.EmpiricalProcess.Countable
The centered supremum of an indexed function class on a sample relative to a population measure μ is the supremum over the class of the absolute difference between each function's empirical average and its population integral.
Definition (Lean source)
def ghostSup reviewed
⚑ flagged
Causalean.Stat.EmpiricalProcess.Countable
The ghost supremum of an indexed function class on two samples x and y of the same size n is the supremum over the class of the absolute difference between the two samples' empirical averages, that is, of |(1/n) Σ_j (f(x_j) − f(y_j))|.
Definition (Lean source)
parameters
def
ghostSup f x y :
ℝ
given by
⨆ i, |(n : ℝ)⁻¹ * ∑ j, (f i (x j) - f i (y j))|
def signedSup reviewed
⚑ flagged
Causalean.Stat.EmpiricalProcess.Countable
The signed supremum of an indexed function class on a sample of size n under a sign vector σ is the supremum over the class of the absolute normalized Rademacher sum |(1/n) Σ_j σ_j f(x_j)|.
def signedGhostSup reviewed
⚑ flagged
Causalean.Stat.EmpiricalProcess.Countable
The signed ghost supremum of an indexed function class on two samples x and y of the same size n under a sign vector σ is the supremum over the class of |(1/n) Σ_j σ_j (f(x_j) − f(y_j))|, one sign per paired difference.
def signAverage reviewed
⚑ flagged
Causalean.Stat.EmpiricalProcess.Countable
The sign average of a real function of sign vectors of length n is its sum over all 2^n sign vectors divided by 2^n, the expectation under independent uniform Rademacher signs.
ChainBasic 2 core · 0 supporting Common notation for finite signed weighted set sums, their real suprema, and squared-weight energy in a containing set.
Weighted chain sums and restricted energy
Common notation for finite signed weighted set sums, their real suprema, and squared-weight energy in a containing set. These definitions carry no maximal inequality and impose no cardinality restriction on the set family.
def chainSignSup reviewed
⚑ flagged
Causalean.Stat.EmpiricalProcess.Countable
The chain supremum of a family of sets on a sample with real sample weights w and a sign vector σ is the supremum over the family of the absolute value of Σ_j σ_j w_j taken over the observations lying in the set.
def chainEnergy reviewed
⚑ flagged
Causalean.Stat.EmpiricalProcess.Countable
The chain energy of a set U on a sample with real sample weights w is the sum of the squared weights w_j over the observations lying in U.
CoverSupremum 4 core · 0 supporting A finite cover assigns every function to one weighted-indicator branch. ★ signedSup_fourth_le_chainAverages
Deterministic comparison of a class with its chain branches
A finite cover assigns every function to one weighted-indicator branch. For each fixed sample, the normalized class supremum's fourth sign average is at most the sum of the unnormalized branch fourth sign averages divided by the fourth power of sample size. This is only a comparison of suprema; it neither assumes nor uses a maximal moment estimate for the chains.
structure ChainCover reviewed
⚑ flagged
Causalean.Stat.EmpiricalProcess.Countable
A chain cover of a bounded function class with m branches assigns each function a branch and a set, gives each branch a fixed signed weight function and a containing set, and requires that the sets of functions in the same branch are nested, each function's set lies in its branch's containing set, and each function equals its branch weight restricted to its set (zero outside).
Definition (Lean source)
parameters
def coverEnergy reviewed
⚑ flagged
Causalean.Stat.EmpiricalProcess.Countable
The energy of branch b of a chain cover on a sample is the sum, over observations lying in the branch's containing set, of the squared branch weight at the observation.
Definition (Lean source)
parameters
def
coverEnergy cover x b :
ℝ
given by
chainEnergy (cover.containing b) x (fun j => cover.weight b (x j))
def branchSignSup reviewed
⚑ flagged
Causalean.Stat.EmpiricalProcess.Countable
The branch signed supremum of branch b of a chain cover on a sample under a sign vector σ is the chain supremum over the sets of the class functions assigned to that branch, with the branch weight evaluated at each observation and no sample-size normalization.
Definition (Lean source)
parameters
def
branchSignSup cover x σ b :
ℝ
given by
chainSignSup (fun i : {i : ι // cover.branch i = b} => cover.sets i.1) x (fun j => cover.weight b (x j)) σ
theorem signedSup_fourth_le_chainAverages reviewed
⚑ flagged
Causalean.Stat.EmpiricalProcess.Countable
For a nonempty countable bounded class with a finite chain cover and any sample of size n, the sign average of the fourth power of the normalized signed supremum is at most 1/n^4 times the sum over branches of the sign averages of the fourth powers of the unnormalized branch signed suprema, including sample size zero.
Formal statement
hypotheses
conclusion
signAverage (fun σ => signedSup F.f x σ ^ 4)
≤ (n : ℝ)⁻¹ ^ 4 * ∑ b, signAverage (fun σ => branchSignSup cover x σ b ^ 4)
Proof (Lean source)
theorem signedSup_fourth_le_chainAverages {Ω ι : Type*} [MeasurableSpace Ω]
[Countable ι] [Nonempty ι] (F : BoundedClass Ω ι) {m : ℕ}
(cover : ChainCover F m) {n : ℕ} (x : Fin n → Ω) :
signAverage (fun σ => signedSup F.f x σ ^ 4) ≤
(n : ℝ)⁻¹ ^ 4 * ∑ b, signAverage (fun σ => branchSignSup cover x σ b ^ 4) := by
classical
let W (b : Fin m) (σ : Fin n → Bool)
(i : {i : ι // cover.branch i = b}) : ℝ :=
|∑ j, if x j ∈ cover.sets i.1 then
(if σ j then (1 : ℝ) else -1) * cover.weight b (x j) else 0|
have hW (b : Fin m) (σ : Fin n → Bool) :
BddAbove (range (W b σ)) := by
refine ⟨∑ j, |cover.weight b (x j)|, ?_⟩
rintro _ ⟨i, rfl⟩
refine (Finset.abs_sum_le_sum_abs _ _).trans (Finset.sum_le_sum ?_)
intro j _
split_ifs <;> simp
have hbranch (σ : Fin n → Bool) (b : Fin m) :
0 ≤ branchSignSup cover x σ b := by
change 0 ≤ iSup (W b σ)
cases isEmpty_or_nonempty {i : ι // cover.branch i = b} with
| inl h =>
let := h
simp
| inr h =>
let := h
exact le_ciSup_of_le (hW b σ) (Classical.arbitrary _) (abs_nonneg _)
have hm : (Finset.univ : Finset (Fin m)).Nonempty :=
⟨cover.branch (Classical.arbitrary ι), Finset.mem_univ _⟩
have hpoint (σ : Fin n → Bool) :
signedSup F.f x σ ^ 4 ≤
(n : ℝ)⁻¹ ^ 4 * ∑ b, branchSignSup cover x σ b ^ 4 := by
let M := Finset.univ.sup' hm (branchSignSup cover x σ)
have hleM (b : Fin m) : branchSignSup cover x σ b ≤ M :=
Finset.le_sup' _ (Finset.mem_univ b)
have hclass (i : ι) :
|(n : ℝ)⁻¹ * ∑ j, (if σ j then (1 : ℝ) else -1) * F.f i (x j)| ≤
(n : ℝ)⁻¹ * M := by
have hsum : (∑ j, (if σ j then (1 : ℝ) else -1) * F.f i (x j)) =
∑ j, if x j ∈ cover.sets i then
(if σ j then (1 : ℝ) else -1) * cover.weight (cover.branch i) (x j)
else 0 := by
apply Finset.sum_congr rfl
intro j _
rw [cover.represents i]
by_cases h : x j ∈ cover.sets i <;> simp [indicator, h]
rw [hsum, abs_mul, abs_of_nonneg (by positivity : 0 ≤ (n : ℝ)⁻¹)]
apply mul_le_mul_of_nonneg_left _ (by positivity)
exact (le_ciSup (hW (cover.branch i) σ) ⟨i, rfl⟩).trans
(hleM (cover.branch i))
have hsup : signedSup F.f x σ ≤ (n : ℝ)⁻¹ * M := ciSup_le hclass
have hsup0 : 0 ≤ signedSup F.f x σ :=
le_ciSup_of_le ⟨(n : ℝ)⁻¹ * M, by rintro _ ⟨i, rfl⟩; exact hclass i⟩
(Classical.arbitrary ι) (abs_nonneg _)
obtain ⟨b, _, hb⟩ := Finset.exists_mem_eq_sup' hm (branchSignSup cover x σ)
have hM4 : M ^ 4 ≤ ∑ b, branchSignSup cover x σ b ^ 4 := by
rw [show M = branchSignSup cover x σ b from hb]
exact Finset.single_le_sum (f := fun b => branchSignSup cover x σ b ^ 4)
(fun b _ => pow_nonneg (hbranch σ b) 4) (Finset.mem_univ b)
calc
signedSup F.f x σ ^ 4 ≤ ((n : ℝ)⁻¹ * M) ^ 4 :=
pow_le_pow_left₀ hsup0 hsup 4
_ = (n : ℝ)⁻¹ ^ 4 * M ^ 4 := mul_pow _ _ _
_ ≤ (n : ℝ)⁻¹ ^ 4 * ∑ b, branchSignSup cover x σ b ^ 4 :=
mul_le_mul_of_nonneg_left hM4 (by positivity)
calc
signAverage (fun σ => signedSup F.f x σ ^ 4) ≤
signAverage (fun σ => (∑ b, branchSignSup cover x σ b ^ 4) *
(n : ℝ)⁻¹ ^ 4) :=
signAverage_mono _ _ (fun σ => by simpa [mul_comm] using hpoint σ)
_ = (n : ℝ)⁻¹ ^ 4 * ∑ b, signAverage (fun σ => branchSignSup cover x σ b ^ 4) := by
rw [signAverage_mul_const, signAverage_sum]
simp only [mul_comm]
OneSidedSkeleton 3 core · 1 supporting A deterministic eligibility set need not be open or have a continuous loss. ★ exists_countable_oneSided_skeleton
Countable one-sided skeletons inside arbitrary real subsets
A deterministic eligibility set need not be open or have a continuous loss. Choose a countable dense subset of that set and adjoin its points isolated on the required side. Those boundary representatives are countable by Mathlib's countable_setOfPred_isolated_left_within/right_within. Approximation stays inside eligibility, even at a closed localization boundary.
def OneSidedApproximates reviewed
⚑ flagged
Causalean.Stat.EmpiricalProcess.Countable
A sequence of cutoffs one-sidedly approximates a cutoff t from the side selected by a Boolean flag when every term lies at or above t if the flag is true, or at or below t if it is false, and the sequence converges to t.
def oneSidedBoundary reviewed
⚑ flagged
Causalean.Stat.EmpiricalProcess.Countable
The one-sided boundary of a set T of eligible cutoffs, on the side selected by a Boolean flag, is the set of points of T that are isolated from the points of T strictly above them (flag true) or strictly below them (flag false).
theorem exists_countable_oneSided_skeleton reviewed
⚑ flagged
Causalean.Stat.EmpiricalProcess.Countable
Every set T of reals has a countable subset that contains its one-sided boundary and approximates every point of T, from the selected side, by a sequence lying entirely in that subset.
Formal statement
hypotheses
conclusion
∃ D : Set ℝ,
Proof (Lean source)
theorem exists_countable_oneSided_skeleton (upper : Bool) (T : Set ℝ) :
∃ D : Set ℝ, D.Countable ∧ D ⊆ T ∧ oneSidedBoundary upper T ⊆ D ∧
∀ t ∈ T, ∃ s : ℕ → ℝ, (∀ k, s k ∈ D) ∧ OneSidedApproximates upper s t := by
classical
obtain ⟨C, hCT, hC, hTC⟩ :=
(TopologicalSpace.IsSeparable.of_separableSpace T).exists_countable_dense_subset
refine ⟨C ∪ oneSidedBoundary upper T,
hC.union (oneSidedBoundary_countable upper T), ?_, subset_union_right, ?_⟩
· rintro x (hx | hx)
· exact hCT hx
· exact hx.1
· intro t ht
by_cases hb : t ∈ oneSidedBoundary upper T
· refine ⟨fun _ => t, fun _ => inr hb, ?_, tendsto_const_nhds⟩
intro k
cases upper <;> exact le_rfl
· let U : Set ℝ := if upper then Ioi t else Iio t
have hU : IsOpen U := by
cases upper <;> simp [U, isOpen_Iio, isOpen_Ioi]
have hn : nhdsWithin t (T ∩ U) ≠ ⊥ := by
intro h
exact hb ⟨ht, h⟩
have hcl : t ∈ closure (T ∩ U) :=
mem_closure_iff_nhdsWithin_neBot.mpr ⟨hn⟩
have hsub : T ∩ U ⊆ closure (C ∩ U) := by
intro x hx
exact hU.closure_inter ⟨hTC hx.1, hx.2⟩
have hd : t ∈ closure (C ∩ U) :=
(closure_minimal hsub isClosed_closure) hcl
obtain ⟨s, hs, hst⟩ := mem_closure_iff_seq_limit.mp hd
refine ⟨s, fun k => inl (hs k).1, ?_, hst⟩
intro k
have hk := (hs k).2
cases upper <;> exact le_of_lt hk
1 supporting declaration (lemmas, instances)
-
oneSidedBoundary_countabletheorem — The one-sided boundary of any set of reals, on either side, is countable.Proof (Lean source)
theorem oneSidedBoundary_countable (upper : Bool) (T : Set ℝ) : (oneSidedBoundary upper T).Countable := by cases upper · exact countable_setOfPred_isolated_left_within · exact countable_setOfPred_isolated_right_within
PrefixProbability 6 core · 6 supporting The uniform probability law on Boolean sign vectors represents the exact finite sign average. ★ signedPrefixProcess_martingale
The finite sign experiment and its reveal martingale
The uniform probability law on Boolean sign vectors represents the exact finite sign average. Mathlib's piFinset filtration reveals the first k signs. Signed partial sums, held constant after all signs are revealed, form a real martingale. The measure conversion, adaptedness, and zero conditional increment are isolated before the Doob application in FiniteSigns.
Reuse leads: PMF.uniformOfFintype, Filtration.piFinset, and martingale_of_condExp_sub_eq_zero_nat. Causalean's design-based prefixCondExp_ae_eq_condExp is an alternative finite-conditioning bridge.
def signedPrefix reviewed
⚑ flagged
Causalean.Stat.EmpiricalProcess.Countable
The signed prefix of a coefficient vector a under a sign vector σ at time k between 0 and n is the signed sum of the first k coefficients, Σ_(j < k) σ_j a_j; it is zero at time zero and the full signed sum at time n.
def signedPrefixMax reviewed
⚑ flagged
Causalean.Stat.EmpiricalProcess.Countable
The signed prefix maximum of a coefficient vector a under a sign vector σ is the largest absolute signed prefix over times 0 through n, including both the empty prefix and the full sum.
Definition (Lean source)
def signLaw reviewed
⚑ flagged
Causalean.Stat.EmpiricalProcess.Countable
The sign law for length n is the uniform probability law on all Boolean sign vectors of length n, including the single empty vector when n is zero.
def signedPrefixProcess reviewed
⚑ flagged
Causalean.Stat.EmpiricalProcess.Countable
The signed prefix process of a coefficient vector a at a natural time k under a sign vector σ is the signed sum Σ_(j < k) σ_j a_j of the coefficients with index below k; it stays constant from time n onward.
def signRevealFiltration reviewed
⚑ flagged
Causalean.Stat.EmpiricalProcess.Countable
The sign reveal filtration on sign vectors of length n is the filtration whose information at time k consists exactly of the signs with index below k.
Definition (Lean source)
parameters
n :
ℕ
def
given by
clause 1
clause 2
mono' := by intro k l hkl apply (Filtration.piFinset (X := fun _ : Fin n => Bool)).mono intro j hj simp only [mem_filter] at hj ⊢ exact ⟨hj.1, lt_of_lt_of_le hj.2 hkl⟩
clause 3
le' k := Filtration.le _ _
theorem signedPrefixProcess_martingale reviewed
⚑ flagged
Causalean.Stat.EmpiricalProcess.Countable
For any coefficient vector, the signed prefix process is a martingale for the sign reveal filtration under the uniform sign law.
Formal statement
Proof (Lean source)
theorem signedPrefixProcess_martingale {n : ℕ} (a : Fin n → ℝ) :
Martingale (signedPrefixProcess a) (signRevealFiltration n) (signLaw n) := by
exact martingale_of_condExp_sub_eq_zero_nat
(signedPrefixProcess_stronglyAdapted a)
(fun k => (signLaw_integral (signedPrefixProcess a k)).1)
(signedPrefixProcess_condExp_increment a)
6 supporting declarations (lemmas, instances)
-
signLaw_isProbabilityMeasureinstance — The uniform sign law of any length n is a probability measure.parametersn :ℕinstancegiven by -
signLaw_integraltheorem — Every real function of sign vectors is integrable under the sign law, and its integral equals its uniform sign average.hypothesesProof (Lean source)
theorem signLaw_integral {n : ℕ} (H : (Fin n → Bool) → ℝ) : Integrable H (signLaw n) ∧ (∫ σ, H σ ∂signLaw n) = signAverage H := by classical have hH : Integrable H (signLaw n) := Integrable.of_finite refine ⟨hH, ?_⟩ rw [integral_fintype hH] simp only [signLaw, measureReal_def, PMF.toMeasure_apply_singleton _ _ (measurableSet_singleton _), PMF.uniformOfFintype_apply, ENNReal.toReal_inv, Fintype.card_fun, Fintype.card_bool, Fintype.card_fin, Nat.cast_pow, Nat.cast_ofNat, smul_eq_mul, signAverage, div_eq_mul_inv] rw [← Finset.mul_sum, mul_comm] simp -
signedPrefixProcess_eqtheorem — At every time between 0 and n the signed prefix process agrees with the signed prefix.hypothesesconclusionsignedPrefixProcess a k σ = signedPrefix a σ kProof (Lean source)
theorem signedPrefixProcess_eq {n : ℕ} (a : Fin n → ℝ) (k : Fin (n + 1)) (σ : Fin n → Bool) : signedPrefixProcess a k σ = signedPrefix a σ k := rfl -
signedPrefixProcess_terminaltheorem — At time n the signed prefix process equals the full signed sum.hypothesesconclusionsignedPrefixProcess a n σ = ∑ j, (if σ j then (1 : ℝ) else -1) * a jProof (Lean source)
theorem signedPrefixProcess_terminal {n : ℕ} (a : Fin n → ℝ) (σ : Fin n → Bool) : signedPrefixProcess a n σ = ∑ j, (if σ j then (1 : ℝ) else -1) * a j := by simp only [signedPrefixProcess, Fin.is_lt, ite_true] -
signedPrefixProcess_stronglyAdaptedtheorem — For any coefficient vector, the signed prefix process is adapted to the sign reveal filtration.Proof (Lean source)
theorem signedPrefixProcess_stronglyAdapted {n : ℕ} (a : Fin n → ℝ) : StronglyAdapted (signRevealFiltration n) (signedPrefixProcess a) := by classical intro k unfold signedPrefixProcess apply Finset.stronglyMeasurable_fun_sum intro j _ by_cases hj : j.val < k · simp only [hj, ite_true] let s := Finset.univ.filter (fun j : Fin n => j.val < k) have hmem : j ∈ s := by simp [s, hj] have hev : Measurable[(signRevealFiltration n) k] (fun σ : Fin n → Bool => σ j) := (measurable_pi_apply (⟨j, hmem⟩ : s)).comp (comap_measurable s.restrict) exact ((measurable_of_finite (fun b : Bool => if b then (1 : ℝ) else -1)).comp hev).stronglyMeasurable.mul_const (a j) · simp only [hj, ite_false] exact stronglyMeasurable_const -
signedPrefixProcess_condExp_incrementtheorem — For any coefficient vector and any time k, the increment of the signed prefix process from time k to k + 1 has conditional expectation zero, almost surely under the sign law, given the signs revealed by time k, also after the terminal time.hypothesesconclusion=ᵐ[signLaw n] 0Proof (Lean source)
theorem signedPrefixProcess_condExp_increment {n : ℕ} (a : Fin n → ℝ) (k : ℕ) : (signLaw n)[signedPrefixProcess a (k + 1) - signedPrefixProcess a k | (signRevealFiltration n) k] =ᵐ[signLaw n] 0 := by classical by_cases hk : k < n · let i : Fin n := ⟨k, hk⟩ let f : (Fin n → Bool) → ℝ := fun σ => (if σ i then 1 else -1) * a i have hinc : signedPrefixProcess a (k + 1) - signedPrefixProcess a k = f := by funext σ change (∑ j : Fin n, if j.val < k + 1 then (if σ j then (1 : ℝ) else -1) * a j else 0) - (∑ j : Fin n, if j.val < k then (if σ j then (1 : ℝ) else -1) * a j else 0) = f σ rw [← Finset.sum_sub_distrib] rw [Finset.sum_eq_single i] · simp [i, f] · intro j _ hji have hjk : j.val ≠ k := fun h => hji (Fin.ext h) by_cases hj : j.val < k · simp [hj, Nat.lt_succ_of_lt hj] · have hj' : ¬j.val < k + 1 := by omega simp [hj, hj'] · simp rw [hinc] let flip : (Fin n → Bool) → (Fin n → Bool) := fun σ j => if j = i then !(σ j) else σ j have hflip : Involutive flip := by intro σ funext j by_cases hj : j = i <;> simp [flip, hj] let e := hflip.toPerm flip have hm := (signRevealFiltration n).le k apply (ae_eq_condExp_of_forall_setIntegral_eq hm (signLaw_integral f).1 (fun _ _ _ => integrable_zero _ _ _) ?_ stronglyMeasurable_zero.aestronglyMeasurable).symm intro s hs _ have hmem : ∀ σ, flip σ ∈ s ↔ σ ∈ s := by change MeasurableSet[MeasurableSpace.pi.comap (Finset.univ.filter (fun j : Fin n => j.val < k)).restrict] s at hs obtain ⟨t, _, rfl⟩ := hs intro σ have heq : (Finset.univ.filter (fun j : Fin n => j.val < k)).restrict (flip σ) = (Finset.univ.filter (fun j : Fin n => j.val < k)).restrict σ := by funext j have hj : j.val ≠ i := by intro h have hjlt := (Finset.mem_filter.mp j.property).2 simp [h, i] at hjlt simp [Finset.restrict, flip, hj] change (_ ∈ t ↔ _ ∈ t) rw [heq] have hneg : ∀ σ, s.indicator f (e σ) = -s.indicator f σ := by intro σ have hf : f (flip σ) = -f σ := by simp only [f, flip, ite_true] cases σ i <;> simp by_cases hσ : σ ∈ s · change s.indicator f (flip σ) = -s.indicator f σ simp only [Set.indicator_of_mem hσ, Set.indicator_of_mem ((hmem σ).2 hσ)] exact hf · have hσ' : flip σ ∉ s := fun h => hσ ((hmem σ).1 h) simp [show e σ = flip σ from rfl, hσ, hσ'] have hsum : ∑ σ, s.indicator f σ = 0 := by have he := Equiv.sum_comp e (s.indicator f) simp only [hneg, Finset.sum_neg_distrib] at he linarith simp only [Pi.zero_apply, integral_zero] rw [← integral_indicator (hm s hs), (signLaw_integral (s.indicator f)).2] simp [signAverage, hsum] · have hinc : signedPrefixProcess a (k + 1) - signedPrefixProcess a k = 0 := by funext σ have hj : ∀ j : Fin n, j.val < k := fun j => lt_of_lt_of_le j.is_lt (by omega) simp [signedPrefixProcess, hj, fun j => Nat.lt_succ_of_lt (hj j)] rw [hinc, condExp_zero]
ChainUnion 1 core · 0 supporting Localization on every member of a countable nested chain passes to its containing union without loss in the population mass budget. ★ countable_chain_union_mass_le
Population mass of a countable nested union
Localization on every member of a countable nested chain passes to its containing union without loss in the population mass budget. This is the bridge needed before using an energy bound on that union. The empty chain is included by requiring the budget to be nonnegative.
theorem countable_chain_union_mass_le reviewed
⚑ flagged
Causalean.Stat.EmpiricalProcess.Countable
Let a countable family of sets be measurable and nested, any two members being comparable by inclusion, and let a weight g be integrable under μ and nonnegative. If a nonnegative budget L bounds the integral of g over every member, then the union of the family is measurable and the integral of g over the union is at most L.
Formal statement
hypotheses
Ω ι :
μ :
Measure Ω
B :
ι → Set Ω
hB :
∀ i, MeasurableSet (B i)
hchain :
∀ i k, B i ⊆ B k ∨ B k ⊆ B i
g :
Ω → ℝ
hg :
Integrable g μ
hpos :
∀ x, 0 ≤ g x
L :
ℝ
hL :
0 ≤ L
hbudget :
∀ i, (∫ x in B i, g x ∂μ) ≤ L
Proof (Lean source)
theorem countable_chain_union_mass_le {Ω ι : Type*} [MeasurableSpace Ω]
[Countable ι] (μ : Measure Ω) (B : ι → Set Ω)
(hB : ∀ i, MeasurableSet (B i))
(hchain : ∀ i k, B i ⊆ B k ∨ B k ⊆ B i)
(g : Ω → ℝ) (hg : Integrable g μ) (hpos : ∀ x, 0 ≤ g x)
(L : ℝ) (hL : 0 ≤ L) (hbudget : ∀ i, (∫ x in B i, g x ∂μ) ≤ L) :
MeasurableSet (⋃ i, B i) ∧ (∫ x in ⋃ i, B i, g x ∂μ) ≤ L := by
refine ⟨MeasurableSet.iUnion hB, ?_⟩
have hd : Directed (· ⊆ ·) B := by
intro i k
rcases hchain i k with h | h
· exact ⟨k, h, Subset.rfl⟩
· exact ⟨i, Subset.rfl, h⟩
have hb : (∫⁻ x in ⋃ i, B i, ofReal (g x) ∂μ) ≤ ofReal L := by
rw [setLIntegral_iUnion_of_directed _ hd]
refine iSup_le fun i => ?_
rw [← ofReal_integral_eq_lintegral_ofReal hg.integrableOn
(Filter.Eventually.of_forall hpos)]
exact ENNReal.ofReal_le_ofReal (hbudget i)
rw [integral_eq_lintegral_of_nonneg_ae (Filter.Eventually.of_forall hpos)
hg.integrableOn.aestronglyMeasurable]
exact (ENNReal.toReal_mono ENNReal.ofReal_ne_top hb).trans_eq
(ENNReal.toReal_ofReal hL)
Composition 1 core · 3 supporting A bounded class can be partitioned into finitely many nested weighted indicator branches with cutoff-independent weights on each branch. ★ centered_fourth_le_energy_budget
From countable symmetrization to chain energy budgets
A bounded class can be partitioned into finitely many nested weighted indicator branches with cutoff-independent weights on each branch. The fourth power of its signed supremum is bounded by the sum of branch fourth powers, so no extra cube of the number of branches is necessary.
The final constant is 16*(256/27)=4096/27, followed by normalization by the fourth power of sample size and the sum of branch energy budgets. A five-branch specialization records the corresponding explicit arithmetic constant.
theorem centered_fourth_le_energy_budget reviewed
⚑ flagged
Causalean.Stat.EmpiricalProcess.Countable
Let a nonempty countable bounded class have a finite nested chain cover, let the sample consist of n independent draws from a probability measure μ with n positive, and suppose each squared branch energy is integrable under the sample law with expectation at most a branch budget. Then the fourth moment of the centered supremum is at most 4096/27 divided by n^4 times the sum of the budgets.
Formal statement
hypotheses
Ω ι :
μ :
F :
BoundedClass Ω ι
m :
ℕ
cover :
ChainCover F m
n :
ℕ
hn :
0 < n
henergy :
∀ b,
budget :
Fin m → ℝ
hbudget :
∀ b,
conclusion
(∫ x, centeredSup μ F.f x ^ 4 ∂Measure.pi (fun _ : Fin n => μ))
≤ ((4096 / 27 : ℝ) / (n : ℝ)^4) * ∑ b, budget b
Proof (Lean source)
theorem centered_fourth_le_energy_budget {Ω ι : Type*} [MeasurableSpace Ω]
[Countable ι] [Nonempty ι] (μ : Measure Ω) [IsProbabilityMeasure μ]
(F : BoundedClass Ω ι) {m : ℕ} (cover : ChainCover F m) (n : ℕ) (hn : 0 < n)
(henergy : ∀ b, Integrable (fun x : Fin n → Ω => coverEnergy cover x b ^ 2)
(Measure.pi (fun _ : Fin n => μ))) (budget : Fin m → ℝ)
(hbudget : ∀ b, (∫ x : Fin n → Ω, coverEnergy cover x b ^ 2
∂Measure.pi (fun _ : Fin n => μ)) ≤ budget b) :
(∫ x, centeredSup μ F.f x ^ 4 ∂Measure.pi (fun _ : Fin n => μ)) ≤
((4096 / 27 : ℝ) / (n : ℝ)^4) * ∑ b, budget b := by
exact (centered_fourth_le_coverEnergy μ F cover n hn henergy).trans
(mul_le_mul_of_nonneg_left (Finset.sum_le_sum (fun b _ => hbudget b))
(by positivity))
3 supporting declarations (lemmas, instances)
-
signedSup_fourth_le_coverEnergytheorem — For a nonempty countable bounded class with a finite nested chain cover and any sample of size n, the sign average of the fourth power of the signed supremum is at most 256/27 divided by n^4 times the sum over branches of the squared branch energies.hypothesesconclusionsignAverage (fun σ => signedSup F.f x σ ^ 4)≤ ((256 / 27 : ℝ) / (n : ℝ)^4) * ∑ b, coverEnergy cover x b ^ 2Proof (Lean source)
theorem signedSup_fourth_le_coverEnergy {Ω ι : Type*} [MeasurableSpace Ω] [Countable ι] [Nonempty ι] (F : BoundedClass Ω ι) {m : ℕ} (cover : ChainCover F m) {n : ℕ} (x : Fin n → Ω) : signAverage (fun σ => signedSup F.f x σ ^ 4) ≤ ((256 / 27 : ℝ) / (n : ℝ)^4) * ∑ b, coverEnergy cover x b ^ 2 := by have hbranch (b : Fin m) : signAverage (fun σ => branchSignSup cover x σ b ^ 4) ≤ (256 / 27 : ℝ) * coverEnergy cover x b ^ 2 := by apply nested_chain_fourth_le_energy (fun i : {i : ι // cover.branch i = b} => cover.sets i.1) (fun i k => cover.nested i.1 k.1 (i.2.trans k.2.symm)) (cover.containing b) intro i simpa only [i.2] using cover.subset_containing i.1 calc _ ≤ (n : ℝ)⁻¹ ^ 4 * ∑ b, signAverage (fun σ => branchSignSup cover x σ b ^ 4) := signedSup_fourth_le_chainAverages F cover x _ ≤ (n : ℝ)⁻¹ ^ 4 * ∑ b, (256 / 27 : ℝ) * coverEnergy cover x b ^ 2 := mul_le_mul_of_nonneg_left (Finset.sum_le_sum (fun b _ => hbranch b)) (by positivity) _ = _ := by rw [← Finset.mul_sum, inv_pow]; ring -
centered_fourth_le_coverEnergytheorem — Let a nonempty countable bounded class have a finite nested chain cover, let the sample consist of n independent draws from a probability measure μ with n positive, and suppose each squared branch energy is integrable under the sample law. Then the fourth moment of the centered supremum is at most 4096/27 divided by n^4 times the sum over branches of the expected squared branch energies.hypothesesconclusion(∫ x, centeredSup μ F.f x ^ 4 ∂Measure.pi (fun _ : Fin n => μ))≤ ((4096 / 27 : ℝ) / (n : ℝ)^4) * ∑ b, ∫ x : Fin n → Ω, coverEnergy cover x b ^ 2 ∂Measure.pi (fun _ : Fin n => μ)Proof (Lean source)
theorem centered_fourth_le_coverEnergy {Ω ι : Type*} [MeasurableSpace Ω] [Countable ι] [Nonempty ι] (μ : Measure Ω) [IsProbabilityMeasure μ] (F : BoundedClass Ω ι) {m : ℕ} (cover : ChainCover F m) (n : ℕ) (hn : 0 < n) (henergy : ∀ b, Integrable (fun x : Fin n → Ω => coverEnergy cover x b ^ 2) (Measure.pi (fun _ : Fin n => μ))) : (∫ x, centeredSup μ F.f x ^ 4 ∂Measure.pi (fun _ : Fin n => μ)) ≤ ((4096 / 27 : ℝ) / (n : ℝ)^4) * ∑ b, ∫ x : Fin n → Ω, coverEnergy cover x b ^ 2 ∂Measure.pi (fun _ : Fin n => μ) := by have hlegal := (signedSup_legal μ F n).2.2 have hright : Integrable (fun x : Fin n → Ω => ((256 / 27 : ℝ) / (n : ℝ)^4) * ∑ b, coverEnergy cover x b ^ 2) (Measure.pi (fun _ : Fin n => μ)) := (integrable_finsetSum _ (fun b _ => henergy b)).const_mul _ have hbound := integral_mono hlegal hright (fun x => signedSup_fourth_le_coverEnergy F cover x) rw [integral_const_mul, integral_finsetSum _ (fun b _ => henergy b)] at hbound calc _ ≤ 16 * ∫ x, signAverage (fun σ => signedSup F.f x σ ^ 4) ∂Measure.pi (fun _ : Fin n => μ) := centered_fourth_le_rademacher μ F n hn _ ≤ 16 * (((256 / 27 : ℝ) / (n : ℝ)^4) * ∑ b, ∫ x : Fin n → Ω, coverEnergy cover x b ^ 2 ∂Measure.pi (fun _ : Fin n => μ)) := mul_le_mul_of_nonneg_left hbound (by norm_num) _ = _ := by ring -
five_branch_budget_arithmetictheorem — For a positive sample size n, a positive clipping level a, and a nonnegative radius z, 4096/27 divided by n^4, times five budgets each equal to 24 n z / a^3 + 36 n^2 z^2 / a^2, is at most 81920/3 times (z^2 / (n^2 a^2) + z / (n^3 a^3)).hypothesesn a z :ℝhn :0 < nha :0 < ahz :0 ≤ zconclusion((4096 / 27 : ℝ) / n ^ 4) * (5 * (24 * n * z / a ^ 3 + 36 * n ^ 2 * z ^ 2 / a ^ 2))≤ (81920 / 3 : ℝ) * (z ^ 2 / (n ^ 2 * a ^ 2) + z / (n ^ 3 * a ^ 3))Proof (Lean source)
theorem five_branch_budget_arithmetic (n a z : ℝ) (hn : 0 < n) (ha : 0 < a) (hz : 0 ≤ z) : ((4096 / 27 : ℝ) / n ^ 4) * (5 * (24 * n * z / a ^ 3 + 36 * n ^ 2 * z ^ 2 / a ^ 2)) ≤ (81920 / 3 : ℝ) * (z ^ 2 / (n ^ 2 * a ^ 2) + z / (n ^ 3 * a ^ 3)) := by have hzterm : 0 ≤ z / (n ^ 3 * a ^ 3) := by positivity calc _ = (81920 / 3 : ℝ) * (z ^ 2 / (n ^ 2 * a ^ 2)) + (163840 / 9 : ℝ) * (z / (n ^ 3 * a ^ 3)) := by field_simp [ne_of_gt hn, ne_of_gt ha] ring _ ≤ _ := by nlinarith
Doob 1 core · 3 supporting Mathlib's stopped-event weak maximal inequality combines with the mixed-moment layer-cake bridge and Holder at orders 4/3 and 4 to give the final martingale estimate with constant (4/3)^4 = 256/81. ★ doob_fourth_maximal
The fourth-moment Doob bridge
Mathlib's stopped-event weak maximal inequality combines with the mixed-moment layer-cake bridge and Holder at orders 4/3 and 4 to give the final martingale estimate with constant (4/3)^4 = 256/81. Reference: Fabrice Baudoin, "Lecture 11. Doob's martingale maximal inequalities", https://fabricebaudoin.blog/2012/04/10/lecture-11-doobs-martingale-maximal-inequalities/
theorem doob_fourth_maximal reviewed
⚑ flagged
Causalean.Stat.EmpiricalProcess.Countable
If a real discrete-time process f is a martingale for a filtration under a probability measure μ and has integrable fourth powers at every time up to a horizon N, then the fourth power of its maximal absolute value over times 0 through N is integrable, with expectation at most 256/81 times the expected fourth power of the terminal value f_N.
Formal statement
hypotheses
Ω :
Type*
μ :
ℱ :
Filtration ℕ m
f :
ℕ → Ω → ℝ
hf :
Martingale f ℱ μ
N :
ℕ
h4 :
∀ k ≤ N, Integrable (fun x => f k x ^ 4) μ
conclusion
conclusion 1
Integrable (fun x => (⨆ k : Fin (N + 1), |f k x|)^4) μ
conclusion 2
(∫ x, (⨆ k : Fin (N + 1), |f k x|)^4 ∂μ) ≤ (256 / 81 : ℝ) * ∫ x, f N x ^ 4 ∂μ
Proof (Lean source)
theorem doob_fourth_maximal {Ω : Type*} {m : MeasurableSpace Ω}
(μ : Measure Ω) [IsProbabilityMeasure μ] (ℱ : Filtration ℕ m)
(f : ℕ → Ω → ℝ) (hf : Martingale f ℱ μ) (N : ℕ)
(h4 : ∀ k ≤ N, Integrable (fun x => f k x ^ 4) μ) :
Integrable (fun x => (⨆ k : Fin (N + 1), |f k x|)^4) μ ∧
(∫ x, (⨆ k : Fin (N + 1), |f k x|)^4 ∂μ) ≤
(256 / 81 : ℝ) * ∫ x, f N x ^ 4 ∂μ := by
have habs : Submartingale (fun k x => |f k x|) ℱ μ := by
have heq : (fun k x => |f k x|) = f ⊔ -f := by
ext k x
exact abs_eq_max_neg
rw [heq]
exact hf.submartingale.sup hf.neg.submartingale
have h4abs (k : ℕ) (hk : k ≤ N) : Integrable (fun x => |f k x| ^ 4) μ := by
have heq : (fun x => |f k x| ^ 4) = (fun x => f k x ^ 4) := by
funext x
rw [← abs_pow, abs_of_nonneg (by positivity)]
rw [heq]
exact h4 k hk
obtain ⟨hi, hmix⟩ := doob_fourth_mixed μ ℱ _ habs (fun k x => abs_nonneg _) N h4abs
let A : Ω → ℝ := fun x => ⨆ k : Fin (N + 1), |f k x|
have hA (x : Ω) : 0 ≤ A x :=
(abs_nonneg (f 0 x)).trans
(le_ciSup (Finite.bddAbove_range (fun k : Fin (N + 1) => |f k x|))
(0 : Fin (N + 1)))
have hAm : Measurable A := (submartingale_max_fourth_legal μ ℱ _ habs N h4abs).1
have hBm : AEStronglyMeasurable (fun x => |f N x|) μ :=
((hf.stronglyMeasurable N).mono (ℱ.le N)).aestronglyMeasurable.norm
obtain ⟨_, hholder⟩ := fourth_moment_holder μ A (fun x => |f N x|) hA
(fun x => abs_nonneg _) hi (h4abs N le_rfl) hAm.aestronglyMeasurable hBm
have hterminal : (∫ x, |f N x| ^ 4 ∂μ) = ∫ x, f N x ^ 4 ∂μ := by
congr 1
funext x
rw [← abs_pow, abs_of_nonneg (by positivity)]
rw [hterminal] at hholder
refine ⟨hi, ?_⟩
let M : ℝ := ∫ x, A x ^ 4 ∂μ
let H : ℝ := ∫ x, A x ^ 3 * |f N x| ∂μ
let T : ℝ := ∫ x, f N x ^ 4 ∂μ
have hM : 0 ≤ M := integral_nonneg fun x => by positivity
have hH : 0 ≤ H := integral_nonneg fun x => mul_nonneg (pow_nonneg (hA x) _) (abs_nonneg _)
have hT : 0 ≤ T := integral_nonneg fun x => by positivity
change M ≤ (256 / 81 : ℝ) * T
change M ≤ (4 / 3 : ℝ) * H at hmix
change H ^ 4 ≤ M ^ 3 * T at hholder
by_cases hzero : M = 0
· rw [hzero]
positivity
· have hMpos : 0 < M := lt_of_le_of_ne hM (Ne.symm hzero)
have hp := pow_le_pow_left₀ hM hmix 4
have hc : M ^ 3 * M ≤ M ^ 3 * ((256 / 81 : ℝ) * T) := by
nlinarith only [hp, hholder]
exact le_of_mul_le_mul_left hc (pow_pos hMpos 3)
3 supporting declarations (lemmas, instances)
-
submartingale_max_fourth_legaltheorem — If a real process f is a submartingale for a filtration under a probability measure μ and its values at every time up to a horizon N have integrable fourth powers, then the running maximum of f over times 0 through N is measurable and has an integrable fourth power.hypothesesΩ :Type*μ :ℱ :Filtration ℕ mf :ℕ → Ω → ℝhf :Submartingale f ℱ μN :ℕh4 :∀ k ≤ N, Integrable (fun x => f k x ^ 4) μconclusionconclusion 1Measurable (fun x => ⨆ k : Fin (N + 1), f k x)conclusion 2Integrable (fun x => (⨆ k : Fin (N + 1), f k x)^4) μProof (Lean source)
theorem submartingale_max_fourth_legal {Ω : Type*} {m : MeasurableSpace Ω} (μ : Measure Ω) [IsProbabilityMeasure μ] (ℱ : Filtration ℕ m) (f : ℕ → Ω → ℝ) (hf : Submartingale f ℱ μ) (N : ℕ) (h4 : ∀ k ≤ N, Integrable (fun x => f k x ^ 4) μ) : Measurable (fun x => ⨆ k : Fin (N + 1), f k x) ∧ Integrable (fun x => (⨆ k : Fin (N + 1), f k x)^4) μ := by have hm (k : ℕ) : Measurable (f k) := (hf.stronglyMeasurable k).measurable.mono (ℱ.le k) le_rfl refine ⟨Measurable.iSup (fun k : Fin (N + 1) => hm k), ?_⟩ exact (finite_iSup_fourth_integrable μ (fun k : Fin (N + 1) => f k) (fun k => (hm k).aestronglyMeasurable) (fun k => h4 k (le_of_lt_succ k.isLt))).2 -
submartingale_max_tail_letheorem — If a real process f is a submartingale for a filtration under a probability measure μ and is nonnegative everywhere, then for any horizon N and any positive level t, t times the probability that the maximum of f over times 0 through N is at least t is at most the integral of the terminal value f_N over that event.hypothesesΩ :Type*μ :ℱ :Filtration ℕ mf :ℕ → Ω → ℝhf :Submartingale f ℱ μhpos :∀ k x, 0 ≤ f k xN :ℕt :ℝht :0 < tProof (Lean source)
theorem submartingale_max_tail_le {Ω : Type*} {m : MeasurableSpace Ω} (μ : Measure Ω) [IsProbabilityMeasure μ] (ℱ : Filtration ℕ m) (f : ℕ → Ω → ℝ) (hf : Submartingale f ℱ μ) (hpos : ∀ k x, 0 ≤ f k x) (N : ℕ) (t : ℝ) (ht : 0 < t) : t * μ.real {x | t ≤ ⨆ k : Fin (N + 1), f k x} ≤ ∫ x in {x | t ≤ ⨆ k : Fin (N + 1), f k x}, f N x ∂μ := by have hsup (x : Ω) : (range (N + 1)).sup' nonempty_range_add_one (fun k => f k x) = ⨆ k : Fin (N + 1), f k x := by apply le_antisymm · apply Finset.sup'_le intro k hk exact le_ciSup (Finite.bddAbove_range (fun k : Fin (N + 1) => f k x)) (⟨k, Finset.mem_range.mp hk⟩ : Fin (N + 1)) · apply ciSup_le intro k exact Finset.le_sup' (f := fun k => f k x) (Finset.mem_range.mpr k.isLt) have hw := maximal_ineq hf (show 0 ≤ f from hpos) (ε := ⟨t, ht.le⟩) N simp_rw [hsup] at hw have hreal := ENNReal.toReal_mono (by finiteness) hw rw [ENNReal.toReal_mul, ENNReal.toReal_ofReal (integral_nonneg (hpos N))] at hreal change t * μ.real {x | t ≤ ⨆ k : Fin (N + 1), f k x} ≤ ∫ x in {x | t ≤ ⨆ k : Fin (N + 1), f k x}, f N x ∂μ at hreal exact hreal -
doob_fourth_mixedtheorem — If a real process f is a submartingale for a filtration under a probability measure μ, is nonnegative everywhere, and has integrable fourth powers at every time up to a horizon N, then the fourth power of its maximum over times 0 through N is integrable, with expectation at most 4/3 times the expectation of the cube of that maximum times the terminal value f_N.hypothesesΩ :Type*μ :ℱ :Filtration ℕ mf :ℕ → Ω → ℝhf :Submartingale f ℱ μhpos :∀ k x, 0 ≤ f k xN :ℕh4 :∀ k ≤ N, Integrable (fun x => f k x ^ 4) μconclusionconclusion 1Integrable (fun x => (⨆ k : Fin (N + 1), f k x)^4) μProof (Lean source)
theorem doob_fourth_mixed {Ω : Type*} {m : MeasurableSpace Ω} (μ : Measure Ω) [IsProbabilityMeasure μ] (ℱ : Filtration ℕ m) (f : ℕ → Ω → ℝ) (hf : Submartingale f ℱ μ) (hpos : ∀ k x, 0 ≤ f k x) (N : ℕ) (h4 : ∀ k ≤ N, Integrable (fun x => f k x ^ 4) μ) : Integrable (fun x => (⨆ k : Fin (N + 1), f k x)^4) μ ∧ (∫ x, (⨆ k : Fin (N + 1), f k x)^4 ∂μ) ≤ (4 / 3 : ℝ) * ∫ x, (⨆ k : Fin (N + 1), f k x)^3 * f N x ∂μ := by obtain ⟨hm, hi⟩ := submartingale_max_fourth_legal μ ℱ f hf N h4 have hmax (x : Ω) : 0 ≤ ⨆ k : Fin (N + 1), f k x := (hpos 0 x).trans (le_ciSup (Finite.bddAbove_range (fun k : Fin (N + 1) => f k x)) (0 : Fin (N + 1))) refine ⟨hi, weak_fourth_mixed μ _ (f N) hmax (hpos N) hm ((hf.stronglyMeasurable N).mono (ℱ.le N)).aestronglyMeasurable hi (h4 N le_rfl) ?_⟩ exact fun t ht => submartingale_max_tail_le μ ℱ f hf hpos N t ht
FiniteAverage 1 core · 3 supporting The exact finite uniform average is nonnegative, order preserving, and linear. ★ signAverage_mono
Algebra of finite sign averages
The exact finite uniform average is nonnegative, order preserving, and linear. These bridges require no probability-space encoding of signs.
theorem signAverage_mono reviewed
⚑ flagged
Causalean.Stat.EmpiricalProcess.Countable
If a real function H of sign vectors is at most another such function K at every sign vector, then the sign average of H is at most the sign average of K.
Formal statement
hypotheses
conclusion
signAverage H ≤ signAverage K
Proof (Lean source)
theorem signAverage_mono {n : ℕ} (H K : (Fin n → Bool) → ℝ)
(h : ∀ σ, H σ ≤ K σ) : signAverage H ≤ signAverage K := by
exact div_le_div_of_nonneg_right (Finset.sum_le_sum (fun σ _ => h σ))
(by positivity)
3 supporting declarations (lemmas, instances)
-
signAverage_nonnegtheorem — If a real function of sign vectors is nonnegative at every sign vector, then its uniform sign average is nonnegative.Proof (Lean source)
theorem signAverage_nonneg {n : ℕ} (H : (Fin n → Bool) → ℝ) (hH : ∀ σ, 0 ≤ H σ) : 0 ≤ signAverage H := by exact div_nonneg (Finset.sum_nonneg (fun σ _ => hH σ)) (by positivity) -
signAverage_mul_consttheorem — The sign average of a function of sign vectors multiplied by a real constant equals the constant times its sign average.hypothesesconclusionsignAverage (fun σ => H σ * c) = signAverage H * cProof (Lean source)
theorem signAverage_mul_const {n : ℕ} (H : (Fin n → Bool) → ℝ) (c : ℝ) : signAverage (fun σ => H σ * c) = signAverage H * c := by simp only [signAverage, ← Finset.sum_mul, div_mul_eq_mul_div] -
signAverage_sumtheorem — The sign average of a finite sum of functions of sign vectors equals the sum of their sign averages.hypothesesconclusionsignAverage (fun σ => ∑ k ∈ s, H k σ) = ∑ k ∈ s, signAverage (H k)Proof (Lean source)
theorem signAverage_sum {n : ℕ} {κ : Type*} (s : Finset κ) (H : κ → (Fin n → Bool) → ℝ) : signAverage (fun σ => ∑ k ∈ s, H k σ) = ∑ k ∈ s, signAverage (H k) := by simp only [signAverage, Finset.sum_div] exact Finset.sum_comm
FiniteSigns 1 core · 1 supporting The scalar fourth moment is exactly 3*(sum a^2)^2 - 2*sum a^4. ★ signedPrefixMax_fourth_le_energy
Finite Rademacher fourth moments and prefix maxima
The scalar fourth moment is exactly 3*(sum a^2)^2 - 2*sum a^4. Revealing independent Boolean signs gives a martingale, so the Doob bridge controls the absolute prefix maximum by 256/27 times squared energy. No maximal estimate is inferred merely from a scalar moment bound.
theorem signedPrefixMax_fourth_le_energy reviewed
⚑ flagged
Causalean.Stat.EmpiricalProcess.Countable
For a real coefficient vector a and independent uniform signs, the sign-average fourth power of the maximal absolute prefix of the signed sum is at most 256/27 times the square of the sum of squared coefficients, uniformly in the dimension.
Formal statement
hypotheses
n :
ℕ
a :
Fin n → ℝ
conclusion
signAverage (fun σ => signedPrefixMax a σ ^ 4) ≤ (256 / 27 : ℝ) * (∑ j, a j ^ 2)^2
Proof (Lean source)
theorem signedPrefixMax_fourth_le_energy {n : ℕ} (a : Fin n → ℝ) :
signAverage (fun σ => signedPrefixMax a σ ^ 4) ≤
(256 / 27 : ℝ) * (∑ j, a j ^ 2)^2 := by
have hterm : signAverage
(fun σ => (∑ j, (if σ j then (1 : ℝ) else -1) * a j)^4) ≤
3 * (∑ j, a j ^ 2)^2 := by
rw [signAverage_fourth_exact]
have hnonneg : 0 ≤ ∑ j, a j ^ 4 :=
Finset.sum_nonneg (fun j _ => by positivity)
linarith
calc
_ ≤ (256 / 81 : ℝ) * signAverage
(fun σ => (∑ j, (if σ j then (1 : ℝ) else -1) * a j)^4) :=
signedPrefixMax_fourth_le_terminal a
_ ≤ (256 / 81 : ℝ) * (3 * (∑ j, a j ^ 2)^2) :=
mul_le_mul_of_nonneg_left hterm (by positivity)
_ = (256 / 27 : ℝ) * (∑ j, a j ^ 2)^2 := by ring
1 supporting declaration (lemmas, instances)
-
signedPrefixMax_fourth_le_terminaltheorem — For a real coefficient vector a and independent uniform signs, the sign-average fourth power of the maximal absolute prefix of the signed sum is at most 256/81 times the sign-average fourth power of the full signed sum.hypothesesn :ℕa :Fin n → ℝconclusionsignAverage (fun σ => signedPrefixMax a σ ^ 4)≤ (256 / 81 : ℝ) * signAverage (fun σ => (∑ j, (if σ j then (1 : ℝ) else -1) * a j)^4)Proof (Lean source)
theorem signedPrefixMax_fourth_le_terminal {n : ℕ} (a : Fin n → ℝ) : signAverage (fun σ => signedPrefixMax a σ ^ 4) ≤ (256 / 81 : ℝ) * signAverage (fun σ => (∑ j, (if σ j then (1 : ℝ) else -1) * a j)^4) := by have h4 (k : ℕ) (_hk : k ≤ n) : Integrable (fun σ => signedPrefixProcess a k σ ^ 4) (signLaw n) := (signLaw_integral _).1 have hd := (doob_fourth_maximal (signLaw n) (signRevealFiltration n) (signedPrefixProcess a) (signedPrefixProcess_martingale a) n h4).2 have hmax (σ : Fin n → Bool) : (⨆ k : Fin (n + 1), |signedPrefixProcess a k σ|) = signedPrefixMax a σ := rfl simp_rw [hmax, signedPrefixProcess_terminal] at hd rw [(signLaw_integral (fun σ => signedPrefixMax a σ ^ 4)).2, (signLaw_integral (fun σ => (∑ j, (if σ j then (1 : ℝ) else -1) * a j)^4)).2] at hd exact hd
Ghost 1 core · 6 supporting The conditional Jensen comparison has constant one; coordinatewise exchange of two iid copies introduces independent signs without changing the product integral. ★ centered_fourth_le_rademacher
Fourth-moment ghost and Rademacher symmetrization
The conditional Jensen comparison has constant one; coordinatewise exchange of two iid copies introduces independent signs without changing the product integral. The fourth-power triangle inequality then gives constant sixteen. Reference: Moulinath Banerjee, "Empirical Processes: Symmetrization", October 12, 2010, Lemma 1.1 (the nondecreasing convex moment comparison): https://dept.stat.lsa.umich.edu/~moulib/emp-proc-notes-symmetrization.pdf FoML's first-moment symmetrization does not prove these fourth-moment claims.
theorem centered_fourth_le_rademacher reviewed
⚑ flagged
Causalean.Stat.EmpiricalProcess.Countable
For a uniformly bounded measurable class with a nonempty countable index set, a probability measure μ, and a positive sample size n, the expected fourth power of the centered supremum over an iid sample from μ is at most sixteen times the expected sign-average fourth power of the signed supremum: the fourth-moment Rademacher symmetrization inequality.
Formal statement
hypotheses
Ω :
Type u_1
ι :
Type u_2
n :
ℕ
hn :
0 < n
conclusion
(∫ x, centeredSup μ F.f x ^ 4 ∂Measure.pi (fun _ : Fin n => μ))
Proof (Lean source)
theorem centered_fourth_le_rademacher (n : ℕ) (hn : 0 < n) :
(∫ x, centeredSup μ F.f x ^ 4 ∂Measure.pi (fun _ : Fin n => μ)) ≤
16 * ∫ x, signAverage (fun σ => signedSup F.f x σ ^ 4)
∂Measure.pi (fun _ : Fin n => μ) := by
exact (centered_fourth_le_ghost_integral μ F n hn).trans
(ghost_fourth_le_rademacher μ F n)
6 supporting declarations (lemmas, instances)
-
integral_fourth_jensentheorem — Under a probability law, if a real function g is integrable and has an integrable fourth power, then the fourth power of the integral of g is at most the integral of its fourth power, by Jensen's inequality.hypothesesconclusion(∫ s, g s ∂ν)^4 ≤ ∫ s, g s ^ 4 ∂νProof (Lean source)
theorem integral_fourth_jensen {S : Type*} [MeasurableSpace S] (ν : Measure S) [IsProbabilityMeasure ν] (g : S → ℝ) (hg : Integrable g ν) (hg4 : Integrable (fun s => g s ^ 4) ν) : (∫ s, g s ∂ν)^4 ≤ ∫ s, g s ^ 4 ∂ν := by have hc : ConvexOn ℝ univ (fun x : ℝ => x ^ 4) := (show Even (4 : ℕ) from ⟨2, rfl⟩).convexOn_pow exact hc.map_integral_le (continuous_id.pow 4).continuousOn isClosed_univ (ae_of_all _ fun _ => Set.mem_univ _) hg hg4 -
centeredAverage_eq_ghost_integraltheorem — For a positive sample size n, any sample x, and any function of the class, the population-centered empirical average of that function equals the expectation, over an independent ghost sample y drawn from μ, of (1/n) Σ_j (f(x_j) − f(y_j)).hypothesesconclusioncenteredEmpiricalAverage μ x (F.f i)Proof (Lean source)
theorem centeredAverage_eq_ghost_integral (n : ℕ) (hn : 0 < n) (x : Fin n → Ω) (i : ι) : centeredEmpiricalAverage μ x (F.f i) = ∫ y : Fin n → Ω, (n : ℝ)⁻¹ * ∑ j, (F.f i (x j) - F.f i (y j)) ∂Measure.pi (fun _ : Fin n => μ) := by -- BoundedClass.integrable and the probability pi evaluation map make -- every summand integrable. Use integral_finsetSum, integral_sub, -- integral_const_mul, and integral_comp_eval. The n equal population -- integrals cancel the inverse sample-size normalization using hn. -- This is an identity for one function, not a supremum exchange. have hj (j : Fin n) : Integrable (fun y : Fin n → Ω => F.f i (x j) - F.f i (y j)) (Measure.pi (fun _ : Fin n => μ)) := (integrable_const _).sub (integrable_comp_eval (F.integrable μ i)) rw [integral_const_mul, integral_finsetSum _ (fun j _ => hj j)] have he (j : Fin n) : (∫ y : Fin n → Ω, F.f i (x j) - F.f i (y j) ∂Measure.pi (fun _ : Fin n => μ)) = F.f i (x j) - ∫ z, F.f i z ∂μ := by rw [integral_sub (integrable_const _) (integrable_comp_eval (μ := fun _ : Fin n => μ) (i := j) (F.integrable μ i)), integral_const, integral_comp_eval (F.measurable i).aestronglyMeasurable] simp simp_rw [he] unfold centeredEmpiricalAverage rw [Finset.sum_sub_distrib] have hn' : (n : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr (Nat.ne_of_gt hn) simp [Finset.sum_const, hn', mul_sub] -
centeredSup_fourth_le_ghosttheorem — For a positive sample size n and any fixed sample x, the fourth power of the centered supremum at x is at most the expected fourth power of the ghost supremum of x against an independent ghost sample drawn from μ.Proof (Lean source)
theorem centeredSup_fourth_le_ghost (n : ℕ) (hn : 0 < n) (x : Fin n → Ω) : centeredSup μ F.f x ^ 4 ≤ ∫ y, ghostSup F.f x y ^ 4 ∂Measure.pi (fun _ : Fin n => μ) := by -- For each index use centeredAverage_eq_ghost_integral, -- apply scalar Jensen, dominate by the ghost supremum, then take the -- bounded real supremum. No interchange of sup and expectation is asserted. let ν := Measure.pi (fun _ : Fin n => μ) let g (i : ι) (y : Fin n → Ω) : ℝ := (n : ℝ)⁻¹ * ∑ j, (F.f i (x j) - F.f i (y j)) have hb (y : Fin n → Ω) : BddAbove (range (fun i => |g i y|)) := by refine ⟨|(n : ℝ)⁻¹| * ∑ _ : Fin n, (2 * F.bound), ?_⟩ rintro _ ⟨i, rfl⟩ dsimp [g] rw [abs_mul] apply mul_le_mul_of_nonneg_left _ (abs_nonneg _) refine (Finset.abs_sum_le_sum_abs _ _).trans (Finset.sum_le_sum ?_) intro j _ exact (abs_sub _ _).trans (by have hx := F.bounded i (x j) have hy := F.bounded i (y j) linarith) have hle (i : ι) (y : Fin n → Ω) : |g i y| ≤ ghostSup F.f x y := le_ciSup (hb y) i have hm : Measurable (fun y : Fin n → Ω => ghostSup F.f x y) := by have hmap : Measurable (fun y : Fin n → Ω => (x, y)) := measurable_const.prodMk measurable_id simpa only [Function.comp_def] using (ghostSup_legal μ F n).1.comp hmap have hG : Integrable (fun y => ghostSup F.f x y ^ 4) ν := by apply Integrable.of_bound (hm.pow_const 4).aestronglyMeasurable ((2 * F.bound) ^ 4) apply ae_of_all intro y rw [Real.norm_eq_abs, abs_of_nonneg (pow_nonneg ((ghostSup_legal μ F n).2.1 x y).1 4)] exact pow_le_pow_left₀ ((ghostSup_legal μ F n).2.1 x y).1 ((ghostSup_legal μ F n).2.1 x y).2 4 unfold centeredSup rw [Real.iSup_pow (fun i => abs_nonneg _) 4] apply ciSup_le intro i have hg : Integrable (g i) ν := by apply Integrable.const_mul exact integrable_finsetSum _ fun j _ => (integrable_const _).sub (integrable_comp_eval (F.integrable μ i)) have hgm : Measurable (g i) := by dsimp [g] exact measurable_const.mul (Finset.measurable_sum _ fun j _ => measurable_const.sub ((F.measurable i).comp (measurable_pi_apply j))) have hp (y : Fin n → Ω) : g i y ^ 4 ≤ ghostSup F.f x y ^ 4 := by calc g i y ^ 4 = |g i y| ^ 4 := by rw [← abs_pow, abs_of_nonneg (by positivity)] _ ≤ ghostSup F.f x y ^ 4 := pow_le_pow_left₀ (abs_nonneg _) (hle i y) 4 have hg4 : Integrable (fun y => g i y ^ 4) ν := hG.mono' (hgm.pow_const 4).aestronglyMeasurable (ae_of_all _ fun y => by rw [Real.norm_eq_abs, abs_of_nonneg (by positivity)] exact hp y) calc |centeredEmpiricalAverage μ x (F.f i)| ^ 4 = (∫ y, g i y ∂ν) ^ 4 := by rw [centeredAverage_eq_ghost_integral μ F n hn x i, ← abs_pow, abs_of_nonneg (by positivity)] _ ≤ ∫ y, g i y ^ 4 ∂ν := integral_fourth_jensen ν (g i) hg hg4 _ ≤ ∫ y, ghostSup F.f x y ^ 4 ∂ν := integral_mono hg4 hG hp -
ghost_fourth_eq_signedGhosttheorem — For two independent samples of size n drawn from μ and any fixed sign vector σ, the expected fourth power of the ghost supremum equals the expected fourth power of the σ-signed ghost supremum, since swapping paired iid coordinates preserves the joint law.hypothesesΩ :sharedType u_1ι :sharedType u_2n :ℕProof (Lean source)
theorem ghost_fourth_eq_signedGhost (n : ℕ) (σ : Fin n → Bool) : (∫ p : (Fin n → Ω) × (Fin n → Ω), ghostSup F.f p.1 p.2 ^ 4 ∂((Measure.pi (fun _ : Fin n => μ)).prod (Measure.pi (fun _ : Fin n => μ)))) = ∫ p : (Fin n → Ω) × (Fin n → Ω), signedGhostSup F.f p.1 p.2 σ ^ 4 ∂((Measure.pi (fun _ : Fin n => μ)).prod (Measure.pi (fun _ : Fin n => μ))) := by have h := (pairedSampleSwap_measurePreserving μ σ).integral_comp' (fun p : (Fin n → Ω) × (Fin n → Ω) => ghostSup F.f p.1 p.2 ^ 4) simpa only [ghostSup_pairedSampleSwap] using h.symm -
centered_fourth_le_ghost_integraltheorem — For a positive sample size n, the expected fourth power of the centered supremum over an iid sample from μ is at most the expected fourth power of the ghost supremum over two independent iid samples, with constant one.hypothesesΩ :sharedType u_1ι :sharedType u_2n :ℕhn :0 < nProof (Lean source)
theorem centered_fourth_le_ghost_integral (n : ℕ) (hn : 0 < n) : (∫ x, centeredSup μ F.f x ^ 4 ∂Measure.pi (fun _ : Fin n => μ)) ≤ ∫ p : (Fin n → Ω) × (Fin n → Ω), ghostSup F.f p.1 p.2 ^ 4 ∂((Measure.pi (fun _ : Fin n => μ)).prod (Measure.pi (fun _ : Fin n => μ))) := by have hG := (ghostSup_legal μ F n).2.2 rw [integral_prod _ hG] exact integral_mono (centeredSup_legal μ F n).2.2 hG.integral_prod_left (fun x => centeredSup_fourth_le_ghost μ F n hn x) -
ghost_fourth_le_rademachertheorem — For any sample size n, the expected fourth power of the ghost supremum over two independent iid samples from μ is at most sixteen times the expected sign-average fourth power of the signed supremum of the class on one iid sample.hypothesesProof (Lean source)
theorem ghost_fourth_le_rademacher (n : ℕ) : (∫ p : (Fin n → Ω) × (Fin n → Ω), ghostSup F.f p.1 p.2 ^ 4 ∂((Measure.pi (fun _ : Fin n => μ)).prod (Measure.pi (fun _ : Fin n => μ)))) ≤ 16 * ∫ x, signAverage (fun σ => signedSup F.f x σ ^ 4) ∂Measure.pi (fun _ : Fin n => μ) := by classical let ν := Measure.pi (fun _ : Fin n => μ) have hs := signedSup_legal μ F n have hb (x : Fin n → Ω) (σ : Fin n → Bool) : BddAbove (range (fun i => |(n : ℝ)⁻¹ * ∑ j, (if σ j then (1 : ℝ) else -1) * F.f i (x j)|)) := by refine ⟨|(n : ℝ)⁻¹| * ∑ _ : Fin n, F.bound, ?_⟩ rintro _ ⟨i, rfl⟩ dsimp only rw [abs_mul] apply mul_le_mul_of_nonneg_left _ (abs_nonneg _) refine (Finset.abs_sum_le_sum_abs _ _).trans (Finset.sum_le_sum ?_) intro j _ have he : |(if σ j then (1 : ℝ) else -1) * F.f i (x j)| = |F.f i (x j)| := by cases σ j <;> simp rw [he] exact F.bounded i (x j) -- Compare each normalized signed difference before taking the supremum. have htriangle (x y : Fin n → Ω) (σ : Fin n → Bool) : signedGhostSup F.f x y σ ≤ signedSup F.f x σ + signedSup F.f y σ := by apply ciSup_le intro i have he : (n : ℝ)⁻¹ * ∑ j, (if σ j then (1 : ℝ) else -1) * (F.f i (x j) - F.f i (y j)) = (n : ℝ)⁻¹ * ∑ j, (if σ j then (1 : ℝ) else -1) * F.f i (x j) - (n : ℝ)⁻¹ * ∑ j, (if σ j then (1 : ℝ) else -1) * F.f i (y j) := by simp only [mul_sub, Finset.sum_sub_distrib] rw [he] exact (abs_sub _ _).trans (add_le_add (le_ciSup (hb x σ) i) (le_ciSup (hb y σ) i)) have hfourth (x y : Fin n → Ω) (σ : Fin n → Bool) : signedGhostSup F.f x y σ ^ 4 ≤ 8 * (signedSup F.f x σ ^ 4 + signedSup F.f y σ ^ 4) := by have hnonneg : 0 ≤ signedGhostSup F.f x y σ := by rw [← ghostSup_pairedSampleSwap F.f σ (x, y)] exact ((ghostSup_legal μ F n).2.1 _ _).1 exact (pow_le_pow_left₀ hnonneg (htriangle x y σ) 4).trans (by convert add_pow_le (hs.2.1 x σ).1 (hs.2.1 y σ).1 4 using 1; norm_num) have hi (σ : Fin n → Bool) : Integrable (fun x : Fin n → Ω => signedSup F.f x σ ^ 4) ν := by apply Integrable.of_bound ((hs.1 σ).pow_const 4).aestronglyMeasurable (F.bound ^ 4) apply ae_of_all intro x rw [Real.norm_eq_abs, abs_of_nonneg (pow_nonneg (hs.2.1 x σ).1 4)] exact pow_le_pow_left₀ (hs.2.1 x σ).1 (hs.2.1 x σ).2 4 have hfixed (σ : Fin n → Bool) : (∫ p : (Fin n → Ω) × (Fin n → Ω), ghostSup F.f p.1 p.2 ^ 4 ∂ν.prod ν) ≤ 16 * ∫ x, signedSup F.f x σ ^ 4 ∂ν := by rw [ghost_fourth_eq_signedGhost μ F n σ] calc _ ≤ ∫ p : (Fin n → Ω) × (Fin n → Ω), 8 * (signedSup F.f p.1 σ ^ 4 + signedSup F.f p.2 σ ^ 4) ∂ν.prod ν := integral_mono (signedGhostSup_legal μ F n σ).2.1 ((((hi σ).comp_fst ν).add ((hi σ).comp_snd ν)).const_mul 8) (fun p => hfourth p.1 p.2 σ) _ = 16 * ∫ x, signedSup F.f x σ ^ 4 ∂ν := by rw [integral_const_mul, integral_add ((hi σ).comp_fst ν) ((hi σ).comp_snd ν), integral_fun_fst (fun x => signedSup F.f x σ ^ 4), integral_fun_snd (fun x => signedSup F.f x σ ^ 4)] simp only [probReal_univ, one_smul] ring -- Average the swap comparisons, then commute the finite sum with the integral. have havg := signAverage_mono (fun _ : Fin n → Bool => ∫ p : (Fin n → Ω) × (Fin n → Ω), ghostSup F.f p.1 p.2 ^ 4 ∂ν.prod ν) (fun σ => 16 * ∫ x, signedSup F.f x σ ^ 4 ∂ν) hfixed have hconst (c : ℝ) : signAverage (fun _ : Fin n → Bool => c) = c := by simp [signAverage, Fintype.card_fin, Fintype.card_bool] have hlin : signAverage (fun σ => 16 * ∫ x, signedSup F.f x σ ^ 4 ∂ν) = 16 * ∫ x, signAverage (fun σ => signedSup F.f x σ ^ 4) ∂ν := by unfold signAverage rw [integral_div, integral_finsetSum _ (fun σ _ => hi σ)] rw [← Finset.mul_sum] ring rw [hconst, hlin] at havg exact havg
Holder 1 core · 2 supporting The fourth-power Holder inequality and finite-maximum moment legality are independent of martingales. ★ fourth_moment_holder
Mixed fourth moments
The fourth-power Holder inequality and finite-maximum moment legality are independent of martingales. They are the lowest analytic layer for Doob's inequality; neither assumes a maximal-moment estimate.
theorem fourth_moment_holder reviewed
⚑ flagged
Causalean.Stat.EmpiricalProcess.Countable
Under any measure μ, if two real functions A and B are nonnegative, almost everywhere strongly measurable, and have integrable fourth powers, then A^3·B is integrable and the fourth power of its integral is at most the cube of the integral of A^4 times the integral of B^4.
Formal statement
hypotheses
Ω :
Type*
μ :
Measure Ω
A B :
Ω → ℝ
hA :
∀ x, 0 ≤ A x
hB :
∀ x, 0 ≤ B x
hA4 :
Integrable (fun x => A x ^ 4) μ
hB4 :
Integrable (fun x => B x ^ 4) μ
hAm :
hBm :
conclusion
conclusion 1
Integrable (fun x => A x ^ 3 * B x) μ
conclusion 2
(∫ x, A x ^ 3 * B x ∂μ)^4 ≤ (∫ x, A x ^ 4 ∂μ)^3 * (∫ x, B x ^ 4 ∂μ)
Proof (Lean source)
theorem fourth_moment_holder {Ω : Type*} [MeasurableSpace Ω]
(μ : Measure Ω) (A B : Ω → ℝ) (hA : ∀ x, 0 ≤ A x) (hB : ∀ x, 0 ≤ B x)
(hA4 : Integrable (fun x => A x ^ 4) μ)
(hB4 : Integrable (fun x => B x ^ 4) μ)
(hAm : AEStronglyMeasurable A μ) (hBm : AEStronglyMeasurable B μ) :
Integrable (fun x => A x ^ 3 * B x) μ ∧
(∫ x, A x ^ 3 * B x ∂μ)^4 ≤
(∫ x, A x ^ 4 ∂μ)^3 * (∫ x, B x ^ 4 ∂μ) := by
have hA2 : Integrable (fun x => (A x ^ 2)^2) μ := by
simpa only [← pow_mul] using hA4
have hB2 : Integrable (fun x => (B x ^ 2)^2) μ := by
simpa only [← pow_mul] using hB4
have hAB2 : Integrable (fun x => (A x * B x)^2) μ := by
refine (hA4.add hB4).mono_nonneg ((hAm.mul hBm).pow 2)
(Filter.Eventually.of_forall fun x => sq_nonneg _) ?_
exact Filter.Eventually.of_forall fun x => by
change (A x * B x)^2 ≤ A x ^ 4 + B x ^ 4
nlinarith [sq_nonneg (A x ^ 2 - B x ^ 2)]
obtain ⟨hi, hc⟩ := integral_product_sq_le μ (fun x => A x ^ 2)
(fun x => A x * B x) (fun x => sq_nonneg _)
(fun x => mul_nonneg (hA x) (hB x)) (hAm.pow 2) (hAm.mul hBm) hA2 hAB2
obtain ⟨_, hd⟩ := integral_product_sq_le μ (fun x => A x ^ 2)
(fun x => B x ^ 2) (fun x => sq_nonneg _) (fun x => sq_nonneg _)
(hAm.pow 2) (hBm.pow 2) hA2 hB2
have heq : (fun x => A x ^ 2 * (A x * B x)) = (fun x => A x ^ 3 * B x) := by
funext x; ring
rw [heq] at hi hc
simp only [← pow_mul, mul_pow] at hc hd
refine ⟨hi, ?_⟩
have hs := pow_le_pow_left₀ (sq_nonneg (∫ x, A x ^ 3 * B x ∂μ)) hc 2
have ht := mul_le_mul_of_nonneg_left hd (sq_nonneg (∫ x, A x ^ 4 ∂μ))
calc
(∫ x, A x ^ 3 * B x ∂μ)^4 ≤
((∫ x, A x ^ 4 ∂μ) * (∫ x, A x ^ 2 * B x ^ 2 ∂μ))^2 := by
simpa only [← pow_mul] using hs
_ ≤ (∫ x, A x ^ 4 ∂μ)^3 * (∫ x, B x ^ 4 ∂μ) := by
nlinarith only [ht]
2 supporting declarations (lemmas, instances)
-
integral_product_sq_letheorem — Under any measure μ, if two real functions f and g are nonnegative, almost everywhere strongly measurable, and have integrable squares, then their product is integrable and the square of its integral is at most the product of the integrals of their squares.hypothesesΩ :Type*μ :Measure Ωf g :Ω → ℝhf :∀ x, 0 ≤ f xhg :∀ x, 0 ≤ g xhfm :hgm :hf2 :Integrable (fun x => f x ^ 2) μhg2 :Integrable (fun x => g x ^ 2) μconclusionconclusion 1Integrable (fun x => f x * g x) μconclusion 2(∫ x, f x * g x ∂μ)^2 ≤ (∫ x, f x ^ 2 ∂μ) * (∫ x, g x ^ 2 ∂μ)Proof (Lean source)
theorem integral_product_sq_le {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) (f g : Ω → ℝ) (hf : ∀ x, 0 ≤ f x) (hg : ∀ x, 0 ≤ g x) (hfm : AEStronglyMeasurable f μ) (hgm : AEStronglyMeasurable g μ) (hf2 : Integrable (fun x => f x ^ 2) μ) (hg2 : Integrable (fun x => g x ^ 2) μ) : Integrable (fun x => f x * g x) μ ∧ (∫ x, f x * g x ∂μ)^2 ≤ (∫ x, f x ^ 2 ∂μ) * (∫ x, g x ^ 2 ∂μ) := by have hfl := (memLp_two_iff_integrable_sq hfm).2 hf2 have hgl := (memLp_two_iff_integrable_sq hgm).2 hg2 have hprod : MemLp (fun x => f x * g x) 1 μ := hgl.mul' hfl refine ⟨(memLp_one_iff_integrable.mp hprod), ?_⟩ have h := integral_mul_le_Lp_mul_Lq_of_nonneg (p := 2) (q := 2) (by rw [Real.holderConjugate_iff]; norm_num) (Filter.Eventually.of_forall hf) (Filter.Eventually.of_forall hg) (by simpa using hfl) (by simpa using hgl) simp only [Real.rpow_two] at h rw [← Real.sqrt_eq_rpow, ← Real.sqrt_eq_rpow] at h have hn : 0 ≤ ∫ x, f x * g x ∂μ := integral_nonneg fun x => mul_nonneg (hf x) (hg x) have hn1 : 0 ≤ ∫ x, f x ^ 2 ∂μ := integral_nonneg fun x => sq_nonneg _ have hn2 : 0 ≤ ∫ x, g x ^ 2 ∂μ := integral_nonneg fun x => sq_nonneg _ have hs := pow_le_pow_left₀ hn h 2 rw [mul_pow, Real.sq_sqrt hn1, Real.sq_sqrt hn2] at hs exact hs -
finite_iSup_fourth_integrabletheorem — Under a measure μ, if a nonempty finite family of real functions consists of almost everywhere strongly measurable functions with integrable fourth powers, then their pointwise maximum is almost everywhere strongly measurable and has an integrable fourth power.hypothesesΩ ι :μ :Measure Ωf :ι → Ω → ℝhm :∀ i, AEStronglyMeasurable (f i) μh4 :∀ i, Integrable (fun x => f i x ^ 4) μconclusionconclusion 1AEStronglyMeasurable (fun x => ⨆ i, f i x) μconclusion 2Integrable (fun x => (⨆ i, f i x)^4) μProof (Lean source)
theorem finite_iSup_fourth_integrable {Ω ι : Type*} [MeasurableSpace Ω] [Finite ι] [Nonempty ι] (μ : Measure Ω) (f : ι → Ω → ℝ) (hm : ∀ i, AEStronglyMeasurable (f i) μ) (h4 : ∀ i, Integrable (fun x => f i x ^ 4) μ) : AEStronglyMeasurable (fun x => ⨆ i, f i x) μ ∧ Integrable (fun x => (⨆ i, f i x)^4) μ := by classical let := Fintype.ofFinite ι have hmax : AEStronglyMeasurable (fun x => ⨆ i, f i x) μ := (AEMeasurable.iSup fun i => (hm i).aemeasurable).aestronglyMeasurable refine ⟨hmax, ?_⟩ have hsum : Integrable (fun x => ∑ i, f i x ^ 4) μ := integrable_finsetSum _ fun i _ => h4 i refine hsum.mono_nonneg (hmax.pow 4) (Filter.Eventually.of_forall fun x => by positivity) ?_ exact Filter.Eventually.of_forall fun x => by obtain ⟨i, hi⟩ := exists_eq_ciSup_of_finite (f := fun i => f i x) rw [← hi] exact Finset.single_le_sum (f := fun j => f j x ^ 4) (fun j _ => by positivity) (Finset.mem_univ i)
NestedChain 1 core · 0 supporting An arbitrary nested set family has only finitely many distinct traces on a finite sample. ★ nested_chain_fourth_le_energy
Signed weighted nested chains
An arbitrary nested set family has only finitely many distinct traces on a finite sample. A permutation places all those traces among prefixes. Signs are invariant under that permutation, and restricting coefficients to a containing union yields the squared-energy estimate with constant 256/27. The indexing family may be infinite; no trace-complexity assumption is needed.
theorem nested_chain_fourth_le_energy reviewed
⚑ flagged
Causalean.Stat.EmpiricalProcess.Countable
If a family of sets is nested, any two members being comparable by inclusion, and every member lies in a containing set U, then for any sample and real sample weights, the sign-average fourth power of the chain supremum is at most 256/27 times the square of the chain energy in U.
Formal statement
Proof (Lean source)
theorem nested_chain_fourth_le_energy {Ω ι : Type*} (B : ι → Set Ω)
(hchain : ∀ i k, B i ⊆ B k ∨ B k ⊆ B i) (U : Set Ω)
(hU : ∀ i, B i ⊆ U) {n : ℕ} (x : Fin n → Ω) (w : Fin n → ℝ) :
signAverage (fun σ => chainSignSup B x w σ ^ 4) ≤
(256 / 27 : ℝ) * chainEnergy U x w ^ 2 := by
-- Use nested_trace_prefix and replace w by its restriction to U.
-- Each chain sum is a prefix sum of the restricted permuted coefficients.
-- Reindex all Boolean signs by p and apply signedPrefixMax_fourth_le_energy.
-- The empty chain has real supremum zero and satisfies the same bound.
classical
obtain ⟨p, hp⟩ := nested_trace_prefix B hchain x
let a : Fin n → ℝ := fun j => if x (p j) ∈ U then w (p j) else 0
have henergy : (∑ j, a j ^ 2) = chainEnergy U x w := by
calc
_ = ∑ j, if x (p j) ∈ U then w (p j) ^ 2 else 0 := by
apply Finset.sum_congr rfl
intro j _
simp only [a]
split_ifs <;> simp
_ = _ := Equiv.sum_comp p (fun j => if x j ∈ U then w j ^ 2 else 0)
have hprefix_nonneg (τ : Fin n → Bool) : 0 ≤ signedPrefixMax a τ := by
exact le_trans (abs_nonneg (signedPrefix a τ 0))
(le_ciSup (Set.finite_range (fun k => |signedPrefix a τ k|)).bddAbove
(0 : Fin (n + 1)))
have htrace (σ : Fin n → Bool) (i : ι) :
|∑ j, if x j ∈ B i then (if σ j then (1 : ℝ) else -1) * w j else 0| ≤
signedPrefixMax a (fun j => σ (p j)) := by
obtain ⟨k, hk⟩ := hp i
have heq : (∑ j, if x j ∈ B i then
(if σ j then (1 : ℝ) else -1) * w j else 0) =
signedPrefix a (fun j => σ (p j)) k := by
rw [← Equiv.sum_comp p (fun j => if x j ∈ B i then
(if σ j then (1 : ℝ) else -1) * w j else 0)]
unfold signedPrefix
apply Finset.sum_congr rfl
intro j _
by_cases hj : x (p j) ∈ B i
· simp [hj, (hk j).mp hj, a, hU i hj]
· simp [hj, mt (hk j).mpr hj]
rw [heq]
exact le_ciSup
(Set.finite_range (fun k => |signedPrefix a (fun j => σ (p j)) k|)).bddAbove k
have hbounded (σ : Fin n → Bool) : BddAbove (range (fun i =>
|∑ j, if x j ∈ B i then (if σ j then (1 : ℝ) else -1) * w j else 0|)) := by
refine ⟨signedPrefixMax a (fun j => σ (p j)), ?_⟩
rintro y ⟨i, rfl⟩
exact htrace σ i
have hle (σ : Fin n → Bool) :
chainSignSup B x w σ ≤ signedPrefixMax a (fun j => σ (p j)) := by
rcases isEmpty_or_nonempty ι with hι | hι
· let := hι
simpa only [chainSignSup, Real.iSup_of_isEmpty] using
hprefix_nonneg (fun j => σ (p j))
· let := hι
exact ciSup_le (htrace σ)
have hnonneg (σ : Fin n → Bool) : 0 ≤ chainSignSup B x w σ := by
rcases isEmpty_or_nonempty ι with hι | hι
· let := hι
simp only [chainSignSup, Real.iSup_of_isEmpty, le_refl]
· let := hι
obtain ⟨i⟩ := hι
exact le_trans (abs_nonneg _) (le_ciSup (hbounded σ) i)
have havg : signAverage (fun σ => chainSignSup B x w σ ^ 4) ≤
signAverage (fun σ => signedPrefixMax a (fun j => σ (p j)) ^ 4) := by
exact signAverage_mono _ _ (fun σ =>
pow_le_pow_left₀ (hnonneg σ) (hle σ) 4)
have hreindex : signAverage (fun σ =>
signedPrefixMax a (fun j => σ (p j)) ^ 4) =
signAverage (fun σ => signedPrefixMax a σ ^ 4) := by
unfold signAverage
congr 1
exact (p.symm.arrowCongr (Equiv.refl Bool)).sum_comp
(fun σ => signedPrefixMax a σ ^ 4)
calc
_ ≤ signAverage (fun σ => signedPrefixMax a (fun j => σ (p j)) ^ 4) := havg
_ = signAverage (fun σ => signedPrefixMax a σ ^ 4) := hreindex
_ ≤ (256 / 27 : ℝ) * (∑ j, a j ^ 2) ^ 2 := signedPrefixMax_fourth_le_energy a
_ = _ := by rw [henergy]
PopulationRange 1 core · 0 supporting A measurable real version need not be bounded at every point. ★ tested_integrals_ae_range
Bounded population versions from set-integral tests
A measurable real version need not be bounded at every point. Testing its integral on every measurable set against fixed lower and upper constants forces an almost-everywhere range bound and integrability on finite measures. No integrability of the tested version is assumed. This bridge allows threshold measurability to use conditional-version primitives without strengthening them to pointwise positivity or boundedness on null sets.
theorem tested_integrals_ae_range reviewed
⚑ flagged
Causalean.Stat.EmpiricalProcess.Countable
Under a finite measure μ, if a real function f is measurable, l and u are two constants, and on every measurable set the integral of f lies between l and u times the set's mass, then f lies between l and u almost everywhere and is integrable.
Formal statement
hypotheses
Ω :
Type*
μ :
f :
Ω → ℝ
hf :
l u :
ℝ
htest :
∀ S : Set Ω
if
then
l * μ.real S ≤ (∫ x in S, f x ∂μ) ∧ (∫ x in S, f x ∂μ) ≤ u * μ.real S
Proof (Lean source)
theorem tested_integrals_ae_range {Ω : Type*} [MeasurableSpace Ω]
(μ : Measure Ω) [IsFiniteMeasure μ] (f : Ω → ℝ) (hf : Measurable f)
(l u : ℝ)
(htest : ∀ S : Set Ω, MeasurableSet S →
l * μ.real S ≤ (∫ x in S, f x ∂μ) ∧
(∫ x in S, f x ∂μ) ≤ u * μ.real S) :
(∀ᵐ x ∂μ, f x ∈ Icc l u) ∧ Integrable f μ := by
-- Work on S_N={x | |f x|≤N}: f is integrable on S_N by of_bound.
-- Apply Mathlib ae_le_of_forall_setIntegral_le to the restricted law,
-- using htest on intersections, to bound f between l and u there.
-- The countable S_N cover all points since f is real-valued. Transfer
-- these AE inequalities to μ and conclude Integrable.of_bound with
-- max |l| |u|. Assuming f integrable at the start would hide the bridge.
let S : ℕ → Set Ω := fun N => {x | |f x| ≤ (N : ℝ)}
have hS (N : ℕ) : MeasurableSet (S N) := by
simpa only [Real.norm_eq_abs] using (measurableSet_le hf.norm
(measurable_const : Measurable (fun _ : Ω => (N : ℝ))))
have hlocal (N : ℕ) : ∀ᵐ x ∂μ.restrict (S N), f x ∈ Icc l u := by
have hfi : Integrable f (μ.restrict (S N)) :=
Integrable.of_bound hf.aestronglyMeasurable.restrict (N : ℝ)
((ae_restrict_mem (hS N)).mono fun x hx => by
simpa only [Real.norm_eq_abs, S, Set.mem_ofPred_eq] using hx)
have hlo : (fun _ : Ω => l) ≤ᵐ[μ.restrict (S N)] f := by
apply ae_le_of_forall_setIntegral_le (integrable_const l) hfi
intro t ht _
simpa [Measure.restrict_restrict ht, integral_const, Measure.real,
Measure.restrict_apply ht, smul_eq_mul, mul_comm] using
(htest (t ∩ S N) (ht.inter (hS N))).1
have hup : f ≤ᵐ[μ.restrict (S N)] (fun _ : Ω => u) := by
apply ae_le_of_forall_setIntegral_le hfi (integrable_const u)
intro t ht _
simpa [Measure.restrict_restrict ht, integral_const, Measure.real,
Measure.restrict_apply ht, smul_eq_mul, mul_comm] using
(htest (t ∩ S N) (ht.inter (hS N))).2
exact hlo.and hup
have hrange : ∀ᵐ x ∂μ, f x ∈ Icc l u := by
have hall : ∀ᵐ x ∂μ, ∀ N : ℕ, x ∈ S N → f x ∈ Icc l u :=
(ae_all_iff).2 fun N => (ae_restrict_iff' (hS N)).1 (hlocal N)
filter_upwards [hall] with x hx
obtain ⟨N, hN⟩ := exists_nat_ge |f x|
exact hx N hN
refine ⟨hrange, Integrable.of_bound hf.aestronglyMeasurable (max |l| |u|) ?_⟩
filter_upwards [hrange] with x hx
rw [Real.norm_eq_abs, abs_le]
constructor
· exact (neg_le_neg (le_max_left |l| |u|)).trans ((neg_abs_le l).trans hx.1)
· exact hx.2.trans ((le_abs_self u).trans (le_max_right |l| |u|))
ProcessMeasurability 1 core · 7 supporting Countability makes the real supremum measurable; uniform bounds justify the conditionally complete real supremum and every fourth-moment integral. ★ centeredSup_legal
Legal fourth moments of countable bounded processes
Countability makes the real supremum measurable; uniform bounds justify the conditionally complete real supremum and every fourth-moment integral. These are genuine conclusions, not moment assumptions in the symmetrization API.
theorem centeredSup_legal reviewed
⚑ flagged
Causalean.Stat.EmpiricalProcess.Countable
For a uniformly bounded measurable class with a nonempty countable index set, a probability measure μ, and any sample size n, the centered supremum of the class relative to μ is a measurable function of the sample, lies between zero and twice the class bound at every sample, and has an integrable fourth power under the law of n independent draws from μ.
Formal statement
hypotheses
Proof (Lean source)
theorem centeredSup_legal (n : ℕ) :
Measurable (centeredSup μ F.f (n := n)) ∧
(∀ x : Fin n → Ω, 0 ≤ centeredSup μ F.f x ∧
centeredSup μ F.f x ≤ 2 * F.bound) ∧
Integrable (fun x => centeredSup μ F.f x ^ 4)
(Measure.pi (fun _ : Fin n => μ)) := by
have hm : Measurable (centeredSup μ F.f (n := n)) := by
apply Measurable.iSup
intro i
unfold centeredEmpiricalAverage
simpa only [Real.norm_eq_abs, Pi.mul_apply, Pi.sub_apply, Function.comp_apply] using
(((measurable_const.mul (Finset.measurable_sum _ fun j _ =>
(F.measurable i).comp (measurable_pi_apply j))).sub measurable_const).norm)
have hb : ∀ x : Fin n → Ω, 0 ≤ centeredSup μ F.f x ∧
centeredSup μ F.f x ≤ 2 * F.bound := by
intro x
apply supremum_bounds
intro i
refine ⟨abs_nonneg _, ?_⟩
have hi : |∫ z, F.f i z ∂μ| ≤ F.bound := by
simpa only [Real.norm_eq_abs, probReal_univ, mul_one] using
(norm_integral_le_of_norm_le_const (f := F.f i) (C := F.bound)
(ae_of_all μ fun z => by simpa only [Real.norm_eq_abs] using F.bounded i z))
exact (abs_sub _ _).trans (by
have ha := normalized_sum_bound (fun j => F.f i (x j)) F.bound
F.bound_nonneg (fun j => F.bounded i (x j))
change |(n : ℝ)⁻¹ * ∑ j, F.f i (x j)| + |∫ z, F.f i z ∂μ| ≤ _
linarith)
exact ⟨hm, hb, fourth_integrable _ _ _ hm hb⟩
7 supporting declarations (lemmas, instances)
-
integrabletheorem — Every member of a uniformly bounded measurable class is integrable under the probability law μ.hypothesesconclusionIntegrable (F.f i) μProof (Lean source)
theorem BoundedClass.integrable (i : ι) : Integrable (F.f i) μ := by exact Integrable.of_bound (F.measurable i).aestronglyMeasurable F.bound (ae_of_all _ (fun x => by simpa only [Real.norm_eq_abs] using F.bounded i x)) -
normalized_sum_boundtheorem — If a bound B is nonnegative and every entry of a real vector of length n is at most B in absolute value, then the absolute value of the entries' sum divided by n is at most B, including the empty sum.hypothesesconclusion|(n : ℝ)⁻¹ * ∑ j, a j| ≤ BProof (Lean source)
theorem normalized_sum_bound {n : ℕ} (a : Fin n → ℝ) (B : ℝ) (hB : 0 ≤ B) (ha : ∀ j, |a j| ≤ B) : |(n : ℝ)⁻¹ * ∑ j, a j| ≤ B := by by_cases hn : n = 0 · subst n simpa using hB have hn' : (n : ℝ) ≠ 0 := Nat.cast_ne_zero.mpr hn calc |(n : ℝ)⁻¹ * ∑ j, a j| = (n : ℝ)⁻¹ * |∑ j, a j| := by rw [abs_mul, abs_of_nonneg (inv_nonneg.mpr (Nat.cast_nonneg n))] _ ≤ (n : ℝ)⁻¹ * ∑ j, |a j| := mul_le_mul_of_nonneg_left (Finset.abs_sum_le_sum_abs _ _) (by positivity) _ ≤ (n : ℝ)⁻¹ * ∑ _ : Fin n, B := mul_le_mul_of_nonneg_left (Finset.sum_le_sum fun j _ => ha j) (by positivity) _ = B := by simp [hn'] -
abs_bool_signtheorem — Multiplying a real number by the sign ±1 attached to a Boolean value leaves its absolute value unchanged.Proof (Lean source)
theorem abs_bool_sign (b : Bool) (a : ℝ) : |(if b then (1 : ℝ) else -1) * a| = |a| := by cases b <;> simp -
supremum_boundstheorem — If every member of a nonempty family of reals lies between 0 and B, then the family's supremum also lies between 0 and B.hypothesesι :sharedType u_2Nonempty ιa :ι → ℝB :ℝha :∀ i, 0 ≤ a i ∧ a i ≤ BProof (Lean source)
theorem supremum_bounds [Nonempty ι] (a : ι → ℝ) (B : ℝ) (ha : ∀ i, 0 ≤ a i ∧ a i ≤ B) : 0 ≤ iSup a ∧ iSup a ≤ B := by have hb : BddAbove (range a) := ⟨B, by rintro _ ⟨i, rfl⟩; exact (ha i).2⟩ exact ⟨le_ciSup_of_le hb (Classical.arbitrary ι) (ha _).1, ciSup_le fun i => (ha i).2⟩ -
ghostSup_legaltheorem — For any sample size n, the ghost supremum is jointly measurable in the two samples, lies between zero and twice the class bound, and has an integrable fourth power under the product of two iid laws.hypothesesconclusionconclusion 1Proof (Lean source)
theorem ghostSup_legal (n : ℕ) : Measurable (fun p : (Fin n → Ω) × (Fin n → Ω) => ghostSup F.f p.1 p.2) ∧ (∀ x y : Fin n → Ω, 0 ≤ ghostSup F.f x y ∧ ghostSup F.f x y ≤ 2 * F.bound) ∧ Integrable (fun p : (Fin n → Ω) × (Fin n → Ω) => ghostSup F.f p.1 p.2 ^ 4) ((Measure.pi (fun _ : Fin n => μ)).prod (Measure.pi (fun _ : Fin n => μ))) := by have hm : Measurable (fun p : (Fin n → Ω) × (Fin n → Ω) => ghostSup F.f p.1 p.2) := by apply Measurable.iSup intro i simpa only [Real.norm_eq_abs, Pi.mul_apply, Pi.sub_apply, Function.comp_apply] using (measurable_const.mul (Finset.measurable_sum _ fun j _ => ((F.measurable i).comp ((measurable_pi_apply j).comp measurable_fst)).sub ((F.measurable i).comp ((measurable_pi_apply j).comp measurable_snd)))).norm have hb : ∀ x y : Fin n → Ω, 0 ≤ ghostSup F.f x y ∧ ghostSup F.f x y ≤ 2 * F.bound := by intro x y apply supremum_bounds intro i refine ⟨abs_nonneg _, normalized_sum_bound _ _ (mul_nonneg (by norm_num) F.bound_nonneg) ?_⟩ intro j exact (abs_sub _ _).trans (by have hx := F.bounded i (x j) have hy := F.bounded i (y j) linarith) exact ⟨hm, hb, fourth_integrable _ _ _ hm (fun p => hb p.1 p.2)⟩ -
signedSup_legaltheorem — For any sample size n, each fixed-sign signed supremum is a measurable function of the sample lying between zero and the class bound, and the sign average of its fourth power is integrable under the iid product law.hypothesesconclusionconclusion 3Integrable (fun x => signAverage (fun σ => signedSup F.f x σ ^ 4)) (Measure.pi (fun _ : Fin n => μ))Proof (Lean source)
theorem signedSup_legal (n : ℕ) : (∀ σ : Fin n → Bool, Measurable (fun x => signedSup F.f x σ)) ∧ (∀ x σ, 0 ≤ signedSup F.f (n := n) x σ ∧ signedSup F.f x σ ≤ F.bound) ∧ Integrable (fun x => signAverage (fun σ => signedSup F.f x σ ^ 4)) (Measure.pi (fun _ : Fin n => μ)) := by have hm (σ : Fin n → Bool) : Measurable (fun x : Fin n → Ω => signedSup F.f x σ) := by apply Measurable.iSup intro i simpa only [Real.norm_eq_abs, Pi.mul_apply, Pi.sub_apply, Function.comp_apply] using (measurable_const.mul (Finset.measurable_sum _ fun j _ => measurable_const.mul ((F.measurable i).comp (measurable_pi_apply j)))).norm have hb : ∀ (x : Fin n → Ω) σ, 0 ≤ signedSup F.f x σ ∧ signedSup F.f x σ ≤ F.bound := by intro x σ apply supremum_bounds intro i refine ⟨abs_nonneg _, normalized_sum_bound _ _ F.bound_nonneg ?_⟩ intro j rw [abs_bool_sign] exact F.bounded i (x j) refine ⟨hm, hb, ?_⟩ unfold signAverage exact (integrable_finsetSum _ fun σ _ => fourth_integrable _ _ _ (hm σ) (fun x => hb x σ)).div_const _ -
signedGhostSup_legaltheorem — For any sample size n and any fixed sign vector σ, the σ-signed ghost supremum is jointly measurable in the two samples, its fourth power is integrable under the product of two iid laws, and so is every section obtained by freezing the first sample.hypothesesΩ :sharedType u_1ι :sharedType u_2n :ℕconclusionconclusion 1conclusion 2Integrable (fun p : (Fin n → Ω) × (Fin n → Ω) => signedGhostSup F.f p.1 p.2 σ ^ 4) ((Measure.pi (fun _ : Fin n => μ)).prod (Measure.pi (fun _ : Fin n => μ)))Proof (Lean source)
theorem signedGhostSup_legal (n : ℕ) (σ : Fin n → Bool) : Measurable (fun p : (Fin n → Ω) × (Fin n → Ω) => signedGhostSup F.f p.1 p.2 σ) ∧ Integrable (fun p : (Fin n → Ω) × (Fin n → Ω) => signedGhostSup F.f p.1 p.2 σ ^ 4) ((Measure.pi (fun _ : Fin n => μ)).prod (Measure.pi (fun _ : Fin n => μ))) ∧ (∀ x : Fin n → Ω, Integrable (fun y => signedGhostSup F.f x y σ ^ 4) (Measure.pi (fun _ : Fin n => μ))) := by have hm : Measurable (fun p : (Fin n → Ω) × (Fin n → Ω) => signedGhostSup F.f p.1 p.2 σ) := by apply Measurable.iSup intro i simpa only [Real.norm_eq_abs, Pi.mul_apply, Pi.sub_apply, Function.comp_apply] using (measurable_const.mul (Finset.measurable_sum _ fun j _ => measurable_const.mul (((F.measurable i).comp ((measurable_pi_apply j).comp measurable_fst)).sub ((F.measurable i).comp ((measurable_pi_apply j).comp measurable_snd))))).norm have hb : ∀ x y : Fin n → Ω, 0 ≤ signedGhostSup F.f x y σ ∧ signedGhostSup F.f x y σ ≤ 2 * F.bound := by intro x y apply supremum_bounds intro i refine ⟨abs_nonneg _, normalized_sum_bound _ _ (mul_nonneg (by norm_num) F.bound_nonneg) ?_⟩ intro j rw [abs_bool_sign] exact (abs_sub _ _).trans (by have hx := F.bounded i (x j) have hy := F.bounded i (y j) linarith) refine ⟨hm, fourth_integrable ((Measure.pi (fun _ : Fin n => μ)).prod (Measure.pi (fun _ : Fin n => μ))) (fun p : (Fin n → Ω) × (Fin n → Ω) => signedGhostSup F.f p.1 p.2 σ) (2 * F.bound) hm (fun p => hb p.1 p.2), ?_⟩ intro x have hmap : Measurable (fun y : Fin n → Ω => (x, y)) := measurable_const.prodMk measurable_id have hs := hm.comp hmap exact fourth_integrable (Measure.pi (fun _ : Fin n => μ)) (fun y => signedGhostSup F.f x y σ) (2 * F.bound) hs (fun y => hb x y)
ProductSwap 2 core · 1 supporting A fixed Boolean sign vector selects which paired coordinates to exchange. ★ pairedSampleSwap_measurePreserving
Coordinatewise exchange of two iid samples
A fixed Boolean sign vector selects which paired coordinates to exchange. The exchange is an involutive measurable equivalence and preserves the two-copy iid product law. Applied to a sample difference, it multiplies each coordinate by the corresponding sign. This module isolates product-law symmetry from the analytic moment comparisons in Ghost.
Mathlib already supplies measurePreserving_arrowProdEquivProdArrow for pairing the sample coordinates and measurePreserving_pi for the coordinate maps. Only their partial-swap composition is needed here.
def pairedSampleSwap reviewed
⚑ flagged
Causalean.Stat.EmpiricalProcess.Countable
The paired-sample swap determined by a fixed sign vector σ is the measurable involution of pairs of samples that keeps the j-th paired coordinates in place when σ_j is positive and exchanges them when σ_j is negative.
Definition (Lean source)
parameters
given by
clause 1
toFun p := (fun j => if σ j then p.1 j else p.2 j, fun j => if σ j then p.2 j else p.1 j)
clause 2
invFun p := (fun j => if σ j then p.1 j else p.2 j, fun j => if σ j then p.2 j else p.1 j)
clause 3
left_inv p := by ext j <;> cases h : σ j <;> simp [h]
clause 4
right_inv p := by ext j <;> cases h : σ j <;> simp [h]
clause 5
measurable_toFun := by apply prodMk <;> apply measurable_pi_lambda <;> intro j · cases σ j <;> simp only [Bool.false_eq_true, ↓reduceIte] · exact (measurable_pi_apply j).comp measurable_snd · exact (measurable_pi_apply j).comp measurable_fst · cases σ j <;> simp only [Bool.false_eq_true, ↓reduceIte] · exact (measurable_pi_apply j).comp measurable_fst · exact (measurable_pi_apply j).comp measurable_snd
clause 6
measurable_invFun := by apply prodMk <;> apply measurable_pi_lambda <;> intro j · cases σ j <;> simp only [Bool.false_eq_true, ↓reduceIte] · exact (measurable_pi_apply j).comp measurable_snd · exact (measurable_pi_apply j).comp measurable_fst · cases σ j <;> simp only [Bool.false_eq_true, ↓reduceIte] · exact (measurable_pi_apply j).comp measurable_fst · exact (measurable_pi_apply j).comp measurable_snd
theorem pairedSampleSwap_measurePreserving reviewed
⚑ flagged
Causalean.Stat.EmpiricalProcess.Countable
For two independent iid samples from a probability law μ and any fixed sign vector σ, the paired-sample swap selected by σ preserves the joint product law of the two samples.
Formal statement
hypotheses
conclusion
MeasurePreserving (pairedSampleSwap (Ω := Ω) σ) ((Measure.pi (fun _ : Fin n => μ)).prod (Measure.pi (fun _ : Fin n => μ))) ((Measure.pi (fun _ : Fin n => μ)).prod (Measure.pi (fun _ : Fin n => μ)))
Proof (Lean source)
theorem pairedSampleSwap_measurePreserving {Ω : Type*} [MeasurableSpace Ω]
(μ : Measure Ω) [IsProbabilityMeasure μ] {n : ℕ} (σ : Fin n → Bool) :
MeasurePreserving (pairedSampleSwap (Ω := Ω) σ)
((Measure.pi (fun _ : Fin n => μ)).prod (Measure.pi (fun _ : Fin n => μ)))
((Measure.pi (fun _ : Fin n => μ)).prod (Measure.pi (fun _ : Fin n => μ))) := by
-- Let e = MeasurableEquiv.arrowProdEquivProdArrow Ω Ω (Fin n).
-- Mathlib proves e preserves pi_j (μ.prod μ) to (pi_j μ).prod (pi_j μ).
-- On paired coordinates use identity when σ j is true and swap
-- otherwise; both preserve μ.prod μ. Apply measurePreserving_pi and
-- conjugate with e and e.symm. This is a law identity, with no moment input.
let e := MeasurableEquiv.arrowProdEquivProdArrow Ω Ω (Fin n)
have he := measurePreserving_arrowProdEquivProdArrow Ω Ω (Fin n)
(fun _ => μ) (fun _ => μ)
let t : Fin n → Ω × Ω → Ω × Ω := fun j p => if σ j then p else p.swap
have ht : ∀ j, MeasurePreserving (t j) (μ.prod μ) (μ.prod μ) := by
intro j
cases h : σ j
· simpa [t, h] using (Measure.measurePreserving_swap (μ := μ) (ν := μ))
· simp only [t, h, ↓reduceIte]
exact ⟨measurable_id, Measure.map_id⟩
have hp := measurePreserving_pi (fun _ : Fin n => μ.prod μ)
(fun _ : Fin n => μ.prod μ) ht
have hc := he.comp (hp.comp (he.symm e))
convert hc using 1
funext p
ext j <;> cases h : σ j <;> simp [pairedSampleSwap, e, t,
MeasurableEquiv.arrowProdEquivProdArrow, h]
1 supporting declaration (lemmas, instances)
-
ghostSup_pairedSampleSwaptheorem — For an indexed function class, a sign vector σ, and a pair of samples, the ghost supremum after applying the paired-sample swap selected by σ equals the σ-signed ghost supremum of the original pair.hypothesesconclusion= signedGhostSup f p.1 p.2 σProof (Lean source)
theorem ghostSup_pairedSampleSwap {Ω ι : Type*} [MeasurableSpace Ω] (f : ι → Ω → ℝ) {n : ℕ} (σ : Fin n → Bool) (p : (Fin n → Ω) × (Fin n → Ω)) : ghostSup f ((pairedSampleSwap σ p).1) ((pairedSampleSwap σ p).2) = signedGhostSup f p.1 p.2 σ := by unfold ghostSup signedGhostSup congr 1 funext i congr 2 apply Finset.sum_congr rfl intro j _ cases h : σ j <;> simp [pairedSampleSwap, h, sub_eq_add_neg, add_comm]
ScalarSigns 3 core · 6 supporting The finite Boolean average of a signed sum has fourth moment exactly three times squared energy minus twice the sum of coefficient fourth powers. ★ signLinear_sq_sum★ signAverage_fourth_exact
Exact scalar fourth moments of finite signs
The finite Boolean average of a signed sum has fourth moment exactly three times squared energy minus twice the sum of coefficient fourth powers. This algebraic layer is independent of martingales and maximal estimates.
def signFlipEquiv reviewed
⚑ flagged
Causalean.Stat.EmpiricalProcess.Countable
Flipping one coordinate is an equivalence of finite Boolean sign vectors.
Definition (Lean source)
parameters
ι :
Type*
j :
ι
theorem signLinear_sq_sum reviewed
⚑ flagged
Causalean.Stat.EmpiricalProcess.Countable
Over any finite coordinate type, the unnormalized second moment of a real linear combination of Boolean signs equals the number of sign vectors times the sum of squared coefficients: the sum, over all Boolean sign vectors (true standing for +1, false for −1), of the squared signed sum of the coefficients.
Formal statement
hypotheses
ι :
a :
ι → ℝ
Proof (Lean source)
theorem signLinear_sq_sum {ι : Type*} [Fintype ι] [DecidableEq ι] (a : ι → ℝ) :
(∑ σ : ι → Bool, (∑ j, (if σ j then (1 : ℝ) else -1) * a j) ^ 2) =
(card (ι → Bool) : ℝ) * ∑ j, a j ^ 2 := by
classical
simp_rw [pow_two, Fintype.sum_mul_sum]
rw [Finset.sum_comm]
apply Eq.trans _ (by rw [Finset.mul_sum])
apply Finset.sum_congr rfl
intro j hj
rw [Finset.sum_comm]
have hterm (k : ι) :
(∑ σ : ι → Bool,
((if σ j then (1 : ℝ) else -1) * a j) *
((if σ k then (1 : ℝ) else -1) * a k)) =
if k = j then (card (ι → Bool) : ℝ) * (a j * a j) else 0 := by
simp_rw [show ∀ σ : ι → Bool,
((if σ j then (1 : ℝ) else -1) * a j) *
((if σ k then (1 : ℝ) else -1) * a k) =
((if σ j then (1 : ℝ) else -1) * (if σ k then (1 : ℝ) else -1)) *
(a j * a k) by
intro σ
ring, ← Finset.sum_mul]
by_cases hk : k = j
· subst k
simp only [if_true]
simp_rw [show ∀ b : Bool,
(if b then (1 : ℝ) else -1) * (if b then (1 : ℝ) else -1) = 1 by
intro b
cases b <;> norm_num]
simp
· rw [if_neg hk, signCoordinate_mul_sum j k (Ne.symm hk), zero_mul]
simp_rw [hterm]
simp [pow_two]
theorem signAverage_fourth_exact reviewed
⚑ flagged
Causalean.Stat.EmpiricalProcess.Countable
For real coefficients, the fourth moment of their finite Rademacher sum equals exactly three times the squared sum of squared coefficients minus twice the sum of their fourth powers.
Formal statement
hypotheses
n :
ℕ
a :
Fin n → ℝ
conclusion
signAverage (fun σ => (∑ j, (if σ j then (1 : ℝ) else -1) * a j)^4)
= 3 * (∑ j, a j ^ 2)^2 - 2 * ∑ j, a j ^ 4
Proof (Lean source)
theorem signAverage_fourth_exact {n : ℕ} (a : Fin n → ℝ) :
signAverage (fun σ => (∑ j, (if σ j then (1 : ℝ) else -1) * a j)^4) =
3 * (∑ j, a j ^ 2)^2 - 2 * ∑ j, a j ^ 4 := by
rw [signAverage, (signSum_moments n a).2]
exact mul_div_cancel_left₀ _ (pow_ne_zero n (by norm_num))
6 supporting declarations (lemmas, instances)
-
boolSign_nottheorem — Complementing a Boolean value negates its scalar sign.Proof (Lean source)
theorem boolSign_not (b : Bool) : (if !b then (1 : ℝ) else -1) = -(if b then (1 : ℝ) else -1) := by cases b <;> norm_num -
signCoordinate_sumtheorem — Over any finite coordinate type, the unnormalized sum of one Boolean sign coordinate vanishes.Proof (Lean source)
theorem signCoordinate_sum {ι : Type*} [Fintype ι] [DecidableEq ι] (j : ι) : (∑ σ : ι → Bool, if σ j then (1 : ℝ) else -1) = 0 := by classical have h := (signFlipEquiv j).sum_comp (fun σ => if σ j then (1 : ℝ) else -1) simp only [signFlipEquiv, Equiv.coe_fn_mk, Function.update_self, boolSign_not, Finset.sum_neg_distrib] at h linarith -
signCoordinate_mul_sumtheorem — Over any finite coordinate type, the unnormalized product sum of two distinct Boolean sign coordinates vanishes.hypothesesconclusion(∑ σ : ι → Bool, (if σ j then (1 : ℝ) else -1) * (if σ k then (1 : ℝ) else -1)) = 0Proof (Lean source)
theorem signCoordinate_mul_sum {ι : Type*} [Fintype ι] [DecidableEq ι] (j k : ι) (hjk : j ≠ k) : (∑ σ : ι → Bool, (if σ j then (1 : ℝ) else -1) * (if σ k then (1 : ℝ) else -1)) = 0 := by classical have h := (signFlipEquiv j).sum_comp (fun σ => (if σ j then (1 : ℝ) else -1) * (if σ k then (1 : ℝ) else -1)) simp only [signFlipEquiv, Equiv.coe_fn_mk, Function.update_self, Function.update_of_ne hjk.symm, boolSign_not, neg_mul, Finset.sum_neg_distrib] at h linarith -
signLinear_sumtheorem — Over any finite coordinate type, every real linear combination of Boolean signs has unnormalized sum zero.Proof (Lean source)
theorem signLinear_sum {ι : Type*} [Fintype ι] [DecidableEq ι] (a : ι → ℝ) : (∑ σ : ι → Bool, ∑ j, (if σ j then (1 : ℝ) else -1) * a j) = 0 := by rw [Finset.sum_comm] simp only [← Finset.sum_mul, signCoordinate_sum, zero_mul, Finset.sum_const_zero] -
signSum_succtheorem — For a real function of n + 1 Boolean signs, its sum over all sign patterns equals the sum, over the patterns of the remaining n signs, of its values with the first sign set to true and to false.hypothesesProof (Lean source)
theorem signSum_succ {n : ℕ} (H : (Fin (n + 1) → Bool) → ℝ) : (∑ σ, H σ) = ∑ σ : Fin n → Bool, (H (cons true σ) + H (cons false σ)) := by rw [← Fintype.sum_equiv (Fin.consEquiv (fun _ : Fin (n + 1) => Bool)) (fun z => H (cons z.1 z.2)) H (fun _ => rfl)] simp only [Fintype.sum_prod_type, Fintype.sum_bool, Finset.sum_add_distrib] -
signSum_momentstheorem — For n real coefficients, summing over all 2^n sign patterns, the squared signed sum of the coefficients totals 2^n times the sum of squared coefficients, and its fourth power totals 2^n times three times the squared sum of squares minus twice the sum of fourth powers.hypothesesn :ℕa :Fin n → ℝProof (Lean source)
theorem signSum_moments (n : ℕ) (a : Fin n → ℝ) : (∑ σ : Fin n → Bool, (∑ j, (if σ j then (1 : ℝ) else -1) * a j)^2) = (2 : ℝ)^n * (∑ j, a j^2) ∧ (∑ σ : Fin n → Bool, (∑ j, (if σ j then (1 : ℝ) else -1) * a j)^4) = (2 : ℝ)^n * (3 * (∑ j, a j^2)^2 - 2 * ∑ j, a j^4) := by induction n with | zero => simp | succ n ih => have h := ih (fun j => a j.succ) constructor · rw [signSum_succ] simp only [Fin.sum_univ_succ, Fin.cons_zero, Fin.cons_succ, Bool.false_eq_true, if_true, if_false, one_mul, neg_one_mul] simp_rw [show ∀ s : ℝ, (a 0 + s)^2 + (-a 0 + s)^2 = 2 * s^2 + 2 * (a 0)^2 by intro s; ring] simp only [Finset.sum_add_distrib, ← Finset.mul_sum, Finset.sum_const, Finset.card_univ, Fintype.card_fun, Fintype.card_bool, Fintype.card_fin, nsmul_eq_mul, Nat.cast_pow, Nat.cast_ofNat] rw [h.1, pow_succ] ring · rw [signSum_succ] simp only [Fin.sum_univ_succ, Fin.cons_zero, Fin.cons_succ, Bool.false_eq_true, if_true, if_false, one_mul, neg_one_mul] simp_rw [show ∀ s : ℝ, (a 0 + s)^4 + (-a 0 + s)^4 = 2 * s^4 + 12 * (a 0)^2 * s^2 + 2 * (a 0)^4 by intro s; ring] simp only [Finset.sum_add_distrib, ← Finset.mul_sum, Finset.sum_const, Finset.card_univ, Fintype.card_fun, Fintype.card_bool, Fintype.card_fin, nsmul_eq_mul, Nat.cast_pow, Nat.cast_ofNat] rw [h.1, h.2, pow_succ] ring
TailMoment 1 core · 3 supporting Layer cake and Tonelli convert a weak tail bound into the mixed fourth-moment estimate used by Doob. ★ weak_fourth_mixed
Fourth-moment tail integration
Layer cake and Tonelli convert a weak tail bound into the mixed fourth-moment estimate used by Doob. Tail integrals use positive real levels and include the event boundary; Layercake already justifies the closed-tail convention. This file has no martingale or empirical-process dependencies.
theorem weak_fourth_mixed reviewed
⚑ flagged
Causalean.Stat.EmpiricalProcess.Countable
Under a probability measure μ, let two real functions A and B be nonnegative, with A measurable and B almost everywhere strongly measurable, and both with integrable fourth powers. If for every positive level t, t times the probability that A ≥ t is at most the integral of B over that event, then the expectation of A^4 is at most 4/3 times the expectation of A^3·B.
Formal statement
hypotheses
Ω :
Type*
μ :
A B :
Ω → ℝ
hA :
∀ x, 0 ≤ A x
hB :
∀ x, 0 ≤ B x
hAm :
hBm :
hA4 :
Integrable (fun x => A x ^ 4) μ
hB4 :
Integrable (fun x => B x ^ 4) μ
hweak :
∀ t : ℝ
if
0 < t
then
t * μ.real {x | t ≤ A x} ≤ ∫ x in {x | t ≤ A x}, B x ∂μ
conclusion
(∫ x, A x ^ 4 ∂μ) ≤ (4 / 3 : ℝ) * ∫ x, A x ^ 3 * B x ∂μ
Proof (Lean source)
theorem weak_fourth_mixed {Ω : Type*} [MeasurableSpace Ω]
(μ : Measure Ω) [IsProbabilityMeasure μ] (A B : Ω → ℝ)
(hA : ∀ x, 0 ≤ A x) (hB : ∀ x, 0 ≤ B x)
(hAm : Measurable A) (hBm : AEStronglyMeasurable B μ)
(hA4 : Integrable (fun x => A x ^ 4) μ)
(hB4 : Integrable (fun x => B x ^ 4) μ)
(hweak : ∀ t : ℝ, 0 < t →
t * μ.real {x | t ≤ A x} ≤ ∫ x in {x | t ≤ A x}, B x ∂μ) :
(∫ x, A x ^ 4 ∂μ) ≤ (4 / 3 : ℝ) * ∫ x, A x ^ 3 * B x ∂μ := by
-- Compare the legal tail integrals after multiplying hweak by 4*t^2.
-- This weak hypothesis is derived from Mathlib maximal_ineq in Doob.lean;
-- it is not an assumed fourth-moment or centered-process inequality.
obtain ⟨hfi, hfe⟩ := fourth_tail_identity μ A hA hAm hA4
obtain ⟨hmi, hme⟩ := mixed_tail_identity μ A B hA hB hAm hBm hA4 hB4
rw [hfe, ← hme]
apply setIntegral_mono_on hfi hmi measurableSet_Ioi
intro t ht
have h := mul_le_mul_of_nonneg_left (hweak t ht) (by positivity : 0 ≤ 4 * t ^ 2)
convert h using 1
ring
3 supporting declarations (lemmas, instances)
-
polynomial_tail_identitytheorem — Under a finite measure μ, if a real function A is nonnegative and measurable, its (n + 1)-st power is integrable, and c is a nonnegative constant, then the function t ↦ c t^n μ(A ≥ t) is integrable over the positive levels t, and its integral equals c/(n + 1) times the integral of A^(n + 1), the polynomial layer-cake formula.hypothesesΩ :Type*μ :A :Ω → ℝhA :∀ x, 0 ≤ A xhm :n :ℕc :ℝhc :0 ≤ chi :Integrable (fun x => A x ^ (n + 1)) μconclusionconclusion 1IntegrableOn (fun t : ℝ => c * t ^ n * μ.real {x | t ≤ A x}) (Ioi 0)conclusion 2(c / (n + 1 : ℝ)) * (∫ x, A x ^ (n + 1) ∂μ)= ∫ t in Ioi (0 : ℝ), c * t ^ n * μ.real {x | t ≤ A x}Proof (Lean source)
theorem polynomial_tail_identity {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsFiniteMeasure μ] (A : Ω → ℝ) (hA : ∀ x, 0 ≤ A x) (hm : Measurable A) (n : ℕ) (c : ℝ) (hc : 0 ≤ c) (hi : Integrable (fun x => A x ^ (n + 1)) μ) : IntegrableOn (fun t : ℝ => c * t ^ n * μ.real {x | t ≤ A x}) (Ioi 0) ∧ (c / (n + 1 : ℝ)) * (∫ x, A x ^ (n + 1) ∂μ) = ∫ t in Ioi (0 : ℝ), c * t ^ n * μ.real {x | t ≤ A x} := by have hp (a : ℝ) : (∫ t in 0..a, c * t ^ n) = c / (n + 1 : ℝ) * a ^ (n + 1) := by rw [intervalIntegral.integral_const_mul, integral_pow] simp only [zero_pow (Nat.succ_ne_zero n), sub_zero] ring have hn : ∀ᵐ t ∂volume.restrict (Ioi (0 : ℝ)), 0 ≤ c * t ^ n := by filter_upwards [ae_restrict_mem measurableSet_Ioi] with t ht exact mul_nonneg hc (pow_nonneg (le_of_lt ht) _) have hl := lintegral_comp_eq_lintegral_meas_le_mul μ (Filter.Eventually.of_forall hA) hm.aemeasurable (g := fun t => c * t ^ n) (fun t _ => (continuous_const.mul (continuous_id.pow n)).intervalIntegrable 0 t) hn simp only [hp] at hl have hleft := hi.const_mul (c / (n + 1 : ℝ)) have hln : ∀ x, 0 ≤ c / (n + 1 : ℝ) * A x ^ (n + 1) := fun x => mul_nonneg (div_nonneg hc (by positivity)) (pow_nonneg (hA x) _) have htm : Measurable (fun t : ℝ => μ {x | t ≤ A x}) := Antitone.measurable (fun _ _ h => measure_mono (fun _ hx => le_trans h hx)) have hrm : Measurable (fun t : ℝ => c * t ^ n * μ.real {x | t ≤ A x}) := ((continuous_const.mul (continuous_id.pow n)).measurable).mul htm.ennreal_toReal have hrn : ∀ᵐ t ∂volume.restrict (Ioi (0 : ℝ)), 0 ≤ c * t ^ n * μ.real {x | t ≤ A x} := by filter_upwards [hn] with t ht using mul_nonneg ht (measureReal_nonneg) have he : (∫⁻ t in Ioi (0 : ℝ), ofReal (c * t ^ n * μ.real {x | t ≤ A x})) = ∫⁻ t in Ioi (0 : ℝ), μ {x | t ≤ A x} * ofReal (c * t ^ n) := by apply lintegral_congr_ae filter_upwards [hn] with t ht rw [ENNReal.ofReal_mul ht, measureReal_def, ENNReal.ofReal_toReal (measure_ne_top μ _), mul_comm] have hri : IntegrableOn (fun t : ℝ => c * t ^ n * μ.real {x | t ≤ A x}) (Ioi 0) := (lintegral_ofReal_ne_top_iff_integrable hrm.aestronglyMeasurable hrn).1 (by rw [he, ← hl]; exact hleft.lintegral_lt_top.ne) refine ⟨hri, ?_⟩ rw [← integral_const_mul] rw [integral_eq_lintegral_of_nonneg_ae (Filter.Eventually.of_forall hln) hleft.aestronglyMeasurable, integral_eq_lintegral_of_nonneg_ae hrn hri.aestronglyMeasurable, he, ← hl] -
fourth_tail_identitytheorem — Under a probability measure μ, if a real function A is nonnegative, measurable, and has an integrable fourth power, then the function t ↦ 4 t^3 μ(A ≥ t) is integrable over the positive levels t, and its integral equals the expectation of A^4.hypothesesconclusionconclusion 1IntegrableOn (fun t : ℝ => 4 * t ^ 3 * μ.real {x | t ≤ A x}) (Ioi 0)conclusion 2(∫ x, A x ^ 4 ∂μ) = ∫ t in Ioi (0 : ℝ), 4 * t ^ 3 * μ.real {x | t ≤ A x}Proof (Lean source)
theorem fourth_tail_identity {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] (A : Ω → ℝ) (hA : ∀ x, 0 ≤ A x) (hm : Measurable A) (h4 : Integrable (fun x => A x ^ 4) μ) : IntegrableOn (fun t : ℝ => 4 * t ^ 3 * μ.real {x | t ≤ A x}) (Ioi 0) ∧ (∫ x, A x ^ 4 ∂μ) = ∫ t in Ioi (0 : ℝ), 4 * t ^ 3 * μ.real {x | t ≤ A x} := by -- Specialize Layercake's lintegral_comp_eq_lintegral_meas_le_mul -- to g(t)=4*t^3, whose integral from 0 to a is a^4, and transfer -- finite nonnegative lintegrals to real integrals. have ht := polynomial_tail_identity μ A hA hm 3 4 (by norm_num) h4 norm_num at ht exact ht -
mixed_tail_identitytheorem — Under a probability measure μ, if two real functions A and B are nonnegative, A is measurable and B almost everywhere strongly measurable, and both have integrable fourth powers, then the function t ↦ 4 t^2 times the integral of B over the event A ≥ t is integrable over the positive levels t, and its integral equals 4/3 times the expectation of A^3·B.hypothesesΩ :Type*μ :A B :Ω → ℝhA :∀ x, 0 ≤ A xhB :∀ x, 0 ≤ B xhAm :hBm :hA4 :Integrable (fun x => A x ^ 4) μhB4 :Integrable (fun x => B x ^ 4) μconclusionconclusion 1IntegrableOn (fun t : ℝ => 4 * t ^ 2 * ∫ x in {x | t ≤ A x}, B x ∂μ) (Ioi 0)conclusion 2(∫ t in Ioi (0 : ℝ), 4 * t ^ 2 * ∫ x in {x | t ≤ A x}, B x ∂μ)= (4 / 3 : ℝ) * ∫ x, A x ^ 3 * B x ∂μProof (Lean source)
theorem mixed_tail_identity {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] (A B : Ω → ℝ) (hA : ∀ x, 0 ≤ A x) (hB : ∀ x, 0 ≤ B x) (hAm : Measurable A) (hBm : AEStronglyMeasurable B μ) (hA4 : Integrable (fun x => A x ^ 4) μ) (hB4 : Integrable (fun x => B x ^ 4) μ) : IntegrableOn (fun t : ℝ => 4 * t ^ 2 * ∫ x in {x | t ≤ A x}, B x ∂μ) (Ioi 0) ∧ (∫ t in Ioi (0 : ℝ), 4 * t ^ 2 * ∫ x in {x | t ≤ A x}, B x ∂μ) = (4 / 3 : ℝ) * ∫ x, A x ^ 3 * B x ∂μ := by -- Apply polynomial Layercake to the finite measure with density B. -- The withDensity integral formula supplies the mixed moment; Holder -- makes it finite, permitting conversion to legal real tail integrals. have hBi : Integrable B μ := by have hn4 : Integrable (fun x => ‖B x‖ ^ 4) μ := by simpa only [Real.norm_eq_abs, abs_of_nonneg (hB _)] using hB4 have hn1 := integrable_norm_pow_of_le hBm (p := 1) (by norm_num : 1 ≤ 4) hn4 simpa only [pow_one, Real.norm_eq_abs, abs_of_nonneg (hB _)] using hn1 let ν := μ.withDensity (fun x => ofReal (B x)) have : IsFiniteMeasure ν := isFiniteMeasure_withDensity_ofReal hBi.hasFiniteIntegral have hdm : AEMeasurable (fun x => ofReal (B x)) μ := hBm.aemeasurable.ennreal_ofReal have hdtop : ∀ᵐ x ∂μ, ofReal (B x) < ⊤ := Filter.Eventually.of_forall fun _ => ENNReal.ofReal_lt_top have hmix := (fourth_moment_holder μ A B hA hB hA4 hB4 hAm.aestronglyMeasurable hBm).1 have hc : Integrable (fun x => A x ^ 3) ν := by apply (integrable_withDensity_iff_integrable_smul₀' hdm hdtop).2 simpa only [ENNReal.toReal_ofReal (hB _), smul_eq_mul, mul_comm] using hmix have htail (t : ℝ) : ν.real {x | t ≤ A x} = ∫ x in {x | t ≤ A x}, B x ∂μ := by rw [measureReal_def, withDensity_apply _ (measurableSet_le measurable_const hAm)] exact (integral_eq_lintegral_of_nonneg_ae (Filter.Eventually.of_forall hB) hBm.restrict).symm have hv : (∫ x, A x ^ 3 ∂ν) = ∫ x, A x ^ 3 * B x ∂μ := by rw [integral_withDensity_eq_integral_toReal_smul₀ hdm hdtop] simp only [ENNReal.toReal_ofReal (hB _), smul_eq_mul, mul_comm] have ht := polynomial_tail_identity ν A hA hAm 2 4 (by norm_num) hc simp only [htail, hv] at ht norm_num only [Nat.cast_ofNat, Nat.reduceAdd] at ht exact ⟨ht.1, ht.2.symm⟩
Threshold 3 core · 5 supporting An affine threshold integrand is an offset plus a marked closed-threshold indicator. ★ localizedThreshold_countable_reduction
Atom-safe population-centered localized thresholds
An affine threshold integrand is an offset plus a marked closed-threshold indicator. This covers both orientations, signed comparison scores, and fixed oracle subtraction. One-sided approximation is pointwise at EVERY score, including all marginal atoms and observed scores. Dominated convergence also approximates the population centers. A skeleton is chosen INSIDE the actual eligible cutoff set, preserving localization exactly, including its boundary. No atomlessness, loss continuity, or sample-dependent class is assumed. Constants and finitely many extra policies may be adjoined to this countable class; this does not change its measurability or symmetrization requirements. For laws supported on a measurable observation subset, use its subtype as the observation space. Mathlib's integral_subtype_comap identifies its population centers with restricted integrals, which equal the original integrals when the law is supported there. Thus the global pointwise bound is only needed on the actual support.
def thresholdFunction reviewed
⚑ flagged
Causalean.Stat.EmpiricalProcess.Countable
The affine closed-threshold integrand with orientation flag, score, offset, and mark functions, and cutoff t, evaluated at an observation x, is the offset at x, plus the mark at x when the score at x is at most t (flag true) or at least t (flag false).
Definition (Lean source)
parameters
def
thresholdFunction upper score offset mark t x :
ℝ
given by
offset x + if (if upper then score x ≤ t else t ≤ score x) then mark x else 0
def localizedThresholdSup reviewed
⚑ flagged
Causalean.Stat.EmpiricalProcess.Countable
The localized threshold supremum on a sample x, relative to a population law μ, with orientation flag, score, offset, and mark functions, an admissible cutoff set T, a deterministic population loss, and a radius z, is the centered supremum of the threshold integrands over the cutoffs in T whose loss is at most z: each empirical average is centered by its own population integral.
Definition (Lean source)
parameters
Ω :
Type*
μ :
Measure Ω
upper :
score offset mark :
Ω → ℝ
T :
Set ℝ
loss :
ℝ → ℝ
z :
ℝ
n :
ℕ
x :
Fin n → Ω
def
localizedThresholdSup μ upper score offset mark T loss z x :
ℝ
given by
centeredSup μ (fun t : {t : ℝ // t ∈ T ∧ loss t ≤ z} => thresholdFunction upper score offset mark t.1) x
theorem localizedThreshold_countable_reduction reviewed
⚑ flagged
Causalean.Stat.EmpiricalProcess.Countable
If the score is measurable, and the offset and the mark are integrable under μ, then for any admissible cutoff set, population loss, and radius z, there is a countable set of eligible cutoffs (those in the admissible set with loss at most z) that contains the one-sided boundary of the eligible set, approximates every eligible cutoff from the correct side both pointwise and in population integral, and gives exactly the same localized threshold supremum as the full eligible set for every finite sample.
Formal statement
hypotheses
Ω :
Type*
μ :
Measure Ω
upper :
score offset mark :
Ω → ℝ
hscore :
Measurable score
hoffset :
Integrable offset μ
hmark :
Integrable mark μ
T :
Set ℝ
loss :
ℝ → ℝ
z :
ℝ
conclusion
∃ D : Set ℝ,
conclusion 1
t ∈ T :
loss t ≤ z
∃ s : ℕ → ℝ,
k :
s k ∈ D
OneSidedApproximates upper s t
x :
Tendsto (fun k => thresholdFunction upper score offset mark (s k) x) atTop (nhds (thresholdFunction upper score offset mark t x))
Tendsto (fun k => ∫ x, thresholdFunction upper score offset mark (s k) x ∂μ) atTop (nhds (∫ x, thresholdFunction upper score offset mark t x ∂μ))
conclusion 2
n :
ℕ
x :
Fin n → Ω
localizedThresholdSup μ upper score offset mark T loss z x
= centeredSup μ (fun t : D => thresholdFunction upper score offset mark t.1) x
Proof (Lean source)
theorem localizedThreshold_countable_reduction {Ω : Type*} [MeasurableSpace Ω]
(μ : Measure Ω) (upper : Bool) (score offset mark : Ω → ℝ)
(hscore : Measurable score) (hoffset : Integrable offset μ)
(hmark : Integrable mark μ) (T : Set ℝ) (loss : ℝ → ℝ) (z : ℝ) :
∃ D : Set ℝ, D.Countable ∧ D ⊆ {t ∈ T | loss t ≤ z} ∧
oneSidedBoundary upper {t ∈ T | loss t ≤ z} ⊆ D ∧
(∀ t ∈ T, loss t ≤ z → ∃ s : ℕ → ℝ,
(∀ k, s k ∈ D) ∧ OneSidedApproximates upper s t ∧
(∀ x, Tendsto (fun k => thresholdFunction upper score offset mark (s k) x)
atTop (nhds (thresholdFunction upper score offset mark t x))) ∧
Tendsto (fun k => ∫ x, thresholdFunction upper score offset mark (s k) x ∂μ)
atTop (nhds (∫ x, thresholdFunction upper score offset mark t x ∂μ))) ∧
(∀ (n : ℕ) (x : Fin n → Ω), localizedThresholdSup μ upper score offset mark
T loss z x = centeredSup μ (fun t : D =>
thresholdFunction upper score offset mark t.1) x) := by
-- Apply exists_countable_oneSided_skeleton to the already-localized set.
-- Bound all real suprema by the sample offset/mark absolute sums and
-- their population absolute integrals. Finite sums, subtraction and abs
-- preserve the pointwise/integral limits, giving both supremum inequalities.
classical
let E : Set ℝ := {t ∈ T | loss t ≤ z}
obtain ⟨D, hD, hDE, hboundary, happrox⟩ :=
exists_countable_oneSided_skeleton upper E
refine ⟨D, hD, hDE, hboundary, ?_, ?_⟩
· intro t ht hz
obtain ⟨s, hsD, hs⟩ := happrox t ⟨ht, hz⟩
exact ⟨s, hsD, hs, thresholdFunction_tendsto upper score offset mark s t hs,
thresholdFunction_integral_tendsto μ upper score offset mark hscore hoffset hmark
s t hs⟩
· intro n x
let F : ℝ → ℝ := fun t =>
|centeredEmpiricalAverage μ x
(thresholdFunction upper score offset mark t)|
let G : Ω → ℝ := fun y => |offset y| + |mark y|
have hG : Integrable G μ := hoffset.abs.add hmark.abs
have hbound (t : ℝ) (y : Ω) : |thresholdFunction upper score offset mark t y| ≤ G y := by
unfold thresholdFunction G
split_ifs <;> first
| exact abs_add_le _ _
| simpa only [add_zero] using le_add_of_nonneg_right (abs_nonneg (mark y))
have hF (t : ℝ) : F t ≤ |(n : ℝ)⁻¹| * ∑ j, G (x j) + ∫ y, G y ∂μ := by
have hint : |∫ y, thresholdFunction upper score offset mark t y ∂μ| ≤
∫ y, G y ∂μ := by
simpa only [Real.norm_eq_abs] using
norm_integral_le_of_norm_le (f := thresholdFunction upper score offset mark t)
hG (ae_of_all _ (fun y => by
simpa only [Real.norm_eq_abs] using hbound t y))
calc
F t ≤ |(n : ℝ)⁻¹ * ∑ j, thresholdFunction upper score offset mark t (x j)| +
|∫ y, thresholdFunction upper score offset mark t y ∂μ| := by
simpa only [F, centeredEmpiricalAverage,
sub_eq_add_neg, abs_neg] using abs_add_le
((n : ℝ)⁻¹ * ∑ j, thresholdFunction upper score offset mark t (x j))
(-(∫ y, thresholdFunction upper score offset mark t y ∂μ))
_ ≤ |(n : ℝ)⁻¹| * ∑ j, G (x j) + ∫ y, G y ∂μ := by
rw [abs_mul]
exact add_le_add (mul_le_mul_of_nonneg_left
((Finset.abs_sum_le_sum_abs _ _).trans
(Finset.sum_le_sum fun j _ => hbound t (x j))) (abs_nonneg _)) hint
have hbed : BddAbove (range (fun t : D => F t.1)) :=
⟨_, by rintro _ ⟨t, rfl⟩; exact hF t⟩
have hbee : BddAbove (range (fun t : E => F t.1)) :=
⟨_, by rintro _ ⟨t, rfl⟩; exact hF t⟩
change (⨆ t : E, F t.1) = ⨆ t : D, F t.1
rcases isEmpty_or_nonempty E with hempty | hnonempty
· have : IsEmpty D := ⟨fun t => isEmptyElim (⟨t.1, hDE t.2⟩ : E)⟩
simp only [iSup_of_empty']
· have : Nonempty E := hnonempty
obtain ⟨t⟩ := hnonempty
obtain ⟨s, hsD, hs⟩ := happrox t.1 t.2
have : Nonempty D := ⟨⟨s 0, hsD 0⟩⟩
apply le_antisymm
· apply ciSup_le
intro t
obtain ⟨s, hsD, hs⟩ := happrox t.1 t.2
have hlim : Tendsto (fun k => F (s k)) atTop (nhds (F t.1)) := by
apply Tendsto.abs
apply Tendsto.sub
· apply Tendsto.const_mul
apply tendsto_finsetSum
intro j _
exact thresholdFunction_tendsto upper score offset mark s t.1 hs (x j)
· exact thresholdFunction_integral_tendsto μ upper score offset mark
hscore hoffset hmark s t.1 hs
exact le_of_tendsto hlim (Eventually.of_forall fun k =>
le_ciSup hbed (⟨s k, hsD k⟩ : D))
· exact ciSup_le fun t => le_ciSup hbee (⟨t.1, hDE t.2⟩ : E)
5 supporting declarations (lemmas, instances)
-
thresholdFunction_measurabletheorem — If the score, offset, and mark are measurable, then the affine closed-threshold integrand is measurable at every fixed cutoff and either orientation.hypothesesΩ :Type*upper :score offset mark :Ω → ℝhs :Measurable scoreho :Measurable offsethm :Measurable markt :ℝconclusionMeasurable (thresholdFunction upper score offset mark t)Proof (Lean source)
@[fun_prop] theorem thresholdFunction_measurable {Ω : Type*} [MeasurableSpace Ω] (upper : Bool) (score offset mark : Ω → ℝ) (hs : Measurable score) (ho : Measurable offset) (hm : Measurable mark) (t : ℝ) : Measurable (thresholdFunction upper score offset mark t) := by cases upper · exact ho.add (hm.ite (measurableSet_le measurable_const hs) measurable_const) · exact ho.add (hm.ite (measurableSet_le hs measurable_const) measurable_const) -
thresholdFunction_tendstotheorem — If a sequence of cutoffs approaches the cutoff t from the side given by the orientation, then at every observation the affine closed-threshold integrand at the sequence's cutoffs converges to its value at t, with exact behavior retained at ties.hypothesesΩ :Type*upper :score offset mark :Ω → ℝs :ℕ → ℝt :ℝhs :OneSidedApproximates upper s tx :ΩconclusionTendsto (fun k => thresholdFunction upper score offset mark (s k) x) atTop (nhds (thresholdFunction upper score offset mark t x))Proof (Lean source)
theorem thresholdFunction_tendsto {Ω : Type*} (upper : Bool) (score offset mark : Ω → ℝ) (s : ℕ → ℝ) (t : ℝ) (hs : OneSidedApproximates upper s t) (x : Ω) : Tendsto (fun k => thresholdFunction upper score offset mark (s k) x) atTop (nhds (thresholdFunction upper score offset mark t x)) := by -- At score x = t all indicators agree exactly by the one-sided condition. -- Away from that tie, convergence of s makes the indicator eventually constant. classical apply Tendsto.congr' (f₁ := fun _ => thresholdFunction upper score offset mark t x) ?_ tendsto_const_nhds cases upper · by_cases h : t ≤ score x · exact Eventually.of_forall fun k => by simp [thresholdFunction, h, (hs.1 k).trans h] · have he := hs.2.eventually (isOpen_Ioi.mem_nhds (lt_of_not_ge h)) filter_upwards [he] with k hk simp [thresholdFunction, h, not_le_of_gt hk] · by_cases h : score x ≤ t · exact Eventually.of_forall fun k => by simp [thresholdFunction, h, h.trans (hs.1 k)] · have he := hs.2.eventually (isOpen_Iio.mem_nhds (lt_of_not_ge h)) filter_upwards [he] with k hk simp [thresholdFunction, h, not_le_of_gt hk] -
thresholdFunction_integral_tendstotheorem — If the score is measurable, the offset and the mark are integrable under μ, and a sequence of cutoffs approaches the cutoff t from the side given by the orientation, then the population integrals of the affine closed-threshold integrand at the sequence's cutoffs converge to its population integral at t.hypothesesΩ :Type*μ :Measure Ωupper :score offset mark :Ω → ℝhscore :Measurable scorehoffset :Integrable offset μhmark :Integrable mark μs :ℕ → ℝt :ℝhs :OneSidedApproximates upper s tconclusionTendsto (fun k => ∫ x, thresholdFunction upper score offset mark (s k) x ∂μ) atTop (nhds (∫ x, thresholdFunction upper score offset mark t x ∂μ))Proof (Lean source)
theorem thresholdFunction_integral_tendsto {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) (upper : Bool) (score offset mark : Ω → ℝ) (hscore : Measurable score) (hoffset : Integrable offset μ) (hmark : Integrable mark μ) (s : ℕ → ℝ) (t : ℝ) (hs : OneSidedApproximates upper s t) : Tendsto (fun k => ∫ x, thresholdFunction upper score offset mark (s k) x ∂μ) atTop (nhds (∫ x, thresholdFunction upper score offset mark t x ∂μ)) := by -- Dominate by |offset| + |mark|. Integrability supplies AE strong -- measurability of those functions, so full offset/mark measurability is unnecessary. classical have hmeas (u : ℝ) : AEStronglyMeasurable (thresholdFunction upper score offset mark u) μ := by cases upper · exact hoffset.aestronglyMeasurable.add (hmark.aestronglyMeasurable.restrict.piecewise (measurableSet_le measurable_const hscore) aestronglyMeasurable_zero) · exact hoffset.aestronglyMeasurable.add (hmark.aestronglyMeasurable.restrict.piecewise (measurableSet_le hscore measurable_const) aestronglyMeasurable_zero) apply tendsto_integral_of_dominated_convergence (fun x => |offset x| + |mark x|) (fun k => hmeas (s k)) (hoffset.abs.add hmark.abs) · intro k apply ae_of_all intro x rw [Real.norm_eq_abs] unfold thresholdFunction split_ifs <;> first | exact abs_add_le _ _ | simpa only [add_zero] using le_add_of_nonneg_right (abs_nonneg (mark x)) · exact ae_of_all _ (thresholdFunction_tendsto upper score offset mark s t hs) -
localizedThresholdSup_measurable_of_integrabletheorem — If the score, offset, and mark are measurable and the offset and the mark are integrable under μ, then for any admissible cutoff set, population loss, radius, and sample size, the localized threshold supremum is a measurable function of the sample.hypothesesΩ :Type*μ :Measure Ωupper :score offset mark :Ω → ℝhscore :Measurable scorehoffset :Measurable offsethmark :Measurable markhoint :Integrable offset μhmint :Integrable mark μT :Set ℝloss :ℝ → ℝz :ℝn :ℕconclusionMeasurable (localizedThresholdSup μ upper score offset mark T loss z (n := n))Proof (Lean source)
@[fun_prop] theorem localizedThresholdSup_measurable_of_integrable {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) (upper : Bool) (score offset mark : Ω → ℝ) (hscore : Measurable score) (hoffset : Measurable offset) (hmark : Measurable mark) (hoint : Integrable offset μ) (hmint : Integrable mark μ) (T : Set ℝ) (loss : ℝ → ℝ) (z : ℝ) (n : ℕ) : Measurable (localizedThresholdSup μ upper score offset mark T loss z (n := n)) := by -- Obtain a fixed eligible D from localizedThreshold_countable_reduction. -- Each centered empirical evaluation on D is measurable: it is a -- finite measurable sum minus a fixed population integral. Measurable.iSup -- applies even if D is empty. The pointwise sample envelopes used in -- the reduction need not be uniformly bounded across observation points. classical obtain ⟨D, hD, _, _, _, heq⟩ := localizedThreshold_countable_reduction μ upper score offset mark hscore hoint hmint T loss z have : Countable D := hD.to_subtype have hm : Measurable (fun x : Fin n → Ω => centeredSup μ (fun t : D => thresholdFunction upper score offset mark t.1) x) := by apply Measurable.iSup intro t apply continuous_abs.measurable.comp apply Measurable.sub _ measurable_const apply Measurable.const_mul apply Finset.measurable_sum intro j _ exact (thresholdFunction_measurable upper score offset mark hscore hoffset hmark t.1).comp (measurable_pi_apply j) have heqfun := funext (heq n) rw [heqfun] exact hm -
localizedThresholdSup_measurabletheorem — Under a probability law μ, if the score, offset, and mark are measurable and the sum of the absolute offset and absolute mark is bounded everywhere by a nonnegative constant K, then for any admissible cutoff set, population loss, radius, and sample size, the localized threshold supremum is a measurable function of the sample.hypothesesΩ :Type*μ :upper :score offset mark :Ω → ℝhscore :Measurable scorehoffset :Measurable offsethmark :Measurable markK :ℝhK :0 ≤ Khb :∀ x, |offset x| + |mark x| ≤ KT :Set ℝloss :ℝ → ℝz :ℝn :ℕconclusionMeasurable (localizedThresholdSup μ upper score offset mark T loss z (n := n))Proof (Lean source)
@[fun_prop] theorem localizedThresholdSup_measurable {Ω : Type*} [MeasurableSpace Ω] (μ : Measure Ω) [IsProbabilityMeasure μ] (upper : Bool) (score offset mark : Ω → ℝ) (hscore : Measurable score) (hoffset : Measurable offset) (hmark : Measurable mark) (K : ℝ) (hK : 0 ≤ K) (hb : ∀ x, |offset x| + |mark x| ≤ K) (T : Set ℝ) (loss : ℝ → ℝ) (z : ℝ) (n : ℕ) : Measurable (localizedThresholdSup μ upper score offset mark T loss z (n := n)) := by have hKabs : |K| = K := abs_of_nonneg hK apply localizedThresholdSup_measurable_of_integrable μ upper score offset mark hscore hoffset hmark ?_ ?_ T loss z n · exact Integrable.of_bound hoffset.aestronglyMeasurable |K| (ae_of_all _ (fun x => by rw [Real.norm_eq_abs, hKabs] exact (le_add_of_nonneg_right (abs_nonneg (mark x))).trans (hb x))) · exact Integrable.of_bound hmark.aestronglyMeasurable |K| (ae_of_all _ (fun x => by rw [Real.norm_eq_abs, hKabs] exact (le_add_of_nonneg_left (abs_nonneg (offset x))).trans (hb x)))
TraceOrdering 1 core · 0 supporting A nested family, even with an uncountable index type, induces a finite chain of observation traces. ★ nested_trace_prefix
Ordering finite traces of arbitrary nested families
A nested family, even with an uncountable index type, induces a finite chain of observation traces. One permutation makes all traces prefixes, including duplicate observations and traces empty or equal to the full sample. This combinatorial statement is independent of sign laws and Doob estimates.
theorem nested_trace_prefix reviewed
⚑ flagged
Causalean.Stat.EmpiricalProcess.Countable
If a family of sets is nested, any two members being comparable by inclusion, then for any finite sample there is a permutation of the sample positions after which the observations lying in each member of the family form an initial segment.
Formal statement
Proof (Lean source)
theorem nested_trace_prefix {Ω ι : Type*} (B : ι → Set Ω)
(hchain : ∀ i k, B i ⊆ B k ∨ B k ⊆ B i) {n : ℕ} (x : Fin n → Ω) :
∃ p : Perm (Fin n), ∀ i, ∃ k : Fin (n + 1),
∀ j : Fin n, x (p j) ∈ B i ↔ j.val < k.val := by
classical
let trace : ι → Finset (Fin n) := fun i => Finset.univ.filter (fun j => x j ∈ B i)
let T := Finset.univ.powerset.filter (fun s : Finset (Fin n) => ∃ i, trace i = s)
let absent := fun j : Fin n => T.filter (fun s => j ∉ s)
let rank := fun j => (absent j).card
have hrank : ∀ i a b, x a ∈ B i → x b ∉ B i → rank a < rank b := by
intro i a b ha hb
have hsub : absent a ⊆ absent b := by
intro s hs
obtain ⟨hsT, has⟩ := Finset.mem_filter.mp hs
obtain ⟨k, rfl⟩ := (Finset.mem_filter.mp hsT).2
refine Finset.mem_filter.mpr ⟨hsT, ?_⟩
simp only [trace, mem_filter, Finset.mem_univ, true_and] at has ⊢
rcases hchain k i with hki | hik
· exact fun hbk => hb (hki hbk)
· exact (has (hik ha)).elim
have hmem : trace i ∈ absent b := by
simp only [absent, mem_filter]
refine ⟨?_, ?_⟩
· simp [T, Finset.mem_powerset, Finset.subset_univ]
· simpa [trace] using hb
have hnmem : trace i ∉ absent a := by
simp [absent, trace, ha]
apply Finset.card_lt_card
refine Finset.ssubset_iff_subset_ne.mpr ⟨hsub, ?_⟩
intro heq
exact hnmem (heq.symm ▸ hmem)
let p := Tuple.sort rank
have hdown : ∀ i (j k : Fin n), j ≤ k → x (p k) ∈ B i → x (p j) ∈ B i := by
intro i j k hjk hk
by_contra hj
have hlt := hrank i (p k) (p j) hk hj
have hle := Tuple.monotone_sort rank hjk
exact (not_lt_of_ge hle) hlt
refine ⟨p, fun i => ?_⟩
let S := Finset.univ.filter (fun j : Fin n => x (p j) ∈ B i)
have hcard : S.card ≤ n := by
simpa using Finset.card_le_card (filter_subset (fun j => x (p j) ∈ B i) univ)
refine ⟨⟨S.card, Nat.lt_succ_of_le hcard⟩, fun j => ?_⟩
change x (p j) ∈ B i ↔ j.val < S.card
constructor
· intro hj
have hsub : Iic j ⊆ S := by
intro k hk
exact Finset.mem_filter.mpr ⟨Finset.mem_univ _, hdown i k j (Finset.mem_Iic.mp hk) hj⟩
have hc := Finset.card_le_card hsub
rw [Fin.card_Iic] at hc
exact Nat.lt_of_succ_le hc
· intro hj
by_contra hnot
have hsub : S ⊆ Finset.Iio j := by
intro k hk
apply Finset.mem_Iio.mpr
by_contra hkj
exact hnot (hdown i j k (le_of_not_gt hkj) (Finset.mem_filter.mp hk).2)
have hc := Finset.card_le_card hsub
rw [Fin.card_Iio] at hc
exact (not_lt_of_ge hc) hj