OneCube

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

Provider: the one-cube descendant bound for the homogenization error

This file proves a local version of the display e.bound.one.cube.by.mathcalE of ABK26: for every k ∈ (-∞,m] ∩ ℤ,

max_{z ∈ 3^k ℤ^d ∩ □_m} 𝓔_{s,∞,q}(z + □_k; a, a₀) ≤ 3^{s(m-k)} 𝓔_{s,∞,q}(□_m; a, a₀), avg_{z ∈ 3^k ℤ^d ∩ □_m} 𝓔_{s,p,q}(z + □_k; a, a₀) ≤ 3^{s(m-k)} 𝓔_{s,p,q}(□_m; a, a₀),

with the ambient quantifiers of the source, i.e. m ∈ ℤ, p, q ∈ [1,∞] and s ∈ (0,∞).

Scope

The per-descendant form of the first line of the display is proved here at p = ∞ for every finite q ∈ [1,∞); CoarseGraining previously had only the case q = 1 (Homogenization.Book.Ch02.homogenizationErrorOnCube_infinity_one_descendantsAtScale_le).

Main results

• scaleResponse_depth_descendant_le: the p = ∞ one-scale responses of a cube and of one of its descendants compare, after the depth shift.
• homogenizationErrorOnCube_infinity_finite_le_of_mem_descendantsAtScale: the per-descendant form of the display at p = ∞ and finite q.

References

• ABK26, e.bound.one.cube.by.mathcalE.

Comparing the scale responses of a cube and of a descendant

theorem Algsuperdiff.Section3.Provider.ErrorComparison.scaleResponse_depth_descendant_le {d : ℕ} {Q R : HCPolySupport.TriadicCube d} {k : ℤ} (F : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (a0 : HCPolySupport.Mat d) (hR : R ∈ HCPolySupport.descendantsAtScale Q k) (l : ℕ) : HCPolySupport.Book.Ch02.scaleResponseAtScale R (R.scale - ↑l) HCPolySupport.Book.Ch02.MultiscaleExponent.infinity F a0 ≤ HCPolySupport.Book.Ch02.scaleResponseAtScale Q (Q.scale - ↑(l + (Q.scale - k).toNat)) HCPolySupport.Book.Ch02.MultiscaleExponent.infinity F a0

Descending l scales below a descendant R of Q at scale k proves on the scale Q.scale - (l + (Q.scale - k)), so the p = ∞ one-scale responses compare.

The finite-q endpoint p = ∞

theorem Algsuperdiff.Section3.Provider.ErrorComparison.homogenizationErrorOnCube_infinity_finite_le_of_mem_descendantsAtScale {d : ℕ} [NeZero d] {Q R : HCPolySupport.TriadicCube d} {k : ℤ} (F : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (a0 : HCPolySupport.Mat d) {s q : ℝ} (hs : 0 < s) (hq : 1 ≤ q) (hR : R ∈ HCPolySupport.descendantsAtScale Q k) : HCPolySupport.Book.Ch02.HomogenizationErrorOnCube R s HCPolySupport.Book.Ch02.MultiscaleExponent.infinity (HCPolySupport.Book.Ch02.MultiscaleExponent.finite q) F a0 ≤ Real.rpow 3 (s * ↑(Q.scale - k).toNat) * HCPolySupport.Book.Ch02.HomogenizationErrorOnCube Q s HCPolySupport.Book.Ch02.MultiscaleExponent.infinity (HCPolySupport.Book.Ch02.MultiscaleExponent.finite q) F a0

Per-descendant form of e.bound.one.cube.by.mathcalE (ABK26) at p = ∞ and finite q.