BoundedMeasurableLimit

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

Bounded pointwise limits of the analytic resolvent

The analytic side of the comparison between the process resolvent and the resolvent of the divergence-form operator has to be continuous along uniformly bounded pointwise convergent data, at every point of the domain.

That does not follow from the interior Hölder estimate alone, because the L^∞ part of its data size does not tend to zero. What is used instead is the mean-plus-oscillation bound

|w x₀| ≤ |⨍_{B ρ} w| + K ρ ^ alpha,

with K the Hölder constant of the interior estimate, uniform along the sequence, and with the mean controlled by the L² norm through Cauchy–Schwarz: |⨍_{B ρ} w| ≤ ‖w‖_{L²} / √(volume (B ρ)). Letting the index go to infinity at fixed ρ and then ρ → 0 gives the convergence.

L² convergence from uniformly bounded pointwise convergence

theorem DivergenceFormProcess.Form.tendsto_norm_scalarL2_sub_of_bounded_ae_tendsto {d : ℕ} {U : Set (HCPolySupport.Vec d)} (hU : HCPolySupport.IsOpenBoundedConvexDomain U) {F : ℕ → ↥(HCPolySupport.ScalarL2 U)} {G : ↥(HCPolySupport.ScalarL2 U)} {C : ℝ} (hbd : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, ∀ (k : ℕ), |↑↑(F k) x - ↑↑G x| ≤ C) (hpt : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, Filter.Tendsto (fun (k : ℕ) => ↑↑(F k) x) Filter.atTop (nhds (↑↑G x))) : Filter.Tendsto (fun (k : ℕ) => ‖F k - G‖) Filter.atTop (nhds 0)

On a bounded domain, uniformly bounded almost everywhere pointwise convergence implies convergence in L².

The mean-plus-oscillation bound

theorem DivergenceFormProcess.Form.abs_setIntegral_le_norm_mul_sqrt {d : ℕ} {U B : Set (HCPolySupport.Vec d)} (hB : MeasurableSet B) (hBU : B ⊆ U) (hBtop : MeasureTheory.volume B ≠ ⊤) (G : ↥(HCPolySupport.ScalarL2 U)) : |∫ (y : HCPolySupport.Vec d) in B, ↑↑G y| ≤ ‖G‖ * √(MeasureTheory.volume B).toReal

Cauchy–Schwarz: the integral of an L² class over a subset of the domain is controlled by its norm times the square root of the volume.

theorem DivergenceFormProcess.Form.abs_representative_le_of_holder {d : ℕ} {U : Set (HCPolySupport.Vec d)} (G : ↥(HCPolySupport.ScalarL2 U)) {w : HCPolySupport.Vec d → ℝ} (hwae : w =ᵐ[HCPolySupport.volumeMeasureOn U] ↑↑G) {x₀ : HCPolySupport.Vec d} {rho K alpha : ℝ} (hrho : 0 < rho) (hK : 0 ≤ K) (halpha : 0 ≤ alpha) (hball : HCPolySupport.euclideanBall x₀ rho ⊆ U) (hholder : Algsuperdiff.StochasticProcess.Common.Regularity.Ported.EuclideanHolderBoundOn (HCPolySupport.euclideanBall x₀ rho) alpha K w) : |w x₀| ≤ ‖G‖ / √(MeasureTheory.volume (HCPolySupport.euclideanBall x₀ rho)).toReal + K * rho ^ alpha

Mean-plus-oscillation bound: a function continuous on the domain, representing an L² class and Hölder on a ball, is controlled at the centre of that ball by the L² norm and the Hölder constant.

The interior estimate for bounded data

theorem DivergenceFormProcess.Form.exists_interior_equation_alphaShifted_with_gradient {d : ℕ} {U : Set (HCPolySupport.Vec d)} (a : HCPolySupport.CoeffField d) (hU : HCPolySupport.IsOpenBoundedConvexDomain U) {α lam Lam : ℝ} (hα : 0 < α) (hlam : 0 < lam) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) (F : ↥(HCPolySupport.ScalarL2 U)) {M : ℝ} (hM : 0 ≤ M) (hFM : ∀ᵐ (x : HCPolySupport.Vec d) ∂HCPolySupport.volumeMeasureOn U, |↑↑F x| ≤ M) {W : Set (HCPolySupport.Vec d)} (hW : IsOpen W) (hWU : W ⊆ U) : ∃ (z : HCPolySupport.H1Function W) (g : HCPolySupport.Vec d → ℝ), z.toFun =ᵐ[MeasureTheory.volume.restrict W] ↑↑((alphaShiftedResolvent a hα hlam hEll) F) ∧ Algsuperdiff.StochasticProcess.Common.Regularity.Ported.MemScalarLInfOn W g ∧ Algsuperdiff.StochasticProcess.Common.Regularity.Ported.scalarLInfSizeOn W g ≤ 2 * M ∧ Algsuperdiff.StochasticProcess.Common.Regularity.Ported.vectorLpSizeOn W 2 z.grad ≤ (min α lam)⁻¹ * ‖F‖ ∧ Algsuperdiff.StochasticProcess.Common.Regularity.Ported.IsMatrixDivFormWeakSolutionZerothOrderOn a W z g 0

