Import Besicovitch’s 0.6934 planar upper bound

LeanPool.lean

@@ -281,6 +281,106 @@ public import LeanPool.AsymptoticTrianglePacking.NibbleRounding
 public import LeanPool.BannaiBannaiStanton
 public import LeanPool.BannaiBannaiStanton.BoundOnDistanceSet
 public import LeanPool.Basic
+public import LeanPool.Besicovitch
+public import LeanPool.Besicovitch.BesicovitchPairCondition.Basic
+public import LeanPool.Besicovitch.BesicovitchPairCondition.Definitions
+public import LeanPool.Besicovitch.BesicovitchPairCondition.Extraction
+public import LeanPool.Besicovitch.BesicovitchPairCondition.PackingMeasure
+public import LeanPool.Besicovitch.BesicovitchPairCondition.Parameters
+public import LeanPool.Besicovitch.BesicovitchPairCondition.Rectifiability
+public import LeanPool.Besicovitch.BesicovitchPairCondition.RootBalls
+public import LeanPool.Besicovitch.BesicovitchPairCondition.SixPointTransfer
+public import LeanPool.Besicovitch.Certificates.DensePolynomial
+public import LeanPool.Besicovitch.Certificates.EndpointBridge
+public import LeanPool.Besicovitch.Certificates.EndpointIsolation
+public import LeanPool.Besicovitch.Certificates.Krawczyk
+public import LeanPool.Besicovitch.Certificates.RadicalInterval
+public import LeanPool.Besicovitch.Certificates.RationalInterval
+public import LeanPool.Besicovitch.Example.Avoid
+public import LeanPool.Besicovitch.Example.Cover
+public import LeanPool.Besicovitch.Example.Density
+public import LeanPool.Besicovitch.Example.Graph
+public import LeanPool.Besicovitch.Example.Hull
+public import LeanPool.Besicovitch.Example.LowerBound
+public import LeanPool.Besicovitch.Example.LowerDensity
+public import LeanPool.Besicovitch.Example.Measurable
+public import LeanPool.Besicovitch.Example.Plane
+public import LeanPool.Besicovitch.Example.Recursion
+public import LeanPool.Besicovitch.Example.Reduction
+public import LeanPool.Besicovitch.Example.Zero
+public import LeanPool.Besicovitch.Geometry.BallUnion
+public import LeanPool.Besicovitch.Geometry.ConvexEnlargement
+public import LeanPool.Besicovitch.Main.Bound
+public import LeanPool.Besicovitch.Main.RationalBound
+public import LeanPool.Besicovitch.Measure.CompactExhaustion
+public import LeanPool.Besicovitch.Measure.DensityBasic
+public import LeanPool.Besicovitch.Measure.DensityLocalization
+public import LeanPool.Besicovitch.Measure.UniformDensity
+public import LeanPool.Besicovitch.Measure.UniformDensityCompact
+public import LeanPool.Besicovitch.Rectifiability.AttachmentLocalization
+public import LeanPool.Besicovitch.Rectifiability.BadConvexLocalization
+public import LeanPool.Besicovitch.Rectifiability.BadConvexPacking
+public import LeanPool.Besicovitch.Rectifiability.BadConvexSets
+public import LeanPool.Besicovitch.Rectifiability.BadConvexThickening
+public import LeanPool.Besicovitch.Rectifiability.Basic
+public import LeanPool.Besicovitch.Rectifiability.CompactAttachmentUnion
+public import LeanPool.Besicovitch.Rectifiability.ComponentDiameter
+public import LeanPool.Besicovitch.Rectifiability.Continuum
+public import LeanPool.Besicovitch.Rectifiability.ContinuumSurgery
+public import LeanPool.Besicovitch.Rectifiability.ConvexAttachment
+public import LeanPool.Besicovitch.Rectifiability.Decomposition
+public import LeanPool.Besicovitch.Rectifiability.DensityPoint
+public import LeanPool.Besicovitch.Rectifiability.FiniteContinuum
+public import LeanPool.Besicovitch.Rectifiability.HoleMerging
+public import LeanPool.Besicovitch.Rectifiability.Selection
+public import LeanPool.Besicovitch.Rectifiability.Straight
+public import LeanPool.Besicovitch.Rectifiability.StraightReduction
+public import LeanPool.Besicovitch.Sigma.Basic
+public import LeanPool.Besicovitch.SixPoint.AlgebraicBasic
+public import LeanPool.Besicovitch.SixPoint.BlueChildSwap
+public import LeanPool.Besicovitch.SixPoint.CanonicalTriangle
+public import LeanPool.Besicovitch.SixPoint.ChildSwapPacking
+public import LeanPool.Besicovitch.SixPoint.Configuration
+public import LeanPool.Besicovitch.SixPoint.EndpointFailureClosed
+public import LeanPool.Besicovitch.SixPoint.EndpointGeometry
+public import LeanPool.Besicovitch.SixPoint.EndpointPacking
+public import LeanPool.Besicovitch.SixPoint.EndpointWeights
+public import LeanPool.Besicovitch.SixPoint.FailureTree
+public import LeanPool.Besicovitch.SixPoint.FiniteProperty
+public import LeanPool.Besicovitch.SixPoint.FourChildren
+public import LeanPool.Besicovitch.SixPoint.GramCertificateCore
+public import LeanPool.Besicovitch.SixPoint.GramCertificateCover
+public import LeanPool.Besicovitch.SixPoint.GramCertificateData
+public import LeanPool.Besicovitch.SixPoint.GramWeightedBound
+public import LeanPool.Besicovitch.SixPoint.LensEndpointBalancedE0S0
+public import LeanPool.Besicovitch.SixPoint.MatrixCorrections
+public import LeanPool.Besicovitch.SixPoint.NormEstimates
+public import LeanPool.Besicovitch.SixPoint.Normalization
+public import LeanPool.Besicovitch.SixPoint.Packing
+public import LeanPool.Besicovitch.SixPoint.PackingRelabel
+public import LeanPool.Besicovitch.SixPoint.RationalChord
+public import LeanPool.Besicovitch.SixPoint.Realization
+public import LeanPool.Besicovitch.SixPoint.RootEdge
+public import LeanPool.Besicovitch.SixPoint.RootEdgeClosed
+public import LeanPool.Besicovitch.SixPoint.RootEdgeFailureTree
+public import LeanPool.Besicovitch.SixPoint.RootEdgeType12
+public import LeanPool.Besicovitch.SixPoint.RowColumnRescue
+public import LeanPool.Besicovitch.SixPoint.Scaling
+public import LeanPool.Besicovitch.SixPoint.Score
+public import LeanPool.Besicovitch.SixPoint.SiblingFailureTree
+public import LeanPool.Besicovitch.SixPoint.SiblingIncidence
+public import LeanPool.Besicovitch.SixPoint.SiblingIncidenceClosed
+public import LeanPool.Besicovitch.SixPoint.SiblingIncidenceLedger
+public import LeanPool.Besicovitch.SixPoint.SiblingLens
+public import LeanPool.Besicovitch.SixPoint.SiblingLensE1S0
+public import LeanPool.Besicovitch.SixPoint.SiblingLensS0S0
+public import LeanPool.Besicovitch.SixPoint.SiblingLensS0S3
+public import LeanPool.Besicovitch.SixPoint.SiblingTangent
+public import LeanPool.Besicovitch.SixPoint.SiblingTriangle
+public import LeanPool.Besicovitch.SixPoint.WeightedFailure
+public import LeanPool.Besicovitch.SixPoint.WeightedReduction
+public import LeanPool.Besicovitch.Statement
+public import LeanPool.Besicovitch.Topology.ConnectedComponent
 public import LeanPool.Biswal
 public import LeanPool.Biswal.Theorem1
 public import LeanPool.Biswal.Theorem23

