OffGridComposeCover

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

The doubled response across the off-grid covering

OffGridStabilitySubadditivity.lean proved countable subadditivity for CoarseGraining's scalar Homogenization.ResponseJ across the maximal grid cubes of an arbitrary real translate w + □_k. The printed transport e.mathcalE.stability.applied (ABK26) needs it for the doubled response 𝐉, and after that for the unit-sphere maximum max_{|e|=1} 𝐉.

Two points make the recombination lossless:

• the majorant of each scalar leg is taken to be that leg's own value on the subcube, so nothing is thrown away before the two legs are added; the required summability of each leg is obtained by comparison, using 0 ≤ J ≤ 2·𝐉 (both summands of the splitting are nonnegative);
• the summed per-cube value is then, by the bridge setDoubledResponseJ_openCubeSet, exactly 𝐉(Q), which is at most max_{|e|=1} 𝐉(Q) — so the constant 1, not 2, is what the composition inherits.

The unit-sphere maximum is then csSup_le against the e-independent right-hand side; the boundedness needed to compare a single e with the maximum is CoarseGraining's descendant-indexed Ch02.normalizedBlockResponseValueSet_bddAbove_of_mem_descendantsAtScale, applied at the enclosing grid cube K — the maximal cubes of w + □_k are forced to be triadic descendants of K by the composition's mem_descendantsAtScale_of_cubeSet_subset, so no off-grid analogue of the boundedness lemma is needed.

Main results

• setDoubledResponseJ_le_tsum_maximalCubes — the doubled response of the off-grid cube across its maximal grid subcubes.
• offGridBlockResponseMax_le_tsum_maximalCubes — the same for the unit-sphere maximum.

References

• ABK26, l.lambdas.stability, (the subadditivity display).
• ABK26, e.mathcalE.stability.applied.
• CoarseGraining, Homogenization/Book/Ch02/Theorems/DeterministicIdentities.lean, Homogenization/Book/Ch02/Theorems/HomogenizationError/ResponseBounds.lean.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.mem_descendantsAtScale_of_maximalCubeIn {d : ℕ} [NeZero d] {w : HCPolySupport.Vec d} {R K Q : HCPolySupport.TriadicCube d} (hKsub : offGridCube w R ⊆ HCPolySupport.cubeSet K) (hRK : R.scale ≤ K.scale) (hQ : MaximalCubeIn (offGridCube w R) Q) : Q ∈ HCPolySupport.descendantsAtScale K Q.scale

Every maximal grid cube of an off-grid cube contained in a grid cube K is a triadic descendant of K. Recognition only; the analytic content is nil.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.setDoubledResponseJ_openCubeSet_le_normalizedBlockResponseMax {d : ℕ} [NeZero d] {w : HCPolySupport.Vec d} {R K Q : HCPolySupport.TriadicCube d} {g : HCPolySupport.CoeffField d} (A : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (a0 : HCPolySupport.Mat d) (hg : ∀ (S : HCPolySupport.TriadicCube d), (A.coeffOn S).toCoeffField = g) (hKsub : offGridCube w R ⊆ HCPolySupport.cubeSet K) (hRK : R.scale ≤ K.scale) (hQ : MaximalCubeIn (offGridCube w R) Q) (e : HCPolySupport.FullBlockVec d) (he : HCPolySupport.Book.Ch02.fullBlockVecNormSq e = 1) : setDoubledResponseJ (HCPolySupport.openCubeSet Q) g (HCPolySupport.ofFullBlockVec (Matrix.mulVec (HCPolySupport.Book.Ch02.constantFullBlockMatrixInvSqrt a0) e)) (HCPolySupport.ofFullBlockVec (Matrix.mulVec (HCPolySupport.Book.Ch02.constantFullBlockMatrixSqrt a0) e)) ≤ HCPolySupport.Book.Ch02.normalizedBlockResponseMax Q A a0

On a maximal grid subcube, the normalized doubled response of a single unit vector is at most the cube's unit-sphere maximum.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.setDoubledResponseJ_le_tsum_maximalCubes {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) (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) (B : HCPolySupport.TriadicCube d → ℝ) (hB : ∀ (Q : HCPolySupport.TriadicCube d), MaximalCubeIn (offGridCube w R) Q → HCPolySupport.Book.Ch02.normalizedBlockResponseMax Q A a0 ≤ B Q) (hsummable : Summable fun (Q : ↑(maximalCubes (offGridCube w R))) => HCPolySupport.cubeVolume ↑Q * B ↑Q) (e : HCPolySupport.FullBlockVec d) (he : HCPolySupport.Book.Ch02.fullBlockVecNormSq e = 1) : setDoubledResponseJ (offGridCube w R) g (HCPolySupport.ofFullBlockVec (Matrix.mulVec (HCPolySupport.Book.Ch02.constantFullBlockMatrixInvSqrt a0) e)) (HCPolySupport.ofFullBlockVec (Matrix.mulVec (HCPolySupport.Book.Ch02.constantFullBlockMatrixSqrt a0) e)) ≤ (HCPolySupport.cubeVolume R)⁻¹ * ∑' (Q : ↑(maximalCubes (offGridCube w R))), HCPolySupport.cubeVolume ↑Q * B ↑Q

The doubled response across the covering.

For an arbitrary real translate w + R contained in the grid cube K, the A₀-normalized doubled response of w + R at a unit vector e is at most the |Q|/|w + R|-weighted sum of any majorant of the unit-sphere maxima of the maximal grid subcubes. Proved by two applications of the countable subadditivity's scalar subadditivity and CoarseGraining's splitting identity; no new variational analysis.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.offGridBlockResponseMax_le_tsum_maximalCubes {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) (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) (B : HCPolySupport.TriadicCube d → ℝ) (hB : ∀ (Q : HCPolySupport.TriadicCube d), MaximalCubeIn (offGridCube w R) Q → HCPolySupport.Book.Ch02.normalizedBlockResponseMax Q A a0 ≤ B Q) (hsummable : Summable fun (Q : ↑(maximalCubes (offGridCube w R))) => HCPolySupport.cubeVolume ↑Q * B ↑Q) : offGridBlockResponseMax w R g a0 ≤ (HCPolySupport.cubeVolume R)⁻¹ * ∑' (Q : ↑(maximalCubes (offGridCube w R))), HCPolySupport.cubeVolume ↑Q * B ↑Q

The unit-sphere maximum across the covering.

The e-free right-hand side of setDoubledResponseJ_le_tsum_maximalCubes bounds the whole unit-sphere maximum, by csSup_le.