StoppedMoments

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

The stopped mean and the stopped second moment

Fix a conservative Feller process with continuous paths, an open set U, a deterministic horizon t, and a starting point x of U. Write theta for the stopped time exitTimeTrunc U t, so that the stopped position is omega theta.

Two observables are treated, and both are treated in the same way: an observable compared with a function reproduced by the exit distribution of U.

• The stopped mean. If u is reproduced by the exit distribution of U, if |b - u| <= K everywhere and b x = 0, then |E_x[b(X_theta)]| <= 2K . The two summands are the value u x, which is within K of b x = 0, and the expectation of b - u, which is within K because the law is a probability measure.

• The stopped second moment. If u = h - sigma * w with h reproduced by the exit distribution and w the expected exit time, if |q - u| <= K everywhere and q x = 0, then |E_x[q(X_theta)] - sigma * t| <= 2K + sigma * t * P_x[tau <= t] . The second identity of the stopped-Dirichlet file turns E_x[u(X_theta)] into u x + sigma E_x[theta], and the expected stopped time is the horizon less a shortfall supported on the event that the exit has already occurred.

The two conclusions are the displays e.displacement.squared.stopped and e.second.moment.stopped of the source, in one direction each: there b is a linear function, q a quadratic one, sigma is twice the effective diffusivity at the scale of the cube, and K is the uniform distance between the heterogeneous solution and its homogenized counterpart. Summing over a family of observables is the last section; it produces the displacement bound and the second moment of the whole displacement vector, with leading term n * sigma * t over n directions.

Nothing here refers to a generator, to a coefficient field, or to a cube. The two inputs that carry the analytic content are HasExitMeanValueOn — the mean-value property of the observable, supplied by the exit mean-value interface — and the uniform bound K, supplied by the renormalization of the generator.

Main results

• ae_eval_exitTimeTrunc_mem_closure — the stopped position lies in the closure of U.
• integral_eval_exitTimeTrunc_congr_of_eqOn_closure — only the values on the closure matter.
• abs_integral_eval_exitTimeTrunc_le_of_hasExitMeanValueOn — the stopped mean.
• abs_integral_eval_exitTimeTrunc_sub_mul_le_of_hasExitMeanValueOn — the stopped second moment.
• abs_integral_sum_eval_exitTimeTrunc_sub_le — the sum over a family of directions.

References

• ABK26, Steps 1 and 3 of the superdiffusive displacement bounds of Section 5.4.

1. Two elementary bounds

2. The stopped position

theorem Algsuperdiff.Section5.Provider.measurable_eval_exitTimeTrunc {alpha : Type u_1} [MetricSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] {U : Set alpha} (hU : IsOpen U) (t : NNReal) {f : alpha → ℝ} (hf : Measurable f) : Measurable fun (omega : MarkovProcess.ContinuousPath alpha) => f (omega (MarkovProcess.ContinuousPath.exitTimeTrunc U t omega))

The composition of a Borel function with the stopped position is Borel.

theorem Algsuperdiff.Section5.Provider.integrable_eval_exitTimeTrunc {alpha : Type u_1} [MetricSpace alpha] [CompleteSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] [SecondCountableTopology alpha] [Nonempty alpha] (P : MarkovProcess.SubMarkovKernelSemigroup alpha) (hP : P.IsConservative) {U : Set alpha} (hU : IsOpen U) (t : NNReal) {f : alpha → ℝ} (hf : Measurable f) {C : ℝ} (hC : ∀ (y : alpha), |f y| ≤ C) (x : alpha) : MeasureTheory.Integrable (fun (omega : MarkovProcess.ContinuousPath alpha) => f (omega (MarkovProcess.ContinuousPath.exitTimeTrunc U t omega))) ((MarkovProcess.SubMarkovKernelSemigroup.IsConservative.continuousProcess P hP) x)

A bounded Borel observable of the stopped position is integrable.

theorem Algsuperdiff.Section5.Provider.ae_eval_exitTimeTrunc_mem_closure {alpha : Type u_1} [MetricSpace alpha] [CompleteSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] [SecondCountableTopology alpha] [Nonempty alpha] (P : MarkovProcess.SubMarkovKernelSemigroup alpha) (hP : P.IsConservative) (hK : P.KolmogorovRegular hP) {U : Set alpha} (hU : IsOpen U) (t : NNReal) {x : alpha} (hx : x ∈ U) : ∀ᵐ (omega : MarkovProcess.ContinuousPath alpha) ∂(MarkovProcess.SubMarkovKernelSemigroup.IsConservative.continuousProcess P hP) x, omega (MarkovProcess.ContinuousPath.exitTimeTrunc U t omega) ∈ closure U

