OneStepLaplaceComposer

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

The contraction factor and the site embedding of the one-step Laplace estimate

The one-step estimate on a good cube produces, at one centre, a strict contraction for the negative exponential of the exit time from the enlarged cube. Its discount rate is (C T(3^n))⁻¹ and its factor is oneStepLaplaceContraction at the two scale constants of the exit-time comparison, and neither depends on the centre of the cell, on the direction of the datum, or on the sample: the constant C of the exit-time comparison is returned once and for all, before the model, the accuracy, the scale and the centre are quantified.

The two indexings

The cells are the closed scale-(n-1) cells z + □_{n-1} centred at the embedded lattice sites 3^{n-1} z, and the enlargements are the open cubes z + □_n. The one-step estimate speaks of the pair (closure (y + □_{n-1}), y + □_n), so the two agree once the site embedding rescaledLatticePoint n is recognized as rescaleSite (n - 1).

Main results

• oneStepLaplaceContraction_ne_top, oneStepLaplaceContraction_lt_one — the contraction factor is finite and strictly below one.
• rescaledLatticePoint_eq_rescaleSite, good_goodSiteEnum — the site embedding of the two indexings above, and the goodness of an enumerated site.

References

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

1. The contraction factor

theorem Algsuperdiff.Section5.Provider.oneStepLaplaceContraction_ne_top (Cup clow : NNReal) : oneStepLaplaceContraction Cup clow ≠ ⊤

The contraction factor is finite.

theorem Algsuperdiff.Section5.Provider.oneStepLaplaceContraction_lt_one {Cup clow : NNReal} (hCup : 0 < Cup) (hclow : 0 < clow) : oneStepLaplaceContraction Cup clow < 1

The contraction factor is strictly below one whenever both scale constants are positive.

3. The site embedding

theorem Algsuperdiff.Section5.Provider.rescaledLatticePoint_eq_rescaleSite {d : ℕ} (n : ℤ) (z : Percolation.Site d) : Support.rescaledLatticePoint n z = Trace.rescaleSite (n - 1) z

The embedding of the site lattice used by the good cube events is the embedding of the scale-(n-1) partition.

theorem Algsuperdiff.Section5.Provider.good_goodSiteEnum {d k : ℕ} (Good : Percolation.Site d → Prop) [DecidablePred Good] (j : Fin (Trace.goodSites k Good).card) : Good ((Trace.goodSiteEnum k Good) j)

Every enumerated site of a centred lattice cube is good.