BadEventIngredients

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

Provider: the two ingredient displays of the bad-event sum

Three displays are delivered:

1. e.mathcalE.crude.bound — the crude deterministic-plus-tails bound on mathcal E^2_{s/4,infty,2}(cu_m; a_m, shom);
2. e.badevent.indicator.propagate — in the S form required, at rho free (hence at rho = s/d, which refutes the printed rho = s/2d);
3. the averaged-indicator display — by Markov plus the deterministic [0,1] ceiling, at the amplitude C d s^{-1} cstar^{-1} 3^{5h} cgamma.

Displays 2 and 3 are independent consumers of the same per-site probability input: display 3 does not route through display 2. It never forms the indicator's Gamma_rho bound at all; it averages the per-site measures and applies the ceiling engine of BadEventCeiling.lean directly.

This is a provider endpoint only. It is not a source node, not a frozen declaration, and it does not close p.multiscale.estimate or any part of it.

1. The crude bound and the gauge index

The consumed inputs are exactly two, both proved:

• the q = 2 face of l.mathcal.E.to.Lambdas, Provider.Tail.sq_cutoffHomogenizationError_le, which gives mathcal E^2 <= 2 Lambda shom^{-1} + 2 lambda^{-1} shom almost surely at a free comparator scale; and
• the frozen p.cg.ellipticity.bounds (Frozen.Section3.coarse_ellipticity_bounds), consumed at sigma = 1/7 (this is the unique sigma at which the endpoints' printed indices Gamma_{(1-sigma)/3} and Gamma_{(1-sigma)/2} become the crude route's Gamma_{2/7} and Gamma_{3/7}), q = 2, and its own s-slot pinned at s/4.

Gauge index. p.cg.ellipticity.bounds normalizes both payloads at shom_{m-1}, while the printed display reads them at shom_m: this is exactly. Both readings are provided:

• It is retained as supporting A only: it bounds a different observable, namely Observable.cutoffHomogenizationErrorAtComparatorScale M m (m-1) (the error normalized at shom_{m-1}), whereas every printed step of p.multiscale.estimate reads Observable.cutoffHomogenizationError M m (= the same observable at comparator scale m). It therefore appears in no printed step and closes no fraction of any display; it is kept because it is certified, harmless, and the honest record of what the frozen ellipticity statement gives before any gauge conversion;

• exists_crude_bound is the display at the printed comparator scale m, at the cost of the two-sided running-diffusivity sandwich shom_{m-1} <= 4 shom_m and shom_m <= 4 . 3^{cgamma} shom_{m-1} (ABK26).

• the binder inductionState M m E is at the multiscale root — the m-th error conjunct of the state at index m is the root's own conclusion, so no consumer at the root can supply it;

• the true statement is narrower: it is the two proved lemmas Provider.Multiscale.sigmaBar_le_four_mul_sigmaBar and ..._le_four_mul_rpow_mul_sigmaBar that require the state at a scale >= m. The clause-direction reason was mis-stated as well: the frozen inductionState M m0 E quantifies both of its clauses over m <= m0, so what a conversion at the pair (m-1, m) needs is the larger scale inside the range; l.shom.continuity supplies exactly that at m0 := m, from a state at m - 1, because its own proof runs the recurrence up to m0.

Consuming l.shom.continuity at m0 := m, m := m, n := m - 1 reads its conjunct 2 (shom_{m-1} shom_m^{-1} <= 4) and its conjunct 3 (shom_m <= 4. 3^{cgamma (m-n)} shom_{m-1}, here at m - n = 1). The complementary branch is now m <= mStarStar M, which is where Provider.Base.exists_baseCaseMStarStarErrorConst reaches.

Constants. l.shom.continuity is an exists C statement, so exists_crude_bound exports two dimensional constants: Ccg, the constant of p.cg.ellipticity.bounds in which the display's own amplitudes are written, and Cshom, the constant of l.shom.continuity appearing only in the E-gate. Each is obtained once, and neither is composed with the other.

The s-window. The frozen ellipticity statement's s-slot carries the window s/4 in [cgamma/2 + exp(-Ccg^{-1} E^{-2} cgamma^{-1}), 1]. The chain is exp(7 Ccg) <= E (the seam gate at sigma = 1/7) => 4 Ccg^2 <= E => 2 Ccg <= sqrt E; the fifth-root gate E <= cgamma^{-1/5} gives sqrt(cgamma^{-1}) >= E^2 sqrt E >= 2 Ccg E^2, and log x <= 2 sqrt x turns this into log(cgamma^{-1}) <= Ccg^{-1} E^{-2} cgamma^{-1}, i.e. exp(-Ccg^{-1} E^{-2} cgamma^{-1}) <= cgamma; and 8 cgamma <= s gives s/4 - cgamma/2 >= 3 cgamma/2 >= cgamma.