The stopped position lies in the closure of the domain. Almost every path of the process started inside U starts inside U, and a continuous path started inside U is in the closure of U at the time at which it either leaves U or reaches the horizon.

theorem Algsuperdiff.Section5.Provider.integral_eval_exitTimeTrunc_congr_of_eqOn_closure {alpha : Type u_1} [MetricSpace alpha] [CompleteSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] [SecondCountableTopology alpha] [Nonempty alpha] (P : MarkovProcess.SubMarkovKernelSemigroup alpha) (hP : P.IsConservative) (hK : P.KolmogorovRegular hP) {U : Set alpha} (hU : IsOpen U) {f g : alpha → ℝ} (hfg : Set.EqOn f g (closure U)) (t : NNReal) {x : alpha} (hx : x ∈ U) : ∫ (omega : MarkovProcess.ContinuousPath alpha), f (omega (MarkovProcess.ContinuousPath.exitTimeTrunc U t omega)) ∂(MarkovProcess.SubMarkovKernelSemigroup.IsConservative.continuousProcess P hP) x = ∫ (omega : MarkovProcess.ContinuousPath alpha), g (omega (MarkovProcess.ContinuousPath.exitTimeTrunc U t omega)) ∂(MarkovProcess.SubMarkovKernelSemigroup.IsConservative.continuousProcess P hP) x

Only the values on the closure matter. Two observables agreeing on the closure of U have the same expectation at the stopped position.

3. The shortfall of the stopped time against the horizon

theorem Algsuperdiff.Section5.Provider.integral_shortfall_nonneg {alpha : Type u_1} [MetricSpace alpha] [CompleteSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] [SecondCountableTopology alpha] [Nonempty alpha] (P : MarkovProcess.SubMarkovKernelSemigroup alpha) (hP : P.IsConservative) {U : Set alpha} (t : NNReal) (x : alpha) : 0 ≤ ∫ (omega : MarkovProcess.ContinuousPath alpha), (DivergenceFormProcess.StoppedDirichlet.survivalEvent U t)ᶜ.indicator (fun (omega : MarkovProcess.ContinuousPath alpha) => ↑t - (MarkovProcess.ContinuousPath.exitTime U omega).toReal) omega ∂(MarkovProcess.SubMarkovKernelSemigroup.IsConservative.continuousProcess P hP) x

The shortfall of the stopped time against the horizon is nonnegative.

theorem Algsuperdiff.Section5.Provider.integral_shortfall_le {alpha : Type u_1} [MetricSpace alpha] [CompleteSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] [SecondCountableTopology alpha] [Nonempty alpha] (P : MarkovProcess.SubMarkovKernelSemigroup alpha) (hP : P.IsConservative) {U : Set alpha} (hU : IsOpen U) (t : NNReal) (x : alpha) : ∫ (omega : MarkovProcess.ContinuousPath alpha), (DivergenceFormProcess.StoppedDirichlet.survivalEvent U t)ᶜ.indicator (fun (omega : MarkovProcess.ContinuousPath alpha) => ↑t - (MarkovProcess.ContinuousPath.exitTime U omega).toReal) omega ∂(MarkovProcess.SubMarkovKernelSemigroup.IsConservative.continuousProcess P hP) x ≤ ↑t * (((MarkovProcess.SubMarkovKernelSemigroup.IsConservative.continuousProcess P hP) x) (DivergenceFormProcess.StoppedDirichlet.survivalEvent U t)ᶜ).toReal

The shortfall of the stopped time against the horizon is at most the horizon times the probability that the exit has already occurred.

4. Summing over a family of directions

theorem Algsuperdiff.Section5.Provider.abs_integral_sum_eval_exitTimeTrunc_sub_le {alpha : Type u_1} [MetricSpace alpha] [CompleteSpace alpha] [MeasurableSpace alpha] [BorelSpace alpha] [SecondCountableTopology alpha] [Nonempty alpha] (P : MarkovProcess.SubMarkovKernelSemigroup alpha) (hP : P.IsConservative) (hK : P.KolmogorovRegular hP) {U : Set alpha} (hU : IsOpen U) {n : ℕ} (Q : Fin n → alpha → ℝ) (N : alpha → ℝ) (hN : Set.EqOn N (fun (y : alpha) => ∑ i : Fin n, Q i y) (closure U)) (hQmeas : ∀ (i : Fin n), Measurable (Q i)) {CQ : ℝ} (hCQ : ∀ (i : Fin n) (y : alpha), |Q i y| ≤ CQ) (t : NNReal) {x : alpha} (hx : x ∈ U) {sigma B : ℝ} (hQ : ∀ (i : Fin n), |∫ (omega : MarkovProcess.ContinuousPath alpha), Q i (omega (MarkovProcess.ContinuousPath.exitTimeTrunc U t omega)) ∂(MarkovProcess.SubMarkovKernelSemigroup.IsConservative.continuousProcess P hP) x - sigma * ↑t| ≤ B) : |∫ (omega : MarkovProcess.ContinuousPath alpha), N (omega (MarkovProcess.ContinuousPath.exitTimeTrunc U t omega)) ∂(MarkovProcess.SubMarkovKernelSemigroup.IsConservative.continuousProcess P hP) x - ↑n * (sigma * ↑t)| ≤ ↑n * B

