OffGridComposeAssembly

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

The composed off-grid stability estimate

This is the composition the printed transport e.mathcalE.stability.applied (ABK26) performs, at an arbitrary real translate:

𝓔_{t,∞,2}(w + □_k; a, ā)  ≤  C(d,t,u)^{1/2} · 3^{u·(K − k)} · 𝓔_{u,∞,2}(□_K; a, ā)

The constant is offGridStabilityConst d t u = 36dt/((t−u)(1−2u)), which at the printed slot (t,u) = (s/6, s/8) is at most 192 d for s ∈ (0,1] — a pure C(d), with no s-power deviation from the printed constant (offGridStabilityConst_slot_le). The pieces:

step	file	output
per-cube cap	OffGridStabilityCap	3^{2u(K − scale Q)}·𝓔_u²
covering	OffGridComposeCover	doubled response across the maximal cubes
packing + depth sum	OffGridComposeDepth	12d/(1−2u)
outer shell sum	OffGridStabilityArith	3t/(t−u)
product	here	36dt/((t−u)(1−2u))

Both depths of the printed display (K − k = 1 and K − k = 2) are covered: the statements quantify over an arbitrary containing grid cube.

Main results

• offGridBlockResponseMax_le_cap — the one-cube off-grid bound.
• offGridShellMax_le_cap — the shell bound, in the A·3^{2ul} shape.
• offGridErrorFunctional_le — the composed off-grid stability estimate.
• offGridErrorFunctional_le_slot — the same at the printed slot (t,u) = (s/6, s/8), with the printed constant 192 d.

References

• ABK26, e.mathcalE.stability.applied.
• ABK26, l.lambdas.stability.
• ABK26, e.bound.one.cube.by.lambdas.

1. The one-cube off-grid bound

theorem Algsuperdiff.Section4.Provider.ExcessDecay.offGridBlockResponseMax_le_cap {d : ℕ} [NeZero d] {w : HCPolySupport.Vec d} {R K : HCPolySupport.TriadicCube d} {g : HCPolySupport.CoeffField d} {lam Lam : ℝ} (A : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (a0 : HCPolySupport.Mat d) {u : ℝ} (hu0 : 0 < u) (hu : u < 1 / 2) (hg : ∀ (S : HCPolySupport.TriadicCube d), (A.coeffOn S).toCoeffField = g) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam (offGridCube w R) g) (hKsub : offGridCube w R ⊆ HCPolySupport.cubeSet K) (hRK : R.scale ≤ K.scale) : offGridBlockResponseMax w R g a0 ≤ 12 * ↑d / (1 - 2 * u) * (3 ^ (2 * u * ↑(K.scale - R.scale).toNat) * HCPolySupport.Book.Ch02.HomogenizationErrorOnCube K u HCPolySupport.Book.Ch02.MultiscaleExponent.infinity (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) A a0 ^ 2)

The off-grid one-cube estimate.

For an arbitrary real translate w + R contained in the grid cube K,

max_{|e|=1} 𝐉(w + R, …)  ≤  (12d/(1−2u))·3^{2u(K.scale − R.scale)}·𝓔_{u,∞,2}(K)² .

The covering, the per-cube cap (OffGridStabilityCap) and the packing/depth sum composed; the majorant and summability interfaces of the countable subadditivity are discharged here.

2. The shell bound

theorem Algsuperdiff.Section4.Provider.ExcessDecay.offGridShellMax_le_cap {d : ℕ} [NeZero d] {w : HCPolySupport.Vec d} {P K : HCPolySupport.TriadicCube d} {g : HCPolySupport.CoeffField d} {lam Lam : ℝ} (A : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (a0 : HCPolySupport.Mat d) {u : ℝ} (hu0 : 0 < u) (hu : u < 1 / 2) (hg : ∀ (S : HCPolySupport.TriadicCube d), (A.coeffOn S).toCoeffField = g) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam (HCPolySupport.translateSet w (HCPolySupport.cubeSet P)) g) (hcontain : HCPolySupport.translateSet w (HCPolySupport.cubeSet P) ⊆ HCPolySupport.cubeSet K) (l : ℕ) : offGridShellMax w P (P.scale - ↑l) g a0 ≤ 12 * ↑d / (1 - 2 * u) * (3 ^ (2 * u * ↑(K.scale - P.scale).toNat) * HCPolySupport.Book.Ch02.HomogenizationErrorOnCube K u HCPolySupport.Book.Ch02.MultiscaleExponent.infinity (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) A a0 ^ 2) * 3 ^ (2 * u * ↑l)

The shell bound of the off-grid cube, in the M l ≤ A·3^{2ul} shape the outer geometric sum of the exponent bookkeeping consumes.

3. The composed estimate

theorem Algsuperdiff.Section4.Provider.ExcessDecay.offGridErrorFunctional_le {d : ℕ} [NeZero d] {w : HCPolySupport.Vec d} {P K : HCPolySupport.TriadicCube d} {g : HCPolySupport.CoeffField d} {lam Lam : ℝ} (A : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (a0 : HCPolySupport.Mat d) {t u : ℝ} (hu0 : 0 < u) (hut : u < t) (ht : t ≤ 1 / 2) (hg : ∀ (S : HCPolySupport.TriadicCube d), (A.coeffOn S).toCoeffField = g) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam (HCPolySupport.translateSet w (HCPolySupport.cubeSet P)) g) (hcontain : HCPolySupport.translateSet w (HCPolySupport.cubeSet P) ⊆ HCPolySupport.cubeSet K) : offGridErrorFunctional w P t g a0 ≤ √(offGridStabilityConst d t u) * (3 ^ (u * ↑(K.scale - P.scale).toNat) * HCPolySupport.Book.Ch02.HomogenizationErrorOnCube K u HCPolySupport.Book.Ch02.MultiscaleExponent.infinity (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) A a0)

The composed off-grid stability estimate — the tex's e.mathcalE.stability.applied shape at an arbitrary real translate w:

𝓔_{t,∞,2}(w + □_k; a, ā)
    ≤ (36dt/((t−u)(1−2u)))^{1/2} · 3^{u·(K − k)} · 𝓔_{u,∞,2}(□_K; a, ā) ,

valid whenever w + □_k ⊆ □_K and 0 < u < t ≤ 1/2, with the same coefficient family and the same comparator on both sides. Both printed depths (K − k = 1, 2) are instances.