GaussianMaximum

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Tail-law transport and finite maxima with one-sided Gaussian tails

This module packages the finite-maximum estimate needed for the cutoff argument. It assumes neither independence nor identically distributed variables: the only probabilistic input is the literal one-sided Gaussian tail for each member of the finite family.

theorem Algsuperdiff.Probability.isBigOWith_gammaSigma_of_map_eq {Ω : Type u_1} {Ω' : Type u_2} [MeasurableSpace Ω] [MeasurableSpace Ω'] {μ : MeasureTheory.Measure Ω} {μ' : MeasureTheory.Measure Ω'} {X : Ω → ℝ} {Y : Ω' → ℝ} {σ A : ℝ} (hX : Measurable X) (hY : Measurable Y) (hmap : MeasureTheory.Measure.map X μ = MeasureTheory.Measure.map Y μ') (hYtail : HCPolySupport.IndependentSums.IsBigOWith μ' (HCPolySupport.IndependentSums.gammaSigma σ) Y A) : HCPolySupport.IndependentSums.IsBigOWith μ (HCPolySupport.IndependentSums.gammaSigma σ) X A

A one-sided Gamma tail depends only on the pushforward law of the observable.

theorem Algsuperdiff.Probability.isBigOWith_gammaSigma_two_of_gaussian_tail {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {X : Ω → ℝ} {A : ℝ} (hTail : ∀ (t : ℝ), 1 ≤ t → μ {ω : Ω | A * t < X ω} ≤ ENNReal.ofReal (Real.exp (-t ^ 2))) : HCPolySupport.IndependentSums.IsBigOWith μ (HCPolySupport.IndependentSums.gammaSigma 2) X A

The literal J2 Gaussian upper-tail estimate, at positive scale A, is the Γ₂ weak-Orlicz estimate used by the finite-maximum A in CoarseGraining.

theorem Algsuperdiff.Probability.finset_sup'_nonneg {Ω : Type u_1} {ι : Type u_2} {s : Finset ι} (hs : s.Nonempty) {X : ι → Ω → ℝ} (hX : ∀ i ∈ s, ∀ (ω : Ω), 0 ≤ X i ω) (ω : Ω) : 0 ≤ s.sup' hs fun (i : ι) => X i ω

Pointwise nonnegativity passes to a nonempty finite supremum.

theorem Algsuperdiff.Probability.measurable_finset_sup' {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {s : Finset ι} (hs : s.Nonempty) {X : ι → Ω → ℝ} (hX : ∀ i ∈ s, Measurable (X i)) : Measurable fun (ω : Ω) => s.sup' hs fun (i : ι) => X i ω

A finite supremum of measurable variables is measurable.

theorem Algsuperdiff.Probability.integrable_finset_sup'_of_gaussian_tail {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {s : Finset ι} (hs : s.Nonempty) {X : ι → Ω → ℝ} {A : ℝ} (hA : 0 < A) (hX_nonneg : ∀ i ∈ s, ∀ (ω : Ω), 0 ≤ X i ω) (hX_meas : ∀ i ∈ s, Measurable (X i)) (hTail : ∀ i ∈ s, ∀ (t : ℝ), 1 ≤ t → μ {ω : Ω | A * t < X i ω} ≤ ENNReal.ofReal (Real.exp (-t ^ 2))) : MeasureTheory.Integrable (fun (ω : Ω) => s.sup' hs fun (i : ι) => X i ω) μ

A nonempty finite family with literal J2 tails has an integrable maximum. The conclusion includes the singleton case; max 1 (log card) is essential there, since log 1 = 0.

theorem Algsuperdiff.Probability.integral_finset_sup'_le_of_gaussian_tail {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {s : Finset ι} (hs : s.Nonempty) {X : ι → Ω → ℝ} {A : ℝ} (hA : 0 < A) (hX_nonneg : ∀ i ∈ s, ∀ (ω : Ω), 0 ≤ X i ω) (hX_meas : ∀ i ∈ s, Measurable (X i)) (hTail : ∀ i ∈ s, ∀ (t : ℝ), 1 ≤ t → μ {ω : Ω | A * t < X i ω} ≤ ENNReal.ofReal (Real.exp (-t ^ 2))) : ∫ (ω : Ω), s.sup' hs fun (i : ι) => X i ω ∂μ ≤ HCPolySupport.IndependentSums.gammaMomentConst 2 * √(3 * max 1 (Real.log ↑s.card)) * A

Quantitative expectation bound for a nonempty finite maximum with literal J2 tails. For a family of size at least two this is the usual sqrt (3 log card) bound; the max 1 is the explicit, nondegenerate singleton convention.

theorem Algsuperdiff.Probability.max_log_three_pow_le (d q : ℕ) : max 1 (Real.log ↑((3 ^ d) ^ q)) ≤ (1 + ↑d * Real.log 3) * (1 + ↑q)

The logarithm of a triadic descendant count has the elementary dimension--depth bound used to turn the preceding estimate into a sqrt (1 + q) estimate.

theorem Algsuperdiff.Probability.integral_finset_sup'_le_of_gaussian_tail_of_card_eq_three_pow_sqrt {Ω : Type u_1} {ι : Type u_2} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {s : Finset ι} (hs : s.Nonempty) {X : ι → Ω → ℝ} {A : ℝ} (hA : 0 < A) {d q : ℕ} (hCard : s.card = (3 ^ d) ^ q) (hX_nonneg : ∀ i ∈ s, ∀ (ω : Ω), 0 ≤ X i ω) (hX_meas : ∀ i ∈ s, Measurable (X i)) (hTail : ∀ i ∈ s, ∀ (t : ℝ), 1 ≤ t → μ {ω : Ω | A * t < X i ω} ≤ ENNReal.ofReal (Real.exp (-t ^ 2))) : ∫ (ω : Ω), s.sup' hs fun (i : ι) => X i ω ∂μ ≤ HCPolySupport.IndependentSums.gammaMomentConst 2 * √(3 * (1 + ↑d * Real.log 3)) * √(1 + ↑q) * A

The descendant-card specialization of the finite Gaussian-maximum estimate, with a constant depending only on the dimension.