OffGridErrorCarrier

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

The multiscale error carrier of an off-grid cube

The OffGridStability*.lean modules deliver the geometry, the countable subadditivity and the arithmetic of the printed transport e.mathcalE.stability.applied (ABK26). The composition they feed cannot even be stated with CoarseGraining's carriers: 𝓔_{t,∞,2} is HomogenizationErrorOnCube, whose shells descendantsAtScale are lattice cubes, so there is no CoarseGraining object for 𝓔_{t,∞,2}(x + □_n) at a real translate x. This module supplies that object.

The design: a set-level doubled response, so no off-grid Domain is needed

CoarseGraining's Ch02.doubledResponseJ is indexed by a Ch02.Domain together with a Ch02.CoeffOn on it, neither of which a real translate of a triadic cube carries. Instead of transporting those structures, this module takes CoarseGraining's own scalar splitting

𝐉(U, (p,q), (q*,p*); a)
  = ½ J(U, p − p*, q* − q; a) + ½ J(U, p* + p, q* + q; aᵗ)

(Ch02.doubledResponseJ_eq_half_responseJ_adjoint_sum) as the definition of the doubled response on an arbitrary measurable set, in terms of CoarseGraining's set-level Homogenization.ResponseJ, which needs no domain structure at all. The bridge setDoubledResponseJ_openCubeSet proves that on a grid cube this definition agrees with CoarseGraining's Ch02.doubledResponseJ on the nose, whenever the triadic family's cube representative is the ambient field (which is how every CoarseGraining consumer builds it: Ch04.triadicCoeffFamilyOfAELocallyUniformlyEllipticField makes it rfl). Consequently

• offGridBlockResponseMax 0 R g a0 = Ch02.normalizedBlockResponseMax a0,
• offGridErrorFunctional 0 P t g a0 = 𝓔_{t,∞,2}(P; A, a0),

so the off-grid carrier is a conservative extension of CoarseGraining's, not a parallel invention: at zero translate it is CoarseGraining's quantity.

The carrier-compatibility binder hg (disclosed)

Several statements below carry hg : (A.coeffOn R).toCoeffField = g (or its ∀ Q form). This is typing/carrier data, not a mathematical hypothesis of any printed statement: it says the abstract Ch02.TriadicCoeffFamily and the ambient CoeffField are the same object, which holds by rfl for every family CoarseGraining constructs from an ambient field. It is never used as a source premise and never appears in a statement that claims a printed display.

Main results

• setDoubledResponseJ, setDoubledResponseJ_openCubeSet — the set-level doubled response and its agreement with CoarseGraining's on a grid cube.
• offGridBlockResponseMax, offGridShellMax, offGridErrorFunctional — the off-grid carrier, shell by shell.
• offGridBlockResponseMax_zero_eq, offGridErrorFunctional_zero_eq — the conservative-extension theorems.

References

• ABK26, e.mathcalE.stability.applied.
• ABK26, l.lambdas.stability; d.mathcal.E.
• CoarseGraining, Homogenization/Book/Ch02/Theorems/DeterministicIdentities.lean (doubledResponseJ_eq_half_responseJ_adjoint_sum), Homogenization/Internal/Ch02/Adapters.lean (book_responseJ_eq_ResponseJ), Homogenization/Book/Ch02/HomogenizationError.lean (the shell carriers).

1. The adjoint of an elliptic field

theorem Algsuperdiff.Section4.Provider.ExcessDecay.isEllipticFieldOn_adjointCoeffField {d : ℕ} {lam Lam : ℝ} {V : Set (HCPolySupport.Vec d)} {g : HCPolySupport.CoeffField d} (hEll : HCPolySupport.IsEllipticFieldOn lam Lam V g) : HCPolySupport.IsEllipticFieldOn lam Lam V (HCPolySupport.adjointCoeffField g)

The adjoint field aᵗ is elliptic on the same set with the same constants. CoarseGraining proves the matrix statement (isEllipticMatrix_transpose); only the measurability clause has to be transposed.

