WholeSpaceKernelConservativity

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

Conservativity of the stream-field kernel resolvent

Continuous compactly supported cutoffs transfer the analytic constant-one normalization to the kernel resolvent generated by the split-skew C₀ resolver. Both the analytic and kernel normalizations are stated explicitly.

theorem Algsuperdiff.Section5.Field.streamAnalyticMinimalResolvent_one_le_kernelResolvent {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (omega : FullSample d M.gamma) (mu : ↑MarkovProcess.Semigroup.PositiveShift) (x : HCPolySupport.Vec d) : (streamWholeSpaceAnalyticData M omega).analyticMinimalResolvent mu (fun (x : HCPolySupport.Vec d) => 1) ⋯ ⋯ x ≤ (streamAnalyticMinimalPositiveC0ContractiveResolvent M omega).kernelSemigroup.kernelResolvent (↑mu) (fun (x : HCPolySupport.Vec d) => 1) x

The analytic minimal resolvent of one is bounded by the kernel resolvent of one generated by the model's split-skew C₀ resolver.

theorem Algsuperdiff.Section5.Field.ofReal_mul_streamKernelResolvent_one {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (omega : FullSample d M.gamma) (mu : ↑MarkovProcess.Semigroup.PositiveShift) (x : HCPolySupport.Vec d) : ENNReal.ofReal ↑mu * (streamAnalyticMinimalPositiveC0ContractiveResolvent M omega).kernelSemigroup.kernelResolvent (↑mu) (fun (x : HCPolySupport.Vec d) => 1) x = 1

The generated stream kernel resolvent carries full constant-one mass.

theorem Algsuperdiff.Section5.Field.isConservative_streamKernelSemigroup {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (omega : FullSample d M.gamma) : (streamAnalyticMinimalPositiveC0ContractiveResolvent M omega).kernelSemigroup.IsConservative

The kernel semigroup generated by the model's split-skew analytic resolvent is conservative.

theorem Algsuperdiff.Section5.Field.kernelResolventIdentifiesAnalyticMinimal_stream {d : ℕ} [NeZero d] (M : Section3.ABKModel d) (omega : FullSample d M.gamma) : (streamWholeSpaceAnalyticData M omega).KernelResolventIdentifiesAnalyticMinimal (streamAnalyticMinimalPositiveC0ContractiveResolvent M omega)

The kernel resolvent generated by the split-skew C₀ resolver agrees with the analytic cubic minimal resolvent on every nonnegative measurable observable bounded by one. The proof uses both model normalizations and the generic monotone-class transfer.