Coarse-graining support: Support.PDE.DirichletRHS

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

Zero-trace Dirichlet problems with right-hand side

This file records the weak solution surface used by the deterministic coarse-grained Poincare-with-RHS argument. At this stage it packages the first-variation identity and the immediate consequences needed in Step 1 of the notes: invariance under subtracting constants from the forcing, zero average gradient of the zero-trace corrector, and the basic elliptic energy bound.

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

Weak zero-trace 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.integral_vecDot_const_zeroTraceGrad_eq_zero {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (u : H10Function U) (c : Vec d) : ∫ (x : Vec d) in U, vecDot c (u.grad x) = 0

theorem HCPolySupport.integral_vecDot_sub_const_zeroTraceGrad_eq {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {g : Vec d → Vec d} (hg : MemVectorL2 U g) (u : H10Function U) (c : Vec d) : ∫ (x : Vec d) in U, vecDot (g x - c) (u.grad x) = ∫ (x : Vec d) in U, vecDot (g x) (u.grad x)

theorem HCPolySupport.integral_vecDot_add_const_zeroTraceGrad_eq {d : ℕ} {U : Set (Vec d)} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] {g : Vec d → Vec d} (hg : MemVectorL2 U g) (u : H10Function U) (c : Vec d) : ∫ (x : Vec d) in U, vecDot (g x + c) (u.grad x) = ∫ (x : Vec d) in U, vecDot (g x) (u.grad x)

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

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

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

theorem HCPolySupport.IsZeroTraceDirichletRhsWeakSolution.averageGradient_eq_zero {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} {u : H10Function U} {g : Vec d → Vec d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (_h : IsZeroTraceDirichletRhsWeakSolution a U u g) : u.averageGradient = 0

theorem HCPolySupport.IsZeroTraceDirichletRhsWeakSolution.sub_const_iff {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} {u : H10Function U} {g : Vec d → Vec d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hmem : MemVectorL2 U g) (c : Vec d) : (IsZeroTraceDirichletRhsWeakSolution a U u fun (x : Vec d) => g x - c) ↔ IsZeroTraceDirichletRhsWeakSolution a U u g

theorem HCPolySupport.IsZeroTraceDirichletRhsWeakSolution.add_const_iff {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} {u : H10Function U} {g : Vec d → Vec d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (hmem : MemVectorL2 U g) (c : Vec d) : (IsZeroTraceDirichletRhsWeakSolution a U u fun (x : Vec d) => g x + c) ↔ IsZeroTraceDirichletRhsWeakSolution a U u g

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

theorem HCPolySupport.IsZeroTraceDirichletRhsWeakSolution.energy_identity_sub_const {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} {u : H10Function U} {g : Vec d → Vec d} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (h : IsZeroTraceDirichletRhsWeakSolution a U u g) (hmem : MemVectorL2 U g) (c : Vec d) : ∫ (x : Vec d) in U, vecDot (u.grad x) (matVecMul (a x) (u.grad x)) = ∫ (x : Vec d) in U, vecDot (g x - c) (u.grad x)

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

theorem HCPolySupport.IsZeroTraceDirichletRhsWeakSolution.energy_le_sub_const_rhs_pairing_of_isEllipticFieldOn {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} {u : H10Function U} {g : Vec d → Vec d} {lam Lam : ℝ} [MeasureTheory.IsFiniteMeasure (volumeMeasureOn U)] (h : IsZeroTraceDirichletRhsWeakSolution a U u g) (hEll : IsEllipticFieldOn lam Lam U a) (hmem : MemVectorL2 U g) (c : Vec d) : lam * ∫ (x : Vec d) in U, vecNormSq (u.grad x) ≤ ∫ (x : Vec d) in U, vecDot (g x - c) (u.grad x)

theorem HCPolySupport.IsZeroTraceDirichletRhsWeakSolution.of_grad_eq {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} {u : H10Function U} {g : Vec d → Vec d} {v : H10Function U} (hu : IsZeroTraceDirichletRhsWeakSolution a U u g) (hgrad : v.grad = u.grad) : IsZeroTraceDirichletRhsWeakSolution a U v g

theorem HCPolySupport.IsZeroTraceDirichletRhsWeakSolution.sub_zero {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} {u : H10Function U} {g : Vec d → Vec d} {v : H10Function U} {lam Lam : ℝ} (hu : IsZeroTraceDirichletRhsWeakSolution a U u g) (hv : IsZeroTraceDirichletRhsWeakSolution a U v g) (hEll : IsEllipticFieldOn lam Lam U a) : IsZeroTraceDirichletRhsWeakSolution a U (u - v) 0

theorem HCPolySupport.IsZeroTraceDirichletRhsWeakSolution.gradToVectorL2_eq_of_isEllipticFieldOn {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} {u : H10Function U} {g : Vec d → Vec d} {v : H10Function U} {lam Lam : ℝ} (hne : U.Nonempty) (hu : IsZeroTraceDirichletRhsWeakSolution a U u g) (hv : IsZeroTraceDirichletRhsWeakSolution a U v g) (hEll : IsEllipticFieldOn lam Lam U a) : u.gradToVectorL2 = v.gradToVectorL2

theorem HCPolySupport.IsZeroTraceDirichletRhsWeakSolution.gradToVectorL2_eq_of_isOpenBoundedConvexDomain {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} {u : H10Function U} {g : Vec d → Vec d} {v : H10Function U} {lam Lam : ℝ} (_hU : IsOpenBoundedConvexDomain U) (hne : U.Nonempty) (hu : IsZeroTraceDirichletRhsWeakSolution a U u g) (hv : IsZeroTraceDirichletRhsWeakSolution a U v g) (hEll : IsEllipticFieldOn lam Lam U a) : u.gradToVectorL2 = v.gradToVectorL2

theorem HCPolySupport.IsZeroTraceDirichletRhsWeakSolution.toScalarL2_eq_of_isOpenBoundedConvexDomain {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} {u : H10Function U} {g : Vec d → Vec d} {v : H10Function U} {lam Lam : ℝ} (hU : IsOpenBoundedConvexDomain U) [NeZero d] (hne : U.Nonempty) (hu : IsZeroTraceDirichletRhsWeakSolution a U u g) (hv : IsZeroTraceDirichletRhsWeakSolution a U v g) (hEll : IsEllipticFieldOn lam Lam U a) : u.toScalarL2 = v.toScalarL2

noncomputable def HCPolySupport.PotentialZeroTraceHilbert.closedSubmodule {d : ℕ} {U : Set (Vec d)} (M : PotentialSolenoidalL2Data U) : ClosedSubmodule ℝ ↥(HilbertVectorL2 U)

The Hilbert realization of the closed L² subspace modeling \Lpoto(U).

Equations

• HCPolySupport.PotentialZeroTraceHilbert.closedSubmodule M = ClosedSubmodule.comap (↑HCPolySupport.continuousLinearEquivVectorL2.symm) M.potentialZeroTrace

@[reducible, inline]

noncomputable abbrev HCPolySupport.PotentialZeroTraceHilbert.submodule {d : ℕ} {U : Set (Vec d)} (M : PotentialSolenoidalL2Data U) : Submodule ℝ ↥(HilbertVectorL2 U)

The submodule of Hilbert L² vector fields corresponding to the closed zero-trace potential subspace.

Equations

• HCPolySupport.PotentialZeroTraceHilbert.submodule M = ↑(HCPolySupport.PotentialZeroTraceHilbert.closedSubmodule M)

@[reducible, inline]

noncomputable abbrev HCPolySupport.PotentialZeroTraceHilbert.Space {d : ℕ} {U : Set (Vec d)} (M : PotentialSolenoidalL2Data U) : Type

The Hilbert-space carrier of the closed zero-trace potential submodule.

Equations

• HCPolySupport.PotentialZeroTraceHilbert.Space M = ↥(HCPolySupport.PotentialZeroTraceHilbert.submodule M)

@[instance_reducible]

noncomputable instance HCPolySupport.PotentialZeroTraceHilbert.instSeminormedAddCommGroup {d : ℕ} {U : Set (Vec d)} (M : PotentialSolenoidalL2Data U) : SeminormedAddCommGroup (Space M)

Equations

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

@[instance_reducible]

noncomputable instance HCPolySupport.PotentialZeroTraceHilbert.instNormedAddCommGroup {d : ℕ} {U : Set (Vec d)} (M : PotentialSolenoidalL2Data U) : NormedAddCommGroup (Space M)

Equations

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

@[instance_reducible]

noncomputable instance HCPolySupport.PotentialZeroTraceHilbert.instNormedSpace {d : ℕ} {U : Set (Vec d)} (M : PotentialSolenoidalL2Data U) : NormedSpace ℝ (Space M)

Equations

• HCPolySupport.PotentialZeroTraceHilbert.instNormedSpace M = { toModule := (HCPolySupport.PotentialZeroTraceHilbert.submodule M).module, norm_smul_le := ⋯ }

@[instance_reducible]

noncomputable instance HCPolySupport.PotentialZeroTraceHilbert.instInnerProductSpace {d : ℕ} {U : Set (Vec d)} (M : PotentialSolenoidalL2Data U) : InnerProductSpace ℝ (Space M)

Equations

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

instance HCPolySupport.PotentialZeroTraceHilbert.instCompleteSpace {d : ℕ} {U : Set (Vec d)} (M : PotentialSolenoidalL2Data U) : CompleteSpace (Space M)

@[reducible, inline]

abbrev HCPolySupport.PotentialZeroTraceHilbert.field {d : ℕ} {U : Set (Vec d)} {M : PotentialSolenoidalL2Data U} (z : Space M) : ↥(HilbertVectorL2 U)

The ambient Hilbert-vector L² field represented by a point of \Lpoto(U).

Equations

• HCPolySupport.PotentialZeroTraceHilbert.field z = ↑z

noncomputable def HCPolySupport.PotentialZeroTraceHilbert.vectorFieldCLM {d : ℕ} {U : Set (Vec d)} (M : PotentialSolenoidalL2Data U) : Space M →L[ℝ] ↥(VectorL2 U)

The ambient vector L² field represented by a point of \Lpoto(U).

Equations

• HCPolySupport.PotentialZeroTraceHilbert.vectorFieldCLM M = ↑HCPolySupport.continuousLinearEquivVectorL2.symm ∘SL (HCPolySupport.PotentialZeroTraceHilbert.submodule M).subtypeL

@[reducible, inline]

noncomputable abbrev HCPolySupport.PotentialZeroTraceHilbert.vectorField {d : ℕ} {U : Set (Vec d)} {M : PotentialSolenoidalL2Data U} (z : Space M) : ↥(VectorL2 U)

The algebraic vector L² field represented by an element of the zero-trace potential Hilbert space.

Equations

• HCPolySupport.PotentialZeroTraceHilbert.vectorField z = (HCPolySupport.PotentialZeroTraceHilbert.vectorFieldCLM M) z

@[simp]

theorem HCPolySupport.PotentialZeroTraceHilbert.vectorFieldCLM_apply {d : ℕ} {U : Set (Vec d)} (M : PotentialSolenoidalL2Data U) (z : Space M) : (vectorFieldCLM M) z = vectorField z

theorem HCPolySupport.PotentialZeroTraceHilbert.mem_potentialZeroTrace {d : ℕ} {U : Set (Vec d)} {M : PotentialSolenoidalL2Data U} (z : Space M) : vectorField z ∈ M.potentialZeroTrace

theorem HCPolySupport.PotentialZeroTraceHilbert.field_eq_toHilbertVectorL2OfVecField {d : ℕ} {U : Set (Vec d)} {M : PotentialSolenoidalL2Data U} (z : Space M) : field z = toHilbertVectorL2OfVecField ⋯

noncomputable def HCPolySupport.PotentialZeroTraceHilbert.ofH10Function {d : ℕ} {U : Set (Vec d)} (M : PotentialSolenoidalL2Data U) (u : H10Function U) : Space M

The Hilbert-space element corresponding to the gradient of an H¹₀ function.

Equations

• HCPolySupport.PotentialZeroTraceHilbert.ofH10Function M u = ⟨u.gradToHilbertVectorL2, ⋯⟩

@[simp]

theorem HCPolySupport.PotentialZeroTraceHilbert.vectorField_ofH10Function {d : ℕ} {U : Set (Vec d)} (M : PotentialSolenoidalL2Data U) (u : H10Function U) : vectorField (ofH10Function M u) = u.gradToVectorL2

noncomputable def HCPolySupport.PotentialZeroTraceHilbert.coeffFieldCLM {d : ℕ} {U : Set (Vec d)} (M : PotentialSolenoidalL2Data U) {a : CoeffField d} {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) : Space M →L[ℝ] ↥(HilbertVectorL2 U)

The coefficient-weighted field associated to a point of \Lpoto(U).

Equations

• HCPolySupport.PotentialZeroTraceHilbert.coeffFieldCLM M hEll = HCPolySupport.hilbertCoeffOperator hEll ∘SL (HCPolySupport.PotentialZeroTraceHilbert.submodule M).subtypeL

noncomputable def HCPolySupport.PotentialZeroTraceHilbert.coeffBilin {d : ℕ} {U : Set (Vec d)} (M : PotentialSolenoidalL2Data U) {a : CoeffField d} {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) : Space M →L[ℝ] Space M →L[ℝ] ℝ

The coefficient-weighted bilinear form on the Hilbert realization of \Lpoto(U).

Equations

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

@[simp]

theorem HCPolySupport.PotentialZeroTraceHilbert.coeffBilin_apply {d : ℕ} {U : Set (Vec d)} {M : PotentialSolenoidalL2Data U} {a : CoeffField d} {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (z w : Space M) : ((coeffBilin M hEll) z) w = inner ℝ ((hilbertCoeffOperator hEll) (field z)) (field w)

noncomputable def HCPolySupport.PotentialZeroTraceHilbert.forcingFunctionalCLM {d : ℕ} {U : Set (Vec d)} (M : PotentialSolenoidalL2Data U) {g : Vec d → Vec d} (hg : MemVectorL2 U g) : Space M →L[ℝ] ℝ

The forcing functional induced by g on the Hilbert realization of \Lpoto(U).

Equations

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

@[simp]

theorem HCPolySupport.PotentialZeroTraceHilbert.forcingFunctionalCLM_apply {d : ℕ} {U : Set (Vec d)} {M : PotentialSolenoidalL2Data U} {g : Vec d → Vec d} (hg : MemVectorL2 U g) (z : Space M) : (forcingFunctionalCLM M hg) z = inner ℝ (toHilbertVectorL2OfVecField hg) (field z)

theorem HCPolySupport.PotentialZeroTraceHilbert.coeffBilin_apply_eq_integral {d : ℕ} {U : Set (Vec d)} {M : PotentialSolenoidalL2Data U} {a : CoeffField d} {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (z w : Space M) : ((coeffBilin M hEll) z) w = ∫ (x : Vec d) in U, vecDot (matVecMul (a x) (↑↑(vectorField z) x)) (↑↑(vectorField w) x)

theorem HCPolySupport.PotentialZeroTraceHilbert.forcingFunctionalCLM_apply_eq_integral {d : ℕ} {U : Set (Vec d)} {M : PotentialSolenoidalL2Data U} {g : Vec d → Vec d} (hg : MemVectorL2 U g) (z : Space M) : (forcingFunctionalCLM M hg) z = ∫ (x : Vec d) in U, vecDot (g x) (↑↑(vectorField z) x)

theorem HCPolySupport.PotentialZeroTraceHilbert.coeffBilin_self_ge_lam_mul_norm_sq {d : ℕ} {U : Set (Vec d)} {M : PotentialSolenoidalL2Data U} {a : CoeffField d} {lam Lam : ℝ} (hEll : IsEllipticFieldOn lam Lam U a) (z : Space M) : lam * ‖z‖ ^ 2 ≤ ((coeffBilin M hEll) z) z

theorem HCPolySupport.PotentialZeroTraceHilbert.isCoercive_coeffBilin {d : ℕ} {U : Set (Vec d)} {M : PotentialSolenoidalL2Data U} {a : CoeffField d} {lam Lam : ℝ} (hne : U.Nonempty) (hEll : IsEllipticFieldOn lam Lam U a) : IsCoercive (coeffBilin M hEll)

noncomputable def HCPolySupport.PotentialZeroTraceHilbert.forcingRieszMap {d : ℕ} {U : Set (Vec d)} (M : PotentialSolenoidalL2Data U) : (Space M →L[ℝ] ℝ) → Space M

The Riesz representative in the zero-trace potential Hilbert space of a continuous real linear functional.

Equations

• HCPolySupport.PotentialZeroTraceHilbert.forcingRieszMap M ℓ = (InnerProductSpace.toDual ℝ (HCPolySupport.PotentialZeroTraceHilbert.Space M)).symm ℓ

theorem HCPolySupport.PotentialZeroTraceHilbert.inner_forcingRieszMap_apply {d : ℕ} {U : Set (Vec d)} (M : PotentialSolenoidalL2Data U) (ℓ : Space M →L[ℝ] ℝ) (z : Space M) : inner ℝ (forcingRieszMap M ℓ) z = ℓ z

noncomputable def HCPolySupport.PotentialZeroTraceHilbert.forcingRieszRep {d : ℕ} {U : Set (Vec d)} (M : PotentialSolenoidalL2Data U) {g : Vec d → Vec d} (hg : MemVectorL2 U g) : Space M

The Riesz representative of the L² pairing with the forcing vector field g on the zero-trace potential Hilbert space.

Equations

• HCPolySupport.PotentialZeroTraceHilbert.forcingRieszRep M hg = HCPolySupport.PotentialZeroTraceHilbert.forcingRieszMap M (HCPolySupport.PotentialZeroTraceHilbert.forcingFunctionalCLM M hg)

theorem HCPolySupport.PotentialZeroTraceHilbert.inner_forcingRieszRep_apply {d : ℕ} {U : Set (Vec d)} (M : PotentialSolenoidalL2Data U) {g : Vec d → Vec d} (hg : MemVectorL2 U g) (z : Space M) : inner ℝ (forcingRieszRep M hg) z = (forcingFunctionalCLM M hg) z

noncomputable def HCPolySupport.PotentialZeroTraceHilbert.coeffProblemSolution {d : ℕ} {U : Set (Vec d)} (M : PotentialSolenoidalL2Data U) {a : CoeffField d} {g : Vec d → Vec d} {lam Lam : ℝ} (hg : MemVectorL2 U g) (hne : U.Nonempty) (hEll : IsEllipticFieldOn lam Lam U a) : Space M

The unique Hilbert-space element of \Lpoto(U) solving the coefficient problem with forcing g.

Equations

• HCPolySupport.PotentialZeroTraceHilbert.coeffProblemSolution M hg hne hEll = ⋯.continuousLinearEquivOfBilin.symm (HCPolySupport.PotentialZeroTraceHilbert.forcingRieszRep M hg)

theorem HCPolySupport.PotentialZeroTraceHilbert.coeffBilin_coeffProblemSolution_apply {d : ℕ} {U : Set (Vec d)} (M : PotentialSolenoidalL2Data U) {a : CoeffField d} {g : Vec d → Vec d} {lam Lam : ℝ} (hg : MemVectorL2 U g) (hne : U.Nonempty) (hEll : IsEllipticFieldOn lam Lam U a) (z : Space M) : ((coeffBilin M hEll) (coeffProblemSolution M hg hne hEll)) z = (forcingFunctionalCLM M hg) z

noncomputable def HCPolySupport.vectorPairingCLM {d : ℕ} {U : Set (Vec d)} {g : Vec d → Vec d} (hg : MemVectorL2 U g) : ↥(VectorL2 U) →L[ℝ] ℝ

The continuous linear functional on vector L² fields given by the integral of their dot product with g over U.

Equations

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

theorem HCPolySupport.exists_isZeroTraceDirichletRhsWeakSolution_of_potentialZeroTraceClosureRealization {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} {g : Vec d → Vec d} {lam Lam : ℝ} (hg : MemVectorL2 U g) (hRealize : PotentialSolenoidalL2Data.HasPotentialZeroTraceClosureRealization U) (hne : U.Nonempty) (hEll : IsEllipticFieldOn lam Lam U a) : ∃ (v : H10Function U), IsZeroTraceDirichletRhsWeakSolution a U v g

noncomputable def HCPolySupport.zeroTraceDirichletRightHandSideSolutionOfClosureRealization {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} {g : Vec d → Vec d} {lam Lam : ℝ} (hg : MemVectorL2 U g) (hRealize : PotentialSolenoidalL2Data.HasPotentialZeroTraceClosureRealization U) (hne : U.Nonempty) (hEll : IsEllipticFieldOn lam Lam U a) : H10Function U

A chosen zero-trace Dirichlet weak solution under the abstract zero-trace-potential closure realization hypothesis.

Equations

• HCPolySupport.zeroTraceDirichletRightHandSideSolutionOfClosureRealization hg hRealize hne hEll = Classical.choose ⋯

theorem HCPolySupport.isZeroTraceDirichletRhsWeakSolution_zeroTraceDirichletRhsProblemSolution {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} {g : Vec d → Vec d} {lam Lam : ℝ} (hg : MemVectorL2 U g) (hRealize : PotentialSolenoidalL2Data.HasPotentialZeroTraceClosureRealization U) (hne : U.Nonempty) (hEll : IsEllipticFieldOn lam Lam U a) : IsZeroTraceDirichletRhsWeakSolution a U (zeroTraceDirichletRightHandSideSolutionOfClosureRealization hg hRealize hne hEll) g

theorem HCPolySupport.gradToVectorL2_eq_zeroTraceDirichletRhsProblemSolution_of_potentialZeroTraceClosureRealization {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} {u : H10Function U} {g : Vec d → Vec d} {lam Lam : ℝ} (hg : MemVectorL2 U g) (hRealize : PotentialSolenoidalL2Data.HasPotentialZeroTraceClosureRealization U) (hne : U.Nonempty) (hu : IsZeroTraceDirichletRhsWeakSolution a U u g) (hEll : IsEllipticFieldOn lam Lam U a) : u.gradToVectorL2 = (zeroTraceDirichletRightHandSideSolutionOfClosureRealization hg hRealize hne hEll).gradToVectorL2

theorem HCPolySupport.exists_isZeroTraceDirichletRhsWeakSolution_of_potentialZeroTrace {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} {f g : Vec d → Vec d} (hfirst : ∀ (φ : H10Function U), ∫ (x : Vec d) in U, vecDot (matVecMul (a x) (f x)) (φ.grad x) = ∫ (x : Vec d) in U, vecDot (g x) (φ.grad x)) (hpot : IsPotentialZeroTraceOn U f) : ∃ (v : H10Function U), IsZeroTraceDirichletRhsWeakSolution a U v g

theorem HCPolySupport.exists_isZeroTraceDirichletRhsWeakSolution_of_firstVariation_eq_integral_of_isPotentialZeroTraceOn {d : ℕ} {a : CoeffField d} {U : Set (Vec d)} {u : H1Function U} {g : Vec d → Vec d} (hfirst : ∀ (φ : H10Function U), ∫ (x : Vec d) in U, vecDot (matVecMul (a x) (u.grad x)) (φ.grad x) = ∫ (x : Vec d) in U, vecDot (g x) (φ.grad x)) (hpot : IsPotentialZeroTraceOn U u.grad) : ∃ (v : H10Function U), IsZeroTraceDirichletRhsWeakSolution a U v g