Documentation

LeanPool.HighContrastHomogenization.Support.Internal.Ch02.DoubledMu

Coarse-graining support: Support.Internal.Ch02.DoubledMu #

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

source
theorem HCPolySupport.Internal.Ch02.BookCh02.book_doubledMu_eq_Mu {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) (P : BlockVec d) :
Book.Ch02.doubledMu U a P = Mu U.carrier P a.toCoeffField
source
theorem HCPolySupport.Internal.Ch02.BookCh02.book_coarseBlockMatrix_eq_old_coarseBlockMatrix_of_data {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) {sigma sigmaStar kappa : Mat d} (hA : IsCoarseBlockMatrix U.carrier a.toCoeffField (deterministicCoarseBlockMatrix U.carrier a.toCoeffField)) (hS : IsSigmaStarCoarse U.carrier a.toCoeffField sigmaStar) (hK : IsKappaCoarse U.carrier a.toCoeffField sigmaStar kappa) (hSigma : IsSigmaCoarse U.carrier a.toCoeffField sigma sigmaStar kappa) (hdet : IsUnit (Matrix.det sigmaStar)) :
Book.Ch02.coarseBlockMatrix U a = coarseBlockMatrix U.carrier a.toCoeffField

Internal bridge identifying the public coarse block matrix with the old coarse-block matrix once the old deterministic coarse data have been produced.

source
theorem HCPolySupport.Internal.Ch02.BookCh02.doubledMuTheory {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) :
Book.Ch02.DoubledMuTheory U a
source
theorem HCPolySupport.Internal.Ch02.BookCh02.doubledMuMinimizer_negLeft_eq_canonicalGradient {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) (p q : Vec d) {X : Book.Ch02.DoubledField d} (hX : Book.Ch02.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) => (Book.Ch02.canonicalMaximizer ⋯ p q).toSolution.toH1.grad x
source
theorem HCPolySupport.Internal.Ch02.BookCh02.doubledMuMinimizer_neg_left_extracts_canonicalMaximizerFlux {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) (p q : Vec d) {X : Book.Ch02.DoubledField d} (hX : Book.Ch02.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) ((Book.Ch02.canonicalMaximizer ⋯ p q).toSolution.toH1.grad x)