ContinuousCoeffPotentialLimit

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

Limits of potential-resolvent representatives

A fixed bounded nonnegative potential can be moved into the forcing term. This reduces pointwise convergence of its continuous resolvent representatives to the continuous-coefficient limit theorem for the zero-potential resolvent. The continuous skew part may have arbitrary size.

theorem DivergenceFormProcess.Form.tendsto_potentialRepresentative_of_tendsto_norm_continuousCoeff {d : ℕ} {U : Set (HCPolySupport.Vec d)} [NeZero d] (a : HCPolySupport.CoeffField d) (hU : HCPolySupport.IsOpenBoundedConvexDomain U) {alpha nu Lam C : ℝ} (halpha : 0 < alpha) (hnu : 0 < nu) (hEll : HCPolySupport.IsEllipticFieldOn nu Lam U a) (hsymm : ∀ (y : HCPolySupport.Vec d), HCPolySupport.symmPart (a y) = nu • 1) (hcont : ContinuousOn (fun (y : HCPolySupport.Vec d) => a y - nu • 1) U) (hd : 2 ≤ d) (q : HCPolySupport.Vec d → ℝ) (hq : IsBoundedNonnegativePotential U q C) {F : ℕ → ↥(HCPolySupport.ScalarL2 U)} {Fl : ↥(HCPolySupport.ScalarL2 U)} {M : ℝ} (hM : 0 ≤ M) (hEffBound : ∀ (k : ℕ), ∀ᵐ (y : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, |↑↑(F k - (potentialMul q hq) ((potentialResolvent a halpha hnu hEll q hq) (F k))) y - ↑↑(Fl - (potentialMul q hq) ((potentialResolvent a halpha hnu hEll q hq) Fl)) y| ≤ M) (hL2 : Filter.Tendsto (fun (k : ℕ) => ‖F k - Fl‖) Filter.atTop (nhds 0)) {wk : ℕ → HCPolySupport.Vec d → ℝ} {w : HCPolySupport.Vec d → ℝ} (hwkcont : ∀ (k : ℕ), ContinuousOn (wk k) U) (hwkae : ∀ (k : ℕ), wk k =ᵐ[HCPolySupport.volumeMeasureOn U] ↑↑((potentialResolvent a halpha hnu hEll q hq) (F k))) (hwcont : ContinuousOn w U) (hwae : w =ᵐ[HCPolySupport.volumeMeasureOn U] ↑↑((potentialResolvent a halpha hnu hEll q hq) Fl)) {x : HCPolySupport.Vec d} (hx : x ∈ U) : Filter.Tendsto (fun (k : ℕ) => wk k x) Filter.atTop (nhds (w x))

Continuous representatives of a fixed-potential resolvent converge pointwise when the data converge in L² and the effective zero-potential forcings have a common pointwise bound.