BadEventLemmaOscillation

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

The oscillation branch of l.bad.event.lemma

ABK26's Lemma l.bad.event.lemma bounds the failure probability of the good local sensitivity event Q(m,n,z) of e.good.local.events. Its proof splits not Q(m,n,z) into a coarse-ellipticity failure and the oscillation event

B_osc(m,n) = { sup_{L >= n} 3^{2m} ||grad (k_L - k_n)||_{W^{1,infinity}(z+square_m)}
                 > c c_star^{1/2} gamma^{-1/2} 3^{gamma n} 3^{-(1/2)(n-m)_+} } ,

and claims for the latter the displayed bound e.oscillation.bound

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

This module proves the corresponding estimate on the branch m <= n (Q.scale <= n) for the internal event goodLocalSensitivityFailure of GoodLocalEvents.lean. That event is a stricter, unrelaxed subset of the printed oscillation event, not an identification with it. The result is a useful branch input to the umbrella proof, but it does not by itself realize or close the printed oscillation node. The induction-state comparison sqrt_cstar_mul_inv_sqrt_gamma_mul_rpow_le_two_mul_sigmaBar is used internally to price this stricter event.

The route

The manuscript decomposes B_osc(m,n) into the waves below scale m and the shells L in [m, infinity). On the branch m <= n the increment k_L - k_n consists of shells k > n >= m only: the wave term k_m - k_{n and m} is identically zero, and every shell that occurs sits at or above the cube scale. The local proof therefore decomposes over the shells k > n (rather than over L >= m), which is what the manuscript's own displays need — see the implementation note at the end of this docstring.

1. shellSensitivityThreshold splits the event's threshold geometrically over the shells k > n, with ratio 3^{-1/5} and prefactor 1/5, exactly as e.Bosc.decomp splits the e.Bosc.def threshold. The arithmetic (1/5) sum_{i >= 1} 3^{-i/5} <= 1 is sum_range_shellSensitivityThreshold_le.
2. goodLocalSensitivityFailure_subset_iUnion is the resulting containment: it uses only the W^{1,infinity} triangle inequality incrementOscGauge₂_le_sum_shellOscGauge of IncrementGaugeTwoIndex.lean.
3. measureReal_shellSensitivityFailure_le prices one shell against the proved translated e.nabla.jk.O tail isBigOWith_gammaSigma_shellOscGauge, after converting the event's sigmabar_{n-1} threshold into the c_star--gamma amplitude by the induction state.
4. measureReal_goodLocalSensitivityFailure_le sums the shells.

The gate

The weak-Orlicz tail of e.nabla.jk.O is available only above its amplitude, so each shell may be priced only when its threshold-to-amplitude ratio is at least one; and the geometric summation of exp(-kappa 3^i) over i >= 1 is below exp(-kappa) only for kappa >= 1. Both are exactly 1 <= rate, where rate is badEventOscRate, the exponent of the displayed bound. This is the same gate as unitGate in OscillationProbability.lean, and on this branch it is discharged from the manuscript's own admissibility e.bad.event.admissibility by one_le_badEventOscRate_of_admissible, using the absolute bound Algsuperdiff.Section3.Provider.Disorder.cstar_le_three_halves; nothing beyond the printed display is assumed by measureReal_goodLocalSensitivityFailure_le_of_admissible.

Implementation notes (not manuscript defects, except where flagged)

• This file treats only m ≤ n. The later provider OscillationBranchLow.lean supplies the other internal branch n < m. Having both internal branch estimates does not identify goodLocalSensitivityFailure with the printed B_osc, so it still does not confer source-node status.
• The constant. c of the display is chosen as badEventOscConst d Ccg = (1/3600) C_sens(d)^{-2} Ccg^{-2}, where Ccg is the explicit parameter carrying C_{(e.cg.ellip.lower)} (the now-proved frozen coarse_ellipticity_bounds supplies such a dimension-only constant to a downstream consumer; this conditional A remains parametrized, exactly as in GoodLocalEllipticity.lean) and C_sens(d) = sensitivityConstMax d is the dimension-only joint sensitivity constant. The manuscript's requirement c depends only on d is respected: both factors are dimension-only.

Main definitions

• shellSensitivityThreshold, shellSensitivityFailure: the geometric split of the event's threshold over the shells above n.
• badEventOscConst, badEventOscRate: the constant and the exponent of e.oscillation.bound.
• badEventOscAdmissibleConst: the dimension-only constant at which the printed admissibility discharges the gate.

Main results

• goodLocalSensitivityFailure_subset_iUnion.
• measureReal_shellSensitivityFailure_le.
• measureReal_goodLocalSensitivityFailure_le.

References

• ABK26, l.bad.event.lemma; e.oscillation.bound; the wave decomposition.
• ABK26, e.good.local.events.
• ABK26, e.nabla.jk.O; e.Bosc.decomp.

Elementary numerics

theorem Algsuperdiff.Section3.Provider.BadEvents.three_rpow_pos (x : ℝ) : 0 < 3 ^ x

Shared support for the high- and low-shell oscillation probability bounds.

