AmplitudeBridge

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

The amplitude bridge: the diagonal fourth moment and the amplitude range

The printed sentence reads

E[mathcal E_{1/4, infinity, 2}(cu_L, a_L; shom_L)^4]^{1/2} <=^2 gamma for every L in (-infinity, m-1] cap Z,

and the next sentence instantiates the preceding proposition at delta_1 :=^2 gamma. Item A.3 fixes the two constants of that instantiation: it sets s = 1/4 and delta_1 = 10^9 E^2 gamma, and it needs delta_1 <= 1/2 before the proposition may be applied.

This module supplies both halves at the genuine cutoff sample law and in the byte shape the proved Step-1 consumer takes them:

1. The diagonal fourth moment. For every cutoff scale L <= m - 1, lintegral (ofReal (E_{1/4}(cu_L; a_L, shom_L)^4)) <= ofReal (delta_1^2) with delta_1 = 10^9 E^2 gamma.
2. The amplitude range. delta_1 in Ioc 0 (1/2).

Where the numerals come from

• The A.3 discounts t = 1/8 and u = 1/16 belong to its observation-scale transport, which enlarges the cube from cu_L to cu_M; the diagonal display proved here is at the cutoff cube itself, so no discount change occurs and the printed 1/4 is kept.
• The 10^9 is not consumed as a sharp constant below: the two-term amplitudes of the preceding-error clause produce 8 ((12 A)^4 + (208 B)^4) with A = 4 E sqrt gamma and B = 16 exp(-E^{-3} gamma^{-1}), which the regime fact gamma <= E^{-10} collapses to at most 1.6 * 10^16 * E^4 gamma^2, against the target 10^18 E^4 gamma^2; the slack factor is about 64 (the honest budget 1.5702e16 against 1e18), and 10^9 is the first power of ten that closes (10^8 fails). Every intermediate numeral is displayed in the private lemmas below.
• 12 = 6 * 2 and 208 = 13 * 16 are the two Chapter 4 moment constants gammaMomentConst sigma * 4^{1/sigma} at sigma = 2 and sigma = 1/2, bounded above by 6 and 13 respectively from the explicit value gammaMomentConst sigma = 2 e max{1, (2 / (sigma e))^{1/sigma}}.
• 8 is the elementary (a + b)^4 <= 8 (a^4 + b^4) used to split the two-term witness pair.

References

• ABK26.

Elementary real arithmetic

The two Chapter 4 moment constants at p = 4

The two-term fourth moment

The E floor available from the c_star upper bound

theorem Algsuperdiff.Section3.Provider.Homogenization.ten_le_of_fifteen_mul_inv_cstar_le {d : ℕ} (M : ABKModel d) {E : ℝ} (hEfloor : 15 * (Disorder.cstar M)⁻¹ ≤ E) : 10 ≤ E

The amplitude range

theorem Algsuperdiff.Section3.Provider.Homogenization.amplitude_mem_Ioc_of_gate {d : ℕ} (M : ABKModel d) {E Chom epsilon : ℝ} (hE : 1 ≤ E) (hChom : 10 ^ 9 ≤ Chom) (hepsilon : epsilon ∈ Set.Ioc 0 (1 / 2)) (hgate : M.gamma ≤ Chom⁻¹ * E⁻¹ ^ 2 * epsilon) : 10 ^ 9 * E ^ 2 * M.gamma ∈ Set.Ioc 0 (1 / 2)

The amplitude range, A.3's 0 < delta_1 <= 1/2 for delta_1 = 10^9 E^2 gamma.

The arithmetic is 10^9 E^2 gamma <= 10^9 Chom^{-1} epsilon <= epsilon <= 1/2.

The diagonal fourth moment

