ExcessiveC0

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

The whole-space barrier as a C₀ function

The observable is bounded, measurable and supported in the bounded part domain, so it is square integrable and compactly supported. Continuity of the barrier then follows from the unconditional local Hölder estimate for the analytic minimal resolvent, and vanishing at infinity from the analytic tail estimate together with the compact support of the continuous part solution.

Continuity uses no contrast hypothesis. Vanishing at infinity is stated under the contrast datum carried by the tail estimate available for the minimal resolvent.

theorem DivergenceFormProcess.Form.WholeSpaceBarrierData.measurable_indicator_f {d : ℕ} [NeZero d] {A : WholeSpaceAnalyticData d} (P : WholeSpaceBarrierData A) : Measurable (P.V.indicator P.f)

The observable restricted to the part domain is measurable.

theorem DivergenceFormProcess.Form.WholeSpaceBarrierData.indicator_f_nonneg {d : ℕ} [NeZero d] {A : WholeSpaceAnalyticData d} (P : WholeSpaceBarrierData A) (x : HCPolySupport.Vec d) : 0 ≤ P.V.indicator P.f x

theorem DivergenceFormProcess.Form.WholeSpaceBarrierData.abs_indicator_f_le {d : ℕ} [NeZero d] {A : WholeSpaceAnalyticData d} (P : WholeSpaceBarrierData A) (x : HCPolySupport.Vec d) : |P.V.indicator P.f x| ≤ P.D

theorem DivergenceFormProcess.Form.WholeSpaceBarrierData.memLp_f {d : ℕ} [NeZero d] {A : WholeSpaceAnalyticData d} (P : WholeSpaceBarrierData A) : MeasureTheory.MemLp P.f 2 MeasureTheory.volume

theorem DivergenceFormProcess.Form.WholeSpaceBarrierData.hasCompactSupport_indicator_f {d : ℕ} [NeZero d] {A : WholeSpaceAnalyticData d} (P : WholeSpaceBarrierData A) : HasCompactSupport (P.V.indicator P.f)

theorem DivergenceFormProcess.Form.WholeSpaceBarrierData.hasCompactSupport_utilde {d : ℕ} [NeZero d] {A : WholeSpaceAnalyticData d} (P : WholeSpaceBarrierData A) : HasCompactSupport P.utilde

theorem DivergenceFormProcess.Form.WholeSpaceBarrierData.continuous_barrier {d : ℕ} [NeZero d] {A : WholeSpaceAnalyticData d} (P : WholeSpaceBarrierData A) : Continuous P.barrier

The whole-space barrier is continuous. No contrast hypothesis is used.