ContinuousCoeffLimit

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

Limits of resolvent representatives for continuous coefficients

Freezing the arbitrary-size continuous skew part supplies the local Hölder witness required by the general representative-limit theorem. No global small-contrast hypothesis is used.

theorem DivergenceFormProcess.Form.tendsto_representative_of_tendsto_norm_continuousCoeff {d : ℕ} {U : Set (HCPolySupport.Vec d)} [NeZero d] (a : HCPolySupport.CoeffField d) (hU : HCPolySupport.IsOpenBoundedConvexDomain U) {alpha nu Lam : ℝ} (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) {F : ℕ → ↥(HCPolySupport.ScalarL2 U)} {Fl : ↥(HCPolySupport.ScalarL2 U)} {M : ℝ} (hM : 0 ≤ M) (hFM : ∀ (k : ℕ), ∀ᵐ (y : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, |↑↑(F k) y - ↑↑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] ↑↑((alphaShiftedResolvent a halpha hnu hEll) (F k))) (hwcont : ContinuousOn w U) (hwae : w =ᵐ[HCPolySupport.volumeMeasureOn U] ↑↑((alphaShiftedResolvent a halpha hnu hEll) Fl)) {x : HCPolySupport.Vec d} (hx : x ∈ U) : Filter.Tendsto (fun (k : ℕ) => wk k x) Filter.atTop (nhds (w x))

Continuous resolvent representatives converge pointwise when their uniformly bounded data converge in L². This is the direct freezing instance of tendsto_representative_of_tendsto_norm_reg.