BoundedMeasurableAgreement

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

The process resolvent and the analytic resolvent agree on C₀ data

The conservative model semigroup lives on OnePoint U, with observables extended by 0 at the point at infinity. For an observable coming from C₀(U, ℝ), its real kernel resolvent at a point of U is the value of the C₀ representative of the analytic resolvent, hence the value of the representative continuous on U of the analytic resolvent applied to the same datum read as a bounded measurable function.

This is the base case of the comparison on bounded measurable observables. The extension from C₀ data to all bounded measurable data by a monotone class argument is not carried out here.

Both statements use the coefficient only through the interior regularity witness HasContinuousShiftedResolvents, so they are stated in that form under the suffix _reg; the small-contrast statements keep their names and are corollaries.

theorem DivergenceFormProcess.Form.domainExtension_of_notMem {d : ℕ} {U : Set (HCPolySupport.Vec d)} {f : ↑U → ℝ} {x : HCPolySupport.Vec d} (hx : x ∉ U) : domainExtension f x = 0

The zero extension vanishes outside the domain.