AlphaShiftedWeakSolution

Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.

Alpha-shifted divergence-form weak solutions

This file proves existence and uniqueness for the scalar-forced weak equation (α - div (a grad)) u = f on the canonical zero-trace value--gradient Hilbert carrier. It also constructs the canonical bounded linear solution operator and proves its weak characterization and coercivity norm bound.

The weak predicate depends only on the coefficient field. Ellipticity is used only in the Lax--Milgram proof.

noncomputable def DivergenceFormProcess.Form.coefficientBilin {d : ℕ} {U : Set (HCPolySupport.Vec d)} {a : HCPolySupport.CoeffField d} {lam Lam : ℝ} (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) : ZeroTraceSobolev U →L[ℝ] ZeroTraceSobolev U →L[ℝ] ℝ

The continuous coefficient-gradient bilinear form on zero-trace Sobolev functions.

Equations

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

noncomputable def DivergenceFormProcess.Form.massBilin {d : ℕ} {U : Set (HCPolySupport.Vec d)} : ZeroTraceSobolev U →L[ℝ] ZeroTraceSobolev U →L[ℝ] ℝ

The continuous L² mass bilinear form on zero-trace Sobolev functions.

Equations

• DivergenceFormProcess.Form.massBilin = ⋯.toContinuousLinearMap.bilinearComp DivergenceFormProcess.Form.ZeroTraceSobolev.toL2 DivergenceFormProcess.Form.ZeroTraceSobolev.toL2

noncomputable def DivergenceFormProcess.Form.shiftedBilin {d : ℕ} {U : Set (HCPolySupport.Vec d)} {a : HCPolySupport.CoeffField d} {lam Lam : ℝ} (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (alpha : ℝ) : ZeroTraceSobolev U →L[ℝ] ZeroTraceSobolev U →L[ℝ] ℝ

The continuous bilinear form for the shifted divergence-form operator.

Equations

• DivergenceFormProcess.Form.shiftedBilin hEll alpha = alpha • DivergenceFormProcess.Form.massBilin + DivergenceFormProcess.Form.coefficientBilin hEll

theorem DivergenceFormProcess.Form.shiftedBilin_apply {d : ℕ} {U : Set (HCPolySupport.Vec d)} {a : HCPolySupport.CoeffField d} {lam Lam : ℝ} (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (alpha : ℝ) (u v : ZeroTraceSobolev U) : ((shiftedBilin hEll alpha) u) v = alpha * inner ℝ (ZeroTraceSobolev.toL2 u) (ZeroTraceSobolev.toL2 v) + coefficientPairing a U (ZeroTraceSobolev.gradient u) (ZeroTraceSobolev.gradient v)

Evaluation of the shifted bilinear form in terms of the mass and coefficient pairings.

theorem DivergenceFormProcess.Form.shiftedBilin_lower_bound {d : ℕ} {U : Set (HCPolySupport.Vec d)} {a : HCPolySupport.CoeffField d} {lam Lam α : ℝ} (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (u : ZeroTraceSobolev U) : min α lam * ‖u‖ * ‖u‖ ≤ ((shiftedBilin hEll α) u) u

Coercive lower bound for the shifted bilinear form.

theorem DivergenceFormProcess.Form.shiftedBilin_coercive {d : ℕ} {U : Set (HCPolySupport.Vec d)} {a : HCPolySupport.CoeffField d} {lam Lam α : ℝ} (hα : 0 < α) (hlam : 0 < lam) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) : IsCoercive (shiftedBilin hEll α)

The shifted bilinear form is coercive for positive shift and ellipticity constant.

noncomputable def DivergenceFormProcess.Form.forcing {d : ℕ} {U : Set (HCPolySupport.Vec d)} (f : ↥(HCPolySupport.ScalarL2 U)) : ZeroTraceSobolev U →L[ℝ] ℝ

The continuous functional induced by an L² forcing term.

Equations

• DivergenceFormProcess.Form.forcing f = (InnerProductSpace.toDual ℝ ↥(HCPolySupport.ScalarL2 U)) f ∘SL DivergenceFormProcess.Form.ZeroTraceSobolev.toL2

noncomputable def DivergenceFormProcess.Form.forcingRep {d : ℕ} {U : Set (HCPolySupport.Vec d)} (f : ↥(HCPolySupport.ScalarL2 U)) : ZeroTraceSobolev U

The Riesz representative of the L² forcing functional in zero-trace Sobolev space.

Equations

• DivergenceFormProcess.Form.forcingRep f = (InnerProductSpace.toDual ℝ (DivergenceFormProcess.Form.ZeroTraceSobolev U)).symm (DivergenceFormProcess.Form.forcing f)

def DivergenceFormProcess.Form.IsAlphaShiftedWeakSolution {d : ℕ} (a : HCPolySupport.CoeffField d) (U : Set (HCPolySupport.Vec d)) (α : ℝ) (f : ↥(HCPolySupport.ScalarL2 U)) (u : ZeroTraceSobolev U) : Prop

The weak equation for (α - div (a grad)) u = f.

Equations

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

theorem DivergenceFormProcess.Form.existsUnique_isAlphaShiftedWeakSolution {d : ℕ} (a : HCPolySupport.CoeffField d) {U : Set (HCPolySupport.Vec d)} {α lam Lam : ℝ} (hα : 0 < α) (hlam : 0 < lam) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (f : ↥(HCPolySupport.ScalarL2 U)) : ∃! u : ZeroTraceSobolev U, IsAlphaShiftedWeakSolution a U α f u

Existence and uniqueness for the alpha-shifted divergence-form weak equation.

noncomputable def DivergenceFormProcess.Form.alphaShiftedSolution {d : ℕ} (a : HCPolySupport.CoeffField d) {U : Set (HCPolySupport.Vec d)} {α lam Lam : ℝ} (hα : 0 < α) (hlam : 0 < lam) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) : ↥(HCPolySupport.ScalarL2 U) →L[ℝ] ZeroTraceSobolev U

The canonical bounded linear solution operator for the alpha-shifted weak equation.

Equations

• DivergenceFormProcess.Form.alphaShiftedSolution a hα hlam hEll = ↑⋯.continuousLinearEquivOfBilin.symm ∘SL ContinuousLinearMap.adjoint DivergenceFormProcess.Form.ZeroTraceSobolev.toL2

theorem DivergenceFormProcess.Form.alphaShiftedSolution_isAlphaShiftedWeakSolution {d : ℕ} (a : HCPolySupport.CoeffField d) {U : Set (HCPolySupport.Vec d)} {α lam Lam : ℝ} (hα : 0 < α) (hlam : 0 < lam) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (f : ↥(HCPolySupport.ScalarL2 U)) : IsAlphaShiftedWeakSolution a U α f ((alphaShiftedSolution a hα hlam hEll) f)

The canonical operator solves the alpha-shifted weak equation.

theorem DivergenceFormProcess.Form.isAlphaShiftedWeakSolution_iff_eq {d : ℕ} (a : HCPolySupport.CoeffField d) {U : Set (HCPolySupport.Vec d)} {α lam Lam : ℝ} (hα : 0 < α) (hlam : 0 < lam) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (f : ↥(HCPolySupport.ScalarL2 U)) (u : ZeroTraceSobolev U) : IsAlphaShiftedWeakSolution a U α f u ↔ u = (alphaShiftedSolution a hα hlam hEll) f

A zero-trace Sobolev element solves the weak equation exactly when it is the value of the canonical solution operator.

noncomputable def DivergenceFormProcess.Form.alphaShiftedResolvent {d : ℕ} (a : HCPolySupport.CoeffField d) {U : Set (HCPolySupport.Vec d)} {α lam Lam : ℝ} (hα : 0 < α) (hlam : 0 < lam) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) : ↥(HCPolySupport.ScalarL2 U) →L[ℝ] ↥(HCPolySupport.ScalarL2 U)

