DoubledAdjointEllipticity

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

Adjoint invariance of the coarse-grained ellipticity constants

ABK26 Remark r.cg.poincare.doubled.variables states the doubled-variables Poincare inequality e.CG.Poincare.doubled.vars with the coarse-grained ellipticity constants lambda_{s,q}(cu_m; a) and Lambda_{s,q}(cu_m; a) of the primal coefficient field, although its proof applies p.coarse.grained.Poincare to the adjoint solution v^* as well, and therefore produces lambda_{s,q}(cu_m; a^t) and Lambda_{s,q}(cu_m; a^t) on that half. The two agree. This module proves that -- item (beta) of the infrastructure list recorded in DoubledEnergyIdentity.lean.

The mechanism

Both constants are geometric sums of the one-cube norms |sigma_*^{-1}(R; a)| and |b(R; a)| over descendants, and the two coarse matrices are adjoint invariant:

• sigma_*(U; a^t) = sigma_*(U; a) (CoarseGraining BlockCoarseMatrixTheory.adjoint_sigmaStar), hence sigma_*^{-1}(U; a^t) = sigma_*^{-1}(U; a) since sigma_*^{-1} has invertible determinant;
• b = sigma + kappa^t sigma_*^{-1} kappa with sigma(U; a^t) = sigma(U; a) and kappa(U; a^t) = -kappa(U; a), so the sign cancels in the quadratic correction.

Main results

• adjointFamily -- the adjoint triadic coefficient family a^t.
• sigmaStarInvCoarse_transpose, bCoarse_transpose -- the two matrix identities.
• lambdaSq_adjointFamily, LambdaSq_adjointFamily -- the display's own invariance, for every exponent q (finite and endpoint).

Scope

No anchor, frozen theorem or external input is consumed, and there is no sorry.

References

• ABK26, r.cg.poincare.doubled.variables; e.bfA.magic.swapping; e.findSfull.

The adjoint family

noncomputable def Algsuperdiff.Section3.Provider.CoarseEllipticity.adjointFamily {d : ℕ} (a : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) : HCPolySupport.Book.Ch02.TriadicCoeffFamily d

The adjoint triadic coefficient family a^t. Cube by cube it is CoarseGraining's CoeffOn.transpose; the restriction compatibility is inherited from a by transposing the almost-everywhere identity.

Equations

• Algsuperdiff.Section3.Provider.CoarseEllipticity.adjointFamily a = { coeffOn := fun (Q : HCPolySupport.TriadicCube d) => (a.coeffOn Q).transpose, restrictsTo_of_subset := ⋯ }

@[simp]

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.adjointFamily_coeffOn {d : ℕ} (a : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) (Q : HCPolySupport.TriadicCube d) : (adjointFamily a).coeffOn Q = (a.coeffOn Q).transpose

Adjoint invariance of the two coarse matrices

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.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

sigma_*^{-1}(U; a^t) = sigma_*^{-1}(U; a).

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.bCoarse_transpose {d : ℕ} (U : HCPolySupport.Book.Ch02.Domain d) (a : HCPolySupport.Book.Ch02.CoeffOn U) : HCPolySupport.Book.Ch02.bCoarse U a.transpose = HCPolySupport.Book.Ch02.bCoarse U a

b(U; a^t) = b(U; a): sigma is invariant, kappa changes sign, and the correction kappa^t sigma_*^{-1} kappa is even in kappa.

Adjoint invariance of the one-cube and descendant norms

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.coarseSigmaStarInvMatrixNorm_adjointFamily {d : ℕ} (Q : HCPolySupport.TriadicCube d) (a : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) : HCPolySupport.Book.Ch02.coarseSigmaStarInvMatrixNorm Q (adjointFamily a) = HCPolySupport.Book.Ch02.coarseSigmaStarInvMatrixNorm Q a

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.coarseBMatrixNorm_adjointFamily {d : ℕ} (Q : HCPolySupport.TriadicCube d) (a : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) : HCPolySupport.Book.Ch02.coarseBMatrixNorm Q (adjointFamily a) = HCPolySupport.Book.Ch02.coarseBMatrixNorm Q a

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.maxDescendantSigmaStarInvMatrixNormAtScale_adjointFamily {d : ℕ} (Q : HCPolySupport.TriadicCube d) (k : ℤ) (a : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) : HCPolySupport.Book.Ch02.maxDescendantSigmaStarInvMatrixNormAtScale Q k (adjointFamily a) = HCPolySupport.Book.Ch02.maxDescendantSigmaStarInvMatrixNormAtScale Q k a

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.maxDescendantBMatrixNormAtScale_adjointFamily {d : ℕ} (Q : HCPolySupport.TriadicCube d) (k : ℤ) (a : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) : HCPolySupport.Book.Ch02.maxDescendantBMatrixNormAtScale Q k (adjointFamily a) = HCPolySupport.Book.Ch02.maxDescendantBMatrixNormAtScale Q k a

Adjoint invariance of the coarse-grained ellipticity constants

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.lambdaSq_adjointFamily {d : ℕ} (Q : HCPolySupport.TriadicCube d) (s : ℝ) (q : HCPolySupport.Book.Ch02.MultiscaleExponent) (a : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) : HCPolySupport.Book.Ch02.lambdaSq Q s q (adjointFamily a) = HCPolySupport.Book.Ch02.lambdaSq Q s q a

lambda_{s,q}(Q; a^t) = lambda_{s,q}(Q; a), for every exponent.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.LambdaSq_adjointFamily {d : ℕ} (Q : HCPolySupport.TriadicCube d) (s : ℝ) (q : HCPolySupport.Book.Ch02.MultiscaleExponent) (a : HCPolySupport.Book.Ch02.TriadicCoeffFamily d) : HCPolySupport.Book.Ch02.LambdaSq Q s q (adjointFamily a) = HCPolySupport.Book.Ch02.LambdaSq Q s q a

Lambda_{s,q}(Q; a^t) = Lambda_{s,q}(Q; a), for every exponent.