Cubes

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

A centered cubic exhaustion of Euclidean space

The whole-space divergence-form construction uses the open cubes (-3^m, 3^m)^d. This file records their elementary geometry independently of the analytic resolvents built on them.

def DivergenceFormProcess.Form.wholeSpaceCube (d m : ℕ) : Set (HCPolySupport.Vec d)

The open cube (-3^m, 3^m)^d.

Equations

• DivergenceFormProcess.Form.wholeSpaceCube d m = HCPolySupport.axisCube (fun (x : Fin d) => -3 ^ m) (2 * 3 ^ m)

@[simp]

theorem DivergenceFormProcess.Form.mem_wholeSpaceCube_iff {d m : ℕ} {x : HCPolySupport.Vec d} : x ∈ wholeSpaceCube d m ↔ ∀ (i : Fin d), -3 ^ m < x i ∧ x i < 3 ^ m

theorem DivergenceFormProcess.Form.isOpenBoundedConvexDomain_wholeSpaceCube (d m : ℕ) : HCPolySupport.IsOpenBoundedConvexDomain (wholeSpaceCube d m)

Every exhaustion cube is an open bounded convex domain.

theorem DivergenceFormProcess.Form.wholeSpaceCube_subset_succ (d m : ℕ) : wholeSpaceCube d m ⊆ wholeSpaceCube d (m + 1)

Consecutive cubes in the exhaustion are nested.