Dyadic cubes in the native three-dimensional carrier

The cubes use the half-open product grid on Vec3 = Fin 3 → ℝ. The scale index is integral so that parent and child cubes are represented uniformly.

@[reducible, inline]

abbrev CKN.Foundation.Euclidean.DyadicCorner : Type

Integer lattice coordinates locating a dyadic cube in three dimensions.

Equations

• CKN.Foundation.Euclidean.DyadicCorner = (Fin 3 → ℤ)

structure CKN.Foundation.Euclidean.DyadicIndex : Type

Integer scale and lattice corner specifying a half-open dyadic cube.

• scale : ℤ

  Dyadic scale index, with side length 2 ^ (-scale).

• corner : DyadicCorner

  Integer lattice corner of the dyadic cube.

noncomputable def CKN.Foundation.Euclidean.dyadicScale (k : ℤ) : ℝ

Side length of the dyadic grid at integer scale k.

Equations

• CKN.Foundation.Euclidean.dyadicScale k = 2 ^ (-k)

def CKN.Foundation.Euclidean.dyadicCube (k : ℤ) (a : DyadicCorner) : Set Parabolic.Vec3

Half-open dyadic cube with scale index k and lattice corner a.

Equations

• CKN.Foundation.Euclidean.dyadicCube k a = Set.univ.pi fun (i : Fin 3) => Set.Ico (↑(a i) * CKN.Foundation.Euclidean.dyadicScale k) ((↑(a i) + 1) * CKN.Foundation.Euclidean.dyadicScale k)

noncomputable def CKN.Foundation.Euclidean.dyadicCubeCenter (k : ℤ) (a : DyadicCorner) : Parabolic.Vec3

Center of a dyadic cube in native Euclidean coordinates.

Equations

• CKN.Foundation.Euclidean.dyadicCubeCenter k a i = (↑(a i) + 1 / 2) * CKN.Foundation.Euclidean.dyadicScale k

noncomputable def CKN.Foundation.Euclidean.dyadicCorner (k : ℤ) (x : Parabolic.Vec3) : DyadicCorner

Lattice corner of the unique grid cube containing a point.

Equations

• CKN.Foundation.Euclidean.dyadicCorner k x i = ⌊x i / CKN.Foundation.Euclidean.dyadicScale k⌋

def CKN.Foundation.Euclidean.dyadicParent (Q : DyadicIndex) : DyadicIndex

Immediate containing dyadic cube at the next coarser scale.

Equations

• CKN.Foundation.Euclidean.dyadicParent Q = { scale := Q.scale - 1, corner := fun (i : Fin 3) => Q.corner i / 2 }

@[simp]

theorem CKN.Foundation.Euclidean.mem_dyadicCube {k : ℤ} {a : DyadicCorner} {x : Parabolic.Vec3} : x ∈ dyadicCube k a ↔ ∀ (i : Fin 3), ↑(a i) * dyadicScale k ≤ x i ∧ x i < (↑(a i) + 1) * dyadicScale k

theorem CKN.Foundation.Euclidean.dyadicScale_pos (k : ℤ) : 0 < dyadicScale k

theorem CKN.Foundation.Euclidean.dyadicCube_measurable (k : ℤ) (a : DyadicCorner) : MeasurableSet (dyadicCube k a)

theorem CKN.Foundation.Euclidean.volume_dyadicCube (k : ℤ) (a : DyadicCorner) : MeasureTheory.volume (dyadicCube k a) = ENNReal.ofReal (dyadicScale k) ^ 3

theorem CKN.Foundation.Euclidean.volume_dyadicCube_eq_pow (k : ℤ) (a : DyadicCorner) : MeasureTheory.volume (dyadicCube k a) = ENNReal.ofReal (8 ^ (-k))

theorem CKN.Foundation.Euclidean.dyadicCube_nonempty (k : ℤ) (a : DyadicCorner) : (dyadicCube k a).Nonempty

theorem CKN.Foundation.Euclidean.mem_dyadicCube_of_corner (k : ℤ) (x : Parabolic.Vec3) : x ∈ dyadicCube k (dyadicCorner k x)

theorem CKN.Foundation.Euclidean.dyadicCorner_unique {k : ℤ} {x : Parabolic.Vec3} {a b : DyadicCorner} (ha : x ∈ dyadicCube k a) (hb : x ∈ dyadicCube k b) : a = b

theorem CKN.Foundation.Euclidean.dyadicCube_unique_at_scale {k : ℤ} {x : Parabolic.Vec3} : ∃! a : DyadicCorner, x ∈ dyadicCube k a

theorem CKN.Foundation.Euclidean.dyadicCube_subset_closedBall {k : ℤ} {a : DyadicCorner} {x : Parabolic.Vec3} (hx : x ∈ dyadicCube k a) : dyadicCube k a ⊆ Metric.closedBall x (dyadicScale k)

theorem CKN.Foundation.Euclidean.supBall_subset_dyadicCubeCenter (k : ℤ) (a : DyadicCorner) : Metric.ball (dyadicCubeCenter k a) (dyadicScale k / 2) ⊆ dyadicCube k a

theorem CKN.Foundation.Euclidean.dyadicScale_ratio {k l : ℤ} (hkl : k ≤ l) : ∃ (m : ℤ), 0 < m ∧ dyadicScale k = ↑m * dyadicScale l

theorem CKN.Foundation.Euclidean.dyadicCube_subset_parent (Q : DyadicIndex) : dyadicCube Q.scale Q.corner ⊆ dyadicCube (Q.scale - 1) fun (i : Fin 3) => Q.corner i / 2

theorem CKN.Foundation.Euclidean.dyadicCube_subset_of_intersect {k l : ℤ} (hkl : k ≤ l) {a b : DyadicCorner} (hint : (dyadicCube k a ∩ dyadicCube l b).Nonempty) : dyadicCube l b ⊆ dyadicCube k a

theorem CKN.Foundation.Euclidean.dyadicCube_nested_or_disjoint (Q R : DyadicIndex) : dyadicCube Q.scale Q.corner ⊆ dyadicCube R.scale R.corner ∨ dyadicCube R.scale R.corner ⊆ dyadicCube Q.scale Q.corner ∨ Disjoint (dyadicCube Q.scale Q.corner) (dyadicCube R.scale R.corner)

theorem CKN.Foundation.Euclidean.dyadicParent_volume_ratio (Q : DyadicIndex) : MeasureTheory.volume (dyadicCube (dyadicParent Q).scale (dyadicParent Q).corner) = 8 * MeasureTheory.volume (dyadicCube Q.scale Q.corner)