A countable lattice cover by backward cells

Spatial mesh r/2 and temporal mesh r²/2 give a countable family of backward parabolic cells of radius r that covers the whole space-time.

noncomputable def CKN.Core.Step4.originLatticeCentre (r : ℝ) (k : (Fin 3 → ℤ) × ℤ) : Foundation.Parabolic.ParabolicPoint

The lattice with spatial mesh r/2 and temporal mesh r²/2.

Equations

• CKN.Core.Step4.originLatticeCentre r k = (fun (i : Fin 3) => r / 2 * ↑(k.1 i), r ^ 2 / 2 * ↑k.2)

theorem CKN.Core.Step4.originLattice_covers (r : ℝ) (hr : 0 < r) (z : Foundation.Parabolic.ParabolicPoint) : ∃ (k : (Fin 3 → ℤ) × ℤ), z ∈ Foundation.Parabolic.parabolicCylinder (originLatticeCentre r k).1 (originLatticeCentre r k).2 r

Every space-time point lies in a lattice cell of any positive radius.