Documentation

LeanPool.Superdiffusion.Algsuperdiff.Section3.Provider.MultiscaleEstimate.BadEventCeiling

BadEventCeiling #

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

Provider: the Markov-plus-[0,1]-ceiling engine of the bad-event sum #

Nothing in this file mentions Section 3 carriers; the Section 3 instances live in BadEventIngredients.lean.

The two mechanisms #

(1) Indicator pricing against a two-summand tail bound. The proved bad-event probability (bad_event_estimate) is a sum of two exponentials — the oscillation lane exp(-a) and the doubly-exponential ellipticity lane exp(-b) — records that the printed e.badevent.indicator.propagate wrongly discards the second summand. isBigOWith_gammaSigma_indicator_of_two_exp keeps both:

    mu.real E <= exp(-a) + exp(-b)
      ==>  1_E <= O_{Gamma_rho}( (4/a)^{1/rho} + (4/b)^{1/rho} ) ,

with no lower bound on a or b beyond positivity. The reason a bound such as min(a,b) >= log 2 is not needed is the deterministic ceiling 1_E <= 1: when the printed amplitude is already >= 1 the conclusion is free, and when it is < 1 the exponent x := A^{-rho} is automatically > 1, which is exactly the margin the union of the two lanes costs. The union itself is the proved Provider.Percolation.exp_add_exp_le (Provider/Percolation/Numerics.lean), consumed at 4x <= a, 4x <= b, 1 <= x.

(2) The rho-th power of a [0,1]-valued mean. records that the manuscript's "crude application of the triangle inequality e.Gamma.sigma.triangle" is not the mechanism of the display

    ( avsum_z 1_{not Q(l,l-h,z)} )^rho  <=  O_{Gamma_1}( C rho^{-1} cstar^{-1} 3^{5h} cgamma ) :

the countable Gamma_sigma triangle costs (1+|log s|)/s, which the display's own eps^{-C} cannot absorb. What proves it is Markov's inequality plus the deterministic [0,1] ceiling, applied to the normalized sum, followed by CoarseGraining's free power rule isBigOWith_gammaSigma_rpow at p = rho (which sends Gamma_rho to Gamma_{rho/rho} = Gamma_1 and the scale A to A^rho). The printed rho^{-1} is the join constant between the Markov branch and the boundedness branch, not a triangle cost; it is obtained here at the explicit constant 4. No union bound, no log |F|, no grid cardinality, and neither gammaGrowthConst nor gammaTriangleConst is invoked.

Consumer fit: the [0,1] ceiling, never an Orlicz product #

The display e.local.bad.events.summed multiplies e.mathcalE.crude.bound against the bad-event factor

    W  =  max_l 3^{-s(m-l)/2} ( avsum_z 1_{not Q(l,l-h,z)} )^{s/d} .

(The Gamma_1 x Gamma_1 lane fails separately, on amplitude: polynomially small against an exponentially small rare budget.)

The mechanism that does work is W's own pointwise [0,1] ceiling, exported here as indicatorAverage_mem_Icc and weightedIndicatorAverage_rpow_mem_Icc. At 0 <= W <= 1 and Y >= 0 one has Y . W <= Y pointwise, so the crude bound's Gamma_1 lane and its Gamma_{2/7} lane both pass through unchanged — the printed amplitudes verbatim, with no index loss — and only the deterministic shift of e.mathcalE.crude.bound consumes the factor's own Gamma_1 smallness. The output is exactly the printed Gamma_1 + Gamma_{2/7} shape of e.local.bad.events.summed.

The Y >= 0 in that pointwise step is not free, and the pass-through is at unchanged amplitude only after the free witness clamp Provider.Tail.isBigOWith_max_zero (Provider/Tail/TailSqrt.lean) has replaced each of the two Orlicz witnesses by max 0 (.) at the same scale: the witnesses of a two-term one-sided display are only known to be measurable and dominating, never nonnegative.

Main results #

Algsuperdiff.Section3.Provider.MultiscaleEstimate.boundedMean_rpow_isBigOWith_gammaOne_of_two_exp

indicatorAverage_rpow_isBigOWith_gammaOne_of_two_exp

In-repo consumed set #

Provider.Orlicz.isBigOWith_gammaSigma_indicator_of_le, Provider.Percolation.exp_add_exp_le; from CoarseGraining, Homogenization.IndependentSums.gammaSigma, isBigOWith_gammaSigma_iff, isBigOWith_gammaSigma_rpow, upperTailEvent, mem_upperTailEvent. Nothing else from this repository is used.

References #

