Coarse-graining support: Support.PDE.NeumannRHS

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

Mean-zero Neumann problems with right-hand side

This file starts the mean-zero Neumann-side RHS development. The current layer packages the weak formulation, the coefficient-weighted Lax-Milgram solution, the energy identity, the basic elliptic energy estimate, and the qualitative uniqueness statement once a mean-zero coercive estimate is supplied.

def HCPolySupport.IsMeanZeroNeumannRhsWeakSolution {d : ℕ} (a : CoeffField d) (U : Set (Vec d)) (u : H1MeanZeroFunction U) (g : Vec d → Vec d) : Prop

Weak mean-zero Neumann formulation of - div (a grad u) = div g on U.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.integrableOn_vecNormSq_meanZeroGrad {d : ℕ} {U : Set (Vec d)} (u : H1MeanZeroFunction U) : MeasureTheory.IntegrableOn (fun (x : Vec d) => vecNormSq (u.toH1Function.grad x)) U MeasureTheory.volume

theorem HCPolySupport.integrableOn_dirichletEnergyDensity_of_isEllipticFieldOn_meanZero {d : ℕ} {U : Set (Vec d)} {a : CoeffField d} {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (u : H1MeanZeroFunction U) : MeasureTheory.IntegrableOn (fun (x : Vec d) => vecDot (u.toH1Function.grad x) (matVecMul (a x) (u.toH1Function.grad x))) U MeasureTheory.volume

noncomputable def HCPolySupport.H1CoerciveHilbert.coeffGradientCLM {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {a : CoeffField d} {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) : H1CoerciveHilbertSpace →L[ℝ] ↥(HilbertVectorL2 U)

The coefficient-weighted gradient projection on the coercive Hilbert graph.

Equations

• HCPolySupport.H1CoerciveHilbert.coeffGradientCLM hEll = HCPolySupport.hilbertCoeffOperator hEll ∘SL HCPolySupport.H1CoerciveHilbert.gradientCLM

noncomputable def HCPolySupport.H1CoerciveHilbert.coeffGradientBilin {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {a : CoeffField d} {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) : H1CoerciveHilbertSpace →L[ℝ] H1CoerciveHilbertSpace →L[ℝ] ℝ

The coefficient-weighted gradient bilinear form on the coercive Hilbert graph.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem HCPolySupport.H1CoerciveHilbert.coeffGradientBilin_apply {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {a : CoeffField d} {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (z w : H1CoerciveHilbertSpace) : ((coeffGradientBilin hEll) z) w = inner ℝ ((hilbertCoeffOperator hEll) (gradient z)) (gradient w)

theorem HCPolySupport.H1CoerciveHilbert.coeffGradientBilin_apply_toH1CoerciveHilbertSpace {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {a : CoeffField d} {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (u v : H1MeanZeroFunction U) : ((coeffGradientBilin hEll) u.toH1CoerciveHilbertSpace) v.toH1CoerciveHilbertSpace = ∫ (x : Vec d) in U, vecDot (matVecMul (a x) (u.toH1Function.grad x)) (v.toH1Function.grad x)

theorem HCPolySupport.H1CoerciveHilbert.coeffGradientBilin_apply_eq_integral {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {a : CoeffField d} {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (z w : H1CoerciveHilbertSpace) : ((coeffGradientBilin hEll) z) w = ∫ (x : Vec d) in U, vecDot (matVecMul (a x) ((toH1MeanZeroFunction z).toH1Function.grad x)) ((toH1MeanZeroFunction w).toH1Function.grad x)

theorem HCPolySupport.H1CoerciveHilbert.coeffGradientBilin_self_ge_lam_mul_norm_gradient_sq {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {a : CoeffField d} {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (z : H1CoerciveHilbertSpace) : lam * ‖gradient z‖ ^ 2 ≤ ((coeffGradientBilin hEll) z) z

theorem HCPolySupport.H1CoerciveHilbert.isCoercive_coeffGradientBilin {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {a : CoeffField d} {lam Lam : ℝ} (hC : H1CoerciveEstimate U) (hne : U.Nonempty) (hEll : IsEllipticFieldOn lam Lam U a) : IsCoercive (coeffGradientBilin hEll)

noncomputable def HCPolySupport.H1CoerciveHilbert.coeffGradientProblemSolution {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {a : CoeffField d} {lam Lam : ℝ} {f : Vec d → Vec d} (hf : MemVectorL2 U f) (hC : H1CoerciveEstimate U) (hne : U.Nonempty) (hEll : IsEllipticFieldOn lam Lam U a) : H1CoerciveHilbertSpace

The unique coercive-Hilbert graph element solving the coefficient-weighted gradient problem with forcing f.

Equations

• HCPolySupport.H1CoerciveHilbert.coeffGradientProblemSolution hf hC hne hEll = ⋯.continuousLinearEquivOfBilin.symm (HCPolySupport.H1CoerciveHilbert.forcingRieszRep hf)

theorem HCPolySupport.H1CoerciveHilbert.coeffGradientBilin_coeffGradientProblemSolution_apply {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {a : CoeffField d} {lam Lam : ℝ} {f : Vec d → Vec d} (hf : MemVectorL2 U f) (hC : H1CoerciveEstimate U) (hne : U.Nonempty) (hEll : IsEllipticFieldOn lam Lam U a) (z : H1CoerciveHilbertSpace) : ((coeffGradientBilin hEll) (coeffGradientProblemSolution hf hC hne hEll)) z = (forcingFunctionalCLM hf) z

noncomputable def HCPolySupport.H1MeanZeroFunction.coeffGradientProblemSolution {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {a : CoeffField d} {lam Lam : ℝ} {f : Vec d → Vec d} (hf : MemVectorL2 U f) (hC : H1CoerciveEstimate U) (hne : U.Nonempty) (hEll : IsEllipticFieldOn lam Lam U a) : H1MeanZeroFunction U

The mean-zero H¹ weak solution represented by the coefficient-weighted coercive Hilbert graph solution.

Equations

• One or more equations did not get rendered due to their size.

theorem HCPolySupport.H1MeanZeroFunction.coeffGradientProblemSolution_firstVariation_eq_integral {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {a : CoeffField d} {lam Lam : ℝ} {f : Vec d → Vec d} (hf : MemVectorL2 U f) (hC : H1CoerciveEstimate U) (hne : U.Nonempty) (hEll : IsEllipticFieldOn lam Lam U a) (u : H1MeanZeroFunction U) : ∫ (x : Vec d) in U, vecDot (matVecMul (a x) ((coeffGradientProblemSolution hf hC hne hEll).toH1Function.grad x)) (u.toH1Function.grad x) = ∫ (x : Vec d) in U, vecDot (f x) (u.toH1Function.grad x)

theorem HCPolySupport.H1Function.coeffGradientProblemSolution_firstVariation_eq_integral {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {a : CoeffField d} {lam Lam : ℝ} {f : Vec d → Vec d} (hf : MemVectorL2 U f) (hC : H1CoerciveEstimate U) (hne : U.Nonempty) (hEll : IsEllipticFieldOn lam Lam U a) (u : H1Function U) : ∫ (x : Vec d) in U, vecDot (matVecMul (a x) ((H1MeanZeroFunction.coeffGradientProblemSolution hf hC hne hEll).toH1Function.grad x)) (u.grad x) = ∫ (x : Vec d) in U, vecDot (f x) (u.grad x)

theorem HCPolySupport.IsMeanZeroNeumannRhsWeakSolution.energy_identity {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} {u : H1MeanZeroFunction U} {g : Vec d → Vec d} (h : IsMeanZeroNeumannRhsWeakSolution a U u g) : ∫ (x : Vec d) in U, vecDot (u.toH1Function.grad x) (matVecMul (a x) (u.toH1Function.grad x)) = ∫ (x : Vec d) in U, vecDot (g x) (u.toH1Function.grad x)

theorem HCPolySupport.IsMeanZeroNeumannRhsWeakSolution.energy_le_rhs_pairing_of_isEllipticFieldOn {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} {u : H1MeanZeroFunction U} {g : Vec d → Vec d} {lam Lam : ℝ} (h : IsMeanZeroNeumannRhsWeakSolution a U u g) (hEll : IsEllipticFieldOn lam Lam U a) : lam * ∫ (x : Vec d) in U, vecNormSq (u.toH1Function.grad x) ≤ ∫ (x : Vec d) in U, vecDot (g x) (u.toH1Function.grad x)

theorem HCPolySupport.IsMeanZeroNeumannRhsWeakSolution.residual_zeroNormalTrace {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {u : H1MeanZeroFunction U} {g : Vec d → Vec d} {lam Lam : ℝ} (h : IsMeanZeroNeumannRhsWeakSolution a U u g) (hEll : IsEllipticFieldOn lam Lam U a) (hg : MemVectorL2 U g) : IsSolenoidalZeroNormalTraceOn U fun (x : Vec d) => matVecMul (a x) (u.toH1Function.grad x) - g x

The residual flux of a mean-zero Neumann RHS weak solution is solenoidal with zero normal trace. This is the Neumann counterpart of the Dirichlet RHS residual bridge, using the mean-zero normalization of an arbitrary H¹ test function.

theorem HCPolySupport.IsMeanZeroNeumannRhsWeakSolution.sub_zero {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {u : H1MeanZeroFunction U} {g : Vec d → Vec d} {v : H1MeanZeroFunction U} {lam Lam : ℝ} (hu : IsMeanZeroNeumannRhsWeakSolution a U u g) (hv : IsMeanZeroNeumannRhsWeakSolution a U v g) (hEll : IsEllipticFieldOn lam Lam U a) : IsMeanZeroNeumannRhsWeakSolution a U (u - v) 0

theorem HCPolySupport.IsMeanZeroNeumannRhsWeakSolution.gradToVectorL2_eq_of_isEllipticFieldOn {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {u : H1MeanZeroFunction U} {g : Vec d → Vec d} {v : H1MeanZeroFunction U} {lam Lam : ℝ} (hne : U.Nonempty) (hu : IsMeanZeroNeumannRhsWeakSolution a U u g) (hv : IsMeanZeroNeumannRhsWeakSolution a U v g) (hEll : IsEllipticFieldOn lam Lam U a) : u.gradToVectorL2 = v.gradToVectorL2

theorem HCPolySupport.IsMeanZeroNeumannRhsWeakSolution.toScalarL2_eq_of_h1CoerciveEstimate {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {u : H1MeanZeroFunction U} {g : Vec d → Vec d} {v : H1MeanZeroFunction U} {lam Lam : ℝ} (hC : H1CoerciveEstimate U) (hne : U.Nonempty) (hu : IsMeanZeroNeumannRhsWeakSolution a U u g) (hv : IsMeanZeroNeumannRhsWeakSolution a U v g) (hEll : IsEllipticFieldOn lam Lam U a) : u.toScalarL2 = v.toScalarL2

theorem HCPolySupport.isMeanZeroNeumannRhsWeakSolution_coeffGradientProblemSolution_of_h1CoerciveEstimate {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {g : Vec d → Vec d} {lam Lam : ℝ} (hg : MemVectorL2 U g) (hC : H1CoerciveEstimate U) (hne : U.Nonempty) (hEll : IsEllipticFieldOn lam Lam U a) : IsMeanZeroNeumannRhsWeakSolution a U (H1MeanZeroFunction.coeffGradientProblemSolution hg hC hne hEll) g

theorem HCPolySupport.gradToVectorL2_eq_coeffGradientProblemSolution_of_h1CoerciveEstimate {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {u : H1MeanZeroFunction U} {g : Vec d → Vec d} {lam Lam : ℝ} (hg : MemVectorL2 U g) (hC : H1CoerciveEstimate U) (hne : U.Nonempty) (hu : IsMeanZeroNeumannRhsWeakSolution a U u g) (hEll : IsEllipticFieldOn lam Lam U a) : u.gradToVectorL2 = (H1MeanZeroFunction.coeffGradientProblemSolution hg hC hne hEll).gradToVectorL2

theorem HCPolySupport.toScalarL2_eq_coeffGradientProblemSolution_of_h1CoerciveEstimate {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {u : H1MeanZeroFunction U} {g : Vec d → Vec d} {lam Lam : ℝ} (hg : MemVectorL2 U g) (hC : H1CoerciveEstimate U) (hne : U.Nonempty) (hu : IsMeanZeroNeumannRhsWeakSolution a U u g) (hEll : IsEllipticFieldOn lam Lam U a) : u.toScalarL2 = (H1MeanZeroFunction.coeffGradientProblemSolution hg hC hne hEll).toScalarL2

theorem HCPolySupport.exists_isMeanZeroNeumannRhsWeakSolution_of_h1CoerciveEstimate {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {g : Vec d → Vec d} {lam Lam : ℝ} (hg : MemVectorL2 U g) (hC : H1CoerciveEstimate U) (hne : U.Nonempty) (hEll : IsEllipticFieldOn lam Lam U a) : ∃ (u : H1MeanZeroFunction U), IsMeanZeroNeumannRhsWeakSolution a U u g