LocalizationOscillationGridMoment

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

Provider: the grid fourth-moment functional of e.lower.bound.oscillations

Source displays in ABK26:

• e.lower.bound.oscillations (label; display) opens with the quantity (avsum_{z in 3^n Zd cap cu_K} E[ ‖grad w - (grad w)_{z+cu_n}‖^4_{L2bar(z+cu_n)} ])^{1/4};
• e.nablaw.oscillations (label; display) is the per-base-point estimate that gets inserted into it.

This module isolates the purely functional-analytic bookkeeping of that passage: the mixed "average over the grid, expectation over the sample" fourth-moment functional and its behaviour under a pointwise two-term majorant.

What is proved

• gridFourthMoment, gridFourthMomentRoot -- the functional avsum_{R in I} integral^4 of the display and its fourth root.
• cubeFamilyAverage_mono, cubeFamilyAverage_add, cubeFamilyAverage_const_mul -- the three elementary facts about the grid average of LocalizationGrid that the assembly uses.
• gridFourthMoment_le_eight_mul_add -- if F <= G + H pointwise on the grid and on the sample space, then M_4(F) <= 8 M_4(G) + 8 M_4(H). The elementary inequality behind it is (a+b)^4 <= 8(a^4+b^4), valid for all reals.
• gridFourthMomentRoot_le_add_of_le -- the shape the display consumes: from M_4(G) <= WG^4 and M_4(H) <= WH^4 one gets M_4(F)^{1/4} <= 8^{1/4} (WG + WH).
• gridFourthMoment_le_of_forall_le -- a per-cube uniform bound transfers to the grid average.

Divergences from the printed statement

• The triangle step costs the absolute factor 8^{1/4}, not 1. The manuscript's implicit step is Minkowski's inequality in L^4(counting x P), whose constant is 1. What is proved here is the elementary (a+b)^4 <= 8(a^4+b^4) route, whose constant is 8^{1/4} < 1.682. The loss is an absolute number, it is written out in the statement, and it is absorbed by the manuscript's dimension-only C; no sharper claim is made and nothing is hidden inside a constant.
• Nothing here relates the full grid to its interior part. The passage from an interior mesh to the full one, and the boundary strip it leaves behind, are LocalizationFluctuationMeshTransfer.cubeFamilyAverage_le_add_sqrt_boundaryFraction and its consumers; this module works at a fixed family I throughout.

Two elementary real facts

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.rpow_four_eq_pow_four (x : ℝ) : x ^ 4 = x ^ 4

The real power x ^ (4 : ℝ) is the monoid power x ^ (4 : ℕ).

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.rpow_four_nonneg (x : ℝ) : 0 ≤ x ^ 4

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.add_pow_four_le_eight_mul (a b : ℝ) : (a + b) ^ 4 ≤ 8 * (a ^ 4 + b ^ 4)

(a + b)^4 ≤ 8 (a^4 + b^4), valid for all reals. This is the elementary substitute for Minkowski's inequality used in the grid assembly; the constant 8 is sharp for this form.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.pow_four_add_pow_four_le (x y : ℝ) (hx : 0 ≤ x) (hy : 0 ≤ y) : x ^ 4 + y ^ 4 ≤ (x + y) ^ 4

x^4 + y^4 ≤ (x + y)^4 for nonnegative x, y.

Three elementary facts about the grid average

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.cubeFamilyAverage_mono {d : ℕ} {I : Finset (HCPolySupport.TriadicCube d)} {F G : HCPolySupport.TriadicCube d → ℝ} (h : ∀ R ∈ I, F R ≤ G R) : cubeFamilyAverage I F ≤ cubeFamilyAverage I G

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.cubeFamilyAverage_add {d : ℕ} (I : Finset (HCPolySupport.TriadicCube d)) (F G : HCPolySupport.TriadicCube d → ℝ) : (cubeFamilyAverage I fun (R : HCPolySupport.TriadicCube d) => F R + G R) = cubeFamilyAverage I F + cubeFamilyAverage I G

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.cubeFamilyAverage_const_mul {d : ℕ} (I : Finset (HCPolySupport.TriadicCube d)) (c : ℝ) (F : HCPolySupport.TriadicCube d → ℝ) : (cubeFamilyAverage I fun (R : HCPolySupport.TriadicCube d) => c * F R) = c * cubeFamilyAverage I F

