PotentialWeakSolution

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

Weak solutions with a bounded nonnegative potential

This module adds a bounded measurable zeroth-order potential to the shifted divergence-form equation. The solution is constructed on the existing ZeroTraceSobolev graph carrier by Lax--Milgram.

def DivergenceFormProcess.Form.IsBoundedNonnegativePotential {d : ℕ} (U : Set (HCPolySupport.Vec d)) (q : HCPolySupport.Vec d → ℝ) (C : ℝ) : Prop

A measurable potential which lies between zero and a finite constant almost everywhere on the domain.

Equations

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

theorem DivergenceFormProcess.Form.boundedPotential_memLp {d : ℕ} {U : Set (HCPolySupport.Vec d)} {C : ℝ} {q : HCPolySupport.Vec d → ℝ} (hq : IsBoundedNonnegativePotential U q C) : MeasureTheory.MemLp q ⊤ (HCPolySupport.volumeMeasureOn U)

noncomputable def DivergenceFormProcess.Form.boundedPotentialLp {d : ℕ} {U : Set (HCPolySupport.Vec d)} {C : ℝ} (q : HCPolySupport.Vec d → ℝ) (hq : IsBoundedNonnegativePotential U q C) : ↥(MeasureTheory.Lp ℝ ⊤ (HCPolySupport.volumeMeasureOn U))

The L∞ class of a bounded nonnegative potential on the domain.

Equations

• DivergenceFormProcess.Form.boundedPotentialLp q hq = MeasureTheory.MemLp.toLp q ⋯

noncomputable def DivergenceFormProcess.Form.potentialMul {d : ℕ} {U : Set (HCPolySupport.Vec d)} {C : ℝ} (q : HCPolySupport.Vec d → ℝ) (hq : IsBoundedNonnegativePotential U q C) : ↥(HCPolySupport.ScalarL2 U) →L[ℝ] ↥(HCPolySupport.ScalarL2 U)

Multiplication by a bounded nonnegative potential as a bounded operator on scalar L².

Equations

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

theorem DivergenceFormProcess.Form.potentialMul_coeFn {d : ℕ} {U : Set (HCPolySupport.Vec d)} {C : ℝ} (q : HCPolySupport.Vec d → ℝ) (hq : IsBoundedNonnegativePotential U q C) (f : ↥(HCPolySupport.ScalarL2 U)) : ↑↑((potentialMul q hq) f) =ᵐ[HCPolySupport.volumeMeasureOn U] fun (x : HCPolySupport.Vec d) => q x * ↑↑f x

Multiplication by the potential agrees almost everywhere with pointwise multiplication.

theorem DivergenceFormProcess.Form.inner_potentialMul_eq_integral {d : ℕ} {U : Set (HCPolySupport.Vec d)} {C : ℝ} (q : HCPolySupport.Vec d → ℝ) (hq : IsBoundedNonnegativePotential U q C) (f g : ↥(HCPolySupport.ScalarL2 U)) : inner ℝ ((potentialMul q hq) f) g = ∫ (x : HCPolySupport.Vec d), q x * ↑↑f x * ↑↑g x ∂HCPolySupport.volumeMeasureOn U

The scalar inner product against a potential multiple is the corresponding triple-product integral.

noncomputable def DivergenceFormProcess.Form.shiftedPotentialBilin {d : ℕ} (a : HCPolySupport.CoeffField d) (α : ℝ) (q : HCPolySupport.Vec d → ℝ) (U : Set (HCPolySupport.Vec d)) (u v : ZeroTraceSobolev U) : ℝ

The unbundled shifted weak form with an additional potential term.

Equations

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

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

The weak equation for a shifted divergence-form operator with potential.

Equations

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

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

The continuous bilinear form of the shifted divergence-form operator with a bounded nonnegative potential.

Equations

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