theorem Algsuperdiff.Section3.Provider.BadEvents.three_rpow_add (x y : ℝ) : 3 ^ x * 3 ^ y = 3 ^ (x + y)

Shared support for the high- and low-shell oscillation probability bounds.

theorem Algsuperdiff.Section3.Provider.BadEvents.three_rpow_half_sq (x : ℝ) : (3 ^ (1 / 2 * x)) ^ 2 = 3 ^ x

Shared support for the high- and low-shell oscillation probability bounds.

theorem Algsuperdiff.Section3.Provider.BadEvents.three_mul_succ_le_three_pow (w : ℕ) : 3 * (w + 1) ≤ 3 ^ (w + 1)

Shared support for the high- and low-shell oscillation probability bounds.

theorem Algsuperdiff.Section3.Provider.BadEvents.exp_pow_eq (x : ℝ) (w : ℕ) : Real.exp x ^ w = Real.exp (↑w * x)

Shared support for the high- and low-shell oscillation probability bounds.

theorem Algsuperdiff.Section3.Provider.BadEvents.two_le_exp_one : 2 ≤ Real.exp 1

Shared support for the high- and low-shell oscillation probability bounds.

theorem Algsuperdiff.Section3.Provider.BadEvents.tsum_exp_pow_le {kappa : ℝ} (hk : 1 ≤ kappa) : ∑' (w : ℕ), Real.exp (-(3 * kappa)) ^ (w + 1) ≤ Real.exp (-kappa)

The geometric summation sum_{i >= 1} exp(-3 kappa)^i <= exp(-kappa) for kappa >= 1.

The geometric split of the event's threshold over shells

noncomputable def Algsuperdiff.Section3.Provider.BadEvents.shellSensitivityThreshold {d : ℕ} (M : ABKModel d) (Ccg : ℝ) (m n k : ℤ) : ℝ

The share of the e.good.local.events threshold allotted to the shell j_k in the decomposition of l.bad.event.lemma: the total budget C_sens^{-1} (1/2) Ccg^{-1} 3^{-(1/2)(n-m)_+} sigmabar_{n-1} split with ratio 3^{-1/5} and prefactor 1/5, exactly as e.Bosc.decomp splits the e.Bosc.def threshold.

Equations

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

def Algsuperdiff.Section3.Provider.BadEvents.shellSensitivityFailure {d : ℕ} (M : ABKModel d) (Ccg : ℝ) (Q : HCPolySupport.TriadicCube d) (n k : ℤ) : Set (Cutoff.CutoffSample d)

The shell j_k exceeds its share of the e.good.local.events threshold. This is the manuscript's B_{osc,k}, stated at the event's own threshold rather than at its sigmabar_{n-1} relaxation.

Equations

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

theorem Algsuperdiff.Section3.Provider.BadEvents.sum_range_shellSensitivityThreshold_le {d : ℕ} (M : ABKModel d) {Ccg : ℝ} (hCcg : 0 < Ccg) (m n : ℤ) (N : ℕ) : ∑ w ∈ Finset.range N, shellSensitivityThreshold M Ccg m n (n + 1 + ↑w) ≤ (sensitivityConstMax d)⁻¹ * goodLocalThreshold M Ccg m n

The partial sums of the shell shares stay below the total budget.

theorem Algsuperdiff.Section3.Provider.BadEvents.goodLocalSensitivityFailure_subset_iUnion {d : ℕ} (M : ABKModel d) {Ccg : ℝ} (hCcg : 0 < Ccg) (Q : HCPolySupport.TriadicCube d) (n : ℤ) : goodLocalSensitivityFailure M Ccg Q n ⊆ ⋃ (w : ℕ), shellSensitivityFailure M Ccg Q n (n + 1 + ↑w)

The shell decomposition of the sensitivity failure (ABK26, on the branch m <= n where the wave term of vanishes): if every shell above n respects its share of the threshold, then so does the whole increment k_L - k_n, for every L >= n.

The constant and the exponent of e.oscillation.bound

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

The local choice of the manuscript's c in e.oscillation.bound: (1/3600) C_sens(d)^{-2} Ccg^{-2}, where Ccg carries C_{(e.cg.ellip.lower)}.

Equations

• Algsuperdiff.Section3.Provider.BadEvents.badEventOscConst d Ccg = 1 / 3600 * (Algsuperdiff.Section3.Provider.BadEvents.sensitivityConstMax d)⁻¹ ^ 2 * Ccg⁻¹ ^ 2

noncomputable def Algsuperdiff.Section3.Provider.BadEvents.badEventOscRate {d : ℕ} (M : ABKModel d) (Ccg : ℝ) (Q : HCPolySupport.TriadicCube d) (n : ℤ) : ℝ

The exponent of e.oscillation.bound on the branch m <= n: c c_star gamma^{-1} 3^{(n-m)_+}.

Equations

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

Abstract endgames

Both probabilistic endgames are stated over abstract reals so that no arithmetic tactic ever meets a power of three or an exponential.

