PotentialBridge #
Ported from scottnarmstrong/Superdiffusion at 7f20476385d4af418f110303085ad0740c9eba46. Module imports, support namespace and local option directives adapted for Lean Pool.
A scalar-forcing bridge for potential weak solutions #
This file translates the zero-trace potential weak formulation into the pointwise scalar-forcing carrier used by the Agmon decay applications. It is kept in the whole-space layer because that is its first consumer.
theorem
DivergenceFormProcess.Form.isScalarForcedWeakSolution_of_isPotentialWeakSolution
{d : ℕ}
{U : Set (HCPolySupport.Vec d)}
{a : HCPolySupport.CoeffField d}
{alpha C : ℝ}
{q : HCPolySupport.Vec d → ℝ}
{f : ↥(HCPolySupport.ScalarL2 U)}
(u : HCPolySupport.H10Function U)
(hq : IsBoundedNonnegativePotential U q C)
(hweak : IsPotentialWeakSolution a alpha q U (ZeroTraceSobolev.ofH10Function u) f)
:
IsScalarForcedWeakSolution a U (fun (x : HCPolySupport.Vec d) => ↑↑f x - (alpha + q x) * u.toFun x) u.toH1Function
A potential weak solution represented by an H¹₀ function solves the
pointwise scalar-forced equation obtained by moving both zeroth-order terms
to the right-hand side.