The L² resolvent obtained by composing the canonical weak solution with its value component.

Equations

• DivergenceFormProcess.Form.alphaShiftedResolvent a hα hlam hEll = DivergenceFormProcess.Form.ZeroTraceSobolev.toL2 ∘SL DivergenceFormProcess.Form.alphaShiftedSolution a hα hlam hEll

@[simp]

theorem DivergenceFormProcess.Form.alphaShiftedResolvent_apply {d : ℕ} (a : HCPolySupport.CoeffField d) {U : Set (HCPolySupport.Vec d)} {α lam Lam : ℝ} (hα : 0 < α) (hlam : 0 < lam) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (f : ↥(HCPolySupport.ScalarL2 U)) : (alphaShiftedResolvent a hα hlam hEll) f = ZeroTraceSobolev.toL2 ((alphaShiftedSolution a hα hlam hEll) f)

theorem DivergenceFormProcess.Form.alphaShiftedSolution_resolvent_identity {d : ℕ} (a : HCPolySupport.CoeffField d) {U : Set (HCPolySupport.Vec d)} {α β lam Lam : ℝ} (hα : 0 < α) (hβ : 0 < β) (hlam : 0 < lam) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (f : ↥(HCPolySupport.ScalarL2 U)) : (alphaShiftedSolution a hα hlam hEll) f - (alphaShiftedSolution a hβ hlam hEll) f = (β - α) • (alphaShiftedSolution a hα hlam hEll) ((alphaShiftedResolvent a hβ hlam hEll) f)

The graph-carrier resolvent identity for two positive shifts.

theorem DivergenceFormProcess.Form.alphaShiftedResolvent_resolvent_identity {d : ℕ} (a : HCPolySupport.CoeffField d) {U : Set (HCPolySupport.Vec d)} {α β lam Lam : ℝ} (hα : 0 < α) (hβ : 0 < β) (hlam : 0 < lam) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) : alphaShiftedResolvent a hα hlam hEll - alphaShiftedResolvent a hβ hlam hEll = (β - α) • alphaShiftedResolvent a hα hlam hEll ∘SL alphaShiftedResolvent a hβ hlam hEll

The L² operator resolvent identity for two positive shifts.

theorem DivergenceFormProcess.Form.norm_alphaShiftedResolvent_apply_le {d : ℕ} (a : HCPolySupport.CoeffField d) {U : Set (HCPolySupport.Vec d)} {α lam Lam : ℝ} (hα : 0 < α) (hlam : 0 < lam) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (f : ↥(HCPolySupport.ScalarL2 U)) : ‖(alphaShiftedResolvent a hα hlam hEll) f‖ ≤ α⁻¹ * ‖f‖

The L² resolvent has the sharp pointwise bound supplied by its positive shift.

theorem DivergenceFormProcess.Form.norm_alphaShiftedSolution_apply_le {d : ℕ} (a : HCPolySupport.CoeffField d) {U : Set (HCPolySupport.Vec d)} {α lam Lam : ℝ} (hα : 0 < α) (hlam : 0 < lam) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (f : ↥(HCPolySupport.ScalarL2 U)) : ‖(alphaShiftedSolution a hα hlam hEll) f‖ ≤ (min α lam)⁻¹ * ‖f‖

The graph-norm estimate supplied by coercivity of the shifted form.