LeanPool/Besicovitch.lean

@@ -0,0 +1,115 @@
+/-
+Copyright (c) 2026 Yongxi Lin. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yongxi Lin
+-/
+
+module
+
+public import LeanPool.Besicovitch.BesicovitchPairCondition.Basic
+public import LeanPool.Besicovitch.BesicovitchPairCondition.Definitions
+public import LeanPool.Besicovitch.BesicovitchPairCondition.Extraction
+public import LeanPool.Besicovitch.BesicovitchPairCondition.PackingMeasure
+public import LeanPool.Besicovitch.BesicovitchPairCondition.Parameters
+public import LeanPool.Besicovitch.BesicovitchPairCondition.Rectifiability
+public import LeanPool.Besicovitch.BesicovitchPairCondition.RootBalls
+public import LeanPool.Besicovitch.BesicovitchPairCondition.SixPointTransfer
+public import LeanPool.Besicovitch.Certificates.DensePolynomial
+public import LeanPool.Besicovitch.Certificates.EndpointBridge
+public import LeanPool.Besicovitch.Certificates.EndpointIsolation
+public import LeanPool.Besicovitch.Certificates.Krawczyk
+public import LeanPool.Besicovitch.Certificates.RadicalInterval
+public import LeanPool.Besicovitch.Certificates.RationalInterval
+public import LeanPool.Besicovitch.Example.Avoid
+public import LeanPool.Besicovitch.Example.Cover
+public import LeanPool.Besicovitch.Example.Density
+public import LeanPool.Besicovitch.Example.Graph
+public import LeanPool.Besicovitch.Example.Hull
+public import LeanPool.Besicovitch.Example.LowerBound
+public import LeanPool.Besicovitch.Example.LowerDensity
+public import LeanPool.Besicovitch.Example.Measurable
+public import LeanPool.Besicovitch.Example.Plane
+public import LeanPool.Besicovitch.Example.Recursion
+public import LeanPool.Besicovitch.Example.Reduction
+public import LeanPool.Besicovitch.Example.Zero
+public import LeanPool.Besicovitch.Geometry.BallUnion
+public import LeanPool.Besicovitch.Geometry.ConvexEnlargement
+public import LeanPool.Besicovitch.Main.Bound
+public import LeanPool.Besicovitch.Main.RationalBound
+public import LeanPool.Besicovitch.Measure.CompactExhaustion
+public import LeanPool.Besicovitch.Measure.DensityBasic
+public import LeanPool.Besicovitch.Measure.DensityLocalization
+public import LeanPool.Besicovitch.Measure.UniformDensity
+public import LeanPool.Besicovitch.Measure.UniformDensityCompact
+public import LeanPool.Besicovitch.Rectifiability.AttachmentLocalization
+public import LeanPool.Besicovitch.Rectifiability.BadConvexLocalization
+public import LeanPool.Besicovitch.Rectifiability.BadConvexPacking
+public import LeanPool.Besicovitch.Rectifiability.BadConvexSets
+public import LeanPool.Besicovitch.Rectifiability.BadConvexThickening
+public import LeanPool.Besicovitch.Rectifiability.Basic
+public import LeanPool.Besicovitch.Rectifiability.CompactAttachmentUnion
+public import LeanPool.Besicovitch.Rectifiability.ComponentDiameter
+public import LeanPool.Besicovitch.Rectifiability.Continuum
+public import LeanPool.Besicovitch.Rectifiability.ContinuumSurgery
+public import LeanPool.Besicovitch.Rectifiability.ConvexAttachment
+public import LeanPool.Besicovitch.Rectifiability.Decomposition
+public import LeanPool.Besicovitch.Rectifiability.DensityPoint
+public import LeanPool.Besicovitch.Rectifiability.FiniteContinuum
+public import LeanPool.Besicovitch.Rectifiability.HoleMerging
+public import LeanPool.Besicovitch.Rectifiability.Selection
+public import LeanPool.Besicovitch.Rectifiability.Straight
+public import LeanPool.Besicovitch.Rectifiability.StraightReduction
+public import LeanPool.Besicovitch.Sigma.Basic
+public import LeanPool.Besicovitch.SixPoint.AlgebraicBasic
+public import LeanPool.Besicovitch.SixPoint.BlueChildSwap
+public import LeanPool.Besicovitch.SixPoint.CanonicalTriangle
+public import LeanPool.Besicovitch.SixPoint.ChildSwapPacking
+public import LeanPool.Besicovitch.SixPoint.Configuration
+public import LeanPool.Besicovitch.SixPoint.EndpointFailureClosed
+public import LeanPool.Besicovitch.SixPoint.EndpointGeometry
+public import LeanPool.Besicovitch.SixPoint.EndpointPacking
+public import LeanPool.Besicovitch.SixPoint.EndpointWeights
+public import LeanPool.Besicovitch.SixPoint.FailureTree
+public import LeanPool.Besicovitch.SixPoint.FiniteProperty
+public import LeanPool.Besicovitch.SixPoint.FourChildren
+public import LeanPool.Besicovitch.SixPoint.GramCertificateCore
+public import LeanPool.Besicovitch.SixPoint.GramCertificateCover
+public import LeanPool.Besicovitch.SixPoint.GramCertificateData
+public import LeanPool.Besicovitch.SixPoint.GramWeightedBound
+public import LeanPool.Besicovitch.SixPoint.LensEndpointBalancedE0S0
+public import LeanPool.Besicovitch.SixPoint.Normalization
+public import LeanPool.Besicovitch.SixPoint.Packing
+public import LeanPool.Besicovitch.SixPoint.RationalChord
+public import LeanPool.Besicovitch.SixPoint.Realization
+public import LeanPool.Besicovitch.SixPoint.RootEdge
+public import LeanPool.Besicovitch.SixPoint.RootEdgeClosed
+public import LeanPool.Besicovitch.SixPoint.RootEdgeFailureTree
+public import LeanPool.Besicovitch.SixPoint.RootEdgeType12
+public import LeanPool.Besicovitch.SixPoint.RowColumnRescue
+public import LeanPool.Besicovitch.SixPoint.Scaling
+public import LeanPool.Besicovitch.SixPoint.Score
+public import LeanPool.Besicovitch.SixPoint.SiblingFailureTree
+public import LeanPool.Besicovitch.SixPoint.SiblingIncidence
+public import LeanPool.Besicovitch.SixPoint.SiblingIncidenceClosed
+public import LeanPool.Besicovitch.SixPoint.SiblingIncidenceLedger
+public import LeanPool.Besicovitch.SixPoint.SiblingLens
+public import LeanPool.Besicovitch.SixPoint.SiblingLensE1S0
+public import LeanPool.Besicovitch.SixPoint.SiblingLensS0S0
+public import LeanPool.Besicovitch.SixPoint.SiblingLensS0S3
+public import LeanPool.Besicovitch.SixPoint.SiblingTangent
+public import LeanPool.Besicovitch.SixPoint.SiblingTriangle
+public import LeanPool.Besicovitch.SixPoint.WeightedFailure
+public import LeanPool.Besicovitch.SixPoint.WeightedReduction
+public import LeanPool.Besicovitch.Statement
+public import LeanPool.Besicovitch.Topology.ConnectedComponent
+
+/-!
+# A machine-checked bound of 0.6934 for Besicovitch's 1/2-problem
+
+Source: url:https://github.com/CoolRmal/Besicovitchs-1-2
+Authors: Yongxi Lin
+Status: verified
+Main declarations: `LeanPool.Besicovitch.sigmaOne_plane_le_barS`
+Tags: besicovitch-problem, measure-theory, rectifiability, finite-certificates, gram-matrices
+MSC: 28A75, 28A78, 49Q15, 68V20, 90C05
+-/

