KernelIdentification

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

Identification of the direct whole-space kernel resolvent

The kernel resolvent generated by the directly assembled analytic minimal C₀ resolvent agrees with the cubic analytic supremum on every nonnegative bounded measurable observable. The proof first establishes monotone continuity of the analytic supremum from the corresponding bounded-domain regularity statement, then uses a monotone-class argument starting from continuous observables vanishing at infinity.

structure DivergenceFormProcess.Form.WholeSpaceAnalyticData.KernelIdentificationInput {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) : Type

Inputs needed by the S-free monotone-class identification: agreement on C₀ data and the analytic and kernel constant-one normalizations.

• R : MarkovProcess.PositiveC0ContractiveResolvent (HCPolySupport.Vec d)

  The positive contractive resolvent to be identified with the analytic resolvent.

• operator_eq (mu : ↑MarkovProcess.Semigroup.PositiveShift) (f : ZeroAtInftyContinuousMap (HCPolySupport.Vec d) ℝ) (x : HCPolySupport.Vec d) : ((self.R.operator mu) f) x = A.analyticMinimalResolventReal mu ⇑f ⋯ ⋯ x
• kernel_one (mu : ↑MarkovProcess.Semigroup.PositiveShift) (x : HCPolySupport.Vec d) : ENNReal.ofReal ↑mu * self.R.kernelSemigroup.kernelResolvent (↑mu) (fun (x : HCPolySupport.Vec d) => 1) x = 1
• analytic_one (mu : ↑MarkovProcess.Semigroup.PositiveShift) (x : HCPolySupport.Vec d) : ENNReal.ofReal ↑mu * A.analyticMinimalResolvent mu (fun (x : HCPolySupport.Vec d) => 1) ⋯ ⋯ x = 1

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.abs_indicator_le_one {d : ℕ} (T : Set (HCPolySupport.Vec d)) (y : HCPolySupport.Vec d) : |T.indicator (fun (x : HCPolySupport.Vec d) => 1) y| ≤ 1

def DivergenceFormProcess.Form.WholeSpaceAnalyticData.IndicatorAgreement {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (S : A.KernelIdentificationInput) (mu : ↑MarkovProcess.Semigroup.PositiveShift) (x : HCPolySupport.Vec d) (T : Set (HCPolySupport.Vec d)) (hT : MeasurableSet T) : Prop

Agreement of the kernel and analytic resolvents on a measurable-set indicator.

Equations

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

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.kernelResolventIdentifiesAnalyticMinimal_of_input {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (S : A.KernelIdentificationInput) : A.KernelResolventIdentifiesAnalyticMinimal S.R

The generated kernel resolvent agrees with the analytic cubic minimal resolvent on every nonnegative measurable observable bounded by one whenever the C₀ identification and both constant-one normalizations are available.