TransposeGauge

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

Transpose invariance of the coarse gauge

Source: ABK26. The proof of l.Dh.bound applies the coarse Poincaré inequality e.w.wstar.to.energy to the adjoint half w^* = ½ v(·, □₀, p, -q; aᵗ), whose maximizer solves the transposed problem. The right-hand side of that inequality carries the coarse gauge of the transposed coefficient, and the frozen statement carries the gauge of a. The two agree:

λ_{s,q}(□₀; aᵗ) = λ_{s,q}(□₀; a) .

The reason is that the whole multiscale gauge is built from the one-cube norms |σ_*^{-1}(R; ·)|, and σ_*^{-1} is defined entrywise from the pure-flux response J(U, 0, ·) (Book.Ch02.sigmaStarInvEntry). The adjoint response identity responseJ_transpose_neg_right at p = 0 says J(U, aᵗ, 0, -w) = J(U, a, 0, w), and the pure-flux response is even in w because it is the quadratic form of σ_*^{-1}. Hence

σ_*^{-1}(U; aᵗ) = σ_*^{-1}(U; a)

at every Chapter 2 domain, and the gauge invariance follows by transporting this through coarseSigmaStarInvMatrixNorm, maxDescendantSigmaStarInvMatrixNormAtScale, lambdaSqFinite / lambdaSqInfinity, and finally through the frozen characterization theorem.

The pure-flux response is even and transpose invariant

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.responseJ_zero_neg_right {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) (w : HCPolySupport.Vec d) : HCPolySupport.Book.Ch02.responseJ U a 0 (-w) = HCPolySupport.Book.Ch02.responseJ U a 0 w

The pure-flux response is an even function of the flux loading.

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.responseJ_transpose_zero_left {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) (w : HCPolySupport.Vec d) : HCPolySupport.Book.Ch02.responseJ U a.transpose 0 w = HCPolySupport.Book.Ch02.responseJ U a 0 w

The pure-flux response does not see the transpose.

Transpose invariance of σ_*^{-1}

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.sigmaStarInvCoarse_transpose {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) : HCPolySupport.Book.Ch02.sigmaStarInvCoarse U a.transpose = HCPolySupport.Book.Ch02.sigmaStarInvCoarse U a

The canonical coarse matrix σ_*^{-1} is transpose invariant.

The transposed coefficient family

noncomputable def Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.transposeCoeffFamily {d : ℕ} (F : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) : HCPolySupport.Book.Ch02.TriadicCoeffFamily d

The entrywise transpose of a CoarseGraining triadic coefficient family.

Equations

• Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.transposeCoeffFamily F = { coeffOn := fun (Q : HCPolySupport.TriadicCube d) => (F.coeffOn Q).transpose, restrictsTo_of_subset := ⋯ }

@[simp]

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.transposeCoeffFamily_coeffOn {d : ℕ} (F : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (Q : HCPolySupport.TriadicCube d) : (transposeCoeffFamily F).coeffOn Q = (F.coeffOn Q).transpose

Transpose invariance of the multiscale gauge

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.coarseSigmaStarInvMatrixNorm_transposeCoeffFamily {d : ℕ} (Q : HCPolySupport.TriadicCube d) (F : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) : HCPolySupport.Book.Ch02.coarseSigmaStarInvMatrixNorm Q (transposeCoeffFamily F) = HCPolySupport.Book.Ch02.coarseSigmaStarInvMatrixNorm Q F

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.maxDescendantSigmaStarInvMatrixNormAtScale_transposeCoeffFamily {d : ℕ} (Q : HCPolySupport.TriadicCube d) (k : ℤ) (F : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) : HCPolySupport.Book.Ch02.maxDescendantSigmaStarInvMatrixNormAtScale Q k (transposeCoeffFamily F) = HCPolySupport.Book.Ch02.maxDescendantSigmaStarInvMatrixNormAtScale Q k F

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.lambdaSq_transposeCoeffFamily {d : ℕ} (Q : HCPolySupport.TriadicCube d) (s : ℝ) (q : HCPolySupport.Book.Ch02.MultiscaleExponent) (F : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) : HCPolySupport.Book.Ch02.lambdaSq Q s q (transposeCoeffFamily F) = HCPolySupport.Book.Ch02.lambdaSq Q s q F

Transpose invariance of the frozen unit-cube gauge

theorem Algsuperdiff.Section24.Sensitivity.Provider.DhBound.Discharge.unitCubeLambda_transpose {d : ℕ} (s : ℝ) (q : HCPolySupport.Book.Ch02.MultiscaleExponent) (a : HCPolySupport.Book.Ch02.CoeffOn (HCPolySupport.Book.Ch02.cubeDomain (HCPolySupport.originCube d 0))) : Frozen.Section24.unitCubeLambda s q a.transpose = Frozen.Section24.unitCubeLambda s q a

The frozen coarse gauge is transpose invariant.