OnePointChainStreamJoint

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

The one-step Laplace estimate for the full stream field

The one-step contraction of OnePointChainLaplace is re-derived here from the per-cell joint of the full stream field. Nothing about the argument changes: the contraction follows from an upper bound on the expected exit time valid from every starting point, a lower bound on the inner cube, the Paley--Zygmund survival probability, and the continuity of the representative. What changes is the analytic input, which is now the exit-time datum problem of the full field ν I + k rather than of a truncation of it, and the good-cube bounds it obeys.

Because the truncation scale no longer enters the coefficient of the cell problem, the statements below carry no truncation scale at all: one sample of the full field and one cube scale determine the cell.

Main results

• one_step_laplace_on_good_cube_stream_image — the one-step contraction at the reading of every point of the closed inner cube.
• one_step_laplace_step_of_good_sites_stream_image — the same over a finite family of good cells, with one discount rate and one contraction factor.
• one_step_laplace_hone_of_good_sites_stream_image — its padded-family form.

References

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

1. The lower bound on the closed inner cube

2. The one-step contraction on a carrier

theorem Algsuperdiff.Section5.Provider.one_step_laplace_on_good_cube_stream_image (d : ℕ) (hdim : 2 ≤ d) (cstar : ℝ) (hcstar : 0 < cstar) (Creg : ℝ) (hCreg : 0 < Creg) : ∃ (gamma0 : ℝ) (Cev : ℝ) (C : ℝ) (c : ℝ), 0 < gamma0 ∧ 0 < Cev ∧ 0 < C ∧ 0 < c ∧ ∀ (M : Section3.ABKModel d), Section3.Disorder.cstar M = cstar → M.gamma ≤ gamma0 → ∀ ep ∈ Set.Ioc 0 (1 / 4), ep ≤ c → ∀ (n : ℤ) (y : HCPolySupport.Vec d) (i : Fin d) (omega : Field.FullSample d M.gamma), ↑omega ∈ Support.qEvent M Creg Cev n y ep → ∀ (alpha : Type) [inst : MetricSpace alpha] [inst_1 : CompleteSpace alpha] [inst_2 : MeasurableSpace alpha] [inst_3 : BorelSpace alpha] [inst_4 : SecondCountableTopology alpha] [inst_5 : Nonempty alpha] [LocallyCompactSpace alpha] (P : MarkovProcess.SubMarkovKernelSemigroup alpha) (hP : P.IsConservative), P.IsFellerKernelSemigroup → P.KolmogorovRegular hP → ∀ (U : Set alpha) (emb : HCPolySupport.Vec d → alpha), IsCubeExitTimeSolutionDataStream M n omega alpha P hP U emb i y → oneStepLaplaceContraction C.toNNReal C⁻¹.toNNReal < 1 ∧ ∀ x ∈ closure (Support.cubeSetAt y (n - 1)), ∫⁻ (eta : MarkovProcess.ContinuousPath alpha), Process.ContinuousPath.discountedStoppingWeight (C * Support.exitTimeScale M n)⁻¹ (MarkovProcess.ContinuousPath.exitTime U) eta ∂(MarkovProcess.SubMarkovKernelSemigroup.IsConservative.continuousProcess P hP) (emb x) ≤ oneStepLaplaceContraction C.toNNReal C⁻¹.toNNReal

The one-step Laplace estimate on a good cube of the full stream field, read inside a carrier. The cube is read in the state space of the process through a map emb, and U is the set it is read as. The constants of the joint exit-time estimate for the full field give a scale-independent strict contraction at the reading of every point of the closed inner cube, at discount rate (C * T(3^n))⁻¹.

3. The collected contraction

