Finite time cells for the Gaussian collar

The Caccioppoli cylinders use open time intervals. Half-step starts ensure that these intervals cover the collar while keeping a uniform overlap bound.

noncomputable def ESS.buGaussianTimeGridCount (σ T δ : ℝ) : ℕ

The finite number of time cells needed to cover (σ,T).

Equations

• ESS.buGaussianTimeGridCount σ T δ = ⌈2 * (T - σ) / δ⌉₊ + 1

noncomputable def ESS.buGaussianTimeGridStart (σ δ : ℝ) (j : ℕ) : ℝ

The start of a half-step time cell.

Equations

• ESS.buGaussianTimeGridStart σ δ j = σ + ↑j * δ / 2

def ESS.buGaussianTimeGridInner (σ δ : ℝ) (j : ℕ) : Set ℝ

The inner time interval in a half-step grid.

Equations

• ESS.buGaussianTimeGridInner σ δ j = Set.Ioo (ESS.buGaussianTimeGridStart σ δ j) (ESS.buGaussianTimeGridStart σ δ j + δ)

def ESS.buGaussianTimeGridOuter (σ δ : ℝ) (j : ℕ) : Set ℝ

The outer time interval needed by ESS.caccioppoli.

Equations

• ESS.buGaussianTimeGridOuter σ δ j = Set.Ioo (ESS.buGaussianTimeGridStart σ δ j) (ESS.buGaussianTimeGridStart σ δ j + 4 * δ)

theorem ESS.buGaussian_time_grid_covers {σ T δ : ℝ} (hσT : σ < T) (hδ : 0 < δ) (s : ℝ) (hs : s ∈ Set.Ioo σ T) : ∃ j ∈ Finset.range (buGaussianTimeGridCount σ T δ), s ∈ buGaussianTimeGridInner σ δ j

Every point strictly between σ and T is in one of the inner cells.

theorem ESS.buGaussian_time_grid_outer_subset {σ T δ : ℝ} (hσT : σ < T) (hδ : 0 < δ) (hmargin : T + 5 * δ ≤ 2) (j : ℕ) (hj : j < buGaussianTimeGridCount σ T δ) : buGaussianTimeGridOuter σ δ j ⊆ Set.Ioo σ 2

All outer time cells stay in (σ,2) when their terminal range has a small fixed margin before time 2.

theorem ESS.buGaussian_time_grid_outer_multiplicity {σ δ : ℝ} (hδ : 0 < δ) (J : Finset ℕ) (s : ℝ) : (∑ j ∈ J, if s ∈ buGaussianTimeGridOuter σ δ j then 1 else 0) ≤ 8

The outer time windows of a half-step grid have multiplicity at most eight, uniformly in the cell length.