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

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

Common Symmetric Dirichlet-Neumann Helpers

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

theorem HCPolySupport.Internal.Ch02.BookCh02.memVectorL2_neg_matVecMul_const {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {a : CoeffField d} {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (p : Vec d) : MemVectorL2 U fun (x : Vec d) => -matVecMul (a x) p

theorem HCPolySupport.Internal.Ch02.BookCh02.memVectorL2_const_vec {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (q : Vec d) : MemVectorL2 U fun (x : Vec d) => q

theorem HCPolySupport.Internal.Ch02.BookCh02.potentialZeroTraceFieldOn_of_isPotentialZeroTraceOn {d : ℕ} {U : Set (Vec d)} {f : Vec d → Vec d} (hf : IsPotentialZeroTraceOn U f) : Book.Ch01.PotentialZeroTraceFieldOn U f

theorem HCPolySupport.Internal.Ch02.BookCh02.isSymmetricDirichletAdmissible_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) : Book.Ch02.IsSymmetricDirichletAdmissible U p u

theorem HCPolySupport.Internal.Ch02.BookCh02.exists_zeroTraceGradientAE_of_dirichlet_difference {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) : ∃ (θ : H10Function U.carrier), (w - u).grad =ᵐ[volumeMeasureOn U.carrier] θ.grad

theorem HCPolySupport.Internal.Ch02.BookCh02.meanZeroOn_of_h1MeanZeroFunction {d : ℕ} {U : Set (Vec d)} (u : H1MeanZeroFunction U) : MeanZeroOn U u.toH1Function.toFun

theorem HCPolySupport.Internal.Ch02.BookCh02.integrableOn_h1_coefficientEnergyDensity {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (u : H1Function U) : MeasureTheory.IntegrableOn (fun (x : Vec d) => vecDot (u.grad x) (matVecMul (a x) (u.grad x))) U MeasureTheory.volume

theorem HCPolySupport.Internal.Ch02.BookCh02.integrableOn_vecDot_const_h1Grad {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (q : Vec d) (u : H1Function U) : MeasureTheory.IntegrableOn (fun (x : Vec d) => vecDot q (u.grad x)) U MeasureTheory.volume

theorem HCPolySupport.Internal.Ch02.BookCh02.integrableOn_symmetricNeumannIntegrand_of_isEllipticFieldOn {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {a : CoeffField d} {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (q : Vec d) (u : H1Function U) : MeasureTheory.IntegrableOn (fun (x : Vec d) => vecDot q (u.grad x) - 1 / 2 * vecDot (u.grad x) (matVecMul (a x) (u.grad x))) U MeasureTheory.volume

theorem HCPolySupport.Internal.Ch02.BookCh02.integrableOn_symmetricDirichletIntegrand_of_isEllipticFieldOn {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (u : H1Function U) : MeasureTheory.IntegrableOn (fun (x : Vec d) => 1 / 2 * vecDot (u.grad x) (matVecMul (a x) (u.grad x))) U MeasureTheory.volume

theorem HCPolySupport.Internal.Ch02.BookCh02.h1_grad_eq_zero_ae_of_volumeAverage_energy_eq_zero {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) (hEll : IsEllipticFieldOn a.lam a.Lam U.carrier a.toCoeffField) (u : H1Function U.carrier) (hEnergyInt : MeasureTheory.IntegrableOn (fun (x : Vec d) => vecDot (u.grad x) (matVecMul (a.toCoeffField x) (u.grad x))) U.carrier MeasureTheory.volume) (hEnergyAvg : (volumeAverage U.carrier fun (x : Vec d) => vecDot (u.grad x) (matVecMul (a.toCoeffField x) (u.grad x))) = 0) : u.grad =ᵐ[volumeMeasureOn U.carrier] 0

theorem HCPolySupport.Internal.Ch02.BookCh02.h1AverageGradient_eq_of_grad_ae {d : ℕ} (U : Book.Ch02.Domain d) {u v : H1Function U.carrier} (hgrad : u.grad =ᵐ[volumeMeasureOn U.carrier] v.grad) : Book.Ch02.h1AverageGradient U u = Book.Ch02.h1AverageGradient U v

theorem HCPolySupport.Internal.Ch02.BookCh02.h1AverageFlux_eq_of_grad_ae {d : ℕ} (U : Book.Ch02.Domain d) (a : Book.Ch02.CoeffOn U) {u v : H1Function U.carrier} (hgrad : u.grad =ᵐ[volumeMeasureOn U.carrier] v.grad) : Book.Ch02.h1AverageFlux U a u = Book.Ch02.h1AverageFlux U a v

theorem HCPolySupport.Internal.Ch02.BookCh02.symmetricDirichletNu_eq_of_minimizer {d : ℕ} {U : Book.Ch02.Domain d} {a : Book.Ch02.CoeffOn U} {p : Vec d} {u : H1Function U.carrier} (hu : Book.Ch02.IsSymmetricDirichletMinimizer U a p u) : Book.Ch02.symmetricDirichletNu U a p = Book.Ch02.symmetricDirichletEnergyValue U a u

theorem HCPolySupport.Internal.Ch02.BookCh02.symmetricNeumannNu_eq_of_maximizer {d : ℕ} {U : Book.Ch02.Domain d} {a : Book.Ch02.CoeffOn U} {q : Vec d} {u : H1Function U.carrier} (hu : Book.Ch02.IsSymmetricNeumannMaximizer U a q u) : Book.Ch02.symmetricNeumannNu U a q = Book.Ch02.symmetricNeumannEnergyValue U a q u