2. The set-level doubled response

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.setDoubledResponseJ {d : ℕ} (V : Set (HCPolySupport.Vec d)) (g : HCPolySupport.CoeffField d) (P Q : HCPolySupport.BlockVec d) : ℝ

The doubled response functional on an arbitrary set.

This is the right-hand side of CoarseGraining's scalar splitting Ch02.doubledResponseJ_eq_half_responseJ_adjoint_sum, written with the set-level Homogenization.ResponseJ, which requires no Ch02.Domain structure. On a grid cube it agrees with Ch02.doubledResponseJ (setDoubledResponseJ_openCubeSet).

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.setDoubledResponseJ_nonneg {d : ℕ} (V : Set (HCPolySupport.Vec d)) (g : HCPolySupport.CoeffField d) (P Q : HCPolySupport.BlockVec d) : 0 ≤ setDoubledResponseJ V g P Q

theorem Algsuperdiff.Section4.Provider.ExcessDecay.responseJ_le_two_mul_setDoubledResponseJ_left {d : ℕ} (V : Set (HCPolySupport.Vec d)) (g : HCPolySupport.CoeffField d) (P Q : HCPolySupport.BlockVec d) : HCPolySupport.ResponseJ V (P.1 - Q.2) (Q.1 - P.2) g ≤ 2 * setDoubledResponseJ V g P Q

Each scalar half of the doubled response is at most twice the whole: the two summands are nonnegative.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.responseJ_le_two_mul_setDoubledResponseJ_right {d : ℕ} (V : Set (HCPolySupport.Vec d)) (g : HCPolySupport.CoeffField d) (P Q : HCPolySupport.BlockVec d) : HCPolySupport.ResponseJ V (Q.2 + P.1) (Q.1 + P.2) (HCPolySupport.adjointCoeffField g) ≤ 2 * setDoubledResponseJ V g P Q

theorem Algsuperdiff.Section4.Provider.ExcessDecay.setDoubledResponseJ_openCubeSet {d : ℕ} (R : HCPolySupport.TriadicCube d) (A : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (g : HCPolySupport.CoeffField d) (hg : (A.coeffOn R).toCoeffField = g) (P Q : HCPolySupport.BlockVec d) : setDoubledResponseJ (HCPolySupport.openCubeSet R) g P Q = HCPolySupport.Book.Ch02.doubledResponseJ (HCPolySupport.Book.Ch02.cubeDomain R) (A.coeffOn R) P Q

The bridge. On the open realization of a grid cube the set-level doubled response is CoarseGraining's Ch02.doubledResponseJ, provided the triadic family's representative on that cube is the ambient field.

3. The off-grid unit-sphere maximum

def Algsuperdiff.Section4.Provider.ExcessDecay.offGridBlockResponseValueSet {d : ℕ} (w : HCPolySupport.Vec d) (R : HCPolySupport.TriadicCube d) (g : HCPolySupport.CoeffField d) (a0 : HCPolySupport.Mat d) : Set ℝ

The value set whose supremum is the off-grid normalized block response maximum: the A₀-normalized doubled response of the off-grid cube w + R over the unit sphere of ℝ^{2d}. Compare Ch02.normalizedBlockResponseValueSet.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.offGridBlockResponseMax {d : ℕ} (w : HCPolySupport.Vec d) (R : HCPolySupport.TriadicCube d) (g : HCPolySupport.CoeffField d) (a0 : HCPolySupport.Mat d) : ℝ

The one-cube quantity at a real translate. max_{|e|=1} 𝐉(w + R, …).

Equations

• Algsuperdiff.Section4.Provider.ExcessDecay.offGridBlockResponseMax w R g a0 = sSup (Algsuperdiff.Section4.Provider.ExcessDecay.offGridBlockResponseValueSet w R g a0)

theorem Algsuperdiff.Section4.Provider.ExcessDecay.offGridBlockResponseValueSet_nonempty {d : ℕ} [NeZero d] (w : HCPolySupport.Vec d) (R : HCPolySupport.TriadicCube d) (g : HCPolySupport.CoeffField d) (a0 : HCPolySupport.Mat d) : (offGridBlockResponseValueSet w R g a0).Nonempty

theorem Algsuperdiff.Section4.Provider.ExcessDecay.offGridBlockResponseMax_nonneg {d : ℕ} (w : HCPolySupport.Vec d) (R : HCPolySupport.TriadicCube d) (g : HCPolySupport.CoeffField d) (a0 : HCPolySupport.Mat d) : 0 ≤ offGridBlockResponseMax w R g a0

theorem Algsuperdiff.Section4.Provider.ExcessDecay.offGridBlockResponseMax_le {d : ℕ} [NeZero d] {w : HCPolySupport.Vec d} {R : HCPolySupport.TriadicCube d} {g : HCPolySupport.CoeffField d} {a0 : HCPolySupport.Mat d} {C : ℝ} (h : ∀ (e : HCPolySupport.FullBlockVec d), 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)) ≤ C) : offGridBlockResponseMax w R g a0 ≤ C

