C0AllShifts

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

Extending analytic C₀ vanishing from large shifts

For a positive shift mu, the resolvent identity with mu + 1 expands the mu-resolvent into a finite geometric sum of (mu + 1)-resolvents and a remainder. The sharp resolvent bound makes the remainder uniformly geometric. Consequently it suffices to prove vanishing at infinity for shifts at least one.

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

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

Vanishing at infinity for the analytic minimal resolvent at every shift at least one.

Equations

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

theorem DivergenceFormProcess.Form.WholeSpaceAnalyticData.hasVanishingAnalyticMinimalResolvent_of_aboveOne {d : ℕ} [NeZero d] (A : WholeSpaceAnalyticData d) (hHigh : A.HasVanishingAnalyticMinimalResolventAboveOne) : A.HasVanishingAnalyticMinimalResolvent

Large-shift C₀ vanishing extends to every positive shift by the resolvent identity and its geometric remainder.