LeanPool/Besicovitch/BesicovitchPairCondition/Basic.lean

@@ -0,0 +1,130 @@
+/-
+Copyright (c) 2026 Yongxi Lin. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yongxi Lin
+-/
+module
+
+public import LeanPool.Besicovitch.BesicovitchPairCondition.Definitions
+
+/-!
+# Basic facts about the Besicovitch pair condition
+
+This file develops the elementary set-distance API needed by the six-point transfer.
+-/
+
+@[expose] public section
+
+noncomputable section
+
+open MeasureTheory Set
+open scoped ENNReal
+
+namespace LeanPool.Besicovitch
+
+variable {X : Type*} [PseudoEMetricSpace X] {s t : Set X}
+
+/-- The set distance is bounded by the distance between any selected pair of points. -/
+theorem setEDist_le_edist_of_mem {x y : X} (hx : x ∈ s) (hy : y ∈ t) :
+    setEDist s t ≤ edist x y := by
+  exact iInf_le_of_le x <| iInf_le_of_le hx <| iInf_le_of_le y <| iInf_le_of_le hy le_rfl
+
+/-- Extended set distance is symmetric. -/
+theorem setEDist_comm (s t : Set X) : setEDist s t = setEDist t s := by
+  apply le_antisymm
+  · refine le_iInf fun y ↦ le_iInf fun hy ↦ le_iInf fun x ↦ le_iInf fun hx ↦ ?_
+    simpa [edist_comm] using setEDist_le_edist_of_mem (s := s) (t := t) hx hy
+  · refine le_iInf fun x ↦ le_iInf fun hx ↦ le_iInf fun y ↦ le_iInf fun hy ↦ ?_
+    simpa [edist_comm] using setEDist_le_edist_of_mem (s := t) (t := s) hy hx
+
+@[simp]
+theorem setEDist_empty_left (t : Set X) : setEDist ∅ t = ∞ := by
+  simp [setEDist]
+
+/-- Two nonempty sets in a metric space have finite extended distance. -/
+theorem setEDist_ne_top {Y : Type*} [PseudoMetricSpace Y] {u v : Set Y}
+    (hu : u.Nonempty) (hv : v.Nonempty) : setEDist u v ≠ ∞ := by
+  obtain ⟨x, hx⟩ := hu
+  obtain ⟨y, hy⟩ := hv
+  exact ne_top_of_le_ne_top (edist_ne_top x y) (setEDist_le_edist_of_mem hx hy)
+
+/-- A positive finite set distance has a positive real value. -/
+theorem setEDist_toReal_pos {Y : Type*} [PseudoMetricSpace Y] {u v : Set Y}
+    (hu : u.Nonempty) (hv : v.Nonempty) (hpos : 0 < setEDist u v) :
+    0 < (setEDist u v).toReal := by
+  exact ENNReal.toReal_pos hpos.ne' (setEDist_ne_top hu hv)
+
+/-- The real set distance is no larger than any distance between the two sets. -/
+theorem setEDist_toReal_le_dist {Y : Type*} [PseudoMetricSpace Y] {u v : Set Y}
+    (hu : u.Nonempty) (hv : v.Nonempty) {x y : Y} (hx : x ∈ u) (hy : y ∈ v) :
+    (setEDist u v).toReal ≤ dist x y := by
+  have h := setEDist_le_edist_of_mem hx hy
+  have hfinite := setEDist_ne_top hu hv
+  rw [← ENNReal.toReal_le_toReal hfinite (edist_ne_top x y)] at h
+  simpa [edist_dist] using h
+
+/-- A ball whose radius is at most the set distance misses the opposite set. -/
+theorem ball_disjoint_of_le_setEDist_toReal {Y : Type*} [PseudoMetricSpace Y]
+    {u v : Set Y} (hu : u.Nonempty) (hv : v.Nonempty) {x : Y} (hx : x ∈ u)
+    {r : ℝ} (hr : r ≤ (setEDist u v).toReal) : Disjoint (Metric.ball x r) v := by
+  rw [Set.disjoint_left]
+  intro y hy hyMem
+  have hlower := setEDist_toReal_le_dist hu hv hx hyMem
+  rw [Metric.mem_ball'] at hy
+  exact (not_lt_of_ge hlower) (hy.trans_le hr)
+
+/-- A strict upper bound on set distance is witnessed by an actual pair of points. -/
+theorem exists_edist_lt_of_setEDist_lt {r : ℝ≥0∞} (h : setEDist s t < r) :
+    ∃ x ∈ s, ∃ y ∈ t, edist x y < r := by
+  rw [setEDist, iInf_lt_iff] at h
+  obtain ⟨x, hx⟩ := h
+  rw [iInf_lt_iff] at hx
+  obtain ⟨hxs, hx⟩ := hx
+  rw [iInf_lt_iff] at hx
+  obtain ⟨y, hy⟩ := hx
+  rw [iInf_lt_iff] at hy
+  obtain ⟨hyt, hy⟩ := hy
+  exact ⟨x, hxs, y, hyt, hy⟩
+
+/-- A real number above the finite set distance bounds some actual pair distance. -/
+theorem exists_dist_lt_of_setEDist_toReal_lt {Y : Type*} [PseudoMetricSpace Y]
+    {u v : Set Y} (hu : u.Nonempty) (hv : v.Nonempty) {r : ℝ}
+    (h : (setEDist u v).toReal < r) : ∃ x ∈ u, ∃ y ∈ v, dist x y < r := by
+  have hr : 0 < r := (ENNReal.toReal_nonneg.trans_lt h)
+  have hfinite := setEDist_ne_top hu hv
+  have hed : setEDist u v < ENNReal.ofReal r := by
+    rw [← ENNReal.toReal_lt_toReal hfinite (by simp)]
+    simpa [ENNReal.toReal_ofReal hr.le] using h
+  obtain ⟨x, hx, y, hy, hxy⟩ := exists_edist_lt_of_setEDist_lt hed
+  refine ⟨x, hx, y, hy, ?_⟩
+  rw [edist_dist, ENNReal.ofReal_lt_ofReal_iff hr] at hxy
+  exact hxy
+
+/-- Raising the density parameter preserves the Besicovitch pair condition. -/
+theorem BesicovitchPairCondition.mono {β γ : ℝ} (hβγ : β ≤ γ)
+    (hβ : BesicovitchPairCondition β) : BesicovitchPairCondition γ := by
+  intro μ hμ
+  obtain ⟨τ, hτ, hβ⟩ := hβ μ hμ
+  refine ⟨τ, hτ, fun scale hscale ↦ ?_⟩
+  obtain ⟨δ, hδ, hβ⟩ := hβ scale hscale
+  refine ⟨δ, hδ, fun e₁ e₂ he₁ he₂ he₁n he₂n hpos hlt hdensity ↦ ?_⟩
+  apply hβ e₁ e₂ he₁ he₂ he₁n he₂n hpos hlt
+  intro x hx r hr hrscale
+  refine lt_of_le_of_lt (ENNReal.ofReal_le_ofReal ?_) (hdensity x hx r hr hrscale)
+  exact mul_le_mul_of_nonneg_right (mul_le_mul_of_nonneg_left hβγ (by norm_num)) hr.le
+
+/-- A straight set whose mass exceeds `a` contains two points more than `a` apart. -/
+theorem IsStraightMeasure.exists_dist_gt {μ : Measure (EuclideanSpace ℝ (Fin 2))}
+    (hμ : IsStraightMeasure μ) {s : Set (EuclideanSpace ℝ (Fin 2))}
+    (hs : MeasurableSet s) {a : ℝ} (ha : ENNReal.ofReal a < μ s) :
+    ∃ x ∈ s, ∃ y ∈ s, a < dist x y := by
+  by_contra h
+  have hall : ∀ x ∈ s, ∀ y ∈ s, dist x y ≤ a := by
+    intro x hx y hy
+    by_contra hxy
+    exact h ⟨x, hx, y, hy, lt_of_not_ge hxy⟩
+  have hed : Metric.ediam s ≤ ENNReal.ofReal a :=
+    Metric.ediam_le_of_forall_dist_le hall
+  exact (not_lt_of_ge hed) (ha.trans_le (hμ s hs))
+
+end LeanPool.Besicovitch