BadEventLemmaCases

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

The coarse-ellipticity branch and the umbrella of l.bad.event.lemma

ABK26's Lemma l.bad.event.lemma decomposes the failure of the good local sensitivity event Q(m,n,z) of e.good.local.events into an oscillation branch (implemented locally in BadEventLemmaOscillation.lean) and a coarse-ellipticity branch, and concludes the displayed estimate e.bad.event.Q.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} ) ) .

This module supplies a conditional local result for the coarse-ellipticity branch case n >= m and the umbrella on the same branch, both conditionally on the exact coarse-ellipticity conclusion. The frozen coarse theorem is now proved, but this local A retains that conclusion as the disclosed hcg binder until a downstream assembly discharges it together with the separate transport obligation.

The two disclosed conditional binders

The frozen Algsuperdiff.Frozen.Section3.coarse_ellipticity_bounds is proved. This conditional helper still carries its conclusion as an explicit A hypothesis, in the exact shape of its specialization at the cube scale n, sigma = 1/2, s = 1/8, q = 2; a downstream assembly may now discharge that hypothesis from the frozen export. This module does not itself perform that assembly or confer graph status:

• hcg is the first conjunct of (coarse_ellipticity_bounds d).choose_spec.2 M n E hS (1/2) hsigma hE hEgamma exponentTwo (1/8) hsWindow, verbatim. The discharge of hcg from the proved frozen theorem is exactly that term.
• The needed lemma, in the exact form the branch consumes, is

  lambda^{-1}_{1/8,2}(z + square_m; a_n) <= lambda^{-1}_{1/8,2}(square_n; a_n)
  

  for m <= n, pointwise in the sample. At an off-centre cube it also absorbs the manuscript's z = 0 stationarity reduction, since the frozen observable lives at the centered cube; at the centered cube of scale m it is exactly the manuscript's unstated step. It is a different statement from the exponent monotonicity e.ellipticities.monotone.ordered.

Two further gates are disclosed:

• hCcg : 1 <= Ccg normalizes the frozen constant C_{(e.cg.ellip.lower)}. It is what turns the tail level Ccg exp(Ccg^{-1} E^{-2} gamma^{-1}) into the manuscript's exp(c E^{-2} gamma^{-1}), and it would be discharged by the frozen theorem's own choice of constant.
• hgamma : gamma <= 1/8 makes the frozen deterministic profile lowerEllipticityProfile Ccg gamma (1/8) 2 = Ccg / (8 (1/4 - gamma)) at most Ccg, which is what the manuscript's threshold 2 C_{(e.cg.ellip.lower)} needs. It is not an addition: gamma_le_one_eighth_of_admissible derives it from the manuscript's own admissibility e.bad.event.admissibility at the dimension-only constant badEventOscAdmissibleConst.

What is not here

The case n < m is not realized. It reduces lambda^{-1}_{1/8,2}(square_m; a_n) to a maximum over the 3^{d(m-n)} cubes z + square_n by e.subadda.nosymm, then applies p.cg.ellipticity.bounds at each translate and l.maximums.Gamma.s.

Main results

• lowerEllipticityProfile_exponentTwo_le: the frozen profile at s = 1/8, q = 2 is below Ccg when gamma <= 1/8.
• gamma_le_one_eighth_of_admissible.
• measureReal_coarseEllipticityFailure_le_of_coarseBounds: the branch n >= m of the coarse-ellipticity half, with the displayed double-exponential bound.

References

• ABK26, l.bad.event.lemma; e.bad.event.Q.estimate; the case n >= m.
• ABK26, p.cg.ellipticity.bounds.

Deterministic profiles at q = 2

theorem Algsuperdiff.Section3.Provider.BadEvents.lowerEllipticityProfile_exponentTwo_eq (Ccg gamma s : ℝ) : lowerEllipticityProfile Ccg gamma s exponentTwo = Ccg * s * (2 * s - gamma)⁻¹

The frozen lower profile at q = 2 and an arbitrary exponent: lowerEllipticityProfile Ccg gamma s 2 = Ccg s (2 s - gamma)^{-1}.

theorem Algsuperdiff.Section3.Provider.BadEvents.lowerEllipticityProfile_exponentTwo_le_of_gamma_le {Ccg gamma s : ℝ} (hCcg : 0 ≤ Ccg) (hs : 0 < s) (hgamma : gamma ≤ s) : lowerEllipticityProfile Ccg gamma s exponentTwo ≤ Ccg

A positive exponent at least gamma bounds the deterministic profile by its coarse-graining constant.

theorem Algsuperdiff.Section3.Provider.BadEvents.lowerEllipticityProfile_exponentTwo (Ccg gamma : ℝ) : lowerEllipticityProfile Ccg gamma (1 / 8) exponentTwo = Ccg * (1 / 8) * (2 * (1 / 8) - gamma)⁻¹

