Documentation

LeanPool.HighContrastHomogenization.Support.Internal.Ch02.SymmetricDirichletNeumann.Dirichlet

Coarse-graining support: Support.Internal.Ch02.SymmetricDirichletNeumann.Dirichlet #

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

Dirichlet Side #

This file is split mechanically out of Internal.Ch02.SymmetricDirichletNeumann.

source
theorem HCPolySupport.Internal.Ch02.BookCh02.exists_isAffineDirichletSolution_of_isEllipticFieldOn {d : ℕ} [NeZero d] (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) (hEll : IsEllipticFieldOn a.lam a.Lam U.carrier a.toCoeffField) (p : Vec d) :
∃ (u : H1Function U.carrier), IsAffineDirichletSolution a.toCoeffField U.carrier p u

Construct the old affine Dirichlet solution predicate from the zero-trace Dirichlet RHS solver on a bounded open convex domain. This is an internal bridge toward the public symmetric Dirichlet minimizer package.

source
theorem HCPolySupport.Internal.Ch02.BookCh02.symmetricDirichletEnergyValue_eq_of_isAffineDirichletSolution {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) {p : Vec d} {u w : H1Function U.carrier} (hu : IsAffineDirichletSolution a.toCoeffField U.carrier p u) (hw : Book.Ch02.IsSymmetricDirichletAdmissible U p w) (ha : IsSymmetricCoeffField a.toCoeffField) (hEll : IsEllipticFieldOn a.lam a.Lam U.carrier a.toCoeffField) :
Book.Ch02.symmetricDirichletEnergyValue U a w = Book.Ch02.symmetricDirichletEnergyValue U a u + 1 / 2 * volumeAverage U.carrier fun (x : Vec d) => vecDot ((w - u).grad x) (matVecMul (a.toCoeffField x) ((w - u).grad x))
source
theorem HCPolySupport.Internal.Ch02.BookCh02.isSymmetricDirichletMinimizer_of_isAffineDirichletSolution {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) {p : Vec d} {u : H1Function U.carrier} (hu : IsAffineDirichletSolution a.toCoeffField U.carrier p u) (ha : IsSymmetricCoeffField a.toCoeffField) (hEll : IsEllipticFieldOn a.lam a.Lam U.carrier a.toCoeffField) :
Book.Ch02.IsSymmetricDirichletMinimizer U a p u
source
theorem HCPolySupport.Internal.Ch02.BookCh02.sameGradientAE_of_isSymmetricDirichletMinimizer_of_isAffineDirichletSolution {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) {p : Vec d} {u w : H1Function U.carrier} (hu : IsAffineDirichletSolution a.toCoeffField U.carrier p u) (ha : IsSymmetricCoeffField a.toCoeffField) (hEll : IsEllipticFieldOn a.lam a.Lam U.carrier a.toCoeffField) (hw : Book.Ch02.IsSymmetricDirichletMinimizer U a p w) :
w.grad =ᵐ[volumeMeasureOn U.carrier] u.grad