InteriorEquationBridge

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

Interior equation bridge for the potential problem

The potential problem is posed on ZeroTraceSobolev U with the pairing coefficientPairing, while the interior Schauder chain consumes IsMatrixDivFormWeakSolutionZerothOrderOn, an equation between explicit set integrals against H¹₀ test functions on an open window. This file connects the two.

The scalar source of the interior equation is f - α u - q u, obtained by moving the mass term and the potential term of

α ⟪u, φ⟫ + ∫ q u φ + coefficientPairing a U ∇u ∇φ = ⟪f, φ⟫

to the right-hand side; the vector source is zero.

Three statements are provided:

• the plain bridge, valid for every f ∈ L²(U);
• its bounded companion, which adds ‖g‖_{L^∞(W)} ≤ (2 + C/α) ‖f‖_{L^∞(U)} under an essential bound on f; and
• the specialization to the penalization potential on a window inside the part domain, where the potential vanishes and the bound collapses to 2 ‖f‖_{L^∞(U)}, uniformly in the penalization index.

noncomputable def DivergenceFormProcess.Form.interiorScalarSource {d : ℕ} {U : Set (HCPolySupport.Vec d)} (alpha : ℝ) {C : ℝ} (q : HCPolySupport.Vec d → ℝ) (hq : IsBoundedNonnegativePotential U q C) (f : ↥(HCPolySupport.ScalarL2 U)) (u : ZeroTraceSobolev U) : ↥(HCPolySupport.ScalarL2 U)

The L² source of the interior equation: the forcing minus the mass and potential contributions of the solution.

Equations

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

theorem DivergenceFormProcess.Form.interiorScalarSource_coeFn {d : ℕ} {U : Set (HCPolySupport.Vec d)} (alpha : ℝ) {C : ℝ} (q : HCPolySupport.Vec d → ℝ) (hq : IsBoundedNonnegativePotential U q C) (f : ↥(HCPolySupport.ScalarL2 U)) (u : ZeroTraceSobolev U) : ↑↑(interiorScalarSource alpha q hq f u) =ᵐ[HCPolySupport.volumeMeasureOn U] fun (x : HCPolySupport.Vec d) => ↑↑f x - alpha * ↑↑(ZeroTraceSobolev.toL2 u) x - q x * ↑↑(ZeroTraceSobolev.toL2 u) x

theorem DivergenceFormProcess.Form.isMatrixDivFormWeakSolutionZerothOrderOn_domain_of_isPotentialWeakSolution {d : ℕ} {U : Set (HCPolySupport.Vec d)} (a : HCPolySupport.CoeffField d) {alpha C : ℝ} (q : HCPolySupport.Vec d → ℝ) (hq : IsBoundedNonnegativePotential U q C) (f : ↥(HCPolySupport.ScalarL2 U)) {u : ZeroTraceSobolev U} (hu : IsPotentialWeakSolution a alpha q U u f) (w : HCPolySupport.H10Function U) (hwgrad : w.gradToHilbertVectorL2 = ZeroTraceSobolev.gradient u) : Algsuperdiff.StochasticProcess.Common.Regularity.Ported.IsMatrixDivFormWeakSolutionZerothOrderOn a U w.toH1Function (fun (x : HCPolySupport.Vec d) => ↑↑(interiorScalarSource alpha q hq f u) x) 0

The interior equation on the whole domain, with the zero-trace solution read through an H¹₀ witness.

theorem DivergenceFormProcess.Form.memScalarLInfOn_of_ae_bound {d : ℕ} {W : Set (HCPolySupport.Vec d)} {g : HCPolySupport.Vec d → ℝ} {K : ℝ} (hK : 0 ≤ K) (hmeas : MeasureTheory.AEStronglyMeasurable g (MeasureTheory.volume.restrict W)) (hbd : ∀ᵐ (x : HCPolySupport.Vec d) ∂MeasureTheory.volume.restrict W, |g x| ≤ K) : Algsuperdiff.StochasticProcess.Common.Regularity.Ported.MemScalarLInfOn W g ∧ Algsuperdiff.StochasticProcess.Common.Regularity.Ported.scalarLInfSizeOn W g ≤ K

An essential bound on a window gives membership in L^∞ there together with the corresponding bound on the essential supremum.