theorem Algsuperdiff.Section3.Provider.Homogenization.lintegral_cutoffHomogenizationErrorRepresentative_pow_four_le {d : ℕ} (M : ABKModel d) {m : ℤ} {E : { E : ℝ // 1 ≤ E }} (hEfloor : 15 * (Disorder.cstar M)⁻¹ ≤ ↑E) (hregime : M.gamma ≤ (↑E)⁻¹ ^ 10) (hLower : ∀ k ≤ m - 1, ∀ (s : ℝ) (hsWindow : s ∈ Set.Icc (8 * M.gamma) 1), Probability.IsTwoTermBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) (HCPolySupport.IndependentSums.gammaSigma (1 / 2)) (Observable.cutoffHomogenizationError M k ⟨s, ⋯⟩) (↑E * s⁻¹ * √M.gamma) (s⁻¹ ^ 2 * Real.exp (-((↑E)⁻¹ ^ 3 * M.gamma⁻¹)))) {L : ℤ} (hL : L ≤ m - 1) : ∫⁻ (omega : Cutoff.CutoffSample d), ENNReal.ofReal (Observable.cutoffHomogenizationErrorRepresentative M L L (1 / 4) (Annealed.sigmaBar M L) omega ^ 4) ∂↑(Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal ((10 ^ 9 * ↑E ^ 2 * M.gamma) ^ 2)

The diagonal fourth moment at s = 1/4. Under the preceding-error clause of the frozen statement and its two regime facts, for every cutoff scale L <= m - 1,

E[mathcal E_{1/4, infinity, 2}(cu_L; a_L, shom_L)^4] <= (10^9 E^2 gamma)^2,

in the lintegral shape the proved Step-1 consumers take.

The cube scale, the coefficient-cutoff scale and the comparator scale are all L, so this is the diagonal display and the clause is used at its own observation scale: no finite-cover transport and no discount halving occurs, and the printed discount 1/4 is kept. The window 1/4 in Icc (8 gamma) 1 required by the clause is supplied from E >= 10 and gamma <= E^{-10}.

theorem Algsuperdiff.Section3.Provider.Homogenization.amplitude_mem_Ioc_and_lintegral_pow_four_le {d : ℕ} (M : ABKModel d) {m : ℤ} {E : { E : ℝ // 1 ≤ E }} {Chom epsilon : ℝ} (hChom : 10 ^ 9 ≤ Chom) (hEfloor : 15 * (Disorder.cstar M)⁻¹ ≤ ↑E) (hregime : M.gamma ≤ (↑E)⁻¹ ^ 10) (hLower : ∀ k ≤ m - 1, ∀ (s : ℝ) (hsWindow : s ∈ Set.Icc (8 * M.gamma) 1), Probability.IsTwoTermBigOWith (↑(Cutoff.cutoffSampleLaw M)) (HCPolySupport.IndependentSums.gammaSigma 2) (HCPolySupport.IndependentSums.gammaSigma (1 / 2)) (Observable.cutoffHomogenizationError M k ⟨s, ⋯⟩) (↑E * s⁻¹ * √M.gamma) (s⁻¹ ^ 2 * Real.exp (-((↑E)⁻¹ ^ 3 * M.gamma⁻¹)))) (hepsilon : epsilon ∈ Set.Ioc 0 (1 / 2)) (hgate : M.gamma ≤ Chom⁻¹ * (↑E)⁻¹ ^ 2 * epsilon) : 10 ^ 9 * ↑E ^ 2 * M.gamma ∈ Set.Ioc 0 (1 / 2) ∧ ∀ L ≤ m - 1, ∫⁻ (omega : Cutoff.CutoffSample d), ENNReal.ofReal (Observable.cutoffHomogenizationErrorRepresentative M L L (1 / 4) (Annealed.sigmaBar M L) omega ^ 4) ∂↑(Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal ((10 ^ 9 * ↑E ^ 2 * M.gamma) ^ 2)

The amplitude bridge, item (I-1) of the corrected Section 3.5 account: the two data the Step-1 display must be instantiated with at delta_1 = 10^9 E^2 gamma, delivered together and uniformly in the cutoff scale.

The amplitude does not depend on L, so the fourth-moment half is uniform over the whole admissible corridor L <= m - 1 and, in particular, over every corridor scale pair the finite recurrence of A.4 reindexes.