The unit-sphere maximum is bounded by any uniform bound on its values. This is the csSup_le interface the covering step consumes.

4. Conservative extension: the zero translate is CoarseGraining's quantity

@[simp]

theorem Algsuperdiff.Section4.Provider.ExcessDecay.offGridCube_zero {d : ℕ} (P : HCPolySupport.TriadicCube d) : offGridCube 0 P = HCPolySupport.openCubeSet P

5. The shells and the off-grid error functional

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.offGridShellMax {d : ℕ} (w : HCPolySupport.Vec d) (P : HCPolySupport.TriadicCube d) (k : ℤ) (g : HCPolySupport.CoeffField d) (a0 : HCPolySupport.Mat d) : ℝ

The shell maximum of an off-grid cube. The w-translated lattice: the grid descendants R of the shape cube P at scale k, each read on the translated cube w + R. At w = 0 this is Ch02.maxDescendantNormalizedBlockResponseAtScale.

Equations

• One or more equations did not get rendered due to their size.

theorem Algsuperdiff.Section4.Provider.ExcessDecay.offGridShellMax_nonneg {d : ℕ} (w : HCPolySupport.Vec d) (P : HCPolySupport.TriadicCube d) (k : ℤ) (g : HCPolySupport.CoeffField d) (a0 : HCPolySupport.Mat d) : 0 ≤ offGridShellMax w P k g a0

theorem Algsuperdiff.Section4.Provider.ExcessDecay.offGridShellMax_le {d : ℕ} {w : HCPolySupport.Vec d} {P : HCPolySupport.TriadicCube d} {k : ℤ} {g : HCPolySupport.CoeffField d} {a0 : HCPolySupport.Mat d} {C : ℝ} (hk : k ≤ P.scale) (h : ∀ R ∈ HCPolySupport.descendantsAtScale P k, offGridBlockResponseMax w R g a0 ≤ C) : offGridShellMax w P k g a0 ≤ C

The shell maximum is bounded by any uniform bound on its cubes.

noncomputable def Algsuperdiff.Section4.Provider.ExcessDecay.offGridErrorFunctional {d : ℕ} (w : HCPolySupport.Vec d) (P : HCPolySupport.TriadicCube d) (t : ℝ) (g : HCPolySupport.CoeffField d) (a0 : HCPolySupport.Mat d) : ℝ

The multiscale error of an off-grid cube, 𝓔_{t,∞,2}(w + P; g, a₀).

The shell series of d.mathcal.E with CoarseGraining's own geometric weights, over the w-translated lattice. At w = 0 it is Ch02.HomogenizationErrorOnCube P t .infinity (.finite 2) (offGridErrorFunctional_zero_eq).

Equations

• One or more equations did not get rendered due to their size.