LocalizationGrid

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

Provider: the meso grid of the localization display, full and interior filtered

Source displays in ABK26:

• e.lower.bound.localization.terms (label) averages its bracketed integrand over the site set z in 3^n Z^d cap cu_K;
• e.recurrence.params (label) fixes the meso scale n;
• the A_4 leg of Step 2 averages |bfAhom^{1/2} P_z|^4 over the same site set.

This module supplies the two grid renderings of that site set and the exact bookkeeping that relates them.

What is proved

• cubeAverage_originCube_eq_descendantsAverage -- the tiling identity fint_{cu_K} f = descendantsAverage (originCube d K) j (fun R => fint_R f) for f integrable on cu_K, at the origin cube. This is a specialization of CoarseGraining's cubeAverage_eq_descendantsAverage_cubeAverage_of_integrableOn, which already holds at an arbitrary triadic cube and arbitrary depth; nothing new is proved here, the named form is recorded because it is the display's carrier.
• mesoCubeGrid -- the full scale-n grid of cu_K, i.e. descendantsAtScale (originCube d K) n, and cubeAverage_originCube_eq_mesoGridAverage, the tiling identity in the scale-indexed grid form, at tiling constant 1.
• interiorMesoCubeGrid -- the subfamily of mesoCubeGrid whose enlarged outer window z + cu_{outer+1} still lies inside cu_K, together with window_subset_of_mem_interiorMesoCubeGrid, the containment that the per-cube estimates consume.
• card_mesoCubeGrid_le_three_pow_mul_card_interior -- the boundary-layer count: the removed layer costs at most the pure model constant 3^d.
• cubeFamilyAverage_interior_le_of_full -- the resulting transfer of a nonnegative grid average from the full family to the interior family.

Divergences from the printed statement

• The tiling identity holds at constant 1; this is mesoCubeGrid and cubeAverage_originCube_eq_mesoGridAverage.
• The display leg is interior-filtered. It runs on the interior-filtered subfamily, on which the tiling identity is false: a boundary layer of width ~3^{outer+1} is removed. This is interiorMesoCubeGrid, and the two legs meet only through the one-directional cardinality bookkeeping below.
• The two legs are different objects. The two previous items describe different legs. mesoCubeGrid carries the A_4 / principal leg, interiorMesoCubeGrid the display leg.
• The count constant is crude and gamma-free. The boundary-layer count below is 3^d, obtained from the concentric child cu_{K-1}; the true ratio is 1 + O(3^{-(K-outer)}). No sharper count is claimed.

What is not proved here

• The full-grid boundary transfer is open. Only interior <= 3^d * full is proved. The opposite direction full <= C * interior -- what a lift of the display leg back to the manuscript's full grid would need -- is NOT proved here and is not attainable by this route: the display's integrand has no sign, and no per-cube bound of any kind is available at boundary cubes. A consumer that wants the full grid must supply that transfer itself; this module does not.
• The grid mismatch is untouched. The manuscript states its per-cube inputs on the cu_m grid while the display averages the cu_K grid; the stationarity argument reconciling them is not supplied below.

The average over a finite family of cubes

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.cubeFamilyAverage {d : ℕ} (I : Finset (HCPolySupport.TriadicCube d)) (F : HCPolySupport.TriadicCube d → ℝ) : ℝ

The unweighted average of a real function over a finite family of cubes. On a family of equal-volume cubes -- which is the only case used below -- this is also the volume-weighted average.

Equations

• Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.cubeFamilyAverage I F = (↑I.card)⁻¹ * ∑ R ∈ I, F R

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.descendantsAverage_eq_cubeFamilyAverage {d : ℕ} (Q : HCPolySupport.TriadicCube d) (j : ℕ) (F : HCPolySupport.TriadicCube d → ℝ) : HCPolySupport.descendantsAverage Q j F = cubeFamilyAverage (HCPolySupport.descendantsAtDepth Q j) F

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

The two grids

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

The manuscript's meso site set 3^n Z^d cap cu_K, rendered as the finite family of scale-n triadic descendants of cu_K.

Equations

• Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.mesoCubeGrid d K n = HCPolySupport.descendantsAtScale (HCPolySupport.originCube d K) n

noncomputable def Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.interiorMesoCubeGrid (d : ℕ) (K n outer : ℤ) : Finset (HCPolySupport.TriadicCube d)

The interior-filtered meso grid: those scale-n descendants of cu_K whose enlarged outer window z + cu_{outer+1}, based at the cube's own site z = triadicCubeShift R, is still contained in cu_K. This is the exact carrier of the per-cube estimates.

