PrincipalResponseLegsBudget

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

Provider: sub-step (iv) of the principal response, the (1/2) gamma^6 budget

Source display in ABK26:

avsum_{z in 3^n Zd cap cu_K} E[ P_z . bfA_m(z+cu_n) P_z 1_{not Q_z} ]
  <= C gamma^{-2} exp(-gamma^{-1})
  <= (1/2) gamma^6 .

The companion module PrincipalResponseLegsHolder supplies the two Hoelder splits behind the first inequality. This module supplies

• the elementary exponential-beats-polynomial estimate closing the second inequality,
• the two-lane envelope that turns the two atomic tails of l.bad.event.lemma (l.bad.event.lemma, label; its display e.bad.event.Q.estimate, label) into the single exp(-gamma^{-1}) the display quotes,
• the per-cube composition, and
• the grid step, which is needed because bounds only the averaged fourth moment while the Hoelder split is applied cube by cube.

Main results

• exp_add_exp_le_exp_neg -- the two-lane envelope.
• badEventEnergy_budget_le -- Emom . tail^{3/8} <= (1/2) gamma^6.
• gridAverage_badEventEnergy_le -- the grid step.

Exponential beats polynomial

The two-lane envelope

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.exp_add_exp_le_exp_neg {x y r : ℝ} (hx : r + Real.log 2 ≤ -x) (hy : r + Real.log 2 ≤ -y) : Real.exp x + Real.exp y ≤ Real.exp (-r)

The envelope. l.bad.event.lemma delivers the probability of the bad event as a sum of two exponentials; if each rate exceeds the target rate by log 2, their sum is at most the single exponential the display quotes.

The budget

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.badEventEnergy_budget_le {Emom tail gamma Cm : ℝ} (hgamma : 0 < gamma) (hCm : 0 < Cm) (htail0 : 0 ≤ tail) (hEmom : Emom ≤ Cm * (gamma ^ 2)⁻¹) (htail : tail ≤ Real.exp (-gamma⁻¹)) (hsmall : gamma ≤ (2 * Cm * 24 ^ 9)⁻¹) : Emom * tail ^ (3 / 8) ≤ gamma ^ 6 / 2

The closing inequality. With the energy moment inside the manuscript's envelope Cm gamma^{-2} and the tail inside exp(-gamma^{-1}), the Hoelder product is within the half budget (1/2) gamma^6 as soon as gamma is small, which is the manuscript's "for a sufficiently large choice of M in e.cgamma.constraints".

The grid step

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.gridAverage_badEventEnergy_le {iota : Type u_2} {s : Finset iota} (hs : s.Nonempty) (pbad m4 : iota → ℝ) {Cb Cv t : ℝ} (hm4 : ∀ z ∈ s, 0 ≤ m4 z) (hCb0 : 0 ≤ Cb) (ht0 : 0 ≤ t) (hpbad : ∀ z ∈ s, pbad z ≤ Cb * √(m4 z) * t) (havg : (∑ z ∈ s, m4 z) / ↑s.card ≤ Cv ^ 4) : (∑ z ∈ s, pbad z) / ↑s.card ≤ Cb * Cv ^ 2 * t

The grid step. ABK26 bounds only the grid average of the fourth moment m4 z = E[|bfAhom_{m-1}^{1/2} P_z|^4], while the Hoelder split is applied cube by cube and produces sqrt (m4 z). Discrete Cauchy--Schwarz closes the gap and returns the manuscript's grid form.