At sigma = 2/7 this is (1 + log 2)^{7/2} < 6.4. gammaTriangleConst and gammaGrowthConst are never invoked.

2. The split indicator display and the averaged-indicator display

The proved bad-event probability is a sum of two exponentials, and the already-applied multiscale-parameter form Provider.BadEvents.exists_measureReal_compl_goodLocalEventAt_le_of_multiscaleParameters delivers it with all gates discharged:

P[ not Q(l, l-h, z) ]
  <= exp( - c cstar cgamma^{-1} 3^{-5h} ) + exp( - exp( c E^{-2} cgamma^{-1} ) ) .

The averaged-indicator display is proved by the engine of BadEventCeiling.lean (Markov plus the deterministic [0,1] ceiling on the normalized sum), never by the Orlicz triangle inequality and that module's header. The grid 3^l Zd cap cu_m enters only as an arbitrary nonempty Finset (Vec d): the per-site bound is uniform in z, and the mean of an average is the average of the means, so no grid cardinality and no union bound occurs.

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

The fourth term of e.local.bad.events.summed multiplies the crude bound of display 1 against the bad-event max factor built from display 3,

    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.

The mechanism is W's own pointwise [0,1] ceiling, exported by the sibling as weightedIndicatorAverage_rpow_mem_Icc (and its base indicatorAverage_mem_Icc): at 0 <= W <= 1 and Y >= 0 one has Y . W <= Y pointwise, so the Gamma_1 lane and the Gamma_{2/7} lane of exists_crude_bound pass through the product unchanged, at their printed amplitudes and indices, and only the deterministic shift consumes W'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 two lanes pass through at unchanged amplitude only after the free witness clamp Provider.Tail.isBigOWith_max_zero (Provider/Tail/TailSqrt.lean) has replaced each of the display's two Orlicz witnesses by max 0 (.) at the same scale: the witnesses of IsDeterministicShiftTwoTermOneSidedOrlicz are only known to be measurable and dominating, never nonnegative. ceiling_product below performs exactly that clamp and exports the finished composition, so the consumer of e.local.bad.events.summed does not re-derive it.

The scale gate on m (-bin statement change)

The landmark premise carried by every endpoint below is mStarStar M < m, not the printed m0 in (mstar, infty) cap Z that it inherits from l.shom.continuity. Nothing else moved: the premise is forwarded verbatim to Provider.Localization.shom_continuity, no proof step here consumes it, and no frozen statement changes.

Main results

isDeterministicShiftTwoTermOneSidedOrlicz_of_ae_le

• Algsuperdiff.Section3.Provider.MultiscaleEstimate.quarter_pos_of_eight_gamma_le
• Algsuperdiff.Section3.Provider.MultiscaleEstimate.quarter_mem_crude_window
• Algsuperdiff.Section3.Provider.MultiscaleEstimate.exists_crude_bound
• Algsuperdiff.Section3.Provider.MultiscaleEstimate.exists_badEvent_indicatorAverage_rpow

Algsuperdiff.Section3.Provider.MultiscaleEstimate.exists_badEvent_indicatorAverage_rpow_at_s_div_d

In-repo consumed set

Frozen.Section3.coarse_ellipticity_bounds, Frozen.Section3.goodLocalEventAt, Frozen.Section3.inductionState, Section3.mStar, Section3.lowerEllipticityProfile, Provider.Localization.shom_continuity, Provider.Tail.sq_cutoffHomogenizationError_le, Provider.Tail.isBigOWith_of_ae_eq, Provider.Tail.isBigOWith_max_zero, Provider.Tail.lowerEllipticityProfile_exponentTwo, Provider.Tail.pow_five_le_inv_of_le_rpow, Provider.Tail.exponentTwo, Provider.BadEvents.exists_measureReal_compl_goodLocalEventAt_le_of_multiscaleParameters, Provider.BadEvents.scaleGapPos (+ _of_le), Provider.BadEvents.measurableSet_goodLocalEvent, Provider.Multiscale.isBigOWith_gammaSigma_add, Provider.Orlicz.isBigOWith_gammaSigma_mono_exponent, Provider.Orlicz.cstar_pos, Provider.Orlicz.sigmaBar_pos, Observable.cutoffUpperEllipticity_nonneg, Observable.cutoffLowerEllipticityInv_nonneg, Observable.cutoffHomogenizationError (+ its measurability), Observable.measurable_cutoffHomogenizationErrorAtComparatorScale, Annealed.sigmaBar, Disorder.cstar, Cutoff.cutoffSampleLaw, Cutoff.measurable_translateCutoffSample, and from the sibling BadEventCeiling.lean the items isBigOWith_gammaSigma_indicator_of_two_exp, indicatorAverage_rpow_isBigOWith_gammaOne_of_two_exp and weightedIndicatorAverage_rpow_mem_Icc.

