Grid increments of the local stable process

The exact product law for all increments along a regular grid, including the empty grid.

theorem BGW.StableTrees.measure_grid_increments_le {θ : ℝ} (hθ : 1 < θ ∧ θ ≤ 2) (a : NNReal) {h : NNReal} (hh : 0 < h) (n : ℕ) (δ : ℝ) : ↑(stableLocalLaw θ) {f : Skorokhod.DLoc | ∀ k < n, ↑f (a + (↑k + 1) * h) - ↑f (a + ↑k * h) ≤ δ} = ↑(stableLaw θ) (Set.Iic (δ * ↑h ^ (-(1 / θ)))) ^ n

Grid increments: the probability that the n increments of the local stable process over the grid a, a + h, …, a + n h are all at most δ is stableLaw θ (Iic (δ h^{-1/θ}))^n (independent increments with laws stableLawAt θ h).