TransposeError

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

Transpose invariance of the (2,2) homogenization error at an isotropic comparator

ABK26, Section 4.1: the manuscript runs the ugly estimate e.ugly.estimate.for.J a second time "for the transposed field", and asserts that the transposed estimate holds with the same right-hand side.

This module supplies the deterministic half of that argument at the 𝓔_{s,2,2} slot: the error functional is pointwise unchanged when the coefficient family is replaced by its adjoint, so nothing has to be paid for the transposed leg's error atom.

The mechanism

𝓔 is built from normalizedBlockResponseMax R a a0, the supremum of the doubled response bfJ(R, P, Q; a) over the normalized 2d-sphere. CoarseGraining's unconditional splitting identity doubledResponseJ_eq_half_responseJ_adjoint_sum

bfJ(U, (p,q), (q*,p*); a) = ½ J(U, p−p*, q*−q; a) + ½ J(U, p*+p, q*+q; aᵀ)

read at aᵀ (and back at aᵀᵀ ≈ a) says exactly that transposing the field is the same as flipping the sign of the flux half of both block loads:

bfJ(U, P, Q; aᵀ) = bfJ(U, ΦP, ΦQ; a) ,      Φ(p,q) = (p, −q) .

At an isotropic background a0 = σ Id the constant block matrix is diag(σ Id, σ⁻¹ Id), which commutes with Φ; and Φ preserves the normalization ⟨P, bfA₀ P⟩. So Φ permutes the admissible probes and the two suprema coincide. No matrix square root is ever computed: the whole argument runs through CoarseGraining's representation-free admission gate normalizedBlockResponseValueSet_mem_of_constantBlockQuadratic_eq_one.

Composing with the proved (J3) carrier identity Cutoff.coefficientCutoff_negateCutoffSample_eq_adjoint (a_m(−ω) = a_m(ω)ᵀ, read at the family level by Localization.coefficientCutoffTriadicCoeffFamily_negateCutoffSample_aeEq) turns this into the sample-level statement that the 𝒢₂ atom 𝓔_{s,2,2}(□_n; a_{n−2}, σ_{n−2}) is invariant under whole-sequence negation.

What is proved

• doubledResponseJ_transpose — the flip identity for the doubled response.
• normalizedBlockResponseMax_adjointFamily — the one-cube invariance.
• scaleResponseAtScale_adjointFamily, homogenizationError_adjointFamily, homogenizationErrorOnCube_adjointFamily — the invariance of the whole 𝓔 chain, for every pair of exponents.
• annularErrorAtom_negateCutoffSample, annularErrorAtomMax_negateCutoffSample — the sample-level invariance of the 𝒢₂ atom and of the annulus maximum.

References

• ABK26, (the transposed ugly estimate); (𝒢₂).

Part A -- the flux sign flip on doubled block vectors

def Algsuperdiff.Section4.Provider.Annular.blockFlip {d : ℕ} (X : HCPolySupport.BlockVec d) : HCPolySupport.BlockVec d

The flux sign flip Φ(p,q) = (p, −q) on doubled block vectors.

Equations

• Algsuperdiff.Section4.Provider.Annular.blockFlip X = (X.1, -X.2)

@[simp]

theorem Algsuperdiff.Section4.Provider.Annular.blockFlip_blockFlip {d : ℕ} (X : HCPolySupport.BlockVec d) : blockFlip (blockFlip X) = X