The grid fourth-moment functional

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.gridFourthMoment {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (I : Finset (HCPolySupport.TriadicCube d)) (F : HCPolySupport.TriadicCube d → Ω → ℝ) : ℝ

The fourth-moment functional of e.lower.bound.oscillations. For a family F of nonnegative random variables indexed by the grid I, this is avsum_{R in I} E[^4], the quantity under the outer fourth root of the display.

Equations

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

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.gridFourthMomentRoot {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (I : Finset (HCPolySupport.TriadicCube d)) (F : HCPolySupport.TriadicCube d → Ω → ℝ) : ℝ

The outer fourth root of the display.

Equations

• Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.gridFourthMomentRoot μ I F = Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.gridFourthMoment μ I F ^ 4⁻¹

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.gridFourthMoment_nonneg {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (I : Finset (HCPolySupport.TriadicCube d)) (F : HCPolySupport.TriadicCube d → Ω → ℝ) : 0 ≤ gridFourthMoment μ I F

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.gridFourthMoment_const_mul {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (I : Finset (HCPolySupport.TriadicCube d)) (c : ℝ) (F : HCPolySupport.TriadicCube d → Ω → ℝ) : (gridFourthMoment μ I fun (R : HCPolySupport.TriadicCube d) (ω : Ω) => c * F R ω) = c ^ 4 * gridFourthMoment μ I F

Scalars come out of the functional at the fourth power.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.gridFourthMoment_le_of_forall_le {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (I : Finset (HCPolySupport.TriadicCube d)) (F : HCPolySupport.TriadicCube d → Ω → ℝ) {B : ℝ} (hB : 0 ≤ B) (h : ∀ R ∈ I, ∫ (ω : Ω), F R ω ^ 4 ∂μ ≤ B) : gridFourthMoment μ I F ≤ B

A uniform per-cube bound transfers to the grid average.

The two-term majorant

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.gridFourthMoment_le_eight_mul_add {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (I : Finset (HCPolySupport.TriadicCube d)) (F G H : HCPolySupport.TriadicCube d → Ω → ℝ) (hF : ∀ R ∈ I, ∀ (ω : Ω), 0 ≤ F R ω) (hle : ∀ R ∈ I, ∀ (ω : Ω), F R ω ≤ G R ω + H R ω) (hGi : ∀ R ∈ I, MeasureTheory.Integrable (fun (ω : Ω) => G R ω ^ 4) μ) (hHi : ∀ R ∈ I, MeasureTheory.Integrable (fun (ω : Ω) => H R ω ^ 4) μ) : gridFourthMoment μ I F ≤ 8 * gridFourthMoment μ I G + 8 * gridFourthMoment μ I H

The grid fourth moment under a pointwise two-term majorant. This is the step of e.lower.bound.oscillations that inserts e.nablaw.oscillations into the grid average, with the elementary constant 8 in place of Minkowski's 1.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.gridFourthMomentRoot_le_of_le {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (I : Finset (HCPolySupport.TriadicCube d)) (F : HCPolySupport.TriadicCube d → Ω → ℝ) {B : ℝ} (hB : 0 ≤ B) (h : gridFourthMoment μ I F ≤ B ^ 4) : gridFourthMomentRoot μ I F ≤ B

From a fourth-power bound on the functional to a bound on its fourth root.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.gridFourthMomentRoot_le_add_of_le {d : ℕ} {Ω : Type u_1} [MeasurableSpace Ω] (μ : MeasureTheory.Measure Ω) (I : Finset (HCPolySupport.TriadicCube d)) (F G H : HCPolySupport.TriadicCube d → Ω → ℝ) {WG WH : ℝ} (hWG : 0 ≤ WG) (hWH : 0 ≤ WH) (hF : ∀ R ∈ I, ∀ (ω : Ω), 0 ≤ F R ω) (hle : ∀ R ∈ I, ∀ (ω : Ω), F R ω ≤ G R ω + H R ω) (hGi : ∀ R ∈ I, MeasureTheory.Integrable (fun (ω : Ω) => G R ω ^ 4) μ) (hHi : ∀ R ∈ I, MeasureTheory.Integrable (fun (ω : Ω) => H R ω ^ 4) μ) (hG : gridFourthMoment μ I G ≤ WG ^ 4) (hH : gridFourthMoment μ I H ≤ WH ^ 4) : gridFourthMomentRoot μ I F ≤ 8 ^ 4⁻¹ * (WG + WH)

The shape e.lower.bound.oscillations consumes. A pointwise two-term majorant on the grid, together with fourth-moment bounds for the two majorants, gives the fourth root of the display's left-hand side at the absolute cost 8^{1/4}.