The frozen lower profile at the parameters of e.good.local.events: lowerEllipticityProfile Ccg gamma (1/8) 2 = Ccg (1/8) (1/4 - gamma)^{-1}.

theorem Algsuperdiff.Section3.Provider.BadEvents.lowerEllipticityProfile_exponentTwo_le {Ccg gamma : ℝ} (hCcg : 0 < Ccg) (hgamma : gamma ≤ 1 / 8) : lowerEllipticityProfile Ccg gamma (1 / 8) exponentTwo ≤ Ccg

At gamma <= 1/8 the frozen deterministic profile is below the frozen constant itself, which is what the manuscript's threshold 2 C_{(e.cg.ellip.lower)} needs.

theorem Algsuperdiff.Section3.Provider.BadEvents.gamma_le_one_thirtysecond_of_admissible {d : ℕ} (M : ABKModel d) {Ccg E : ℝ} (hadm : badEventOscAdmissibleConst d Ccg ≤ E * Disorder.cstar M) (hgammaE : M.gamma ≤ E ^ (-5)) : M.gamma ≤ 1 / 32

The manuscript's own admissibility e.bad.event.admissibility, at the dimension-only constant badEventOscAdmissibleConst, implies gamma <= 1/32.

theorem Algsuperdiff.Section3.Provider.BadEvents.gamma_le_one_eighth_of_admissible {d : ℕ} (M : ABKModel d) {Ccg E : ℝ} (hadm : badEventOscAdmissibleConst d Ccg ≤ E * Disorder.cstar M) (hgammaE : M.gamma ≤ E ^ (-5)) : M.gamma ≤ 1 / 8

The original one-eighth specialization of admissibility.

theorem Algsuperdiff.Section3.Provider.BadEvents.measureReal_upperTail_le_double_exp {Omega : Type u_1} [MeasurableSpace Omega] (mu : MeasureTheory.Measure Omega) (Y : Omega → ℝ) {C X a : ℝ} (hC : 1 ≤ C) (hX : 0 ≤ X) (ha : 0 ≤ a) (htail : ∀ (t : ℝ), 1 ≤ t → mu.real (HCPolySupport.IndependentSums.upperTailEvent Y (Real.exp (-X) * t)) ≤ Real.exp (-t ^ a)) : mu.real (HCPolySupport.IndependentSums.upperTailEvent Y C) ≤ Real.exp (-Real.exp (a * X))

A Weibull tail with exponentially small scale gives a double-exponential bound at any level at least one. No measurability or finiteness is added to the supplied real-measure tail estimate.

The coarse-ellipticity branch, case n >= m

theorem Algsuperdiff.Section3.Provider.BadEvents.measureReal_coarseEllipticityFailure_le_of_coarseBounds {d : ℕ} (M : ABKModel d) {Ccg : ℝ} (hCcg : 1 ≤ Ccg) (Q : HCPolySupport.TriadicCube d) {n : ℤ} {E : ℝ} (hgamma : M.gamma ≤ 1 / 8) (hmono : ∀ (omega : Cutoff.CutoffSample d), cubeLowerEllipticityInv M Q n (1 / 8) measureReal_coarseEllipticityFailure_le_of_coarseBounds._proof_1 exponentTwo omega ≤ 3 ^ (1 / 4 * scaleGapPos Q.scale n) * Observable.cutoffLowerEllipticityInv M n n (1 / 8) measureReal_coarseEllipticityFailure_le_of_coarseBounds._proof_1 exponentTwo omega) (hcg : Probability.IsLowerIntegerFamilyOrlicz (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma ((1 - 1 / 2) / 2)) (fun (L : ℤ) (omega : Cutoff.CutoffSample d) => Observable.cutoffLowerEllipticityInv M n L (1 / 8) measureReal_coarseEllipticityFailure_le_of_coarseBounds._proof_1 exponentTwo omega * ↑(Annealed.sigmaBar M (n - 1))) (n - 1) (lowerEllipticityProfile Ccg M.gamma (1 / 8) exponentTwo) (Real.exp (-(Ccg⁻¹ * E⁻¹ ^ 2 * M.gamma⁻¹)))) : (↑(Cutoff.cutoffSampleLaw M)).real (coarseEllipticityFailure M Ccg Q n) ≤ Real.exp (-Real.exp (1 / 4 * (Ccg⁻¹ * E⁻¹ ^ 2 * M.gamma⁻¹)))

The case n >= m of the coarse-ellipticity branch (ABK26):

P[ lambda^{-1}_{1/8,2}(z+square_m; a_n) sigmabar_{n-1}
     > 2 . 3^{(1/4)(n-m)_+} C_{(e.cg.ellip.lower)} ]
  <= exp( - exp( c E^{-2} gamma^{-1} ) ) ,   c = Ccg^{-1}/4 .