Equations

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

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.mem_interiorMesoCubeGrid_iff {d : ℕ} {K n outer : ℤ} {R : HCPolySupport.TriadicCube d} : R ∈ interiorMesoCubeGrid d K n outer ↔ R ∈ mesoCubeGrid d K n ∧ HCPolySupport.translateSet (HCPolySupport.triadicCubeShift R) (HCPolySupport.openCubeSet (HCPolySupport.originCube d (outer + 1))) ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d K)

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.interiorMesoCubeGrid_subset {d : ℕ} {K n outer : ℤ} : interiorMesoCubeGrid d K n outer ⊆ mesoCubeGrid d K n

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.window_subset_of_mem_interiorMesoCubeGrid {d : ℕ} {K n outer : ℤ} {R : HCPolySupport.TriadicCube d} (hR : R ∈ interiorMesoCubeGrid d K n outer) : HCPolySupport.translateSet (HCPolySupport.triadicCubeShift R) (HCPolySupport.openCubeSet (HCPolySupport.originCube d (outer + 1))) ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d K)

The containment that the per-cube estimates consume. A member of the interior grid has its enlarged outer window inside cu_K; this is the hparent input of the nested Campanato tower.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.mesoCubeGrid_eq_descendantsAtDepth {d : ℕ} {K n : ℤ} (hn : n ≤ K) : mesoCubeGrid d K n = HCPolySupport.descendantsAtDepth (HCPolySupport.originCube d K) (K - n).toNat

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.card_mesoCubeGrid {d : ℕ} {K n : ℤ} (hn : n ≤ K) : (mesoCubeGrid d K n).card = (3 ^ d) ^ (K - n).toNat

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.mesoCubeGrid_nonempty {d : ℕ} {K n : ℤ} (hn : n ≤ K) : (mesoCubeGrid d K n).Nonempty

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.scale_eq_of_mem_mesoCubeGrid {d : ℕ} {K n : ℤ} {R : HCPolySupport.TriadicCube d} (hR : R ∈ mesoCubeGrid d K n) : R.scale = n

The tiling identity

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.cubeAverage_originCube_eq_descendantsAverage {d : ℕ} (K : ℤ) (j : ℕ) (f : HCPolySupport.Vec d → ℝ) (hf : MeasureTheory.IntegrableOn f (HCPolySupport.cubeSet (HCPolySupport.originCube d K)) MeasureTheory.volume) : HCPolySupport.cubeAverage (HCPolySupport.originCube d K) f = HCPolySupport.descendantsAverage (HCPolySupport.originCube d K) j fun (R : HCPolySupport.TriadicCube d) => HCPolySupport.cubeAverage R f

The mesh tiling identity at the origin cube. For f integrable on cu_K, fint_{cu_K} f = descendantsAverage (originCube d K) j (fun R => fint_R f).

This is CoarseGraining's cubeAverage_eq_descendantsAverage_cubeAverage_of_integrableOn specialized to the origin cube; the general identity was already available at an arbitrary triadic cube and an arbitrary depth.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.cubeAverage_originCube_eq_mesoGridAverage {d : ℕ} {K n : ℤ} (hn : n ≤ K) (f : HCPolySupport.Vec d → ℝ) (hf : MeasureTheory.IntegrableOn f (HCPolySupport.cubeSet (HCPolySupport.originCube d K)) MeasureTheory.volume) : HCPolySupport.cubeAverage (HCPolySupport.originCube d K) f = cubeFamilyAverage (mesoCubeGrid d K n) fun (R : HCPolySupport.TriadicCube d) => HCPolySupport.cubeAverage R f

The tiling identity in the scale-indexed grid form. The manuscript's avsum_{z in 3^n Z^d cap cu_K} fint_{z + cu_n} f is fint_{cu_K} f exactly: the tiling constant is 1.

The concentric child, and the boundary-layer count

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.card_mesoCubeGrid_le_three_pow_mul_card_interior {d : ℕ} {K n outer : ℤ} (hn : n ≤ K - 1) (houter : outer + 1 ≤ K - 1) : (mesoCubeGrid d K n).card ≤ 3 ^ d * (interiorMesoCubeGrid d K n outer).card

The boundary-layer count. The full meso grid exceeds the interior grid by at most the pure model constant 3^d, free of gamma, of m, of h and of K.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.interiorMesoCubeGrid_nonempty {d : ℕ} {K n outer : ℤ} (hn : n ≤ K - 1) (houter : outer + 1 ≤ K - 1) : (interiorMesoCubeGrid d K n outer).Nonempty

The transfer of a nonnegative average

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.cubeFamilyAverage_interior_le_of_full {d : ℕ} {K n outer : ℤ} {F : HCPolySupport.TriadicCube d → ℝ} (hn : n ≤ K - 1) (houter : outer + 1 ≤ K - 1) (hF : ∀ R ∈ mesoCubeGrid d K n, 0 ≤ F R) : cubeFamilyAverage (interiorMesoCubeGrid d K n outer) F ≤ 3 ^ d * cubeFamilyAverage (mesoCubeGrid d K n) F

Transfer of a nonnegative grid average from the full family to the interior family, at the boundary-layer cost 3^d.