Coarse-graining support: Support.Book.Ch02.Theorems.DoubledMu

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

theorem HCPolySupport.Book.Ch02.doubledMuTheory {d : ℕ} (U : Domain d) (a : CoeffOn U) : DoubledMuTheory U a

Public doubled-mu theory package. The internal proof may replace the coefficient field by an a.e.-equal pointwise representative, but this theorem is stated only for the public a.e.-native coefficient field a.

theorem HCPolySupport.Book.Ch02.IsDoubledMuMinimizer.doubledMuValue_eq_doubledMu {d : ℕ} {U : Domain d} {a : CoeffOn U} {P : BlockVec d} {X : DoubledField d} (hX : IsDoubledMuMinimizer U a P X) : doubledMuValue U a X = doubledMu U a P

A pointwise doubled-mu minimizer realizes the public infimum.

theorem HCPolySupport.Book.Ch02.doubledMuMinimizer_negLeft_eq_canonicalGradient {d : ℕ} (U : Domain d) (a : CoeffOn U) (p q : Vec d) {X : DoubledField d} (hX : IsDoubledMuMinimizer U a (-p, q) X) : (fun (x : Vec d) => X.potential x + (blockMatVecMul (blockCoeffField a.toCoeffField x) (X.eval x)).2) =ᵐ[volumeMeasureOn U.carrier] fun (x : Vec d) => (canonicalMaximizer ⋯ p q).toSolution.toH1.grad x

A doubled-mu minimizer at loading (-p, q) extracts the gradient of the scalar canonical response maximizer from its lower block image.

theorem HCPolySupport.Book.Ch02.doubledMuMinimizer_neg_left_extracts_canonicalMaximizerFlux {d : ℕ} (U : Domain d) (a : CoeffOn U) (p q : Vec d) {X : DoubledField d} (hX : IsDoubledMuMinimizer U a (-p, q) X) : (fun (x : Vec d) => X.flux x + (blockMatVecMul (blockCoeffField a.toCoeffField x) (X.eval x)).1) =ᵐ[volumeMeasureOn U.carrier] fun (x : Vec d) => matVecMul (a.toCoeffField x) ((canonicalMaximizer ⋯ p q).toSolution.toH1.grad x)

A doubled-mu minimizer at loading (-p, q) extracts the flux of the scalar canonical response maximizer from its upper block image.