OnePointChainLaplace

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

The survival probability and the padded family, on a general carrier

The one-step Laplace contraction rests on the Paley--Zygmund survival probability of the exit time, and the chaining estimate consumes the resulting per-cell bounds as one padded family. Both are stated here on an arbitrary carrier, the cube being read inside it by a map emb and the cell by an open set carrying no other starting point. Neither argument uses anything about the state space: the survival probability is the Paley--Zygmund inequality at the level one half, and the reindexing contributes no starting point at a padded index.

Main results

• survivalProbabilityConstant_le_measure_le_exitTime_on — the survival probability on a carrier.
• one_step_laplace_hone_of_partition_cubes_image — the padded-family form of a scale-by-scale cube estimate on a carrier.

References

• ABK26, the one-step Laplace estimate of Section 5.3.

1. The survival probability on a carrier

theorem Algsuperdiff.Section5.Provider.survivalProbabilityConstant_le_measure_le_exitTime_on {alpha : Type u_1} [MetricSpace alpha] [CompleteSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] [SecondCountableTopology alpha] [Nonempty alpha] [LocallyCompactSpace alpha] (P : MarkovProcess.SubMarkovKernelSemigroup alpha) (hP : P.IsConservative) (hFeller : P.IsFellerKernelSemigroup) (hKol : P.KolmogorovRegular hP) (U : Set alpha) (hU : IsOpen U) (T Cup clow : NNReal) (hT : 0 < T) (hupper : ∀ (y : alpha), ∫⁻ (eta : MarkovProcess.ContinuousPath alpha), MarkovProcess.ContinuousPath.exitTime U eta ∂(MarkovProcess.SubMarkovKernelSemigroup.IsConservative.continuousProcess P hP) y ≤ ↑(Cup * T)) (x : alpha) (hlower : ↑(clow * T) ≤ ∫⁻ (eta : MarkovProcess.ContinuousPath alpha), MarkovProcess.ContinuousPath.exitTime U eta ∂(MarkovProcess.SubMarkovKernelSemigroup.IsConservative.continuousProcess P hP) x) : ↑(Trace.survivalProbabilityConstant Cup clow) ≤ ((MarkovProcess.SubMarkovKernelSemigroup.IsConservative.continuousProcess P hP) x) {eta : MarkovProcess.ContinuousPath alpha | ↑(clow * T / 2) ≤ MarkovProcess.ContinuousPath.exitTime U eta}

Survival at half the guaranteed expected exit time, on a general carrier. This is the Paley--Zygmund estimate, whose proof uses no property of the state space: an upper bound Cup * T on the expected exit time from the open set U, valid from every starting point, and a lower bound clow * T at the starting point x, give clow ^ 2 / (1152 * Cup ^ 2) ≤ Q_x {clow * T / 2 ≤ tau_U}.

3. The padded family of the chaining estimate

theorem Algsuperdiff.Section5.Provider.one_step_laplace_hone_of_partition_cubes_image {d r : ℕ} {alpha : Type u_1} [MetricSpace alpha] [CompleteSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] [SecondCountableTopology alpha] [Nonempty alpha] (emb : C(HCPolySupport.Vec d, alpha)) (P : MarkovProcess.SubMarkovKernelSemigroup alpha) (hP : P.IsConservative) (n : ℤ) (sites : Fin r ↪ Percolation.Site d) (lam : ℝ) (rho : ENNReal) (hstep : ∀ (j : Fin r), ∀ z ∈ closure (Support.cubeSetAt (Trace.rescaleSite n (sites j)) n), ∫⁻ (eta : MarkovProcess.ContinuousPath alpha), Process.ContinuousPath.discountedStoppingWeight lam (MarkovProcess.ContinuousPath.exitTime (⇑emb '' Support.cubeSetAt (Trace.rescaleSite n (sites j)) (n + 1))) eta ∂(MarkovProcess.SubMarkovKernelSemigroup.IsConservative.continuousProcess P hP) (emb z) ≤ rho) (i : ℕ) (z : alpha) : z ∈ ⇑emb '' Trace.enumeratedClosedCubeFamily n sites i → ∫⁻ (eta : MarkovProcess.ContinuousPath alpha), Process.ContinuousPath.discountedStoppingWeight lam (MarkovProcess.ContinuousPath.exitTime (⇑emb '' Trace.enumeratedOpenEnlargementFamily n sites i)) eta ∂(MarkovProcess.SubMarkovKernelSemigroup.IsConservative.continuousProcess P hP) z ≤ rho

Reindex a scale-by-scale cube estimate on a carrier into the literal hone family of the chaining estimate. The padded indices contribute no starting points.