OnePointExhaustionTail

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

Exhaustion-metric resolvent tails from amplified live tails

The resolvent tail decay a compactified semigroup needs is stated in the metric an exhaustion function determines on the one-point compactification, while the analysis produces tail decay in the metric of the live space. This file converts the second into the first.

The conversion is a set inclusion. The complement of the exhaustion-metric ball of radius r about a live point x meets the live space in points that are simultaneously at live distance at least r from x and at exhaustion level at least r - rho x (OnePoint.coe_preimage_compl_ball_subset). Both constraints are available at once, so the tail set is contained in the complement of the live ball of any amplified radius amp x r the two constraints force. Where the exhaustion function is small the amplification is large: a starting point deep in a tail of the space must be displaced far in the live metric before its exhaustion level can rise. Under conservativity the compactified potential of the tail set about a live point is the live potential of its live preimage, and about the added point it vanishes, so the amplified live tail estimate is exactly what the compactified tail decay asks for (PositiveC0ContractiveResolvent.hasResolventTail_onePoint_of_amplified).

Taking amp x r = r recovers the plain transport of a live tail, since the exhaustion metric is bounded by the live metric. No analytic estimate is asserted here: the live tail bound and the amplification are the consumer's hypotheses.

theorem Algsuperdiff.Process.OnePoint.coe_preimage_compl_ball_subset {X : Type u_1} [MetricSpace X] (rho : X → ℝ) (hrho_cont : Continuous rho) (hrho_pos : ∀ (x : X), 0 < rho x) (hrho_lipschitz : LipschitzWith 1 rho) (hrho_compact : ∀ epsilon > 0, IsCompact {x : X | epsilon ≤ rho x}) (x : X) (r : ℝ) : OnePoint.some ⁻¹' (Metric.ball (↑x) r)ᶜ ⊆ {z : X | r ≤ dist z x} ∩ {z : X | r - rho x ≤ rho z}

The live part of an exhaustion-metric tail about a live point is Euclidean-far and lies in a compact superlevel set of the exhaustion function.

theorem Algsuperdiff.Process.PositiveC0ContractiveResolvent.hasResolventTail_onePoint_of_amplified {X : Type u_1} [MetricSpace X] [ProperSpace X] [MeasurableSpace X] [BorelSpace X] (R : MarkovProcess.PositiveC0ContractiveResolvent X) (hcons : R.kernelSemigroup.IsConservative) (rho : X → ℝ) (hrho_cont : Continuous rho) (hrho_pos : ∀ (x : X), 0 < rho x) (hrho_lipschitz : LipschitzWith 1 rho) (hrho_compact : ∀ epsilon > 0, IsCompact {x : X | epsilon ≤ rho x}) {lam : ℝ} {phi : ℝ → ℝ} (amp : X → ℝ → ℝ) (hamp_le : ∀ (x : X) (r : ℝ) (z : X), r ≤ dist z x → r - rho x ≤ rho z → amp x r ≤ dist z x) (hlive : ∀ (x : X) (r : ℝ), 0 < r → ENNReal.ofReal lam * (R.kernelSemigroup.resolventPotential lam x) (Metric.ball x (amp x r))ᶜ ≤ ENNReal.ofReal (phi (√lam * r))) : SubMarkovKernelSemigroup.HasResolventTail R.onePointKernelSemigroup lam phi

Exhaustion-metric resolvent tails from amplified Euclidean tails. Under conservativity the compactified potential of an exhaustion tail of radius r about a live point is dominated by the live potential of the Euclidean tail of the amplified radius amp x r; about the added point it vanishes.