LocalizationFluctuationMeshTransfer

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

The interior-to-full mesh passage

  z in 3^n Zd cap cu_K   with   z + cu_{m-h} subseteq cu_K ,

whereas the display that consumes it, e.lower.bound.oscillations, averages over the full mesh 3^n Zd cap cu_K.

This module takes the second route, which is the one the formalization needs: the downstream carrier is the full descendantsAtDepth family of LocalizationRecurrenceMesh, so the interior restriction cannot be pushed forward. The transfer has two halves, both proved here and both unconditional.

The signed transfer is also proved here in the Closure namespace, with the interior average replaced by its maximum with zero. The nonnegative estimate is a corollary of that common calculation.

• A Cauchy--Schwarz split: for a nonnegative family F on a finite grid I and any sub-grid J,

  avsum_{R in I} F R
    <= avsum_{R in J} F R
       + sqrt(1 - |J| / |I|) * sqrt(avsum_{R in I} (F R)^2) .
  

  Nothing is assumed about F beyond nonnegativity; the boundary contribution is paid by the square root of the missing fraction against the square function of the same average.

• A boundary count: the interior mesh of LocalizationGrid contains the index box of radius halfRange p - halfRange g, where p = K - n is the depth of the mesh and g = (m-h) - n the window gap, so

  1 - |interiorMesoCubeGrid d K n (m-h-1)| / |mesoCubeGrid d K n|
    <= d * 3^{g - p} = d * 3^{(m-h) - K} .
  

  Under the recurrence's own large-cube gate 10^10 gamma^{-1} <= K - m the right-hand side is below 3^{-10^10 gamma^{-1}} up to the dimensional factor, i.e. smaller than every power of gamma.

Combining the two gives gridFourthMoment_mesoCubeGrid_le_interior_add: the full-mesh fourth-moment average of e.lower.bound.oscillations is the interior one plus sqrt(d 3^{(m-h)-K}) times the square root of the squared grid average. The remaining input a consumer owes is exactly that squared average, i.e. an eighth-moment envelope of the same per-cell quantity; no boundary geometry, no artificial cutoff and no stationarity argument is introduced.

Binders

Every statement below is finite combinatorics or cube-index arithmetic. The only hypotheses are the scale bookkeeping K = n + p, outer + 1 = n + g, g <= p -- which merely name the depth and the window gap of the recurrence mesh -- and the nonnegativity of the averaged family. No smallness, moment, measurability or integrability proposition occurs, and nothing about the corrector or the sample space is assumed.

Scope

There is no sorry.

References

• ABK26, e.nablaw.oscillations, e.lower.bound.oscillations, e.recurrence.params.

The Cauchy--Schwarz split of a grid average

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.sum_le_sqrt_card_mul_sqrt_sum_sq {d : ℕ} (s : Finset (HCPolySupport.TriadicCube d)) (F : HCPolySupport.TriadicCube d → ℝ) (hF : ∀ R ∈ s, 0 ≤ F R) : ∑ R ∈ s, F R ≤ √↑s.card * √(∑ R ∈ s, F R ^ 2)

Cauchy--Schwarz for a nonnegative family on a finite grid.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.Closure.cubeFamilyAverage_le_max_add_sqrt_boundaryFraction {d : ℕ} {I J : Finset (HCPolySupport.TriadicCube d)} (hJI : J ⊆ I) (F : HCPolySupport.TriadicCube d → ℝ) : cubeFamilyAverage I F ≤ max (cubeFamilyAverage J F) 0 + √(1 - ↑J.card / ↑I.card) * √(cubeFamilyAverage I fun (R : HCPolySupport.TriadicCube d) => F R ^ 2)

The boundary transfer without a sign hypothesis.

For any sub-family J of I and any real family F,

  avsum_I F  <=  max (avsum_J F) 0  +  sqrt (1 - |J|/|I|) . sqrt (avsum_I F^2) .

The interior half uses only |J| <= |I| and 0 <= max (avsum_J F) 0; the strip half is Cauchy--Schwarz at |F|. Unconditional.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.cubeFamilyAverage_le_add_sqrt_boundaryFraction {d : ℕ} {I J : Finset (HCPolySupport.TriadicCube d)} (hJI : J ⊆ I) (F : HCPolySupport.TriadicCube d → ℝ) (hF : ∀ R ∈ I, 0 ≤ F R) : cubeFamilyAverage I F ≤ cubeFamilyAverage J F + √(1 - ↑J.card / ↑I.card) * √(cubeFamilyAverage I fun (R : HCPolySupport.TriadicCube d) => F R ^ 2)

The boundary transfer. For a nonnegative family, the average over the full grid is the average over any sub-grid plus a Cauchy--Schwarz remainder carrying the square root of the missing fraction. Unconditional.

