Coarse-graining support: Support.Internal.Ch02.SymmetricDirichletNeumann.ZeroDim

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

Zero-Dimensional Symmetric Dirichlet-Neumann Theory

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

theorem HCPolySupport.Internal.Ch02.BookCh02.matLoewnerLE_zero_dim {A B : Mat 0} : MatLoewnerLE A B

theorem HCPolySupport.Internal.Ch02.BookCh02.symmetricDirichletEnergyValue_zero_dim (U : Book.Ch02.Domain 0) (a : Book.Ch02.CoeffOn U) (u : H1Function U.carrier) : Book.Ch02.symmetricDirichletEnergyValue U a u = 0

theorem HCPolySupport.Internal.Ch02.BookCh02.symmetricNeumannEnergyValue_zero_dim (U : Book.Ch02.Domain 0) (a : Book.Ch02.CoeffOn U) (q : Vec 0) (u : H1Function U.carrier) : Book.Ch02.symmetricNeumannEnergyValue U a q u = 0

theorem HCPolySupport.Internal.Ch02.BookCh02.isSymmetricDirichletAdmissible_zero_dim (U : Book.Ch02.Domain 0) (p : Vec 0) (u : H1Function U.carrier) : Book.Ch02.IsSymmetricDirichletAdmissible U p u

theorem HCPolySupport.Internal.Ch02.BookCh02.isSymmetricDirichletMinimizer_zero_dim (U : Book.Ch02.Domain 0) (a : Book.Ch02.CoeffOn U) (p : Vec 0) (u : H1Function U.carrier) : Book.Ch02.IsSymmetricDirichletMinimizer U a p u

theorem HCPolySupport.Internal.Ch02.BookCh02.isSymmetricNeumannMaximizer_zero_dim (U : Book.Ch02.Domain 0) (a : Book.Ch02.CoeffOn U) (q : Vec 0) (u : H1Function U.carrier) : Book.Ch02.IsSymmetricNeumannMaximizer U a q u

theorem HCPolySupport.Internal.Ch02.BookCh02.symmetricDirichletNu_zero_dim (U : Book.Ch02.Domain 0) (a : Book.Ch02.CoeffOn U) (p : Vec 0) : Book.Ch02.symmetricDirichletNu U a p = 0

theorem HCPolySupport.Internal.Ch02.BookCh02.symmetricNeumannNu_zero_dim (U : Book.Ch02.Domain 0) (a : Book.Ch02.CoeffOn U) (q : Vec 0) : Book.Ch02.symmetricNeumannNu U a q = 0

theorem HCPolySupport.Internal.Ch02.BookCh02.responseJ_zero_dim (U : Book.Ch02.Domain 0) (a : Book.Ch02.CoeffOn U) (p q : Vec 0) : Book.Ch02.responseJ U a p q = 0

theorem HCPolySupport.Internal.Ch02.BookCh02.responseSymmetricDirichletNeumannTheory_zero_dim (U : Book.Ch02.Domain 0) (a : Book.Ch02.CoeffOn U) (hsym : a.IsSymmetric) : Book.Ch02.ResponseSymmetricDirichletNeumannTheory U a hsym