C0FromVanishing

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

The analytic minimal resolvent on C₀ from vanishing at infinity

This module separates the coefficient-dependent proof of vanishing at infinity from the coefficient-free algebraic assembly. The resulting operator is definitionally the signed analytic minimal resolvent; in particular, later kernel-identification arguments do not require an operator rewrite.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.abs_le_norm_c0_generic {d : ℕ} (f : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ) (x : HCPolySupport.Vec d) : |f x| ≤ ‖f‖

def DivergenceFormProcess.Form.WholeSpaceAnalyticData.HasVanishingAnalyticMinimalResolvent {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) : Prop

The coefficient-dependent input needed to realize the signed analytic minimal resolvent as a map from C₀ to C₀.

Equations

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

noncomputable def DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticMinimalC0ResolventOfVanishing {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (hVanish : A.HasVanishingAnalyticMinimalResolvent) (mu : ↑MarkovProcess.Semigroup.PositiveShift) (f : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ) : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ

The analytic minimal resolvent as a C₀ map, given its coefficient-dependent vanishing theorem.

Equations

• A.analyticMinimalC0ResolventOfVanishing hVanish mu f = { toFun := A.analyticMinimalResolventReal mu ⇑f ⋯ ⋯, continuous_toFun := ⋯, zero_at_infty' := ⋯ }

@[simp]

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticMinimalC0ResolventOfVanishing_apply {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (hVanish : A.HasVanishingAnalyticMinimalResolvent) (mu : ↑MarkovProcess.Semigroup.PositiveShift) (f : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ) (x : HCPolySupport.Vec d) : (A.analyticMinimalC0ResolventOfVanishing hVanish mu f) x = A.analyticMinimalResolventReal mu ⇑f ⋯ ⋯ x

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticMinimalC0ResolventOfVanishing_add {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (hVanish : A.HasVanishingAnalyticMinimalResolvent) (mu : ↑MarkovProcess.Semigroup.PositiveShift) (f g : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ) : A.analyticMinimalC0ResolventOfVanishing hVanish mu (f + g) = A.analyticMinimalC0ResolventOfVanishing hVanish mu f + A.analyticMinimalC0ResolventOfVanishing hVanish mu g

Additivity of the analytic minimal C₀ resolver constructed from a vanishing theorem.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticMinimalC0ResolventOfVanishing_smul {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (hVanish : A.HasVanishingAnalyticMinimalResolvent) (mu : ↑MarkovProcess.Semigroup.PositiveShift) (c : ℝ) (f : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ) : A.analyticMinimalC0ResolventOfVanishing hVanish mu (c • f) = c • A.analyticMinimalC0ResolventOfVanishing hVanish mu f

Homogeneity of the analytic minimal C₀ resolver constructed from a vanishing theorem.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.norm_analyticMinimalC0ResolventOfVanishing_le {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (hVanish : A.HasVanishingAnalyticMinimalResolvent) (mu : ↑MarkovProcess.Semigroup.PositiveShift) (f : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ) : ‖A.analyticMinimalC0ResolventOfVanishing hVanish mu f‖ ≤ (↑mu)⁻¹ * ‖f‖

The analytic minimal C₀ resolver constructed from a vanishing theorem has the sharp pointwise operator bound.

noncomputable def DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticMinimalC0ResolventCLMOfVanishing {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (hVanish : A.HasVanishingAnalyticMinimalResolvent) (mu : ↑MarkovProcess.Semigroup.PositiveShift) : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ →L[ℝ] ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ

The analytic minimal resolver constructed from a vanishing theorem as a continuous linear map on C₀.

Equations

• A.analyticMinimalC0ResolventCLMOfVanishing hVanish mu = { toFun := A.analyticMinimalC0ResolventOfVanishing hVanish mu, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous (↑mu)⁻¹ ⋯

@[simp]

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticMinimalC0ResolventCLMOfVanishing_apply {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (hVanish : A.HasVanishingAnalyticMinimalResolvent) (mu : ↑MarkovProcess.Semigroup.PositiveShift) (f : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ) : (A.analyticMinimalC0ResolventCLMOfVanishing hVanish mu) f = A.analyticMinimalC0ResolventOfVanishing hVanish mu f

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticMinimalC0ResolventCLMOfVanishing_resolvent_identity {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (hVanish : A.HasVanishingAnalyticMinimalResolvent) (lam mu : ↑MarkovProcess.Semigroup.PositiveShift) : A.analyticMinimalC0ResolventCLMOfVanishing hVanish lam - A.analyticMinimalC0ResolventCLMOfVanishing hVanish mu = (↑mu - ↑lam) • A.analyticMinimalC0ResolventCLMOfVanishing hVanish lam ∘SL A.analyticMinimalC0ResolventCLMOfVanishing hVanish mu

The analytic minimal C₀ operators constructed from a vanishing theorem satisfy the resolvent identity.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.norm_analyticMinimalC0ResolventCLMOfVanishing_le {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (hVanish : A.HasVanishingAnalyticMinimalResolvent) (mu : ↑MarkovProcess.Semigroup.PositiveShift) : ‖A.analyticMinimalC0ResolventCLMOfVanishing hVanish mu‖ ≤ (↑mu)⁻¹

The constructed analytic minimal operator has the sharp Hille--Yosida norm bound.

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticMinimalC0ResolventCLMOfVanishing_nonnegative {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (hVanish : A.HasVanishingAnalyticMinimalResolvent) (mu : ↑MarkovProcess.Semigroup.PositiveShift) (f : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ) (hf : ∀ (x : HCPolySupport.Vec d), 0 ≤ f x) (x : HCPolySupport.Vec d) : 0 ≤ ((A.analyticMinimalC0ResolventCLMOfVanishing hVanish mu) f) x

The constructed analytic minimal operator preserves pointwise nonnegativity.

def DivergenceFormProcess.Form.WholeSpaceAnalyticData.HasDenseRangeAnalyticMinimalC0OfVanishing {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (hVanish : A.HasVanishingAnalyticMinimalResolvent) : Prop

The dense-range input for the analytic minimal C₀ resolver constructed from a vanishing theorem.

Equations

• A.HasDenseRangeAnalyticMinimalC0OfVanishing hVanish = ∀ (mu : ↑MarkovProcess.Semigroup.PositiveShift), DenseRange (A.analyticMinimalC0ResolventOfVanishing hVanish mu)

noncomputable def DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticMinimalPositiveC0ContractiveResolventOfVanishing {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (hVanish : A.HasVanishingAnalyticMinimalResolvent) (hDense : A.HasDenseRangeAnalyticMinimalC0OfVanishing hVanish) : MarkovProcess.PositiveC0ContractiveResolvent (HCPolySupport.Vec d)

The analytic minimal resolver assembled as a positive contractive C₀ resolvent from coefficient-dependent vanishing and dense-range proofs.

Equations

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

@[simp]

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.analyticMinimalPositiveC0ContractiveResolventOfVanishing_operator {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (hVanish : A.HasVanishingAnalyticMinimalResolvent) (hDense : A.HasDenseRangeAnalyticMinimalC0OfVanishing hVanish) (mu : ↑MarkovProcess.Semigroup.PositiveShift) (f : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ) : ((A.analyticMinimalPositiveC0ContractiveResolventOfVanishing hVanish hDense).operator mu) f = A.analyticMinimalC0ResolventOfVanishing hVanish mu f