Basic facts about the one-dimensional rectifiability threshold

The forcing property is monotone in its density threshold.

theorem LeanPool.Besicovitch.ForcesOneRectifiability.mono (X : Type u_1) [MetricSpace X] [MeasurableSpace X] [BorelSpace X] {β β' : ENNReal} (h : β ≤ β') (hβ : ForcesOneRectifiability X β) : ForcesOneRectifiability X β'

Forcing is monotone in the threshold: a larger density hypothesis is a stronger one.

theorem LeanPool.Besicovitch.bddBelow_admissibleThresholds (X : Type u_1) [MetricSpace X] [MeasurableSpace X] [BorelSpace X] : BddBelow {β : ℝ | 0 ≤ β ∧ ForcesOneRectifiability X (ENNReal.ofReal β)}

The admissible thresholds are bounded below, by 0.

theorem LeanPool.Besicovitch.sigmaOne_le_of_forces (X : Type u_1) [MetricSpace X] [MeasurableSpace X] [BorelSpace X] {b : ℝ} (hb : 0 ≤ b) (hforce : ForcesOneRectifiability X (ENNReal.ofReal b)) : sigmaOne X ≤ b

An admissible nonnegative threshold bounds sigmaOne from above.

theorem LeanPool.Besicovitch.sigmaOne_le_of_forall_gt (X : Type u_1) [MetricSpace X] [MeasurableSpace X] [BorelSpace X] {b : ℝ} (hb : 0 ≤ b) (hforce : ∀ (c : ℝ), b < c → ForcesOneRectifiability X (ENNReal.ofReal c)) : sigmaOne X ≤ b

Forcing rectifiability at every threshold above b proves sigmaOne ≤ b.