InteriorGlueFrame

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

The off-grid error is a cube error in the translated frame

It is not new: CoarseGraining already proves it, unconditionally, sorry-free, with oleans built — Homogenization/CoarseGraining/Translation.lean carries the full covariance of the coarse-graining apparatus under a real translation:

  ResponseJ (w + U) p q a = ResponseJ U p q (a(· + w))        (:372)
  BlockJ    (w + U) P Q a = BlockJ    U P Q (a(· + w))        (:303)
  Mu        (w + U) P   a = Mu        U P   (a(· + w))        (:116)
  σ⋆, σ⋆⁻¹, κ, σ, b coarse: the same, at :378--:439 .

  𝓔_{t,∞,2}(w + P; g, a₀) = 𝓔_{t,∞,2}(P; g(·+w), a₀) .

What this unblocks (and what it does not)

With this bridge, the child-frame composition can feed InteriorGlueCap's cap at the root, provided the child-frame family is built from the parent's flux-corrected field rather than the child's own (the child-frame family uses the child's own antisymmetric increment, which is a different — equally valid — shift of the same equation). That re-basing, the analogous transport of the coarse-grained ellipticity factors λ_{r,q}, Λ_{r,q}, and the energy-average transport are the remaining assembly steps; none of them is assumed here.

References

• CoarseGraining, Homogenization/CoarseGraining/Translation.lean.

1. The adjoint commutes with the translation

theorem Algsuperdiff.Section4.Provider.ExcessDecay.adjointCoeffField_translateCoeffField {d : ℕ} (w : HCPolySupport.Vec d) (g : HCPolySupport.CoeffField d) : HCPolySupport.adjointCoeffField (HCPolySupport.translateCoeffField w g) = HCPolySupport.translateCoeffField w (HCPolySupport.adjointCoeffField g)

Transposition and translation of a coefficient field commute.

2. The set-level doubled response is translation covariant

theorem Algsuperdiff.Section4.Provider.ExcessDecay.setDoubledResponseJ_translateSet {d : ℕ} (w : HCPolySupport.Vec d) (V : Set (HCPolySupport.Vec d)) (g : HCPolySupport.CoeffField d) (P Q : HCPolySupport.BlockVec d) : setDoubledResponseJ (HCPolySupport.translateSet w V) g P Q = setDoubledResponseJ V (HCPolySupport.translateCoeffField w g) P Q

The doubled response of a translated set. Both halves move by CoarseGraining's ResponseJ_translateSet_eq_translateCoeffField; the adjoint half needs the commutation of §1.

3. The one-cube quantity

theorem Algsuperdiff.Section4.Provider.ExcessDecay.offGridBlockResponseValueSet_eq_translate {d : ℕ} (w : HCPolySupport.Vec d) (R : HCPolySupport.TriadicCube d) (A : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (g : HCPolySupport.CoeffField d) (hg : (A.coeffOn R).toCoeffField = HCPolySupport.translateCoeffField w g) (a0 : HCPolySupport.Mat d) : offGridBlockResponseValueSet w R g a0 = HCPolySupport.Book.Ch02.normalizedBlockResponseValueSet R A a0

The off-grid one-cube maximum is CoarseGraining's, in the translated frame.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.offGridBlockResponseMax_eq_translate {d : ℕ} (w : HCPolySupport.Vec d) (R : HCPolySupport.TriadicCube d) (A : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (g : HCPolySupport.CoeffField d) (hg : (A.coeffOn R).toCoeffField = HCPolySupport.translateCoeffField w g) (a0 : HCPolySupport.Mat d) : offGridBlockResponseMax w R g a0 = HCPolySupport.Book.Ch02.normalizedBlockResponseMax R A a0

4. The shells and the multiscale error

theorem Algsuperdiff.Section4.Provider.ExcessDecay.offGridShellMax_eq_translate {d : ℕ} (w : HCPolySupport.Vec d) (P : HCPolySupport.TriadicCube d) (k : ℤ) (A : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (g : HCPolySupport.CoeffField d) (hg : ∀ (Q : HCPolySupport.TriadicCube d), (A.coeffOn Q).toCoeffField = HCPolySupport.translateCoeffField w g) (a0 : HCPolySupport.Mat d) : offGridShellMax w P k g a0 = HCPolySupport.Book.Ch02.maxDescendantNormalizedBlockResponseAtScale P k A a0

theorem Algsuperdiff.Section4.Provider.ExcessDecay.offGridErrorFunctional_eq_homogenizationErrorOnCube_translate {d : ℕ} (w : HCPolySupport.Vec d) (P : HCPolySupport.TriadicCube d) {t : ℝ} (ht : 0 < t) (A : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (g : HCPolySupport.CoeffField d) (hg : ∀ (Q : HCPolySupport.TriadicCube d), (A.coeffOn Q).toCoeffField = HCPolySupport.translateCoeffField w g) (a0 : HCPolySupport.Mat d) : offGridErrorFunctional w P t g a0 = HCPolySupport.Book.Ch02.HomogenizationErrorOnCube P t HCPolySupport.Book.Ch02.MultiscaleExponent.infinity (HCPolySupport.Book.Ch02.MultiscaleExponent.finite 2) A a0

The frame bridge.

The multiscale error of the off-grid cube w + P, taken with the ambient field g, equals CoarseGraining's cube error of P taken with the translated field g(· + w).