Reduction from Lipschitz curves to Lipschitz pieces of g

If a Lipschitz curve f : ℝ → ℝ² meets Besicovitch's set Π in positive μH[1]-measure, then g is Lipschitz on a subset of [0, 1] of positive Lebesgue measure.

Let f₁ = π₁ ∘ f be the first coordinate of the curve and B = f ⁻¹ Π. By Rademacher's theorem f₁ is differentiable almost everywhere, and the curve over the null set of non-differentiability points carries no μH[1]-measure. Over the points where f₁' = 0 the image of f₁ is Lebesgue-null (the one-dimensional area formula), so the graph over it, which contains the curve there, is μH[1]-null by LeanPool.Besicovitch.Example.Hull. Hence the curve over the points with f₁' ≠ 0 has positive measure; a countable partition of these into pieces on which f₁ is well approximated by a nonzero linear map produces a piece P on which f₁ is bi-Lipschitz. On A = f₁ '' P the function g is then Lipschitz, since g (f₁ t) = f₂ t is Lipschitz in t and t is Lipschitz in f₁ t; and A has positive Lebesgue measure since the graph over A contains f '' P.

Besicovitch's set as a graph

theorem LeanPool.Besicovitch.Example.graphMap_eq_of_apply_one {p : Plane} (h : p.ofLp 1 = besicovitchFun (p.ofLp 0)) : graphMap (p.ofLp 0) = p

A point whose second coordinate is g of its first lies on the graph over that first coordinate.

theorem LeanPool.Besicovitch.Example.mem_besicovitchSet_iff {p : Plane} : p ∈ besicovitchSet ↔ p.ofLp 0 ∈ Set.Icc 0 1 ∧ p.ofLp 1 = besicovitchFun (p.ofLp 0)

Membership in Besicovitch's set in terms of coordinates.

theorem LeanPool.Besicovitch.Example.graphMap_eq_of_mem {p : Plane} (hp : p ∈ besicovitchSet) : graphMap (p.ofLp 0) = p

A point of Besicovitch's set is the graph point over its first coordinate.

theorem LeanPool.Besicovitch.Example.measurableSet_besicovitchSet : MeasurableSet besicovitchSet

Besicovitch's set is measurable.

Coordinates of a Lipschitz curve

theorem LeanPool.Besicovitch.Example.lipschitzWith_coord (i : Fin 2) : LipschitzWith 1 fun (p : Plane) => p.ofLp i

Each coordinate of the plane is 1-Lipschitz.

theorem LeanPool.Besicovitch.Example.lipschitzWith_curve_coord {K : NNReal} {f : ℝ → Plane} (hf : LipschitzWith K f) (i : Fin 2) : LipschitzWith K fun (t : ℝ) => (f t).ofLp i

A coordinate of a K-Lipschitz curve is K-Lipschitz.

theorem LeanPool.Besicovitch.Example.image_subset_graphMap_image {f : ℝ → Plane} {S : Set ℝ} (hS : S ⊆ f ⁻¹' besicovitchSet) : f '' S ⊆ graphMap '' (fun (t : ℝ) => (f t).ofLp 0) '' S

The curve over a set of its preimage of Π lies in the graph over the first coordinates.

theorem LeanPool.Besicovitch.Example.hausdorffMeasure_image_le_volume_image {f : ℝ → Plane} {S : Set ℝ} (hS : S ⊆ f ⁻¹' besicovitchSet) : (MeasureTheory.Measure.hausdorffMeasure 1) (f '' S) ≤ 2 * MeasureTheory.volume ((fun (t : ℝ) => (f t).ofLp 0) '' S)

The curve over a piece of its preimage of Π has μH[1]-measure at most twice the Lebesgue measure of the first coordinates.

theorem LeanPool.Besicovitch.Example.hausdorffMeasure_image_eq_zero_of_volume_eq_zero {K : NNReal} {f : ℝ → Plane} (hf : LipschitzWith K f) {N : Set ℝ} (hN : MeasureTheory.volume N = 0) : (MeasureTheory.Measure.hausdorffMeasure 1) (f '' N) = 0

A Lipschitz curve over a Lebesgue-null set is μH[1]-null.

theorem LeanPool.Besicovitch.Example.volume_image_eq_zero_of_fderiv_eq_zero {f₁ : ℝ → ℝ} {S : Set ℝ} (hS : ∀ t ∈ S, DifferentiableAt ℝ f₁ t ∧ fderiv ℝ f₁ t = 0) : MeasureTheory.volume (f₁ '' S) = 0

The image of a set on which a real function has zero derivative is Lebesgue-null.

Pieces on which the first coordinate is bi-Lipschitz

theorem LeanPool.Besicovitch.Example.clm_apply_eq_mul (A : ℝ →L[ℝ] ℝ) (z : ℝ) : A z = z * A 1

A linear map ℝ → ℝ is multiplication by its value at 1.

theorem LeanPool.Besicovitch.Example.clm_norm_le_abs_apply_one (A : ℝ →L[ℝ] ℝ) : ‖A‖ ≤ |A 1|

The operator norm of a linear map ℝ → ℝ is at most its value at 1.

theorem LeanPool.Besicovitch.Example.clm_abs_apply_one_pos {A : ℝ →L[ℝ] ℝ} (hA : A ≠ 0) : 0 < |A 1|

A nonzero linear map ℝ → ℝ has nonzero value at 1.

theorem LeanPool.Besicovitch.Example.abs_sub_le_of_approximatesLinearOn {f₁ : ℝ → ℝ} {A : ℝ →L[ℝ] ℝ} {P : Set ℝ} (happ : ApproximatesLinearOn f₁ A P (‖A‖₊ / 2)) {x y : ℝ} (hx : x ∈ P) (hy : y ∈ P) : |A 1| / 2 * |x - y| ≤ |f₁ x - f₁ y|

A function approximated by a nonzero linear map A on P within ‖A‖ / 2 is bi-Lipschitz from below on P with constant |A 1| / 2.

theorem LeanPool.Besicovitch.Example.exists_lipschitzOnWith_of_piece {K : NNReal} {f : ℝ → Plane} (hf : LipschitzWith K f) {P : Set ℝ} (hP : P ⊆ f ⁻¹' besicovitchSet) {A : ℝ →L[ℝ] ℝ} (hA : A ≠ 0) (happ : ApproximatesLinearOn (fun (t : ℝ) => (f t).ofLp 0) A P (‖A‖₊ / 2)) (hpos : 0 < (MeasureTheory.Measure.hausdorffMeasure 1) (f '' P)) : ∃ (L : NNReal), ∃ S ⊆ Set.Icc 0 1, 0 < MeasureTheory.volume S ∧ LipschitzOnWith L besicovitchFun S

The conclusion on a single piece: if the curve over P ⊆ f ⁻¹' Π has positive μH[1]-measure and the first coordinate is well approximated on P by a nonzero linear map, then g is Lipschitz on the first coordinates of P, a set of positive measure.

The reduction

theorem LeanPool.Besicovitch.Example.exists_lipschitzOnWith_of_hausdorffMeasure_pos {K : NNReal} {f : ℝ → Plane} (hf : LipschitzWith K f) (hpos : 0 < (MeasureTheory.Measure.hausdorffMeasure 1) (Set.range f ∩ besicovitchSet)) : ∃ (L : NNReal), ∃ A ⊆ Set.Icc 0 1, 0 < MeasureTheory.volume A ∧ LipschitzOnWith L besicovitchFun A

Reduction. A Lipschitz curve meeting Besicovitch's set in positive μH[1]-measure yields a subset of [0, 1] of positive Lebesgue measure on which g is Lipschitz.