LocalizationOverlapTransfer

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

Provider: the bounded-overlap covering transfer for the meso windows

Source displays in ABK26:

• e.nablaw.oscillations (label; display), whose outer window is z + cu_{m-h};
• e.lower.bound.oscillations (label; display), which averages over the mesh z in 3^n Zd cap cu_K and is deduced "by e.nablaw.in.L.eight" -- a statement about the single global normalized norm on cu_K;
• e.nablaw.in.L.eight (label; display).

The passage from the global quantity on cu_K to the mesh average of window quantities is the covering step that the manuscript does not write out. This module supplies it.

What is proved

With N = m - h - n the gap and W_R = z + cu_{n+N} the window based at the site z = triadicCubeShift R of a scale-n cube R:

• sum_setIntegral_openCubeAtScale_le -- for a nonnegative f integrable on cu_K, and a family of scale-n cubes whose windows lie in cu_K, sum_R int_{W_R} f <= 3^{dN} int_{cu_K} f. The multiplicity 3^{dN} is the exact overlap count of LocalizationOverlapCount, and is attained there.
• cubeFamilyAverage_volumeAverage_openCubeAtScale_le_of_card -- the same statement after both normalizations, at a caller-supplied constant C controlled by the cardinality gate 3^{d(K-n)} <= C |I|. This is the general form: the constant is exactly the ratio of the full lattice count 3^{d(K-n)} to the number of cubes actually summed, and the overlap multiplicity has cancelled against the window volume completely.
• cubeFamilyAverage_volumeAverage_openCubeAtScale_interior_le -- the instance the display consumes, on interiorMesoCubeGrid d K n (n + N - 1), at the absolute constant 3^d.

Where the constant comes from, exactly

The multiplicity 3^{dN} and the window volume 3^{(n+N)d} cancel exactly: the volume-normalized transfer constant produced by the covering alone is 1. The entire constant 3^d of the interior instance is the interior-grid deficit: the interior grid is only guaranteed to contain the scale-n descendants of the concentric child cu_{K-1}, i.e. at least 3^{-d} of the full grid (card_mesoCubeGrid_le_three_pow_mul_card_interior, module LocalizationGrid), and the grid average divides by the number of cubes summed. On the full grid mesoCubeGrid d K n the same argument gives the constant 1, but the full grid's boundary windows are not contained in cu_K and the hypothesis hsub fails there; that is the content.

Divergences from the printed statement

• The manuscript's unrestricted mesh is not such a family, and no bound at the boundary sites is claimed here.
• The count is not clipped. sum_setIntegral_openCubeAtScale_le uses the full lattice multiplicity 3^{dN}; clipping the family to cu_K could only improve it, and no such improvement is claimed.
• Nonnegativity is required everywhere, not almost everywhere. The applications supply a pointwise nonnegative integrand (a squared or fourth power), so the cheaper hypothesis is used. Nothing below is false for the a.e. version; it is simply not proved here.

The covering bound on the sum of window integrals

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.sum_setIntegral_openCubeAtScale_le {d : ℕ} {K n : ℤ} {N : ℕ} {I : Finset (HCPolySupport.TriadicCube d)} {f : HCPolySupport.Vec d → ℝ} (hI : ∀ R ∈ I, R.scale = n) (hsub : ∀ R ∈ I, HCPolySupport.Book.Ch03.openCubeAtScale (HCPolySupport.triadicCubeShift R) (n + ↑N) ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d K)) (hf : MeasureTheory.IntegrableOn f (HCPolySupport.openCubeSet (HCPolySupport.originCube d K)) MeasureTheory.volume) (hf0 : ∀ (x : HCPolySupport.Vec d), 0 ≤ f x) : ∑ R ∈ I, ∫ (x : HCPolySupport.Vec d) in HCPolySupport.Book.Ch03.openCubeAtScale (HCPolySupport.triadicCubeShift R) (n + ↑N), f x ≤ (3 ^ N) ^ d * ∫ (x : HCPolySupport.Vec d) in HCPolySupport.openCubeSet (HCPolySupport.originCube d K), f x

The bounded-overlap covering bound. For a nonnegative integrable f and a family of scale-n cubes whose windows z + cu_{n+N} lie in cu_K, the sum of the window integrals exceeds the integral over cu_K by at most the overlap multiplicity 3^{dN} of card_filter_mem_openCubeAtScale_le.

: the caller supplies hI, hsub, hf, hf0.

The normalized transfer

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.cubeFamilyAverage_volumeAverage_openCubeAtScale_le_of_card {d : ℕ} {K n : ℤ} {N : ℕ} {I : Finset (HCPolySupport.TriadicCube d)} {f : HCPolySupport.Vec d → ℝ} {C : ℝ} (hInon : I.Nonempty) (hI : ∀ R ∈ I, R.scale = n) (hsub : ∀ R ∈ I, HCPolySupport.Book.Ch03.openCubeAtScale (HCPolySupport.triadicCubeShift R) (n + ↑N) ⊆ HCPolySupport.openCubeSet (HCPolySupport.originCube d K)) (hcard : (3 ^ (K - n)) ^ d ≤ C * ↑I.card) (hf : MeasureTheory.IntegrableOn f (HCPolySupport.openCubeSet (HCPolySupport.originCube d K)) MeasureTheory.volume) (hf0 : ∀ (x : HCPolySupport.Vec d), 0 ≤ f x) : (cubeFamilyAverage I fun (R : HCPolySupport.TriadicCube d) => HCPolySupport.volumeAverage (HCPolySupport.Book.Ch03.openCubeAtScale (HCPolySupport.triadicCubeShift R) (n + ↑N)) f) ≤ C * HCPolySupport.volumeAverage (HCPolySupport.openCubeSet (HCPolySupport.originCube d K)) f

The normalized bounded-overlap transfer. After dividing by the window volume and by the number of cubes summed, the overlap multiplicity has cancelled against the window volume exactly, and the whole constant is the cardinality ratio supplied by hcard.

: the caller supplies hInon, hI, hsub, hcard, hf, hf0.

theorem Algsuperdiff.Section3.Provider.Diffusivity.ApproximateRecurrence.cubeFamilyAverage_volumeAverage_openCubeAtScale_interior_le {d : ℕ} {K n : ℤ} {N : ℕ} {f : HCPolySupport.Vec d → ℝ} (hn : n ≤ K - 1) (hN : n + ↑N ≤ K - 1) (hf : MeasureTheory.IntegrableOn f (HCPolySupport.openCubeSet (HCPolySupport.originCube d K)) MeasureTheory.volume) (hf0 : ∀ (x : HCPolySupport.Vec d), 0 ≤ f x) : (cubeFamilyAverage (interiorMesoCubeGrid d K n (n + ↑N - 1)) fun (R : HCPolySupport.TriadicCube d) => HCPolySupport.volumeAverage (HCPolySupport.Book.Ch03.openCubeAtScale (HCPolySupport.triadicCubeShift R) (n + ↑N)) f) ≤ 3 ^ d * HCPolySupport.volumeAverage (HCPolySupport.openCubeSet (HCPolySupport.originCube d K)) f

The transfer on the interior meso grid, at the absolute constant 3^d.

This is the form e.lower.bound.oscillations consumes. The constant is not the overlap multiplicity -- that has cancelled exactly -- but the interior-grid deficit of LocalizationGrid.

: the caller supplies hn : n <= K - 1, hN : n + N <= K - 1, hf, hf0.