Normal height of Gaussian cell centers #
Cells meeting the high normal strip have centers far enough above the boundary for their averaging balls to remain in the positive half-space.
theorem
ESS.bu_short_ball_subset_halfspace
(X : CKN.Foundation.Parabolic.Vec3)
(R : ℝ)
(hX : R < X 2)
:
CKN.Foundation.Parabolic.vec3Ball X R ⊆ {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2}
A Euclidean ball stays above the boundary when its center height exceeds its radius.
theorem
ESS.bu_short_dyadic_center_height_gt_two
(k : ℤ)
(m : Fin 3 → ℤ)
(ell : Fin 2048)
(scale : ℝ)
(hscale : 0 < scale)
(hk : 0 ≤ k)
(z : CKN.Foundation.Parabolic.ParabolicPoint)
(hz : z ∈ CKN.Foundation.buSmallTimeDyadicCell k m ell)
(hheight : buShortYMinus scale ≤ z.1 2)
:
The center of a cell meeting the high normal strip has physical height greater than two.
theorem
ESS.bu_short_dyadic_center_average_geometry
(k : ℤ)
(m : Fin 3 → ℤ)
(ell : Fin 2048)
(scale : ℝ)
(hscale : 0 < scale)
(hscale1 : scale ≤ 1)
(hk : 1 ≤ k)
(z : CKN.Foundation.Parabolic.ParabolicPoint)
(hz : z ∈ CKN.Foundation.buSmallTimeDyadicCell k m ell)
(hheight : buShortYMinus scale ≤ z.1 2)
:
have Y := (CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).1;
have δ := (CKN.Foundation.buSmallTimeDyadicCellCenter k m ell).2;
2 < (scale • Y) 2 ∧ δ < 1 / 2 ∧ CKN.Foundation.Parabolic.vec3Ball Y √(3 * δ / 2) ⊆ {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2} ∧ CKN.Foundation.Parabolic.vec3Ball Y (2 * (√δ / 8)) ⊆ {x : CKN.Foundation.Parabolic.Vec3 | 0 < x 2}
A cell meeting the high strip has an averaging center and ball inside the positive half-space.