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

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

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

Public theorem package for l.symmetric.dirichlet.neumann.split.basic.definitions.

The symmetric hypothesis is a.e.-native: no public theorem in this package uses pointwise symmetry of the coefficient representative. The canonical public theorem proving this package is responseSymmetricDirichletNeumannTheory in SymmetricDirichletNeumann.lean.

• dirichlet_minimizer_exists (p : Vec d) : ∃ (u : H1Function U.carrier), IsSymmetricDirichletMinimizer U a p u
• neumann_meanZero_maximizer_exists (q : Vec d) : ∃ (u : H1Function U.carrier), MeanZeroOn U.carrier u.toFun ∧ IsSymmetricNeumannMaximizer U a q u
• response_maximizer_split (p q : Vec d) (v : Solution U a) : IsResponseMaximizer U a p q v → ∀ (uD uN : H1Function U.carrier), IsSymmetricDirichletMinimizer U a p uD → IsSymmetricNeumannMaximizer U a q uN → v.toH1.grad =ᵐ[volumeMeasureOn U.carrier] fun (x : Vec d) => uN.grad x - uD.grad x
• response_dirichlet_neumann_split (p q : Vec d) : responseJ U a p q = symmetricDirichletNu U a p + symmetricNeumannNu U a q - vecDot p q
• dirichlet_value_by_sigma (p : Vec d) : symmetricDirichletNu U a p = 1 / 2 * vecDot p (matVecMul (sigmaCoarse U a) p)
• neumann_value_by_sigmaStarInv (q : Vec d) : symmetricNeumannNu U a q = 1 / 2 * vecDot q (matVecMul (sigmaStarInvCoarse U a) q)
• kappa_eq_zero : kappaCoarse U a = 0
• dirichlet_average_gradient (p : Vec d) (uD : H1Function U.carrier) : IsSymmetricDirichletMinimizer U a p uD → h1AverageGradient U uD = p
• dirichlet_average_flux (p : Vec d) (uD : H1Function U.carrier) : IsSymmetricDirichletMinimizer U a p uD → h1AverageFlux U a uD = matVecMul (sigmaCoarse U a) p
• neumann_average_flux (q : Vec d) (uN : H1Function U.carrier) : IsSymmetricNeumannMaximizer U a q uN → h1AverageFlux U a uN = q
• neumann_average_gradient (q : Vec d) (uN : H1Function U.carrier) : IsSymmetricNeumannMaximizer U a q uN → h1AverageGradient U uN = matVecMul (sigmaStarInvCoarse U a) q
• response_completed_square (p q : Vec d) : responseJ U a p q = 1 / 2 * vecDot p (matVecMul (sigmaCoarse U a - sigmaStarCoarse U a) p) + 1 / 2 * vecDot (q - matVecMul (sigmaStarCoarse U a) p) (matVecMul (sigmaStarInvCoarse U a) (q - matVecMul (sigmaStarCoarse U a) p))
• derived_matrices : aCoarse U a = sigmaCoarse U a ∧ aStarCoarse U a = sigmaStarCoarse U a ∧ bCoarse U a = sigmaCoarse U a
• dirichlet_neumann_bracketing : MatLoewnerLE (averagedSymmPartInv U a)⁻¹ (sigmaStarCoarse U a) ∧ MatLoewnerLE (sigmaStarCoarse U a) (sigmaCoarse U a) ∧ MatLoewnerLE (sigmaCoarse U a) (averageMat U a.toCoeffField)

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

Transport the full symmetric Dirichlet--Neumann theorem package across an a.e. coefficient change.

theorem HCPolySupport.Book.Ch02.ResponseSymmetricDirichletNeumannTheory.iff_ofAEEq {d : ℕ} {U : Domain d} {a b : CoeffOn U} {hsym_a : a.IsSymmetric} {hsym_b : b.IsSymmetric} (h : a.AEEq b) : ResponseSymmetricDirichletNeumannTheory U a hsym_a ↔ ResponseSymmetricDirichletNeumannTheory U b hsym_b

A.e.-equivalent coefficient representatives satisfy the same symmetric Dirichlet--Neumann theorem package.

theorem HCPolySupport.Book.Ch02.ResponseSymmetricDirichletNeumannTheory.response_completed_square_eq {d : ℕ} {U : Domain d} {a : CoeffOn U} {hsym : a.IsSymmetric} (h : ResponseSymmetricDirichletNeumannTheory U a hsym) (p q : Vec d) : responseJ U a p q = 1 / 2 * vecDot p (matVecMul (sigmaCoarse U a - sigmaStarCoarse U a) p) + 1 / 2 * vecDot (q - matVecMul (sigmaStarCoarse U a) p) (matVecMul (sigmaStarInvCoarse U a) (q - matVecMul (sigmaStarCoarse U a) p))

Accessor for the symmetric completed-square formula e.symmetric.J.completed.square.basic.definitions.

theorem HCPolySupport.Book.Ch02.ResponseSymmetricDirichletNeumannTheory.response_gap_eq {d : ℕ} {U : Domain d} {a : CoeffOn U} {hsym : a.IsSymmetric} (h : ResponseSymmetricDirichletNeumannTheory U a hsym) (p : Vec d) : responseJ U a p (matVecMul (sigmaStarCoarse U a) p) = 1 / 2 * vecDot p (matVecMul (sigmaCoarse U a - sigmaStarCoarse U a) p)

Accessor for the symmetric Dirichlet--Neumann gap formula e.symmetric.J.DN.gap.basic.definitions, in the public coarse-matrix form.