Continuity

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

Continuity of the analytic minimal resolvent

For square-integrable bounded data, the local Dirichlet resolvents have a common interior Hölder modulus on each fixed ball. Their monotone pointwise supremum therefore has the same modulus. Applying this argument to the positive and negative parts gives continuity of the real minimal resolvent.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.wholeSpaceCube_mono {d m n : ℕ} (hmn : m ≤ n) : wholeSpaceCube d m ⊆ wholeSpaceCube d n

The cubic exhaustion is monotone at arbitrary indices.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.exists_euclideanBall_subset_wholeSpaceCube {d : ℕ} (x : HCPolySupport.Vec d) {r : ℝ} (hr : 0 < r) : ∃ (m : ℕ), HCPolySupport.euclideanBall x r ⊆ wholeSpaceCube d m

Every fixed Euclidean ball is eventually contained in the cubic exhaustion.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.norm_cubeDatum_le {d : ℕ} {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) {D : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (hfLp : MeasureTheory.MemLp f 2 MeasureTheory.volume) (m : ℕ) : ‖boundedMeasurableToScalarL2 ⋯ ⋯ ⋯‖ ≤ (MeasureTheory.eLpNorm f 2 MeasureTheory.volume).toReal

Restricting a globally square-integrable bounded datum to one exhaustion cube does not increase its L² norm.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.euclideanHolderBoundOn_iSup {d : ℕ} {W : Set (HCPolySupport.Vec d)} {alpha K : ℝ} {rep : ℕ → HCPolySupport.Vec d → ℝ} (hbdd : ∀ x ∈ W, BddAbove (Set.range fun (n : ℕ) => rep n x)) (h : ∀ (n : ℕ), Algsuperdiff.StochasticProcess.Common.Regularity.Ported.EuclideanHolderBoundOn W alpha K (rep n)) : Algsuperdiff.StochasticProcess.Common.Regularity.Ported.EuclideanHolderBoundOn W alpha K fun (x : HCPolySupport.Vec d) => ⨆ (n : ℕ), rep n x

A common Hölder bound on a pointwise bounded-above family is inherited by its pointwise supremum.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.ciSup_nat_add_of_monotone {u : ℕ → ℝ} (hu : Monotone u) (hbdd : BddAbove (Set.range u)) (N : ℕ) : ⨆ (k : ℕ), u (k + N) = ⨆ (m : ℕ), u m

Shifting the index of a bounded-above monotone real sequence does not change its supremum.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticMinimalResolvent_mono {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (mu : ↑MarkovProcess.Semigroup.PositiveShift) {f g : HCPolySupport.Vec d → ℝ} (hf : Measurable f) (hg : Measurable g) {D E : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (hgE : ∀ (x : HCPolySupport.Vec d), |g x| ≤ E) (hfg : ∀ (x : HCPolySupport.Vec d), f x ≤ g x) (x : HCPolySupport.Vec d) : A.analyticMinimalResolvent mu f hf hfD x ≤ A.analyticMinimalResolvent mu g hg hgE x

The positive minimal resolvent preserves pointwise order.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.toReal_analyticMinimalResolvent_smul {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (mu : ↑MarkovProcess.Semigroup.PositiveShift) {c : ℝ} (hc : 0 ≤ c) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) (hf0 : ∀ (x : HCPolySupport.Vec d), 0 ≤ f x) {D : ℝ} (hD : 0 ≤ D) (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (x : HCPolySupport.Vec d) : (A.analyticMinimalResolvent mu (fun (y : HCPolySupport.Vec d) => c * f y) ⋯ ⋯ x).toReal = c * (A.analyticMinimalResolvent mu f hf hfD x).toReal

Nonnegative scalar multiplication commutes with the real value of the positive minimal resolvent.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.abs_analyticMinimalResolventReal_sub_le {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (mu : ↑MarkovProcess.Semigroup.PositiveShift) {f g : HCPolySupport.Vec d → ℝ} (hf : Measurable f) (hg : Measurable g) {D E eps : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (hgE : ∀ (x : HCPolySupport.Vec d), |g x| ≤ E) (hclose : ∀ (x : HCPolySupport.Vec d), |f x - g x| ≤ eps) (x : HCPolySupport.Vec d) : |A.analyticMinimalResolventReal mu f hf hfD x - A.analyticMinimalResolventReal mu g hg hgE x| ≤ eps / ↑mu

The real minimal resolvent is uniformly stable in the supremum norm, with the sharp maximum-principle constant.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.exists_holderBound_cubeResolvent_tail {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (mu : ↑MarkovProcess.Semigroup.PositiveShift) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) {D : ℝ} (hD : 0 ≤ D) (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (hfLp : MeasureTheory.MemLp f 2 MeasureTheory.volume) (x : HCPolySupport.Vec d) : ∃ r > 0, ∃ (N : ℕ) (K : ℝ), ∀ (k : ℕ), Algsuperdiff.StochasticProcess.Common.Regularity.Ported.EuclideanHolderBoundOn (HCPolySupport.euclideanBall x r) (1 / 2) K (A.analyticCubeResolvent mu f hf hfD (k + N))

At every point, a tail of the cubic exhaustion has one common local C^{0,1/2} modulus. The radius is obtained by freezing the continuous skew part at that point; its size is unrestricted.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.locally_holder_analyticMinimalResolvent {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (mu : ↑MarkovProcess.Semigroup.PositiveShift) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) (hf0 : ∀ (x : HCPolySupport.Vec d), 0 ≤ f x) {D : ℝ} (hD : 0 ≤ D) (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (hfLp : MeasureTheory.MemLp f 2 MeasureTheory.volume) (x : HCPolySupport.Vec d) : ∃ r > 0, ∃ (K : ℝ), Algsuperdiff.StochasticProcess.Common.Regularity.Ported.EuclideanHolderBoundOn (HCPolySupport.euclideanBall x r) (1 / 2) K fun (y : HCPolySupport.Vec d) => (A.analyticMinimalResolvent mu f hf hfD y).toReal

For nonnegative globally square-integrable data, the real value of the minimal resolvent has a local Hölder bound at every point.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.continuous_analyticMinimalResolventReal_of_memLp {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (mu : ↑MarkovProcess.Semigroup.PositiveShift) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) {D : ℝ} (hD : 0 ≤ D) (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (hfLp : MeasureTheory.MemLp f 2 MeasureTheory.volume) : Continuous (A.analyticMinimalResolventReal mu f hf hfD)

The real analytic minimal resolvent is continuous for every bounded measurable datum which is globally square-integrable.