Coarse-graining support: Support.Internal.Ch02.SymmetricDirichletNeumann.Neumann #
Imported from the Apache-2.0 CoarseGraining development at commit
c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.
Neumann Side #
This file is split mechanically out of Internal.Ch02.SymmetricDirichletNeumann.
theorem
HCPolySupport.Internal.Ch02.BookCh02.exists_isConstantFluxNeumannSolution_of_isEllipticFieldOn
{d : ℕ}
(U : Book.Ch02.Domain d)
(a : Book.Ch02.CoeffOn U)
(hEll : IsEllipticFieldOn a.lam a.Lam U.carrier a.toCoeffField)
(q : Vec d)
:
∃ (u : H1MeanZeroFunction U.carrier), IsConstantFluxNeumannSolution a.toCoeffField U.carrier q u
Construct the old constant-flux Neumann solution predicate from the mean-zero Neumann RHS solver on a bounded open convex domain.
theorem
HCPolySupport.Internal.Ch02.BookCh02.symmetricNeumannEnergyValue_eq_of_isConstantFluxNeumannSolution
{d : ℕ}
(U : Book.Ch02.Domain d)
(a : Book.Ch02.CoeffOn U)
{q : Vec d}
{u : H1MeanZeroFunction U.carrier}
(hu : IsConstantFluxNeumannSolution a.toCoeffField U.carrier q u)
(ha : IsSymmetricCoeffField a.toCoeffField)
(hEll : IsEllipticFieldOn a.lam a.Lam U.carrier a.toCoeffField)
(w : H1Function U.carrier)
:
Book.Ch02.symmetricNeumannEnergyValue U a q w = Book.Ch02.symmetricNeumannEnergyValue U a q u.toH1Function - 1 / 2 * volumeAverage U.carrier fun (x : Vec d) =>
vecDot ((w - u.toH1Function).grad x) (matVecMul (a.toCoeffField x) ((w - u.toH1Function).grad x))
theorem
HCPolySupport.Internal.Ch02.BookCh02.symmetricNeumannEnergyValue_eq_half_variationEnergy_of_isConstantFluxNeumannSolution
{d : ℕ}
(U : Book.Ch02.Domain d)
(a : Book.Ch02.CoeffOn U)
{q : Vec d}
{u : H1MeanZeroFunction U.carrier}
(hu : IsConstantFluxNeumannSolution a.toCoeffField U.carrier q u)
(hEll : IsEllipticFieldOn a.lam a.Lam U.carrier a.toCoeffField)
:
theorem
HCPolySupport.Internal.Ch02.BookCh02.isSymmetricNeumannMaximizer_of_isConstantFluxNeumannSolution
{d : ℕ}
(U : Book.Ch02.Domain d)
(a : Book.Ch02.CoeffOn U)
{q : Vec d}
{u : H1MeanZeroFunction U.carrier}
(hu : IsConstantFluxNeumannSolution a.toCoeffField U.carrier q u)
(ha : IsSymmetricCoeffField a.toCoeffField)
(hEll : IsEllipticFieldOn a.lam a.Lam U.carrier a.toCoeffField)
:
theorem
HCPolySupport.Internal.Ch02.BookCh02.sameGradientAE_of_isSymmetricNeumannMaximizer_of_isConstantFluxNeumannSolution
{d : ℕ}
(U : Book.Ch02.Domain d)
(a : Book.Ch02.CoeffOn U)
{q : Vec d}
{u : H1MeanZeroFunction U.carrier}
(hu : IsConstantFluxNeumannSolution a.toCoeffField U.carrier q u)
(ha : IsSymmetricCoeffField a.toCoeffField)
(hEll : IsEllipticFieldOn a.lam a.Lam U.carrier a.toCoeffField)
{w : H1Function U.carrier}
(hw : Book.Ch02.IsSymmetricNeumannMaximizer U a q w)
:
w.grad =ᵐ[volumeMeasureOn U.carrier] u.toH1Function.grad