Documentation

LeanPool.Besicovitch.Rectifiability.Basic

Basic facts about one-dimensional rectifiability #

Countable one-rectifiability is inherited by subsets and countable unions.

source
def LeanPool.Besicovitch.IsPurelyOneUnrectifiable {X : Type u_1} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] (s : Set X) :
Prop

A set is purely one-unrectifiable if it meets every rectifiable set in a null set.

Equations
Instances For
    source
    theorem LeanPool.Besicovitch.IsCountablyOneRectifiable.mono {X : Type u_1} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] {s t : Set X} (hs : IsCountablyOneRectifiable s) (ht : t ⊆ s) :
    IsCountablyOneRectifiable t

    A subset of a countably one-rectifiable set is countably one-rectifiable.

    source
    theorem LeanPool.Besicovitch.isCountablyOneRectifiable_of_measure_zero {X : Type u_1} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] [Nonempty X] {s : Set X} (hs : (MeasureTheory.Measure.hausdorffMeasure 1) s = 0) :
    IsCountablyOneRectifiable s

    A set of zero Hausdorff one-measure is countably one-rectifiable.

    source
    @[simp]
    theorem LeanPool.Besicovitch.isCountablyOneRectifiable_empty {X : Type u_1} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] [Nonempty X] :
    IsCountablyOneRectifiable ∅

    The empty set is countably one-rectifiable in a nonempty metric space.

    source
    theorem LeanPool.Besicovitch.isCountablyOneRectifiable_iUnion {X : Type u_1} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] {s : ℕ → Set X} (hs : ∀ (i : ℕ), IsCountablyOneRectifiable (s i)) :
    IsCountablyOneRectifiable (⋃ (i : ℕ), s i)

    A countable union of countably one-rectifiable sets is countably one-rectifiable.

    source
    theorem LeanPool.Besicovitch.IsCountablyOneRectifiable.union {X : Type u_1} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] {s t : Set X} (hs : IsCountablyOneRectifiable s) (ht : IsCountablyOneRectifiable t) :
    IsCountablyOneRectifiable (s ∪ t)

    The union of two countably one-rectifiable sets is countably one-rectifiable.

    source
    theorem LeanPool.Besicovitch.IsPurelyOneUnrectifiable.mono {X : Type u_1} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] {s t : Set X} (hs : IsPurelyOneUnrectifiable s) (ht : t ⊆ s) :
    IsPurelyOneUnrectifiable t

    Pure one-unrectifiability is inherited by subsets.

    source
    theorem LeanPool.Besicovitch.IsPurelyOneUnrectifiable.measure_zero_of_rectifiable_subset {X : Type u_1} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] {s t : Set X} (hs : IsPurelyOneUnrectifiable s) (ht : IsCountablyOneRectifiable t) (hts : t ⊆ s) :
    (MeasureTheory.Measure.hausdorffMeasure 1) t = 0

    A rectifiable subset of a purely unrectifiable set has zero Hausdorff one-measure.