Provider.Multiscale.sigmaBar_le_four_mul_sigmaBar and Provider.Multiscale.sigmaBar_le_four_mul_rpow_mul_sigmaBar are no longer consumed: they carry the circular inductionState-at-m binder, and the gauge conversions now come from l.shom.continuity.

References

• ABK26: e.mathcalE.crude.bound, e.badevent.indicator.propagate, the averaged display, e.bound.Lambdas.by.Es, p.cg.ellipticity.bounds, e.bad.event.Q.estimate, e.param.conditions.in.main, e.indc.O.sigma, e.Gamma.sigma.triangle, e.multGammasig.

1. The null-set modification of a two-term display

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.isDeterministicShiftTwoTermOneSidedOrlicz_of_ae_le {Ω : Type u_1} [MeasurableSpace Ω] {μ : MeasureTheory.Measure Ω} {X Y Z : Ω → ℝ} {b A₁ A₂ sigma₁ sigma₂ : ℝ} (hs₁ : 0 < sigma₁) (hs₂ : 0 < sigma₂) (hA₁ : 0 < A₁) (hA₂ : 0 < A₂) (hXm : Measurable X) (hYm : Measurable Y) (hZm : Measurable Z) (hY : HCPolySupport.IndependentSums.IsBigOWith μ (HCPolySupport.IndependentSums.gammaSigma sigma₁) Y A₁) (hZ : HCPolySupport.IndependentSums.IsBigOWith μ (HCPolySupport.IndependentSums.gammaSigma sigma₂) Z A₂) (hae : ∀ᵐ (omega : Ω) ∂μ, X omega ≤ b + Y omega + Z omega) : Probability.IsDeterministicShiftTwoTermOneSidedOrlicz μ (HCPolySupport.IndependentSums.gammaSigma sigma₁) (HCPolySupport.IndependentSums.gammaSigma sigma₂) X b A₁ A₂

The null-set modification. The source's additive notation X <= b + O_{Psi_1}(A_1) + O_{Psi_2}(A_2) is carried by IsDeterministicShiftTwoTermOneSidedOrlicz, whose domination clause is pointwise; the q = 2 face of l.mathcal.E.to.Lambdas delivers its inequality only almost surely, because the cutoff observables are identified with their literals off a null set. Replacing the first witness by X - b - Z on the null set removes the mismatch at no cost: the modified witness is almost everywhere equal to the original, and the proved Provider.Tail.isBigOWith_of_ae_eq (Provider/Tail/TailSqrt.lean) transports the tail.

This is not Provider.Tail.isTwoTermBigOWith_of_ae_le (Provider/Tail/TailSqrt.lean), which makes the same modification for Probability.IsTwoTermBigOWith; the carrier here is Probability.IsDeterministicShiftTwoTermOneSidedOrlicz, whose domination clause carries the deterministic shift b that the source's additive notation needs.

2. The gauge index

4. The window bridge: the printed 8 cgamma <= s <= 1 implies the

frozen ellipticity window

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.quarter_pos_of_eight_gamma_le {gamma s : ℝ} (hgamma : 0 < gamma) (hs : 8 * gamma ≤ s) : 0 < s / 4

The pinned scale s/4 is positive on the printed window 8 cgamma <= s.

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.quarter_mem_crude_window {Ccg E gamma s : ℝ} (hCcg : 0 < Ccg) (hE : 1 ≤ E) (hCE : Real.exp (Ccg / (1 / 7)) ≤ E) (hEgamma : E ≤ gamma ^ (-(1 / 5))) (hgamma : 0 < gamma) (hs8 : 8 * gamma ≤ s) (hs1 : s ≤ 1) : s / 4 ∈ Set.Icc (gamma / 2 + Real.exp (-(Ccg⁻¹ * E⁻¹ ^ 2 * gamma⁻¹))) 1

The window bridge. On the printed window 8 cgamma <= s <= 1 of e.mathcalE.crude.bound, and under the E-gates the frozen p.cg.ellipticity.bounds already carries at sigma = 1/7, the pinned scale s/4 lies in the frozen statement's own window

    s/4  in  [ cgamma/2 + exp(-Ccg^{-1} E^{-2} cgamma^{-1}) ,  1 ] .

