Minimal

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

The analytic minimal resolvent on the cubic exhaustion

This file transports the bounded-domain analytic Dirichlet resolvents to Vec d by zero extension and takes their pointwise supremum. All coefficient hypotheses are imposed on the whole space and restricted to the individual cubes in the definitions below.

structure DivergenceFormProcess.Form.WholeSpaceAnalyticData (d : ℕ) [NeZero d] : Type

The coefficient and regularity data used by the whole-space cubic exhaustion. The field has the form a = nu I + k, where nu > 0 and k is continuous and skew with arbitrary size; no whole-space small-contrast hypothesis is included.

• a : HCPolySupport.CoeffField d

  The measurable whole-space coefficient field with fixed symmetric part.

• nu : ℝ

  The positive molecular diffusivity determining the symmetric coefficient part.

• hnu : 0 < self.nu
• hsymm (y : HCPolySupport.Vec d) : HCPolySupport.symmPart (self.a y) = self.nu • 1
• hskewContinuous : ContinuousOn (fun (y : HCPolySupport.Vec d) => self.a y - self.nu • 1) Set.univ
• hd : 2 ≤ d
• hameas : Measurable self.a

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.skewContinuousOnCube {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (m : ℕ) : ContinuousOn (fun (y : HCPolySupport.Vec d) => A.a y - A.nu • 1) (wholeSpaceCube d m)

Continuity of the arbitrary-size skew part restricted to an exhaustion cube.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.skewContinuousOnCubeClosure {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (m : ℕ) : ContinuousOn (fun (y : HCPolySupport.Vec d) => A.a y - A.nu • 1) {x : HCPolySupport.Vec d | Algsuperdiff.StochasticProcess.Common.Regularity.MemAxisCubeClosure (fun (x : Fin d) => -3 ^ m) (2 * 3 ^ m) x}

Continuity of the skew part on the closed box underlying an exhaustion cube. Boundary regularity uses this carrier rather than the open cube.

noncomputable def DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeEllipticityUpper {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (m : ℕ) : ℝ

The compactness-supplied upper ellipticity constant on the mth cube.

Equations

• A.cubeEllipticityUpper m = Algsuperdiff.StochasticProcess.Common.Regularity.Freezing.axisCubeEllipticUpper (fun (x : Fin d) => -3 ^ m) (2 * 3 ^ m) ⋯ ⋯ ⋯

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.cubeEllipticity {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (m : ℕ) : HCPolySupport.IsEllipticFieldOn A.nu (A.cubeEllipticityUpper m) (wholeSpaceCube d m) A.a

The mth cube is elliptic with lower constant nu; continuity on its compact closure supplies the upper constant.

noncomputable def DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticCubeResolvent {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (mu : ↑MarkovProcess.Semigroup.PositiveShift) (f : HCPolySupport.Vec d → ℝ) (hf : Measurable f) {D : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (m : ℕ) (x : HCPolySupport.Vec d) : ℝ

The analytic Dirichlet resolvent on the mth cube, extended by zero to the whole space.

Equations

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

noncomputable def DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticCubeResolventENN {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (mu : ↑MarkovProcess.Semigroup.PositiveShift) (f : HCPolySupport.Vec d → ℝ) (hf : Measurable f) {D : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (m : ℕ) (x : HCPolySupport.Vec d) : ENNReal

The nonnegative extended-real form of a local analytic resolvent.

Equations

• A.analyticCubeResolventENN mu f hf hfD m x = ENNReal.ofReal (A.analyticCubeResolvent mu f hf hfD m x)

noncomputable def DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticMinimalResolvent {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (mu : ↑MarkovProcess.Semigroup.PositiveShift) (f : HCPolySupport.Vec d → ℝ) (hf : Measurable f) {D : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (x : HCPolySupport.Vec d) : ENNReal

The analytic minimal resolvent of a nonnegative bounded measurable observable is the pointwise supremum of its zero-extended cube resolvents.

Equations

• A.analyticMinimalResolvent mu f hf hfD x = ⨆ (m : ℕ), A.analyticCubeResolventENN mu f hf hfD m x

def DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticPositivePart {d : ℕ} (f : HCPolySupport.Vec d → ℝ) (x : HCPolySupport.Vec d) : ℝ

The nonnegative part of a real observable.

Equations

• DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticPositivePart f x = max (f x) 0

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.measurable_analyticPositivePart {d : ℕ} {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) : Measurable (analyticPositivePart f)

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.abs_analyticPositivePart_le {d : ℕ} {f : HCPolySupport.Vec d → ℝ} {D : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (x : HCPolySupport.Vec d) : |analyticPositivePart f x| ≤ D

noncomputable def DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticMinimalResolventReal {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (mu : ↑MarkovProcess.Semigroup.PositiveShift) (f : HCPolySupport.Vec d → ℝ) (hf : Measurable f) {D : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (x : HCPolySupport.Vec d) : ℝ

The real form of the analytic minimal resolvent, defined by positive and negative parts.

Equations

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

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.restrict_boundedMeasurableToScalarL2_succ {d : ℕ} {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) {D : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (m : ℕ) : restrictScalarL2ToPart ⋯ (boundedMeasurableToScalarL2 ⋯ ⋯ ⋯) = boundedMeasurableToScalarL2 ⋯ ⋯ ⋯

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticCubeResolvent_nonneg {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 : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (m : ℕ) (x : HCPolySupport.Vec d) : 0 ≤ A.analyticCubeResolvent mu f hf hfD m x

A local analytic cube resolvent is pointwise nonnegative on nonnegative data.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticCubeResolvent_le_succ {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 : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (m : ℕ) (x : HCPolySupport.Vec d) : A.analyticCubeResolvent mu f hf hfD m x ≤ A.analyticCubeResolvent mu f hf hfD (m + 1) x

The zero-extended analytic Dirichlet resolvents increase with the cubic exhaustion on nonnegative data.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.monotone_analyticCubeResolvent {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 : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (x : HCPolySupport.Vec d) : Monotone fun (m : ℕ) => A.analyticCubeResolvent mu f hf hfD m x

At each point, the local analytic resolvents form a monotone sequence.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.measurable_analyticCubeResolvent {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (mu : ↑MarkovProcess.Semigroup.PositiveShift) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) {D : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (m : ℕ) : Measurable (A.analyticCubeResolvent mu f hf hfD m)

A zero-extended cube resolvent is measurable on the ambient space.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.continuousOn_analyticCubeResolvent {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (mu : ↑MarkovProcess.Semigroup.PositiveShift) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) {D : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (m : ℕ) : ContinuousOn (A.analyticCubeResolvent mu f hf hfD m) (wholeSpaceCube d m)

On its defining cube, the zero-extended analytic resolvent is continuous.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticCubeResolvent_ae {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (mu : ↑MarkovProcess.Semigroup.PositiveShift) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) {D : ℝ} (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (m : ℕ) : A.analyticCubeResolvent mu f hf hfD m =ᵐ[HCPolySupport.volumeMeasureOn (wholeSpaceCube d m)] ↑↑((alphaShiftedResolvent A.a ⋯ ⋯ ⋯) (boundedMeasurableToScalarL2 ⋯ ⋯ ⋯))

On its defining cube, the analytic representative agrees almost everywhere with the L² resolvent class.

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

The analytic minimal resolvent is measurable as a pointwise supremum.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticCubeResolvent_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) (m : ℕ) (x : HCPolySupport.Vec d) : A.analyticCubeResolvent mu f hf hfD m x ≤ A.analyticCubeResolvent mu g hg hgE m x

A local analytic cube resolvent preserves pointwise order between bounded measurable data.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticCubeResolvent_add {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| ≤ D + E) (m : ℕ) (x : HCPolySupport.Vec d) : A.analyticCubeResolvent mu (fun (y : HCPolySupport.Vec d) => f y + g y) ⋯ hfg m x = A.analyticCubeResolvent mu f hf hfD m x + A.analyticCubeResolvent mu g hg hgE m x

The local analytic cube resolvent is additive on nonnegative bounded measurable data.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticCubeResolventENN_add {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (mu : ↑MarkovProcess.Semigroup.PositiveShift) {f g : HCPolySupport.Vec d → ℝ} (hf : Measurable f) (hg : Measurable g) (hf0 : ∀ (x : HCPolySupport.Vec d), 0 ≤ f x) (hg0 : ∀ (x : HCPolySupport.Vec d), 0 ≤ g x) {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| ≤ D + E) (m : ℕ) (x : HCPolySupport.Vec d) : A.analyticCubeResolventENN mu (fun (y : HCPolySupport.Vec d) => f y + g y) ⋯ hfg m x = A.analyticCubeResolventENN mu f hf hfD m x + A.analyticCubeResolventENN mu g hg hgE m x

The extended-real local resolvent is additive on nonnegative data.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticMinimalResolvent_add {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (mu : ↑MarkovProcess.Semigroup.PositiveShift) {f g : HCPolySupport.Vec d → ℝ} (hf : Measurable f) (hg : Measurable g) (hf0 : ∀ (x : HCPolySupport.Vec d), 0 ≤ f x) (hg0 : ∀ (x : HCPolySupport.Vec d), 0 ≤ g x) {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| ≤ D + E) (x : HCPolySupport.Vec d) : A.analyticMinimalResolvent mu (fun (y : HCPolySupport.Vec d) => f y + g y) ⋯ hfg x = A.analyticMinimalResolvent mu f hf hfD x + A.analyticMinimalResolvent mu g hg hgE x

The analytic minimal resolvent is additive on nonnegative bounded measurable observables.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.abs_analyticCubeResolvent_le {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) (m : ℕ) (x : HCPolySupport.Vec d) : |A.analyticCubeResolvent mu f hf hfD m x| ≤ D / ↑mu

The local analytic cube resolvent obeys the uniform resolvent bound.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticMinimalResolvent_le {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) (x : HCPolySupport.Vec d) : A.analyticMinimalResolvent mu f hf hfD x ≤ ENNReal.ofReal (D / ↑mu)

The analytic minimal resolvent of nonnegative data satisfies the sharp uniform bound inherited from the bounded domains.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticMinimalResolvent_ne_top {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) (x : HCPolySupport.Vec d) : A.analyticMinimalResolvent mu f hf hfD x ≠ ⊤

The bounded analytic minimal resolvent never takes the value infinity.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticCubeResolvent_resolvent_identity {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (mu nu : ↑MarkovProcess.Semigroup.PositiveShift) {f : HCPolySupport.Vec d → ℝ} (hf : Measurable f) {D : ℝ} (hD : 0 ≤ D) (hfD : ∀ (x : HCPolySupport.Vec d), |f x| ≤ D) (m : ℕ) (x : HCPolySupport.Vec d) : A.analyticCubeResolvent mu f hf hfD m x = A.analyticCubeResolvent nu f hf hfD m x + (↑nu - ↑mu) * A.analyticCubeResolvent nu (A.analyticCubeResolvent mu f hf hfD m) ⋯ ⋯ m x

The zero-extended analytic resolvent on one cube satisfies the resolvent identity pointwise on the ambient space.