EarlyExitScaleMoments

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

The confinement scale with its moment field and its restricted displacement tail

The quenched estimates at the random confinement scale are read by two further layers, and both of them ask for more about the family of displacement scales than the early-exit probability alone.

The annealed components of the superdiffusive bound need uniform bounds on the moments of that family, of orders 4p and 8p, at one constant and over a range of exponents. The removal steps of the quenched composer need the displacement tail of the process at every scale above the confinement scale, not only at the confinement scale itself.

Both are consequences of the same construction: the crossing scales of the percolation estimate have an exponential tail, whose integration gives the moments; and the regime of the chained early-exit estimate is met at every scale above the confinement scale, which gives the tail there. This module packages them with the data they must be read at — one family, one confinement constant, one deterministic factor, hence one confinement scale.

Main results

• measureReal_exitEvent_confinementScale_le_pow_of_threshold — the early-exit probability at the confinement scale together with the moment field of the displacement scales and the restricted displacement tail, at one and the same family.

References

• ABK26, the early-exit estimate of Section 5.3 and the superdiffusive displacement bounds of Section 5.4.

theorem Algsuperdiff.Section5.Provider.measureReal_exitEvent_confinementScale_le_pow_of_threshold (d : ℕ) [NeZero d] (hdim : 2 ≤ d) (cstar : ℝ) (hcstar : 0 < cstar) : ∃ (gamma0 : ℝ) (Cscale : ℝ) (CSbar : ℝ) (Kbar : ℝ) (cbar : ℝ), 0 < gamma0 ∧ 1 ≤ Cscale ∧ 1 ≤ CSbar ∧ 1 ≤ Kbar ∧ 0 < cbar ∧ cbar ≤ 1 ∧ ∀ (M : Section3.ABKModel d), Section3.Disorder.cstar M = cstar → M.gamma ≤ gamma0 → ∀ (t : ℝ), 0 < t → ∀ (Kmin : ℝ), ∃ (S : ℤ → Section3.Cutoff.CutoffSample d → ℝ) (K : ℝ) (L : ℝ) (c : ℝ) (CS : ℝ) (pS : ℝ), 1 ≤ K ∧ Kmin ≤ K ∧ 0 < c ∧ c ≤ 1 ∧ cbar ≤ c ∧ L = K * √|Real.log M.gamma| * Support.intrinsicScale M.nu cstar M.gamma t ∧ (∃ (delta : ℝ) (Y : ℤ → Section3.Cutoff.CutoffSample d → ℕ), 0 < delta ∧ delta ≤ 1 ∧ (∀ (i : ℤ), Measurable (Y i)) ∧ ∀ (i : ℤ) (omega : Section3.Cutoff.CutoffSample d), S i omega = Support.displacementScale delta M.gamma (Y i omega)) ∧ (∀ (n : ℤ), Measurable (S n)) ∧ (∀ (n : ℤ) (omega : Section3.Cutoff.CutoffSample d), 0 ≤ S n omega) ∧ 1 ≤ CS ∧ 1 ≤ pS ∧ CS ≤ CSbar ∧ K ≤ max Kbar Kmin ∧ Cscale⁻¹ * M.gamma⁻¹ * |Real.log M.gamma| ^ (-6) ≤ pS ∧ (∀ (p : ℝ), 1 ≤ p → p ≤ pS → (∀ (n : ℤ), ∫⁻ (omega : Section3.Cutoff.CutoffSample d), ENNReal.ofReal (S n omega) ^ (4 * p) ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal CS ^ (4 * p)) ∧ ∀ (n : ℤ), ∫⁻ (omega : Section3.Cutoff.CutoffSample d), ENNReal.ofReal (S n omega) ^ (8 * p) ∂↑(Section3.Cutoff.cutoffSampleLaw M) ≤ ENNReal.ofReal CS ^ (8 * p)) ∧ (∀ᵐ (omega : Field.FullSample d M.gamma) ∂↑(Field.fullSampleLaw M), Support.IsConfinementScale (fun (n : ℤ) => Support.widenedScale (fun (i : ℤ) => S i ↑omega) n) L (Support.confinementScale S L ↑omega)) ∧ (∀ᵐ (omega : Field.FullSample d M.gamma) ∂↑(Field.fullSampleLaw M), (((Field.streamExhaustionTailInput M omega).wholeSpaceProcess ↑0) (DivergenceFormProcess.StoppedDirichlet.survivalEvent (OnePoint.some '' Support.cubeSetAt 0 (Support.confinementScale S L ↑omega)) t.toNNReal)ᶜ).toReal ≤ M.gamma ^ 100) ∧ (∀ᵐ (omega : Field.FullSample d M.gamma) ∂↑(Field.fullSampleLaw M), ∀ (k : ℤ), 3 ^ Support.confinementScale S L ↑omega ≤ 3 ^ k → ((Field.streamExhaustionTailInput M omega).wholeSpaceProcess ↑0) {eta : MarkovProcess.ContinuousPath (OnePoint (HCPolySupport.Vec d)) | 1 / 2 * 3 ^ k ≤ ‖DivergenceFormProcess.Form.onePointRetract 0 ⋯‖} ≤ ENNReal.ofReal (Real.exp (-c * Support.displacementMinScale M.nu cstar M.gamma t k))) ∧ (∀ᵐ (omega : Field.FullSample d M.gamma) ∂↑(Field.fullSampleLaw M), ∀ (k : ℤ), 3 ^ Support.confinementScale S L ↑omega ≤ 3 ^ k → ((Field.streamProcess M omega) ↑0).real {eta : MarkovProcess.ContinuousPath (OnePoint (HCPolySupport.Vec d)) | 1 / 2 * 3 ^ k ≤ ‖⋯‖} ≤ Real.exp (-c * (3 ^ k / 3 ^ Support.confinementScale S L ↑omega) ^ 2)) ∧ ∀ᵐ (omega : Field.FullSample d M.gamma) ∂↑(Field.fullSampleLaw M), ∀ (k : ℤ), 3 ^ Support.confinementScale S L ↑omega ≤ 3 ^ k → ((Field.streamProcess M omega) ↑0).real {eta : MarkovProcess.ContinuousPath (OnePoint (HCPolySupport.Vec d)) | 1 / 2 * 3 ^ k ≤ ‖⋯‖} ≤ Real.exp (-cbar * (3 ^ k / 3 ^ Support.confinementScale S L ↑omega) ^ 2)

The early-exit probability, the moment field and the restricted displacement tail at one confinement scale, with uniform constants. Beside the early-exit probability at the confinement scale, the family of displacement scales is returned with its measurability, its nonnegativity and a uniform bound on its moments of order 4p and 8p for every exponent p between 1 and the returned pS, at the single constant CS; and the process is returned with its displacement tail at every scale above the confinement scale, in the form carrying the two-branch minimum and in the form carrying the confinement radius, the latter at both the returned rate and the uniform rate cbar, which is the shape the removal steps read.

Four constants are returned before the model and the time, so that a caller whose own constants are fixed at that level can use them: Cscale, which bounds the range of exponents from below by Cscale⁻¹ γ^{-1} |log γ|^{-6} ≤ pS; CSbar and Kbar, which bound CS and K from above; and cbar, which bounds the exponential rate from below.

Everything is stated at one and the same S, K and L, hence at one and the same confinement scale, and the confinement constant is above the prescribed threshold Kmin, so a consumer with a further lower bound on it can impose that bound here.