DoubledEnergyIdentity

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

The doubled-variable energy identity

ABK26 Remark r.cg.poincare.doubled.variables restates the coarse-grained Poincare inequality p.coarse.grained.Poincare in terms of the doubled-variable solution space S(cu_m) of e.bfS. Its right-hand side is the doubled energy || bfA^(1/2) X ||_{underline L^2(cu_m)}, whereas the two Poincare inequalities it is derived from are stated with the scalar energies || s^(1/2) grad v ||_{underline L^2} and || s^(1/2) grad v* ||.

The bridge between the two is the pointwise algebraic identity proved here: along the characterization e.findSfull

X = (grad v + grad v*, a grad v - a^t grad v*),

the block quadratic form collapses, by the swapping identity e.bfA.magic.swapping, to twice the sum of the two scalar energy densities. In CoarseGraining's normalization the block density carries a factor 1/2, so the identity reads

blockEnergyDensityAt a (X x) x
  = variationEnergyIntegrand U a v x + variationEnergyIntegrand U a^t v* x .

This is a pointwise statement about the integrands; it carries no integral and therefore no integrability side condition.

Scope

This file is infrastructure for e.CG.Poincare.doubled.vars and claims no node status. The displayed inequality of that node additionally requires a block negative-Besov seminorm on R^{2d}-valued fields, the adjoint invariance of the coarse-grained ellipticity constants, and a per-truncation form of the CoarseGraining coarse-grained Poincare inequality; none of those are supplied here.

Main results

• blockEnergyDensityAt_doubledFieldOfSolutions: the pointwise identity.
• add_le_sqrt_two_mul_add_sq: the elementary two-term step that converts the pair of scalar energies into the single doubled energy.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.blockEnergyDensityAt_doubledFieldOfSolutions {d : ℕ} {U : HCPolySupport.Book.Ch02.Domain d} (a : HCPolySupport.Book.Ch02.CoeffOn U) (v : HCPolySupport.Book.Ch02.Solution U a) (vStar : HCPolySupport.Book.Ch02.Solution U a.transpose) {x : HCPolySupport.Vec d} (hdet : IsUnit (Matrix.det (HCPolySupport.symmPart (a.toCoeffField x)))) : HCPolySupport.Book.Ch02.blockEnergyDensityAt a ((HCPolySupport.Book.Ch02.doubledFieldOfSolutions a v vStar).eval x) x = HCPolySupport.Book.Ch02.variationEnergyIntegrand U a v x + HCPolySupport.Book.Ch02.variationEnergyIntegrand U a.transpose vStar x

The doubled-variable energy identity. For the doubled field generated by a primal solution v and an adjoint solution vStar, the block energy density is the sum of the two scalar energy densities.

theorem Algsuperdiff.Section3.Provider.CoarseEllipticity.add_le_sqrt_two_mul_add_sq {A B : ℝ} (hA : 0 ≤ A) (hB : 0 ≤ B) : A + B ≤ √(2 * (A ^ 2 + B ^ 2))

The elementary two-term step: a sum of two nonnegative quantities is dominated by the square root of twice the sum of their squares. With A = || s^(1/2) grad v || and B = || s^(1/2) grad v* || the right-hand side is exactly the doubled energy || bfA^(1/2) X ||, by the identity above.