The second moment of the whole displacement. If a finite family of observables adds up on the closure of U to a single observable N, and each member is within B of sigma * t at the stopped position, then N is within n * B of n * sigma * t there.

With N the squared norm and sigma twice the effective diffusivity, the leading term is n * sigma * t, the source's 2 d shom_m t over the d coordinate directions.

5. The stopped mean

theorem Algsuperdiff.Section5.Provider.abs_integral_eval_exitTimeTrunc_le_of_hasExitMeanValueOn {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) (hK : P.KolmogorovRegular hP) {U : Set alpha} (hU : IsOpen U) {u b : alpha → ℝ} (hu : Measurable u) {Cu : ℝ} (hCu : ∀ (y : alpha), |u y| ≤ Cu) (hharm : DivergenceFormProcess.StoppedDirichlet.HasExitMeanValueOn P hP U u) (hb : Measurable b) {K : ℝ} (hKb : ∀ (y : alpha), |b y - u y| ≤ K) (t : NNReal) {x : alpha} (hx : x ∈ U) (hb0 : b x = 0) (hwfin : DivergenceFormProcess.StoppedDirichlet.expectedExitTime P hP U x ≠ ⊤) : |∫ (omega : MarkovProcess.ContinuousPath alpha), b (omega (MarkovProcess.ContinuousPath.exitTimeTrunc U t omega)) ∂(MarkovProcess.SubMarkovKernelSemigroup.IsConservative.continuousProcess P hP) x| ≤ 2 * K

The stopped mean. Let u be reproduced by the exit distribution of U and let b be a Borel observable within K of u everywhere and vanishing at the starting point. Then the expectation of b at the stopped position is at most 2K in absolute value.

This is the display e.displacement.squared.stopped of the source before squaring: b is the linear function e ⬝ x, u is the heterogeneous solution taking those boundary values, and K is the uniform distance between them.

6. The stopped second moment

theorem Algsuperdiff.Section5.Provider.abs_integral_eval_exitTimeTrunc_sub_mul_le_of_hasExitMeanValueOn {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) (hK : P.KolmogorovRegular hP) {U : Set alpha} (hU : IsOpen U) {h q u : alpha → ℝ} (hh : Measurable h) {Ch : ℝ} (hCh : ∀ (y : alpha), |h y| ≤ Ch) (hharm : DivergenceFormProcess.StoppedDirichlet.HasExitMeanValueOn P hP U h) {sigma : ℝ} (hsigma : 0 ≤ sigma) (hu : ∀ (y : alpha), u y = h y - sigma * (DivergenceFormProcess.StoppedDirichlet.expectedExitTime P hP U y).toReal) (hq : Measurable q) {Cq : ℝ} (hCq : ∀ (y : alpha), |q y| ≤ Cq) {K : ℝ} (hKb : ∀ (y : alpha), |q y - u y| ≤ K) (t : NNReal) {x : alpha} (hx : x ∈ U) (hq0 : q x = 0) (hwfin : DivergenceFormProcess.StoppedDirichlet.expectedExitTime P hP U x ≠ ⊤) : |∫ (omega : MarkovProcess.ContinuousPath alpha), q (omega (MarkovProcess.ContinuousPath.exitTimeTrunc U t omega)) ∂(MarkovProcess.SubMarkovKernelSemigroup.IsConservative.continuousProcess P hP) x - sigma * ↑t| ≤ 2 * K + sigma * (↑t * (((MarkovProcess.SubMarkovKernelSemigroup.IsConservative.continuousProcess P hP) x) (DivergenceFormProcess.StoppedDirichlet.survivalEvent U t)ᶜ).toReal)

The stopped second moment. Let h be reproduced by the exit distribution of U, let u be h corrected by sigma times the expected exit time, and let q be a bounded Borel observable within K of u everywhere and vanishing at the starting point. Then the expectation of q at the stopped position is within 2K of sigma times the horizon, up to the shortfall carried by the event that the exit has already occurred.

This is the display e.second.moment.stopped of the source: q is the quadratic observable (e ⬝ x)^2, sigma is twice the effective diffusivity at the scale of the cube, u is the heterogeneous solution with that constant right-hand side and those boundary values, and K is the uniform distance between u and q.