theorem DivergenceFormProcess.Form.potentialBilin_apply {d : ℕ} {U : Set (HCPolySupport.Vec d)} {a : HCPolySupport.CoeffField d} {α lam Lam C : ℝ} (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (q : HCPolySupport.Vec d → ℝ) (hq : IsBoundedNonnegativePotential U q C) (u v : ZeroTraceSobolev U) : ((potentialBilin hEll q hq) u) v = shiftedPotentialBilin a α q U u v

Evaluation of the bundled potential form agrees with the stated weak form.

theorem DivergenceFormProcess.Form.potentialBilin_coercive {d : ℕ} {U : Set (HCPolySupport.Vec d)} {a : HCPolySupport.CoeffField d} {α lam Lam C : ℝ} {q : HCPolySupport.Vec d → ℝ} (hα : 0 < α) (hlam : 0 < lam) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (hq : IsBoundedNonnegativePotential U q C) : IsCoercive (potentialBilin hEll q hq)

theorem DivergenceFormProcess.Form.existsUnique_isPotentialWeakSolution {d : ℕ} (a : HCPolySupport.CoeffField d) {U : Set (HCPolySupport.Vec d)} {α lam Lam C : ℝ} (hα : 0 < α) (hlam : 0 < lam) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (q : HCPolySupport.Vec d → ℝ) (hq : IsBoundedNonnegativePotential U q C) (f : ↥(HCPolySupport.ScalarL2 U)) : ∃! u : ZeroTraceSobolev U, IsPotentialWeakSolution a α q U u f

Existence and uniqueness for the weak equation with bounded nonnegative potential.

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

The canonical bounded linear weak-solution operator with potential.

Equations

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

theorem DivergenceFormProcess.Form.potentialSolution_isPotentialWeakSolution {d : ℕ} (a : HCPolySupport.CoeffField d) {U : Set (HCPolySupport.Vec d)} {α lam Lam C : ℝ} (hα : 0 < α) (hlam : 0 < lam) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (q : HCPolySupport.Vec d → ℝ) (hq : IsBoundedNonnegativePotential U q C) (f : ↥(HCPolySupport.ScalarL2 U)) : IsPotentialWeakSolution a α q U ((potentialSolution a hα hlam hEll q hq) f) f

The canonical operator solves the weak equation with potential.

theorem DivergenceFormProcess.Form.isPotentialWeakSolution_iff_eq {d : ℕ} (a : HCPolySupport.CoeffField d) {U : Set (HCPolySupport.Vec d)} {α lam Lam C : ℝ} (hα : 0 < α) (hlam : 0 < lam) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (q : HCPolySupport.Vec d → ℝ) (hq : IsBoundedNonnegativePotential U q C) (f : ↥(HCPolySupport.ScalarL2 U)) (u : ZeroTraceSobolev U) : IsPotentialWeakSolution a α q U u f ↔ u = (potentialSolution a hα hlam hEll q hq) f

A weak solution with potential is exactly the canonical solution.

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

The scalar L² resolvent with bounded nonnegative potential.

Equations

• DivergenceFormProcess.Form.potentialResolvent a hα hlam hEll q hq = DivergenceFormProcess.Form.ZeroTraceSobolev.toL2 ∘SL DivergenceFormProcess.Form.potentialSolution a hα hlam hEll q hq

@[simp]

theorem DivergenceFormProcess.Form.potentialResolvent_apply {d : ℕ} (a : HCPolySupport.CoeffField d) {U : Set (HCPolySupport.Vec d)} {α lam Lam C : ℝ} (hα : 0 < α) (hlam : 0 < lam) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (q : HCPolySupport.Vec d → ℝ) (hq : IsBoundedNonnegativePotential U q C) (f : ↥(HCPolySupport.ScalarL2 U)) : (potentialResolvent a hα hlam hEll q hq) f = ZeroTraceSobolev.toL2 ((potentialSolution a hα hlam hEll q hq) f)

The potential resolvent is the value component of the weak solution.

theorem DivergenceFormProcess.Form.isBoundedNonnegativePotential_zero {d : ℕ} (U : Set (HCPolySupport.Vec d)) : IsBoundedNonnegativePotential U (fun (x : HCPolySupport.Vec d) => 0) 0

The identically zero function is a bounded nonnegative potential.

theorem DivergenceFormProcess.Form.potentialSolution_zero_potential {d : ℕ} (a : HCPolySupport.CoeffField d) {U : Set (HCPolySupport.Vec d)} {α lam Lam C : ℝ} (hα : 0 < α) (hlam : 0 < lam) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (hq : IsBoundedNonnegativePotential U (fun (x : HCPolySupport.Vec d) => 0) C) (f : ↥(HCPolySupport.ScalarL2 U)) : (potentialSolution a hα hlam hEll (fun (x : HCPolySupport.Vec d) => 0) hq) f = (alphaShiftedSolution a hα hlam hEll) f

For the zero potential the weak-solution operator with potential is the alpha-shifted weak-solution operator.

theorem DivergenceFormProcess.Form.potentialResolvent_zero_potential {d : ℕ} (a : HCPolySupport.CoeffField d) {U : Set (HCPolySupport.Vec d)} {α lam Lam C : ℝ} (hα : 0 < α) (hlam : 0 < lam) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (hq : IsBoundedNonnegativePotential U (fun (x : HCPolySupport.Vec d) => 0) C) (f : ↥(HCPolySupport.ScalarL2 U)) : (potentialResolvent a hα hlam hEll (fun (x : HCPolySupport.Vec d) => 0) hq) f = (alphaShiftedResolvent a hα hlam hEll) f

For the zero potential the scalar resolvent with potential is the alpha-shifted resolvent.

theorem DivergenceFormProcess.Form.potentialSolution_resolvent_identity {d : ℕ} (a : HCPolySupport.CoeffField d) {U : Set (HCPolySupport.Vec d)} {α β lam Lam C : ℝ} (hα : 0 < α) (hβ : 0 < β) (hlam : 0 < lam) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (q : HCPolySupport.Vec d → ℝ) (hq : IsBoundedNonnegativePotential U q C) (f : ↥(HCPolySupport.ScalarL2 U)) : (potentialSolution a hα hlam hEll q hq) f - (potentialSolution a hβ hlam hEll q hq) f = (β - α) • (potentialSolution a hα hlam hEll q hq) ((potentialResolvent a hβ hlam hEll q hq) f)

Resolvent identity in the positive shift for a fixed potential.

theorem DivergenceFormProcess.Form.potentialResolvent_resolvent_identity {d : ℕ} (a : HCPolySupport.CoeffField d) {U : Set (HCPolySupport.Vec d)} {α β lam Lam C : ℝ} (hα : 0 < α) (hβ : 0 < β) (hlam : 0 < lam) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (q : HCPolySupport.Vec d → ℝ) (hq : IsBoundedNonnegativePotential U q C) : potentialResolvent a hα hlam hEll q hq - potentialResolvent a hβ hlam hEll q hq = (β - α) • potentialResolvent a hα hlam hEll q hq ∘SL potentialResolvent a hβ hlam hEll q hq

Operator resolvent identity in the positive shift for a fixed potential.

theorem DivergenceFormProcess.Form.potentialResolvent_perturbation_identity {d : ℕ} (a : HCPolySupport.CoeffField d) {U : Set (HCPolySupport.Vec d)} {α lam Lam C : ℝ} (hα : 0 < α) (hlam : 0 < lam) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (q : HCPolySupport.Vec d → ℝ) (hq : IsBoundedNonnegativePotential U q C) (f : ↥(HCPolySupport.ScalarL2 U)) : (potentialResolvent a hα hlam hEll q hq) f = (alphaShiftedResolvent a hα hlam hEll) f - (alphaShiftedResolvent a hα hlam hEll) ((potentialMul q hq) ((potentialResolvent a hα hlam hEll q hq) f))

The solution with potential is the unperturbed solution minus the unperturbed resolvent applied to the potential load.

theorem DivergenceFormProcess.Form.potentialSolution_energy_le {d : ℕ} (a : HCPolySupport.CoeffField d) {U : Set (HCPolySupport.Vec d)} {α lam Lam C : ℝ} (hα : 0 < α) (hlam : 0 < lam) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (q : HCPolySupport.Vec d → ℝ) (hq : IsBoundedNonnegativePotential U q C) (f : ↥(HCPolySupport.ScalarL2 U)) : min α lam * ‖(potentialSolution a hα hlam hEll q hq) f‖ ^ 2 ≤ ‖f‖ * ‖(potentialResolvent a hα hlam hEll q hq) f‖

Coercive graph-norm energy estimate for the potential solution.

theorem DivergenceFormProcess.Form.potentialIntegral_sq_le {d : ℕ} (a : HCPolySupport.CoeffField d) {U : Set (HCPolySupport.Vec d)} {α lam Lam C : ℝ} (hα : 0 < α) (hlam : 0 < lam) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (q : HCPolySupport.Vec d → ℝ) (hq : IsBoundedNonnegativePotential U q C) (f : ↥(HCPolySupport.ScalarL2 U)) : ∫ (x : HCPolySupport.Vec d), q x * ↑↑((potentialResolvent a hα hlam hEll q hq) f) x ^ 2 ∂HCPolySupport.volumeMeasureOn U ≤ ‖f‖ * ‖(potentialResolvent a hα hlam hEll q hq) f‖

The potential energy is bounded by the forcing paired with the solution.