The chain, all of it elementary:

• exp(7 Ccg) <= E and exp(x) >= 1 + x give E >= (1 + 7Ccg/2)^2 >= (7Ccg/2)^2 >= 4 Ccg^2, i.e. sqrt E >= 2 Ccg;
• E <= cgamma^{-1/5} gives E^5 <= cgamma^{-1}, hence sqrt(cgamma^{-1}) >= sqrt(E^5) = E^2 sqrt E >= 2 Ccg E^2;
• log x <= 2 sqrt x (from log y <= y - 1 at y = sqrt x) then gives log(cgamma^{-1}) <= 2 sqrt(cgamma^{-1}) <= Ccg^{-1} E^{-2} cgamma^{-1}, i.e. exp(-Ccg^{-1} E^{-2} cgamma^{-1}) <= cgamma;
• finally 8 cgamma <= s gives s/4 - cgamma/2 >= 2 cgamma - cgamma/2 >= cgamma.

So the crude-bound publics need no window binder: they take the printed 8 cgamma <= s <= 1.

The fifth-root gate is not an extra demand. hEgamma : E <= cgamma^{-1/5} is implied by two binders the multiscale root already carries, namely cgamma <= (E^{-1})^{10} and 1 <= E: from the first, cgamma^{-1/5} >= ((E^{-1})^{10})^{-1/5} = E^2, and E^2 >= E at E >= 1. It is kept as an explicit binder anyway, because the frozen p.cg.ellipticity.bounds statement carries it in exactly this shape and the consumers pass it through verbatim; the point of the note is that no consumer acquires a new obligation by supplying it.

