CenteredIndicator

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

Weak-Orlicz pricing of indicators and of centered indicators

ABK26's estimate e.indc.O.sigma prices the indicator of a rare event, 1_E ≤ O_{Γ_σ}(|log ℙ[E]|^{-1/σ}). CoarseGraining proves that estimate at the exact scale gammaIndicatorScale σ ℙ[E] = (-log ℙ[E])^{-1/σ}, under the standing assumption 0 < ℙ[E] < 1.

Two adjustments are needed before the estimate can feed the ABK26 concentration inequality, and both are supplied here.

• Call sites carry a majorant of the scale, in the form ℙ[E] ≤ exp(-A^{-σ}), and must tolerate a null event. isBigOWith_gammaSigma_indicator_of_le proves the indicator bound directly at such an A, with no positivity assumption on ℙ[E].
• The concentration inequality consumes centered, two-sided summands.

Main results

• Algsuperdiff.Section3.Provider.Orlicz.isBigOWith_gammaSigma_indicator_of_le
• Algsuperdiff.Section3.Provider.Orlicz.isBigO_gammaSigma_indicator_sub_measureReal
• Algsuperdiff.Section3.Provider.Orlicz.exp_neg_rpow_neg_two_le
• Algsuperdiff.Section3.Provider.Orlicz.isBigO_gammaSigma_two_indicator_sub_measureReal

References

• ABK26, e.indc.O.sigma.
• ABK26, Step 1 of l.percolation.bound.general.

theorem Algsuperdiff.Section3.Provider.Orlicz.isBigOWith_gammaSigma_indicator_of_le {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {E : Set Ω} {σ A : ℝ} (hσ : 0 ≤ σ) (hA : 0 < A) (hE : μ.real E ≤ Real.exp (-A ^ (-σ))) : HCPolySupport.IndependentSums.IsBigOWith μ (HCPolySupport.IndependentSums.gammaSigma σ) (E.indicator fun (x : Ω) => 1) A

Indicator pricing at a majorant scale.

If ℙ[E] ≤ exp(-A^{-σ}) with A > 0 then 1_E ≤ O_{Γ_σ}(A).

theorem Algsuperdiff.Section3.Provider.Orlicz.isBigO_gammaSigma_indicator_sub_measureReal {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {E : Set Ω} {σ A : ℝ} (hσ : 0 ≤ σ) (hA : 0 < A) (hE : μ.real E ≤ Real.exp (-A ^ (-σ))) (hpA : μ.real E ≤ A) : HCPolySupport.IndependentSums.IsBigO μ (HCPolySupport.IndependentSums.gammaSigma σ) (fun (ω : Ω) => E.indicator (fun (x : Ω) => 1) ω - μ.real E) (2 * A)

Centered indicator pricing.

For a rare event E with ℙ[E] ≤ exp(-A^{-σ}) and ℙ[E] ≤ A, the centered indicator satisfies the two-sided relation 1_E - ℙ[E] = O_{Γ_σ}(2A). This is the form required by the ABK26 concentration inequality, which consumes centered summands with two-sided tails.

theorem Algsuperdiff.Section3.Provider.Orlicz.exp_neg_rpow_neg_two_le {A : ℝ} (hA : 0 < A) (hA1 : A ≤ 1) : Real.exp (-A ^ (-2)) ≤ A

For 0 < A ≤ 1 the tail bound exp(-A^{-2}) is itself at most A. This is the elementary inequality that makes the hypothesis ℙ[E] ≤ A of isBigO_gammaSigma_indicator_sub_measureReal automatic at σ = 2.

theorem Algsuperdiff.Section3.Provider.Orlicz.isBigO_gammaSigma_two_indicator_sub_measureReal {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ] {E : Set Ω} {A : ℝ} (hA : 0 < A) (hA1 : A ≤ 1) (hE : μ.real E ≤ Real.exp (-A ^ (-2))) : HCPolySupport.IndependentSums.IsBigO μ (HCPolySupport.IndependentSums.gammaSigma 2) (fun (ω : Ω) => E.indicator (fun (x : Ω) => 1) ω - μ.real E) (2 * A)

Centered indicator pricing at σ = 2, in call-site form.

For 0 < A ≤ 1 and ℙ[E] ≤ exp(-A^{-2}), the centered indicator satisfies 1_E - ℙ[E] = O_{Γ₂}(2A). This is the exact form consumed by Step 1 of ABK26's l.percolation.bound.general, where A = T^{-1} 3^{-aL/2} and the tail hypothesis is ℙ[B_L(z)] ≤ exp(-T² 3^{aL}).