Straight pieces of finite Hausdorff sets #
This file proves the positive-piece form of Delaware's straight-set theorem for Hausdorff one-measure in the Euclidean plane. It also records the elementary restriction API used later.
theorem
LeanPool.Besicovitch.IsStraightMeasure.mono
{μ ν : MeasureTheory.Measure (EuclideanSpace ℝ (Fin 2))}
(hμ : IsStraightMeasure μ)
(hν : ν ≤ μ)
:
Straightness passes to a smaller measure.
theorem
LeanPool.Besicovitch.IsStraightMeasure.restrict
{μ : MeasureTheory.Measure (EuclideanSpace ℝ (Fin 2))}
(hμ : IsStraightMeasure μ)
(s : Set (EuclideanSpace ℝ (Fin 2)))
:
IsStraightMeasure (μ.restrict s)
Every restriction of a straight measure is straight.
theorem
LeanPool.Besicovitch.isStraightMeasure_restrict_mono
{s t : Set (EuclideanSpace ℝ (Fin 2))}
(hs : IsStraightMeasure ((MeasureTheory.Measure.hausdorffMeasure 1).restrict s))
(ht : t ⊆ s)
:
Straightness of a Hausdorff restriction passes to measurable subsets.
theorem
LeanPool.Besicovitch.exists_straight_measure_restrict_subset
{e : Set (EuclideanSpace ℝ (Fin 2))}
(he : MeasurableSet e)
(he_pos : 0 < (MeasureTheory.Measure.hausdorffMeasure 1) e)
(he_fin : (MeasureTheory.Measure.hausdorffMeasure 1) e < ⊤)
:
∃ (a : Set (EuclideanSpace ℝ (Fin 2))),
MeasurableSet a ∧ a ⊆ e ∧ 0 < (MeasureTheory.Measure.hausdorffMeasure 1) a ∧ IsStraightMeasure ((MeasureTheory.Measure.hausdorffMeasure 1).restrict a)
Every measurable set of positive finite Hausdorff one-measure has a positive straight piece.