theorem Algsuperdiff.Section5.Provider.one_step_laplace_step_of_good_sites_stream_image (d : ℕ) (hdim : 2 ≤ d) (cstar : ℝ) (hcstar : 0 < cstar) (Creg : ℝ) (hCreg : 0 < Creg) : ∃ (gamma0 : ℝ) (Cev : ℝ) (C : ℝ) (c : ℝ), 0 < gamma0 ∧ 0 < Cev ∧ 0 < C ∧ 0 < c ∧ ∀ (M : Section3.ABKModel d), Section3.Disorder.cstar M = cstar → M.gamma ≤ gamma0 → ∀ ep ∈ Set.Ioc 0 (1 / 4), ep ≤ c → ∀ (n : ℤ) (omega : Field.FullSample d M.gamma) (i : Fin d) (r : ℕ) (sites : Fin r ↪ Percolation.Site d), (∀ (j : Fin r), ↑omega ∈ Support.qEvent M Creg Cev n (Support.rescaledLatticePoint n (sites j)) ep) → ∀ (alpha : Type) [inst : MetricSpace alpha] [inst_1 : CompleteSpace alpha] [inst_2 : MeasurableSpace alpha] [inst_3 : BorelSpace alpha] [inst_4 : SecondCountableTopology alpha] [inst_5 : Nonempty alpha] [LocallyCompactSpace alpha] (emb : HCPolySupport.Vec d → alpha) (P : MarkovProcess.SubMarkovKernelSemigroup alpha) (hP : P.IsConservative), P.IsFellerKernelSemigroup → P.KolmogorovRegular hP → (∀ (j : Fin r), IsCubeExitTimeSolutionDataStream M n omega alpha P hP (emb '' Support.cubeSetAt (Support.rescaledLatticePoint n (sites j)) n) emb i (Support.rescaledLatticePoint n (sites j))) → 0 < (C * Support.exitTimeScale M n)⁻¹ ∧ oneStepLaplaceContraction C.toNNReal C⁻¹.toNNReal < 1 ∧ ∀ (j : Fin r), ∀ z ∈ closure (Support.cubeSetAt (Trace.rescaleSite (n - 1) (sites j)) (n - 1)), ∫⁻ (eta : MarkovProcess.ContinuousPath alpha), Process.ContinuousPath.discountedStoppingWeight (C * Support.exitTimeScale M n)⁻¹ (MarkovProcess.ContinuousPath.exitTime (emb '' Support.cubeSetAt (Trace.rescaleSite (n - 1) (sites j)) n)) eta ∂(MarkovProcess.SubMarkovKernelSemigroup.IsConservative.continuousProcess P hP) (emb z) ≤ oneStepLaplaceContraction C.toNNReal C⁻¹.toNNReal

The one-step estimate for the full stream field, collected over a family of good cells. For a finite injective family of scale-n lattice sites whose cells are all good at one sample of the full field, one common discount rate (C T(3^n))⁻¹ and one common contraction factor serve every read cell at once.

theorem Algsuperdiff.Section5.Provider.one_step_laplace_hone_of_good_sites_stream_image (d : ℕ) (hdim : 2 ≤ d) (cstar : ℝ) (hcstar : 0 < cstar) (Creg : ℝ) (hCreg : 0 < Creg) : ∃ (gamma0 : ℝ) (Cev : ℝ) (C : ℝ) (c : ℝ), 0 < gamma0 ∧ 0 < Cev ∧ 0 < C ∧ 0 < c ∧ ∀ (M : Section3.ABKModel d), Section3.Disorder.cstar M = cstar → M.gamma ≤ gamma0 → ∀ ep ∈ Set.Ioc 0 (1 / 4), ep ≤ c → ∀ (n : ℤ) (omega : Field.FullSample d M.gamma) (i : Fin d) (r : ℕ) (sites : Fin r ↪ Percolation.Site d), (∀ (j : Fin r), ↑omega ∈ Support.qEvent M Creg Cev n (Support.rescaledLatticePoint n (sites j)) ep) → ∀ (alpha : Type) [inst : MetricSpace alpha] [inst_1 : CompleteSpace alpha] [inst_2 : MeasurableSpace alpha] [inst_3 : BorelSpace alpha] [inst_4 : SecondCountableTopology alpha] [inst_5 : Nonempty alpha] [LocallyCompactSpace alpha] (emb : C(HCPolySupport.Vec d, alpha)) (P : MarkovProcess.SubMarkovKernelSemigroup alpha) (hP : P.IsConservative), P.IsFellerKernelSemigroup → P.KolmogorovRegular hP → (∀ (j : Fin r), IsCubeExitTimeSolutionDataStream M n omega alpha P hP (⇑emb '' Support.cubeSetAt (Support.rescaledLatticePoint n (sites j)) n) (⇑emb) i (Support.rescaledLatticePoint n (sites j))) → 0 < (C * Support.exitTimeScale M n)⁻¹ ∧ oneStepLaplaceContraction C.toNNReal C⁻¹.toNNReal < 1 ∧ ∀ (l : ℕ), ∀ z ∈ ⇑emb '' Trace.enumeratedClosedCubeFamily (n - 1) sites l, ∫⁻ (eta : MarkovProcess.ContinuousPath alpha), Process.ContinuousPath.discountedStoppingWeight (C * Support.exitTimeScale M n)⁻¹ (MarkovProcess.ContinuousPath.exitTime (⇑emb '' Trace.enumeratedOpenEnlargementFamily (n - 1) sites l)) eta ∂(MarkovProcess.SubMarkovKernelSemigroup.IsConservative.continuousProcess P hP) z ≤ oneStepLaplaceContraction C.toNNReal C⁻¹.toNNReal

The collected estimate for the full stream field, in the padded-family form. The read cells and their read enlargements are the padded families indexed by ℕ, which is the hypothesis the hit-then-exit estimate consumes.