1. The deterministic [0,1] ceiling #

source
theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.isBigOWith_gammaSigma_of_le_one {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {sigma A : ℝ} (h1 : ∀ (omega : Ω), X omega ≤ 1) (hA : 1 ≤ A) :
HCPolySupport.IndependentSums.IsBigOWith μ (HCPolySupport.IndependentSums.gammaSigma sigma) X A

The ceiling branch. An observable bounded above by 1 satisfies every stretched-exponential upper-tail relation at every scale A ≥ 1, because the tail event {X > A t} is empty for t ≥ 1.

This is one of the two branches of the manuscript's averaged-indicator display, and it is also what makes the two-summand indicator bound below unconditional: whenever the printed amplitude is already at least one, there is nothing to prove.

2. The two-lane exponential arithmetic #

The union of the two lanes is the proved Provider.Percolation.exp_add_exp_le (Provider/Percolation/Numerics.lean): at 1 ≤ x, 4x ≤ a and 4x ≤ b one has -a + 1 ≤ -x and -b + 1 ≤ -x, hence exp(-a) + exp(-b) ≤ exp(-x).

4. The arithmetic core of the Markov/ceiling join (abstract reals) #

5. Markov plus boundedness #

source
theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.boundedMean_isBigOWith_gammaSigma {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : Ω → ℝ} {K rho : ℝ} (hrho : 0 < rho) (hrho2 : rho ≤ 2) (hK : 0 < K) (hmeas : MeasureTheory.AEStronglyMeasurable X μ) (h0 : ∀ (omega : Ω), 0 ≤ X omega) (h1 : ∀ (omega : Ω), X omega ≤ 1) (hmean : ∫ (omega : Ω), X omega ∂μ ≤ Real.exp (-K⁻¹)) :
HCPolySupport.IndependentSums.IsBigOWith μ (HCPolySupport.IndependentSums.gammaSigma rho) X ((4 * rho⁻¹ * K) ^ rho⁻¹)

The Gamma_rho bound of the Markov/ceiling join. A [0,1]-valued observable whose mean is at most e^{-1/K} is O_{Gamma_rho} at scale (4 rho^{-1} K)^{1/rho}, for every rho ∈ (0,2].

Two branches on the tail height A t:

  • A t ≥ 1: the event {X > A t} is empty, because X ≤ 1;
  • A t < 1: Markov gives mass ≤ e^{-1/K}/(A t), and join_algebra says this is ≤ e^{-t^rho} (using t < A⁻¹, hence t^rho ≤ (A^rho)⁻¹ = rho/(4K)).

The rho^{-1} in the scale is exactly what makes the two branches meet: it is the join constant, and not a triangle-inequality cost.

source
theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.boundedMean_rpow_isBigOWith_gammaOne {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : Ω → ℝ} {K rho : ℝ} (hrho : 0 < rho) (hrho2 : rho ≤ 2) (hK : 0 < K) (hmeas : MeasureTheory.AEStronglyMeasurable X μ) (h0 : ∀ (omega : Ω), 0 ≤ X omega) (h1 : ∀ (omega : Ω), X omega ≤ 1) (hmean : ∫ (omega : Ω), X omega ∂μ ≤ Real.exp (-K⁻¹)) :
HCPolySupport.IndependentSums.IsBigOWith μ (HCPolySupport.IndependentSums.gammaSigma 1) (fun (omega : Ω) => X omega ^ rho) (4 * rho⁻¹ * K)

The Gamma_1 bound after the free power conversion. A [0,1]-valued observable with mean at most e^{-1/K} satisfies

    X^rho  <=  O_{Gamma_1}( 4 rho^{-1} K )      (0 < rho <= 2) .

This is boundedMean_isBigOWith_gammaSigma followed by CoarseGraining's power rule isBigOWith_gammaSigma_rpow at p = rho, which is exact and free: it sends Gamma_rho to Gamma_{rho/rho} = Gamma_1 and the scale A to A^rho = 4 rho^{-1} K.

source
theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.boundedMean_rpow_isBigOWith_gammaOne_of_two_exp {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : Ω → ℝ} {a b rho : ℝ} (hrho : 0 < rho) (hrho2 : rho ≤ 2) (ha : 0 < a) (hb : 0 < b) (hmeas : MeasureTheory.AEStronglyMeasurable X μ) (h0 : ∀ (omega : Ω), 0 ≤ X omega) (h1 : ∀ (omega : Ω), X omega ≤ 1) (hmean : ∫ (omega : Ω), X omega ∂μ ≤ Real.exp (-a) + Real.exp (-b)) :
HCPolySupport.IndependentSums.IsBigOWith μ (HCPolySupport.IndependentSums.gammaSigma 1) (fun (omega : Ω) => X omega ^ rho) (4 * rho⁻¹ * (4 / a + 4 / b))

The two-lane form of the Markov/ceiling display. A [0,1]-valued observable whose mean obeys the two-summand bound E[X] ≤ exp(-a) + exp(-b) satisfies

    X^rho  <=  O_{Gamma_1}( 4 rho^{-1} (4/a + 4/b) )     (0 < rho <= 2) .

Both lanes survive at their own amplitude, as requires; the manuscript's display keeps only the first. As in isBigOWith_gammaSigma_indicator_of_two_exp, no size hypothesis on a or b is needed: if K := 4/a + 4/b ≥ 1 the deterministic ceiling already gives the conclusion (the amplitude is then ≥ 4 rho^{-1} ≥ 2), and otherwise K⁻¹ > 1 with 4 K⁻¹ ≤ a and 4 K⁻¹ ≤ b, which is the input of Provider.Percolation.exp_add_exp_le.

6. The pointwise [0,1] ceiling of a weighted indicator average #

source
theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.indicatorAverage_mem_Icc {Ω : Type u_1} {iota : Type u_2} (F : Finset iota) (B : iota → Set Ω) (omega : Ω) :
(↑F.card)⁻¹ * ∑ z ∈ F, (B z).indicator (fun (x : Ω) => 1) omega ∈ Set.Icc 0 1

The pointwise ceiling. A volume-normalized average of indicators takes values in [0,1] at every sample point, for an arbitrary finite index set — the empty one included, where (F.card : ℝ)⁻¹ = 0 makes the average 0.

This is the deterministic fact behind the Markov/ceiling join below, and it is also the consumer mechanism recorded: the bad-event factor of e.local.bad.events.summed is built from this average, hence is [0,1]-valued pointwise, hence multiplies the crude bound's lanes without touching their Orlicz indices.

source
theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.weightedIndicatorAverage_rpow_mem_Icc {Ω : Type u_1} {iota : Type u_2} (F : Finset iota) (B : iota → Set Ω) {w rho : ℝ} (hw0 : 0 ≤ w) (hw1 : w ≤ 1) (hrho : 0 ≤ rho) (omega : Ω) :
w * ((↑F.card)⁻¹ * ∑ z ∈ F, (B z).indicator (fun (x : Ω) => 1) omega) ^ rho ∈ Set.Icc 0 1

The weighted rho-th power of the ceiling. For a weight w ∈ [0,1] and any exponent rho ≥ 0,

    0  <=  w . ( avsum_{z in F} 1_{B z} )^rho  <=  1        pointwise.

Consequently the crude bound's Gamma_1 lane and its Gamma_{2/7} lane pass through the product unchanged, at their printed amplitudes and indices, and only the deterministic shift consumes the factor's own smallness. No Orlicz product e.multGammasig is taken; that route is index-refuted (2/9 < 1/4).

7. The averaged-indicator instance #

source
theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.indicatorAverage_rpow_isBigOWith_gammaOne_of_two_exp {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {iota : Type u_2} {F : Finset iota} (hF : F.Nonempty) {B : iota → Set Ω} (hBmeas : ∀ z ∈ F, MeasurableSet (B z)) {a b rho : ℝ} (hrho : 0 < rho) (hrho2 : rho ≤ 2) (ha : 0 < a) (hb : 0 < b) (hB : ∀ z ∈ F, μ.real (B z) ≤ Real.exp (-a) + Real.exp (-b)) :
HCPolySupport.IndependentSums.IsBigOWith μ (HCPolySupport.IndependentSums.gammaSigma 1) (fun (omega : Ω) => ((↑F.card)⁻¹ * ∑ z ∈ F, (B z).indicator (fun (x : Ω) => 1) omega) ^ rho) (4 * rho⁻¹ * (4 / a + 4 / b))

The volume-normalized average of indicators, at a two-summand per-event tail bound. If every event of a finite nonempty family has mass at most exp(-a) + exp(-b), then for every rho ∈ (0,2]

    ( avsum_{z in F} 1_{B z} )^rho  <=  O_{Gamma_1}( 4 rho^{-1} (4/a + 4/b) ) .

The mean is computed by linearity — E[ avsum_z 1_{B z} ] = avsum_z P[B z] — so no union bound and no log |F| occurs: means average, they do not add. This is why the manuscript's display carries no grid-cardinality factor, and it is the honest content of the sentence corrects.