Reduction to a straight purely unrectifiable set

A hypothetical nonrectifiable finite set has a positive purely unrectifiable part. A straight piece of that part retains every strictly smaller lower-density threshold almost everywhere.

theorem LeanPool.Besicovitch.exists_pure_straight_subset_of_not_rectifiable {e : Set (EuclideanSpace ℝ (Fin 2))} (he : MeasurableSet e) (he_fin : (MeasureTheory.Measure.hausdorffMeasure 1) e < ⊤) (he_not_rectifiable : ¬IsCountablyOneRectifiable e) {beta gamma : ℝ} (hbeta : 0 ≤ beta) (hbeta_gamma : beta < gamma) (hdensity : ∀ᵐ (x : EuclideanSpace ℝ (Fin 2)) ∂(MeasureTheory.Measure.hausdorffMeasure 1).restrict e, ENNReal.ofReal gamma ≤ lowerOneDensity e x) : ∃ (a : Set (EuclideanSpace ℝ (Fin 2))), MeasurableSet a ∧ a ⊆ e ∧ 0 < (MeasureTheory.Measure.hausdorffMeasure 1) a ∧ (MeasureTheory.Measure.hausdorffMeasure 1) a < ⊤ ∧ IsPurelyOneUnrectifiable a ∧ IsStraightMeasure ((MeasureTheory.Measure.hausdorffMeasure 1).restrict a) ∧ ∀ᵐ (x : EuclideanSpace ℝ (Fin 2)) ∂(MeasureTheory.Measure.hausdorffMeasure 1).restrict a, ENNReal.ofReal beta < lowerOneDensity a x

A nonrectifiable finite set with density at least gamma contains a positive straight, purely unrectifiable subset with density strictly above every beta < gamma.