BadEventLemmaFull

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

l.bad.event.lemma over the full range of m and n

BadEventLemmaOscillation.lean supplies a local oscillation-branch result for ABK26's Lemma l.bad.event.lemma on the branch m <= n, and OscillationBranchLow.lean supplies its local n < m counterpart. This ordinary Provider module combines them into a conditional full-range estimate matching the displayed form over all m, n,

P[ B_osc(m,n) ]  <=  exp( - c c_star gamma^{-1} 3^{-5(m-n)_+} 3^{(n-m)_+} ) ,

and then assembles the corresponding conditional complement-event estimate

P[ not Q(m,n,z) ]
  <= exp( - c c_star gamma^{-1} 3^{-5(m-n)_+} 3^{(n-m)_+} )
     + exp( - exp( c' E^{-2} gamma^{-1} ) )

over the same full range, from the coarse-ellipticity branch of BadEventLemmaCases.lean.

Where each hypothesis comes from

• The printed admissibility e.bad.event.admissibility is carried as hadm/hgammaE at the dimension-only constant badEventOscLowAdmissibleConst d Ccg. As in the branch m <= n, this discharges the weak-Orlicz gate of the oscillation half and the gate gamma <= 1/8 of the coarse-ellipticity half (through badEventOscAdmissibleConst_le_badEventOscLowAdmissibleConst and the proved gamma_le_one_eighth_of_admissible). Choosing a larger dimension-only constant is exactly what the lemma's own existential c(d) permits.
• On the branch m <= n no such hypothesis is present: there the gate is derived from the printed admissibility.
• The two conditional binders of the coarse-ellipticity half, hmono and hcg, are the proved ones of BadEventLemmaCases.lean, verbatim: hcg is the exact specialization of the now-proved frozen coarse_ellipticity_bounds conclusion, retained here as a conditional A binder for a downstream assembly to discharge, and hmono is the W cube-monotonicity step (whose weight-free form is false —). On the branch n < m the binder hmono additionally absorbs the manuscript's subadditivity step e.subadda.nosymm, which has no realization in this repository.

Main definitions

• badEventOscLowAdmissibleConst: the dimension-only constant at which the printed admissibility discharges both gates over the full range.

Main results

• one_le_badEventOscFullRate_of_admissible: the gate on the branch m <= n.
• measureReal_goodLocalSensitivityFailure_le_full: e.oscillation.bound over the full range, from the display's own exponent being at least one.
• measureReal_goodLocalSensitivityFailure_le_full_of_admissible: the same, with the branch m <= n discharged from the printed admissibility and the restriction confined to n < m.

References

• ABK26, l.bad.event.lemma; e.bad.event.Q.estimate; e.oscillation.bound.

The admissibility constant of the full range

noncomputable def Algsuperdiff.Section3.Provider.BadEvents.badEventOscLowAdmissibleConst (d : ℕ) (Ccg : ℝ) : ℝ

The dimension-only constant at which the manuscript's admissibility display e.bad.event.admissibility (c^{-1} c_star^{-1} <= E <= gamma^{-1/5}) discharges the gate of the oscillation branch on m <= n at the full-range constant badEventOscLowConst. It is the constant badEventOscAdmissibleConst of the branch m <= n, enlarged by the square of the dimension-only covering constant of e.W1inf.jL.bound.smaller.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section3.Provider.BadEvents.badEventOscAdmissibleConst_le_badEventOscLowAdmissibleConst (d : ℕ) {Ccg : ℝ} (hCcg : 0 < Ccg) : badEventOscAdmissibleConst d Ccg ≤ badEventOscLowAdmissibleConst d Ccg

theorem Algsuperdiff.Section3.Provider.BadEvents.one_le_badEventOscFullRate_of_admissible {d : ℕ} (M : ABKModel d) {Ccg : ℝ} (hCcg : 0 < Ccg) (Q : HCPolySupport.TriadicCube d) {n : ℤ} {E : ℝ} (hmn : Q.scale ≤ n) (hadm : badEventOscLowAdmissibleConst d Ccg ≤ E * Disorder.cstar M) (hgamma : M.gamma ≤ E ^ (-5)) : 1 ≤ badEventOscFullRate M Ccg Q n

The gate on the branch m <= n from the printed admissibility. With the absolute bound c_star <= 3/2 (Provider.Disorder.cstar_le_three_halves), the manuscript's own admissibility at badEventOscLowAdmissibleConst gives 1 <= badEventOscFullRate. Nothing is assumed on this branch beyond the printed display.

e.oscillation.bound over the full range

theorem Algsuperdiff.Section3.Provider.BadEvents.measureReal_goodLocalSensitivityFailure_le_full {d : ℕ} (M : ABKModel d) {Ccg : ℝ} (hCcg : 0 < Ccg) (Q : HCPolySupport.TriadicCube d) {n m0 : ℤ} {E : { E : ℝ // 1 ≤ E }} (hS : Frozen.Section3.inductionState M (m0 - 1) E) (hn : n ≤ m0 - 1) (hrestrict : 1 ≤ badEventOscFullRate M Ccg Q n) : (↑(Cutoff.cutoffSampleLaw M)).real (goodLocalSensitivityFailure M Ccg Q n) ≤ Real.exp (-badEventOscFullRate M Ccg Q n)

e.oscillation.bound over the full range of m, n (ABK26):

P[ sensitivity clause of Q(m,n,z) fails ]
  <= exp( - c c_star gamma^{-1} 3^{-5(m-n)_+} 3^{(n-m)_+} ) ,

with c = badEventOscLowConst d Ccg, dimension-only. The single hypothesis hrestrict says that the displayed exponent is at least one; on the branch m <= n it follows from the printed admissibility (one_le_badEventOscFullRate_of_admissible), and on the branch n < m it is the restriction.

theorem Algsuperdiff.Section3.Provider.BadEvents.measureReal_goodLocalSensitivityFailure_le_full_of_admissible {d : ℕ} (M : ABKModel d) {Ccg : ℝ} (hCcg : 0 < Ccg) (Q : HCPolySupport.TriadicCube d) {n m0 : ℤ} {E : { E : ℝ // 1 ≤ E }} (hS : Frozen.Section3.inductionState M (m0 - 1) E) (hn : n ≤ m0 - 1) (hadm : badEventOscLowAdmissibleConst d Ccg ≤ ↑E * Disorder.cstar M) (hgammaE : M.gamma ≤ ↑E ^ (-5)) (hrestrict : n < Q.scale → 1 ≤ badEventOscFullRate M Ccg Q n) : (↑(Cutoff.cutoffSampleLaw M)).real (goodLocalSensitivityFailure M Ccg Q n) ≤ Real.exp (-badEventOscFullRate M Ccg Q n)