Definitions in the public statement

This module contains the transparent definitions used by the solution. They are repeated in Challenge.lean, whose statement is checked independently by the comparator.

noncomputable def LeanPool.Besicovitch.lowerOneDensity {X : Type u_1} [MetricSpace X] [MeasurableSpace X] [BorelSpace X] (s : Set X) (x : X) : ENNReal

The lower one-density of s at x, normalized by the diameter 2 * r of a ball.

Equations

• One or more equations did not get rendered due to their size.

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

A set is countably one-rectifiable if Lipschitz curves cover it up to Hausdorff null measure.

Equations

• One or more equations did not get rendered due to their size.

def LeanPool.Besicovitch.ForcesOneRectifiability (X : Type u_2) [MetricSpace X] [MeasurableSpace X] [BorelSpace X] (β : ENNReal) : Prop

Every finite-measure set with lower density at least β is one-rectifiable.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LeanPool.Besicovitch.sigmaOne (X : Type u_2) [MetricSpace X] [MeasurableSpace X] [BorelSpace X] : ℝ

The infimum of the nonnegative thresholds forcing one-rectifiability in X.

Equations

• LeanPool.Besicovitch.sigmaOne X = sInf {β : ℝ | 0 ≤ β ∧ LeanPool.Besicovitch.ForcesOneRectifiability X (ENNReal.ofReal β)}

def LeanPool.Besicovitch.IsEndpointPair (c B : ℝ) : Prop

The isolated radical system whose first coordinate is twice the six-point endpoint.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def LeanPool.Besicovitch.cStar : ℝ

Twice the optimal six-point constant, defined by its isolated exact system.

Equations

• LeanPool.Besicovitch.cStar = sInf {c : ℝ | ∃ (B : ℝ), LeanPool.Besicovitch.IsEndpointPair c B}

noncomputable def LeanPool.Besicovitch.sStar : ℝ

The optimal two-colour six-point constant.

Equations

• LeanPool.Besicovitch.sStar = LeanPool.Besicovitch.cStar / 2