The interior equation for the α-shifted problem together with the bounds on its data.

theorem DivergenceFormProcess.Form.penalizationInteriorHolderConstant_mono_gradient (d : ℕ) (alpha : ℝ) {r : ℝ} (hr : 0 ≤ r) (M : ℝ) {G G' : ℝ} (h : G ≤ G') : penalizationInteriorHolderConstant d alpha r G M ≤ penalizationInteriorHolderConstant d alpha r G' M

Continuity of the interior representative along bounded limits

theorem DivergenceFormProcess.Form.penalizationInteriorHolderConstant_nonneg (d : ℕ) (alpha : ℝ) {r G M : ℝ} (hr : 0 ≤ r) (hG : 0 ≤ G) (hM : 0 ≤ M) : 0 ≤ penalizationInteriorHolderConstant d alpha r G M

The quantitative interior witness

theorem DivergenceFormProcess.Form.hasLocalHolderShiftedResolvents_continuousCoeff {d : ℕ} {U : Set (HCPolySupport.Vec d)} [NeZero d] (hd : 2 ≤ d) (a : HCPolySupport.CoeffField d) (hU : HCPolySupport.IsOpenBoundedConvexDomain U) {nu : ℝ} (hnu : 0 < nu) (hsymm : ∀ (y : HCPolySupport.Vec d), HCPolySupport.symmPart (a y) = nu • 1) (hcont : ContinuousOn (fun (y : HCPolySupport.Vec d) => a y - nu • 1) U) {lam Lam : ℝ} (hlam : 0 < lam) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) : HasLocalHolderShiftedResolvents a hlam hEll (1 / 2) nu⁻¹

The freezing route to the quantitative witness. For a coefficient with symmetric part nu • 1 and continuous skew part of arbitrary size, the frozen radius at a point serves every bounded datum, and the constant is the same Schauder constant with the forcing budget scaled by nu⁻¹.

theorem DivergenceFormProcess.Form.tendsto_representative_of_tendsto_norm_reg {d : ℕ} {U : Set (HCPolySupport.Vec d)} (a : HCPolySupport.CoeffField d) {α lam Lam : ℝ} (hα : 0 < α) (hlam : 0 < lam) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) {alpha B : ℝ} (halpha0 : 0 < alpha) (hB : 0 ≤ B) (hReg : HasLocalHolderShiftedResolvents a hlam hEll alpha B) {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 hα hlam hEll) (F k))) (hwcont : ContinuousOn w U) (hwae : w =ᵐ[HCPolySupport.volumeMeasureOn U] ↑↑((alphaShiftedResolvent a hα hlam hEll) Fl)) {x : HCPolySupport.Vec d} (hx : x ∈ U) : Filter.Tendsto (fun (k : ℕ) => wk k x) Filter.atTop (nhds (w x))

The analytic side is continuous along uniformly bounded L²-convergent data, at every point of the domain. The L² norm controls the mean of the difference over a small ball and the quantitative interior witness controls its oscillation there, with a constant that stays bounded along the sequence.

theorem DivergenceFormProcess.Form.tendsto_representative_of_tendsto_norm_freezing {d : ℕ} {U : Set (HCPolySupport.Vec d)} [NeZero d] (hd : 2 ≤ d) (a : HCPolySupport.CoeffField d) (hU : HCPolySupport.IsOpenBoundedConvexDomain U) {nu : ℝ} (hnu : 0 < nu) (hsymm : ∀ (y : HCPolySupport.Vec d), HCPolySupport.symmPart (a y) = nu • 1) (hcont : ContinuousOn (fun (y : HCPolySupport.Vec d) => a y - nu • 1) U) {α lam Lam : ℝ} (hα : 0 < α) (hlam : 0 < lam) (hEll : HCPolySupport.IsEllipticFieldOn lam Lam U a) {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 hα hlam hEll) (F k))) (hwcont : ContinuousOn w U) (hwae : w =ᵐ[HCPolySupport.volumeMeasureOn U] ↑↑((alphaShiftedResolvent a hα hlam hEll) Fl)) {x : HCPolySupport.Vec d} (hx : x ∈ U) : Filter.Tendsto (fun (k : ℕ) => wk k x) Filter.atTop (nhds (w x))

The freezing instance of the headline. For a coefficient whose symmetric part is the scalar field nu • 1 and whose skew part is continuous of arbitrary size, the analytic side is continuous along uniformly bounded L²-convergent data at every point of the domain, with no contrast hypothesis.