5. e.mathcalE.crude.bound

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.exists_crude_bound (d : ℕ) : ∃ (Ccg : ℝ) (Cshom : ℝ), 0 < Ccg ∧ 0 < Cshom ∧ ∀ (M : ABKModel d) (m : ℤ) (E : { E : ℝ // 1 ≤ E }), Frozen.Section3.inductionState M (m - 1) E → mStarStar M < m → max (Real.exp (Ccg / (1 / 7))) (Disorder.cstar M)⁻¹ ≤ ↑E → Cshom * (Disorder.cstar M)⁻¹ ≤ ↑E → ↑E ≤ M.gamma ^ (-(1 / 5)) → M.gamma ≤ (↑E)⁻¹ ^ 10 → ∀ (s : ℝ) (hs8 : 8 * M.gamma ≤ s), s ≤ 1 → Probability.IsDeterministicShiftTwoTermOneSidedOrlicz (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 1) (HCPolySupport.IndependentSums.gammaSigma (2 / 7)) (fun (omega : Cutoff.CutoffSample d) => Observable.cutoffHomogenizationError M m ⟨s / 4, ⋯⟩ omega ^ 2) (8 * Ccg + 8 * 3 ^ M.gamma * lowerEllipticityProfile Ccg M.gamma (s / 4) Tail.exponentTwo) (8 * (Ccg * (Disorder.cstar M)⁻¹ * (s / 4) * M.gamma * (2 * (s / 4) - M.gamma)⁻¹ ^ 3)) ((1 + Real.log 2) ^ (2 / 7)⁻¹ * (8 * Real.exp (-(Ccg⁻¹ * (↑E)⁻¹ ^ 2 * M.gamma⁻¹)) + 8 * 3 ^ M.gamma * Real.exp (-(Ccg⁻¹ * (↑E)⁻¹ ^ 2 * M.gamma⁻¹))))

e.mathcalE.crude.bound at the printed gauge shom_m.

Identical to exists_crude_bound_at_predecessor_gauge except that the comparator scale is the printed m, at the cost of the two gauge conversions (factor 4 on the upper lane, factor 4 . 3^{cgamma} on the lower lane).

The earlier reading of this theorem under inductionState M m E is withdrawn as circular at the root; see the module header.

Two dimensional constants are exported: Ccg from p.cg.ellipticity.bounds, in which the display's amplitudes are written, and Cshom from l.shom.continuity, which appears only in the E-gate. They are obtained once each and never composed.

The <= 4 Ccg reading of the deterministic part belongs to the predecessor gauge only; here the deterministic part is 8 Ccg + 8 . 3^{cgamma} . lowerEllipticityProfile Ccg cgamma (s/4) 2.

6. e.badevent.indicator.propagate, in the split form

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.exists_badEvent_indicatorAverage_rpow (d : ℕ) : ∃ (Ccg : ℝ) (c : ℝ), 1 ≤ Ccg ∧ 0 < c ∧ ∀ (H : ℝ), 0 ≤ H → ∃ (C : ℝ), 1 ≤ C ∧ ∀ (M : ABKModel d) (m0 : ℤ) (E : { E : ℝ // 1 ≤ E }) (epsilon : ℝ) (h : ℕ) (l : ℤ), Frozen.Section3.inductionState M (m0 - 1) E → epsilon ∈ Set.Ioc 0 (1 / 2) → ↑h ≤ H * |Real.log epsilon| + 1 → (Disorder.cstar M)⁻¹ * epsilon ^ (-C) ≤ ↑E → M.gamma ≤ (↑E)⁻¹ ^ 10 → l - ↑h ≤ m0 - 1 → ∀ (rho : ℝ), 0 < rho → rho ≤ 2 → ∀ (F : Finset (HCPolySupport.Vec d)), F.Nonempty → HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 1) (fun (omega : Cutoff.CutoffSample d) => ((↑F.card)⁻¹ * ∑ z ∈ F, (Frozen.Section3.goodLocalEventAt M (2 * Ccg) l (l - ↑h) z)ᶜ.indicator (fun (x : Cutoff.CutoffSample d) => 1) omega) ^ rho) (4 * rho⁻¹ * (4 * c⁻¹ * (Disorder.cstar M)⁻¹ * 3 ^ (5 * ↑h) * M.gamma + 4 * Real.exp (-(c * (↑E)⁻¹ ^ 2 * M.gamma⁻¹))))

The averaged-indicator display, by Markov plus the [0,1] ceiling.

For every nonempty finite set F of base points and every rho ∈ (0,2],

( avsum_{z in F} 1_{not Q(l,l-h,z)} )^rho
   <= O_{Gamma_1}( 4 rho^{-1} ( 4 c^{-1} cstar^{-1} 3^{5h} cgamma
                                + 4 exp(-c E^{-2} cgamma^{-1}) ) ) .

: the printed "crude application of the triangle inequality" does not produce this display (the countable Gamma_sigma triangle costs a further 1 + |log s|, which the display's own eps^{-C} cannot absorb). The mechanism is Markov's inequality plus the deterministic [0,1] ceiling on the normalized sum, and the printed rho^{-1} is the join constant between the two branches. The finite index set is arbitrary — in the manuscript it is 3^l Zd cap cu_m — and no cardinality factor appears, because means average rather than add.

theorem Algsuperdiff.Section3.Provider.MultiscaleEstimate.exists_badEvent_indicatorAverage_rpow_at_s_div_d (d : ℕ) : ∃ (Ccg : ℝ) (c : ℝ), 1 ≤ Ccg ∧ 0 < c ∧ ∀ (H : ℝ), 0 ≤ H → ∃ (C : ℝ), 1 ≤ C ∧ ∀ (M : ABKModel d) (m0 : ℤ) (E : { E : ℝ // 1 ≤ E }) (epsilon : ℝ) (h : ℕ) (l : ℤ), Frozen.Section3.inductionState M (m0 - 1) E → epsilon ∈ Set.Ioc 0 (1 / 2) → ↑h ≤ H * |Real.log epsilon| + 1 → (Disorder.cstar M)⁻¹ * epsilon ^ (-C) ≤ ↑E → M.gamma ≤ (↑E)⁻¹ ^ 10 → l - ↑h ≤ m0 - 1 → ∀ (s : ℝ), 0 < s → s ≤ 1 → ∀ (F : Finset (HCPolySupport.Vec d)), F.Nonempty → HCPolySupport.IndependentSums.IsBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 1) (fun (omega : Cutoff.CutoffSample d) => ((↑F.card)⁻¹ * ∑ z ∈ F, (Frozen.Section3.goodLocalEventAt M (2 * Ccg) l (l - ↑h) z)ᶜ.indicator (fun (x : Cutoff.CutoffSample d) => 1) omega) ^ (s / ↑d)) (16 * ↑d * s⁻¹ * (c⁻¹ * (Disorder.cstar M)⁻¹ * 3 ^ (5 * ↑h) * M.gamma + Real.exp (-(c * (↑E)⁻¹ ^ 2 * M.gamma⁻¹))))

The averaged-indicator display at the corrected exponent rho = s/d.

( avsum_{z in F} 1_{not Q(l,l-h,z)} )^{s/d}
   <= O_{Gamma_1}( 16 d s^{-1} ( c^{-1} cstar^{-1} 3^{5h} cgamma
                                 + exp(-c E^{-2} cgamma^{-1}) ) ) .

The admissibility s/d <= 2 is automatic on the source window s <= 1 because 2 <= d.