PenalizedInterchangeGeometry

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

Cube geometry for the exterior-penalization interchange

The support cube is surrounded by a fixed compact collar inside the next exhaustion cube. Every point beyond that collar has a unit Euclidean ball disjoint from the support, and unit balls around the inner cube fit in its successor.

def DivergenceFormProcess.Form.interchangeCollar (d v : ℕ) : Set (HCPolySupport.Vec d)

The closed sup-norm collar used around the support cube.

Equations

• DivergenceFormProcess.Form.interchangeCollar d v = Metric.closedBall 0 (3 ^ v + 1)

theorem DivergenceFormProcess.Form.wholeSpaceCube_subset_interchangeCollar (d v : ℕ) : wholeSpaceCube d v ⊆ interchangeCollar d v

The support cube lies in its closed collar.

theorem DivergenceFormProcess.Form.isCompact_interchangeCollar (d v : ℕ) : IsCompact (interchangeCollar d v)

The closed collar is compact.

theorem DivergenceFormProcess.Form.interchangeCollar_subset_wholeSpaceCube_succ (d v : ℕ) : interchangeCollar d v ⊆ wholeSpaceCube d (v + 1)

The closed collar lies strictly inside the next exhaustion cube.

theorem DivergenceFormProcess.Form.disjoint_unitBall_wholeSpaceCube_of_notMem_interchangeCollar {d : ℕ} (v : ℕ) {x : HCPolySupport.Vec d} (hx : x ∉ interchangeCollar d v) : Disjoint (HCPolySupport.euclideanBall x 1) (wholeSpaceCube d v)

A point beyond the collar has a unit Euclidean ball disjoint from the support cube.

theorem DivergenceFormProcess.Form.unitBall_subset_wholeSpaceCube_succ {d m : ℕ} {x : HCPolySupport.Vec d} (hx : x ∈ wholeSpaceCube d m) : HCPolySupport.euclideanBall x 1 ⊆ wholeSpaceCube d (m + 1)

A unit Euclidean ball around the m-th cube lies in the successor cube.