theorem Algsuperdiff.Section4.Provider.Annular.doubledResponseJ_transpose {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) (P Q' : HCPolySupport.BlockVec d) : HCPolySupport.Book.Ch02.doubledResponseJ U a.transpose P Q' = HCPolySupport.Book.Ch02.doubledResponseJ U a (blockFlip P) (blockFlip Q')

Transposing the field is flipping the flux half of both block loads.

Read off CoarseGraining's unconditional splitting identity doubledResponseJ_eq_half_responseJ_adjoint_sum at aᵀ and at a, together with responseJ U aᵀᵀ = responseJ U a.

Part B -- the flip is a symmetry of the isotropic normalization

theorem Algsuperdiff.Section4.Provider.Annular.blockProbe_normalization {d : ℕ} {a0 : HCPolySupport.Mat d} {lam Lam : ℝ} (ha0 : HCPolySupport.IsEllipticMatrix lam Lam a0) {e : HCPolySupport.FullBlockVec d} (he : HCPolySupport.Book.Ch02.fullBlockVecNormSq e = 1) : HCPolySupport.ofFullBlockVec (Matrix.mulVec (HCPolySupport.Book.Ch02.constantFullBlockMatrixSqrt a0) e) = HCPolySupport.blockMatVecMul (HCPolySupport.Book.Ch02.constantBlockMatrix a0) (HCPolySupport.ofFullBlockVec (Matrix.mulVec (HCPolySupport.Book.Ch02.constantFullBlockMatrixInvSqrt a0) e)) ∧ HCPolySupport.blockVecDot (HCPolySupport.ofFullBlockVec (Matrix.mulVec (HCPolySupport.Book.Ch02.constantFullBlockMatrixInvSqrt a0) e)) (HCPolySupport.blockMatVecMul (HCPolySupport.Book.Ch02.constantBlockMatrix a0) (HCPolySupport.ofFullBlockVec (Matrix.mulVec (HCPolySupport.Book.Ch02.constantFullBlockMatrixInvSqrt a0) e))) = 1

The structure of a normalized block probe. Its co-load is the image under the constant block matrix, and its quadratic normalization is 1; the matrix square root never has to be computed.

This interface uses the common block-probe normalization from BlockResponse.

theorem Algsuperdiff.Section4.Provider.Annular.blockFlip_blockMatVecMul_scalarMatrix {d : ℕ} {σ0 : ℝ} (hσ0 : 0 < σ0) (P : HCPolySupport.BlockVec d) : blockFlip (HCPolySupport.blockMatVecMul (HCPolySupport.Book.Ch02.constantBlockMatrix (HCPolySupport.scalarMatrix σ0)) P) = HCPolySupport.blockMatVecMul (HCPolySupport.Book.Ch02.constantBlockMatrix (HCPolySupport.scalarMatrix σ0)) (blockFlip P)

At an isotropic background the constant block matrix diag(σ Id, σ⁻¹ Id) commutes with the flux sign flip.

theorem Algsuperdiff.Section4.Provider.Annular.blockVecDot_blockFlip_scalarMatrix {d : ℕ} {σ0 : ℝ} (hσ0 : 0 < σ0) (P : HCPolySupport.BlockVec d) : HCPolySupport.blockVecDot (blockFlip P) (HCPolySupport.blockMatVecMul (HCPolySupport.Book.Ch02.constantBlockMatrix (HCPolySupport.scalarMatrix σ0)) (blockFlip P)) = HCPolySupport.blockVecDot P (HCPolySupport.blockMatVecMul (HCPolySupport.Book.Ch02.constantBlockMatrix (HCPolySupport.scalarMatrix σ0)) P)

The flip preserves the isotropic block normalization.

Part C -- the one-cube block maximum is transpose invariant

theorem Algsuperdiff.Section4.Provider.Annular.normalizedBlockResponseMax_adjointFamily {d : ℕ} (F : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (R : HCPolySupport.TriadicCube d) {σ0 : ℝ} (hσ0 : 0 < σ0) : HCPolySupport.Book.Ch02.normalizedBlockResponseMax R (Section3.Provider.CoarseEllipticity.adjointFamily F) (HCPolySupport.scalarMatrix σ0) = HCPolySupport.Book.Ch02.normalizedBlockResponseMax R F (HCPolySupport.scalarMatrix σ0)

The normalized block-response maximum is transpose invariant at an isotropic comparator. This is the inner quantity of d.mathcal.E, so it is the whole content at the (2,2) error slot.

Part D -- the whole 𝓔 chain

theorem Algsuperdiff.Section4.Provider.Annular.maxDescendantNormalizedBlockResponseAtScale_adjointFamily {d : ℕ} (F : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (Q : HCPolySupport.TriadicCube d) (k : ℤ) {σ0 : ℝ} (hσ0 : 0 < σ0) : HCPolySupport.Book.Ch02.maxDescendantNormalizedBlockResponseAtScale Q k (Section3.Provider.CoarseEllipticity.adjointFamily F) (HCPolySupport.scalarMatrix σ0) = HCPolySupport.Book.Ch02.maxDescendantNormalizedBlockResponseAtScale Q k F (HCPolySupport.scalarMatrix σ0)

theorem Algsuperdiff.Section4.Provider.Annular.scaleResponseAtScale_adjointFamily {d : ℕ} (F : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (Q : HCPolySupport.TriadicCube d) (k : ℤ) (p : HCPolySupport.Book.Ch02.MultiscaleExponent) {σ0 : ℝ} (hσ0 : 0 < σ0) : HCPolySupport.Book.Ch02.scaleResponseAtScale Q k p (Section3.Provider.CoarseEllipticity.adjointFamily F) (HCPolySupport.scalarMatrix σ0) = HCPolySupport.Book.Ch02.scaleResponseAtScale Q k p F (HCPolySupport.scalarMatrix σ0)

theorem Algsuperdiff.Section4.Provider.Annular.homogenizationError_adjointFamily {d : ℕ} (F : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (Q : HCPolySupport.TriadicCube d) (n : ℤ) (s : ℝ) (p q : HCPolySupport.Book.Ch02.MultiscaleExponent) {σ0 : ℝ} (hσ0 : 0 < σ0) : HCPolySupport.Book.Ch02.HomogenizationError Q n s p q (Section3.Provider.CoarseEllipticity.adjointFamily F) (HCPolySupport.scalarMatrix σ0) = HCPolySupport.Book.Ch02.HomogenizationError Q n s p q F (HCPolySupport.scalarMatrix σ0)

theorem Algsuperdiff.Section4.Provider.Annular.homogenizationErrorOnCube_adjointFamily {d : ℕ} (F : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (Q : HCPolySupport.TriadicCube d) (s : ℝ) (p q : HCPolySupport.Book.Ch02.MultiscaleExponent) {σ0 : ℝ} (hσ0 : 0 < σ0) : HCPolySupport.Book.Ch02.HomogenizationErrorOnCube Q s p q (Section3.Provider.CoarseEllipticity.adjointFamily F) (HCPolySupport.scalarMatrix σ0) = HCPolySupport.Book.Ch02.HomogenizationErrorOnCube Q s p q F (HCPolySupport.scalarMatrix σ0)

𝓔_{s,p,q}(Q; aᵀ, σ Id) = 𝓔_{s,p,q}(Q; a, σ Id), for every pair of exponents.

Part E -- the sample-level 𝒢₂ atom

theorem Algsuperdiff.Section4.Provider.Annular.translateCutoffSample_negateCutoffSample {d : ℕ} (z : HCPolySupport.Vec d) (omega : Section3.Cutoff.CutoffSample d) : Section3.Cutoff.translateCutoffSample z (Section3.Cutoff.negateCutoffSample omega) = Section3.Cutoff.negateCutoffSample (Section3.Cutoff.translateCutoffSample z omega)

Whole-sequence negation commutes with real translation on the cutoff carrier.

theorem Algsuperdiff.Section4.Provider.Annular.annularErrorAtom_negateCutoffSample {d : ℕ} (M : Section3.ABKModel d) (n : ℤ) (s : ℝ) (omega : Section3.Cutoff.CutoffSample d) : Support.annularErrorAtom M n s (Section3.Cutoff.negateCutoffSample omega) = Support.annularErrorAtom M n s omega

The 𝒢₂ atom is invariant under whole-sequence negation.

𝓔_{s,2,2}(□_n; a_{n−2}(−ω), σ_{n−2}) = 𝓔_{s,2,2}(□_n; a_{n−2}(ω), σ_{n−2}), pointwise in ω: the (J3) carrier identity a_m(−ω) = a_m(ω)ᵀ composed with homogenizationErrorOnCube_adjointFamily.

theorem Algsuperdiff.Section4.Provider.Annular.annularErrorAtomMax_negateCutoffSample {d : ℕ} (M : Section3.ABKModel d) (s : ℝ) (omega : Section3.Cutoff.CutoffSample d) (j n : ℤ) : annularErrorAtomMax M s (Section3.Cutoff.negateCutoffSample omega) j n = annularErrorAtomMax M s omega j n

The annulus maximum of the 𝒢₂ atoms is invariant under whole-sequence negation. The lattice index set is deterministic and the translations commute with the negation.