The index box inside the interior mesh

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.translateSet_subset_openCubeSet_originCube {d : ℕ} {K L n : ℤ} {R : HCPolySupport.TriadicCube d} (hsc : R.scale = n) (hidx : ∀ (i : Fin d), |↑(R.index i)| * 3 ^ n + 3 ^ L / 2 ≤ 3 ^ K / 2) : HCPolySupport.translateSet (HCPolySupport.triadicCubeShift R) (HCPolySupport.openCubeSet (HCPolySupport.originCube d L)) ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d K)

The window of a cube whose site is far enough from the boundary stays inside the big cube. Unconditional cube-index arithmetic.

def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.indexBoxGrid (d : ℕ) (n r : ℤ) : Finset (HCPolySupport.TriadicCube d)

The family of scale-n triadic cubes whose index lies in the centred box of radius r. This is the interior sub-mesh of the boundary count.

Equations

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

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.mem_indexBoxGrid_iff {d : ℕ} {n r : ℤ} {R : HCPolySupport.TriadicCube d} : R ∈ indexBoxGrid d n r ↔ R.scale = n ∧ ∀ (i : Fin d), -r ≤ R.index i ∧ R.index i ≤ r

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.card_indexBoxGrid (d : ℕ) (n r : ℤ) : (indexBoxGrid d n r).card = (2 * r + 1).toNat ^ d

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.indexBoxGrid_subset_mesoCubeGrid (d : ℕ) {K n r : ℤ} (hnK : n ≤ K) (hr : r ≤ HCPolySupport.Gagliardo.halfRange (K - n).toNat) : indexBoxGrid d n r ⊆ mesoCubeGrid d K n

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.indexBoxGrid_subset_interiorMesoCubeGrid (d : ℕ) {K n outer r : ℤ} (hnK : n ≤ K) (hr : r ≤ HCPolySupport.Gagliardo.halfRange (K - n).toNat) (hgeom : ↑r * 3 ^ n + 3 ^ (outer + 1) / 2 ≤ 3 ^ K / 2) : indexBoxGrid d n r ⊆ interiorMesoCubeGrid d K n outer

The boundary fraction

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.two_mul_halfRange_real (m : ℕ) : 2 * ↑(HCPolySupport.Gagliardo.halfRange m) = 3 ^ m - 1

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.card_interiorMesoCubeGrid_ge (d : ℕ) {K n outer : ℤ} {p g : ℕ} (hK : K = n + ↑p) (houter : outer + 1 = n + ↑g) (hgp : g ≤ p) : (3 ^ p - 3 ^ g + 1) ^ d ≤ ↑(interiorMesoCubeGrid d K n outer).card

The interior mesh is large. At mesh depth p = K - n and window gap g = (outer + 1) - n, the interior grid contains the index box of radius halfRange p - halfRange g, whose cardinality is (3^p - 3^g + 1)^d.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.one_sub_interior_card_ratio_le (d : ℕ) {K n outer : ℤ} {p g : ℕ} (hK : K = n + ↑p) (houter : outer + 1 = n + ↑g) (hgp : g ≤ p) : 1 - ↑(interiorMesoCubeGrid d K n outer).card / ↑(mesoCubeGrid d K n).card ≤ ↑d * (3 ^ g / 3 ^ p)

The boundary fraction. The fraction of the full mesh that the interior mesh misses is at most d 3^{g - p}, i.e. d 3^{L - K} where L = outer + 1 is the window scale and K the big-cube scale.

The transfer of the fourth-moment grid average

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.gridFourthMoment_mesoCubeGrid_le_interior_add {Omega : Type u_1} [MeasurableSpace Omega] (mu : MeasureTheory.Measure Omega) (d : ℕ) {K n outer : ℤ} {p g : ℕ} (hK : K = n + ↑p) (houter : outer + 1 = n + ↑g) (hgp : g ≤ p) (F : HCPolySupport.TriadicCube d → Omega → ℝ) : gridFourthMoment mu (mesoCubeGrid d K n) F ≤ gridFourthMoment mu (interiorMesoCubeGrid d K n outer) F + √(↑d * (3 ^ g / 3 ^ p)) * √(cubeFamilyAverage (mesoCubeGrid d K n) fun (R : HCPolySupport.TriadicCube d) => (∫ (omega : Omega), F R omega ^ 4 ∂mu) ^ 2)

The transfer at the display's own functional. The full-mesh fourth-moment average of e.lower.bound.oscillations is the interior one plus sqrt(d 3^{g-p}) times the square root of the squared grid average.

only on the scale bookkeeping; nothing about F, the corrector or the sample space is assumed.