theorem Algsuperdiff.Section3.Provider.BadEvents.one_le_mul_one_le {a b : ℝ} (ha : 1 ≤ a) (hb : 1 ≤ b) : 1 ≤ a * b

Shared support for the high- and low-shell oscillation probability bounds.

theorem Algsuperdiff.Section3.Provider.BadEvents.one_le_of_one_le_sq {B : ℝ} (hB : 0 < B) (h : 1 ≤ B ^ 2) : 1 ≤ B

Shared support for the high- and low-shell oscillation probability bounds.

theorem Algsuperdiff.Section3.Provider.BadEvents.measureReal_upperTail_le_exp {Omega : Type u_1} [MeasurableSpace Omega] {mu : MeasureTheory.Measure Omega} {X : Omega → ℝ} {A B thr rate : ℝ} (hA : 0 < A) (hB : 0 < B) (hBA : B * A ≤ thr) (hBsq : B ^ 2 = rate) (hrate : 1 ≤ rate) (htail : HCPolySupport.IndependentSums.IsBigOWith mu (HCPolySupport.IndependentSums.gammaSigma 2) X A) : mu.real {omega : Omega | thr < X omega} ≤ Real.exp (-rate)

The weak-Orlicz tail, read at the threshold-to-amplitude ratio: if the threshold dominates B times the amplitude and B^2 is the claimed rate, then the upper-tail event at the threshold has probability at most exp(-rate).

theorem Algsuperdiff.Section3.Provider.BadEvents.measureReal_le_exp_of_iUnion {Omega : Type u_1} [MeasurableSpace Omega] (mu : MeasureTheory.Measure Omega) [MeasureTheory.IsFiniteMeasure mu] {S : Set Omega} {T : ℕ → Set Omega} {kappa : ℝ} (hk : 1 ≤ kappa) (hsub : S ⊆ ⋃ (w : ℕ), T w) (hterm : ∀ (w : ℕ), mu.real (T w) ≤ Real.exp (-(kappa * 3 ^ (↑w + 1)))) : mu.real S ≤ Real.exp (-kappa)

The geometric union bound: a set covered by events whose probabilities decay like exp(-kappa 3^{i}) has probability at most exp(-kappa), for kappa >= 1.

The per-shell probability bound

theorem Algsuperdiff.Section3.Provider.BadEvents.measureReal_shellSensitivityFailure_le {d : ℕ} (M : ABKModel d) {Ccg : ℝ} (hCcg : 0 < Ccg) (Q : HCPolySupport.TriadicCube d) {n k m0 : ℤ} {E : { E : ℝ // 1 ≤ E }} (hS : Frozen.Section3.inductionState M (m0 - 1) E) (hn : n ≤ m0 - 1) (hmn : Q.scale ≤ n) (hnk : n < k) (hgate : 1 ≤ badEventOscRate M Ccg Q n) : (↑(Cutoff.cutoffSampleLaw M)).real (shellSensitivityFailure M Ccg Q n k) ≤ Real.exp (-(badEventOscRate M Ccg Q n * 3 ^ (↑k - ↑n)))

One shell of the oscillation branch. For a shell k > n at or above the cube scale, the probability that j_k exceeds its share of the e.good.local.events threshold is at most exp(- rate 3^{k-n}), where rate is the exponent of e.oscillation.bound.

The input is the proved translated e.nabla.jk.O tail isBigOWith_gammaSigma_shellOscGauge; the induction state enters only through the lower bound c_star^{1/2} gamma^{-1/2} 3^{gamma (n-1)} <= 2 sigmabar_{n-1} of e.shom.h.bounds, which is the manuscript's own relaxation of the e.good.local.events threshold.

The oscillation branch of l.bad.event.lemma

theorem Algsuperdiff.Section3.Provider.BadEvents.measureReal_goodLocalSensitivityFailure_le {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) (hmn : Q.scale ≤ n) (hgate : 1 ≤ badEventOscRate M Ccg Q n) : (↑(Cutoff.cutoffSampleLaw M)).real (goodLocalSensitivityFailure M Ccg Q n) ≤ Real.exp (-badEventOscRate M Ccg Q n)

The oscillation branch of l.bad.event.lemma (ABK26, e.oscillation.bound), on the branch m <= n where (m-n)_+ = 0:

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

with c = badEventOscConst d Ccg. The gate hgate is the threshold-to- amplitude condition of the weak-Orlicz tail, discharged from the manuscript's own admissibility by measureReal_goodLocalSensitivityFailure_le_of_admissible below.

Discharging the gate from the printed admissibility

noncomputable def Algsuperdiff.Section3.Provider.BadEvents.badEventOscAdmissibleConst (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 measureReal_goodLocalSensitivityFailure_le. As in GoodLocalEllipticity.lean, Ccg carries the still-parametrized C_{(e.cg.ellip.lower)}.

Equations

• Algsuperdiff.Section3.Provider.BadEvents.badEventOscAdmissibleConst d Ccg = max 3 (3600 * Algsuperdiff.Section3.Provider.BadEvents.sensitivityConstMax d ^ 2 * Ccg ^ 2)