Null projected triple ties

Coordinate projections of triple-tie strata form a null exceptional set for line slicing.

theorem LiebThirring.volume_planeProjection_affineSubspace_eq_zero (a : Fin 3) (S : AffineSubspace ℝ Position) (hS : Module.finrank ℝ ↥S.direction ≤ 1) : MeasureTheory.volume (planeProjection a '' ↑S) = 0

theorem LiebThirring.volume_planeProjection_voronoiTripleStratum {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) (a : Fin 3) : MeasureTheory.volume (planeProjection a '' voronoiTripleStratum R) = 0

theorem LiebThirring.volume_planeProjection_affinePlane_of_coordinate_zero (n b : Position) (hn : n ≠ 0) (a : Fin 3) (ha : n.ofLp a = 0) : MeasureTheory.volume (planeProjection a '' ↑(affinePlane n b)) = 0

A nontransverse plane projects into an affine line in the base plane.

theorem LiebThirring.volume_planeProjection_bisector_of_coordinate_zero {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) (k l : Fin M) (hkl : k ≠ l) (a : Fin 3) (ha : (bisectorNormal R k l).ofLp a = 0) : MeasureTheory.volume (planeProjection a '' ↑(bisectorPlane R k l)) = 0

def LiebThirring.slicingExceptionalSet {M : ℕ} (R : Fin M → Position) (a : Fin 3) : Set Planar

Bases excluded in the slicing proof: triple ties and nontransverse planes.

Equations

• One or more equations did not get rendered due to their size.

theorem LiebThirring.volume_slicingExceptionalSet {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) (a : Fin 3) : MeasureTheory.volume (slicingExceptionalSet R a) = 0

theorem LiebThirring.ae_notMem_slicingExceptionalSet {M : ℕ} (R : Fin M → Position) (hR : Function.Injective R) (a : Fin 3) : ∀ᵐ (q : Planar), q ∉ slicingExceptionalSet R a