ExitTimeHomogenizationJointEvent

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

Monotonicity of the good cube event in its two parameters

The percolation estimate counts the sites at which the event

  Q(z + □_n, ε) = 𝒢(z + □_n, ε) ∩ 𝒥(z + □_n, C⁻¹ ε γ^{-1/2})

occurs, and the exit-time comparison on a good cube is stated on the same event with its own constant in place of C. The two therefore speak the same event as soon as the two constants agree, and where they do not agree the inclusions of this file convert one into the other: the event grows with the accuracy ε and shrinks as the constant C grows, because C enters only through the threshold C⁻¹ ε γ^{-1/2} of the large-scale event.

The consequence used downstream is the rescaling of the accuracy: replacing ε by ε / max 1 C turns the event formed with the constant 1 into the event formed with the constant C, at every centre and every scale.

References

• ABK26, the chains of good cubes of Section 5.2.

1. The two halves

theorem Algsuperdiff.Section5.Support.largeScaleEventBase_mono {d : ℕ} (M : Section3.ABKModel d) (n : ℤ) {theta theta' : ℝ} (h : theta ≤ theta') : largeScaleEventBase M n theta ⊆ largeScaleEventBase M n theta'

The large-scale event grows with its threshold.

theorem Algsuperdiff.Section5.Support.largeScaleEvent_mono {d : ℕ} (M : Section3.ABKModel d) (n : ℤ) (y : HCPolySupport.Vec d) {theta theta' : ℝ} (h : theta ≤ theta') : largeScaleEvent M n y theta ⊆ largeScaleEvent M n y theta'

The large-scale event on a translated cube grows with its threshold.

theorem Algsuperdiff.Section5.Support.goodCubeEvent_mono {d : ℕ} (M : Section3.ABKModel d) (n : ℤ) (y : HCPolySupport.Vec d) {Creg Creg' ep ep' : ℝ} (hCreg : Creg ≤ Creg') (hep : ep ≤ ep') : goodCubeEvent M Creg n y ep ⊆ goodCubeEvent M Creg' n y ep'

The good cube event grows with the accuracy and with the regularity constant.

2. The event Q

theorem Algsuperdiff.Section5.Support.qEvent_antitone_const {d : ℕ} (M : Section3.ABKModel d) (Creg : ℝ) {Cinj Cinj' : ℝ} (hCinj : 0 < Cinj) (hle : Cinj ≤ Cinj') (n : ℤ) (z : HCPolySupport.Vec d) {ep : ℝ} (hep : 0 ≤ ep) : qEvent M Creg Cinj' n z ep ⊆ qEvent M Creg Cinj n z ep

Q shrinks as the constant grows. The constant enters only through the threshold C⁻¹ ε γ^{-1/2} of the large-scale event, which decreases.

theorem Algsuperdiff.Section5.Support.qEvent_rescaled_accuracy_subset {d : ℕ} (M : Section3.ABKModel d) (Creg : ℝ) {Cinj : ℝ} (hCinj : 0 < Cinj) (n : ℤ) (z : HCPolySupport.Vec d) {ep : ℝ} (hep : 0 ≤ ep) : qEvent M Creg 1 n z (ep / max 1 Cinj) ⊆ qEvent M Creg Cinj n z ep

The accuracy rescaling. Dividing the accuracy by max 1 C turns the event formed with the constant 1 into the event formed with the constant C; both halves only improve, since ε / max 1 C ≤ ε and ε / max 1 C ≤ C⁻¹ ε.

3. The site count

theorem Algsuperdiff.Section5.Support.qSiteCount_mono {d : ℕ} (M : Section3.ABKModel d) (Creg : ℝ) {Cinj Cinj' : ℝ} (n : ℤ) {ep ep' : ℝ} (S : Finset (Fin d → ℤ)) (omega : Section3.Cutoff.CutoffSample d) (hsub : ∀ (z : Fin d → ℤ), qEvent M Creg Cinj n (rescaledLatticePoint n z) ep ⊆ qEvent M Creg Cinj' n (rescaledLatticePoint n z) ep') : qSiteCount M Creg Cinj n ep S omega ≤ qSiteCount M Creg Cinj' n ep' S omega

The site count is monotone under an inclusion of events.