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

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

theorem HCPolySupport.Book.Ch02.blockMatrixField_ae_eq_ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) : blockMatrixField a =ᵐ[volumeMeasureOn U.carrier] blockMatrixField b

theorem HCPolySupport.Book.Ch02.blockEnergyDensityAt_ae_eq_ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) (P : BlockVec d) : (fun (x : Vec d) => blockEnergyDensityAt a P x) =ᵐ[volumeMeasureOn U.carrier] fun (x : Vec d) => blockEnergyDensityAt b P x

theorem HCPolySupport.Book.Ch02.doubledBlockPairingIntegrand_ae_eq_ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) (Y X : DoubledField d) : doubledBlockPairingIntegrand U a Y X =ᵐ[volumeMeasureOn U.carrier] doubledBlockPairingIntegrand U b Y X

theorem HCPolySupport.Book.Ch02.doubledMuValue_eq_ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) (X : DoubledField d) : doubledMuValue U a X = doubledMuValue U b X

theorem HCPolySupport.Book.Ch02.doubledMuValueSet_eq_ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) (P : BlockVec d) : doubledMuValueSet U a P = doubledMuValueSet U b P

theorem HCPolySupport.Book.Ch02.doubledMu_eq_ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) (P : BlockVec d) : doubledMu U a P = doubledMu U b P

theorem HCPolySupport.Book.Ch02.IsDoubledMuMinimizer.ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) {P : BlockVec d} {X : DoubledField d} (hX : IsDoubledMuMinimizer U a P X) : IsDoubledMuMinimizer U b P X

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

Public theorem package for the variational quantity e.def.block.mu.basic.definitions and the coarse block matrix definition e.def.block.coarse.matrix.basic.definitions.

The canonical public theorem proving this package is doubledMuTheory in DoubledMu.lean.

• minimizer_exists (P : BlockVec d) : ∃ (X : DoubledField d), IsDoubledMuMinimizer U a P X
• minimizer_unique_ae (P : BlockVec d) (X Y : DoubledField d) : IsDoubledMuMinimizer U a P X → IsDoubledMuMinimizer U a P Y → X.SameAE Y
• mu_quadratic (P : BlockVec d) : doubledMu U a P = 1 / 2 * blockVecDot P (blockMatVecMul (coarseBlockMatrix U a) P)
• minimizer_first_variation (P : BlockVec d) (X : DoubledField d) : IsDoubledMuMinimizer U a P X → ∀ (Y : DoubledField d), IsDoubledTestField U Y → ∫ (x : Vec d) in U.carrier, doubledBlockPairingIntegrand U a Y X x = 0

theorem HCPolySupport.Book.Ch02.DoubledMuTheory.ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} (h : a.AEEq b) (hTheory : DoubledMuTheory U a) : DoubledMuTheory U b

theorem HCPolySupport.Book.Ch02.DoubledMuTheory.doubledMu_eq_coarseBlockMatrix {d : ℕ} {U : Domain d} {a : CoeffOn U} (h : DoubledMuTheory U a) (P : BlockVec d) : doubledMu U a P = 1 / 2 * blockVecDot P (blockMatVecMul (coarseBlockMatrix U a) P)

Accessor for the public quadratic formula defining the coarse block matrix.