FormalConjecturesForMathlib.Geometry.Metric

/-
Copyright 2025 The Formal Conjectures Authors.

Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at

    https://www.apache.org/licenses/LICENSE-2.0

Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
module

public import FormalConjecturesForMathlib.Data.Sym.Sym2
public import Mathlib.Data.Finset.Sym
public import Mathlib.Data.Sym.Card
public import Mathlib.Topology.MetricSpace.Defs

@[expose] public sectionopen scoped Finsetvariable {X : Type*} [MetricSpace X]

The number of pairs of points of a finite set s in a metric space that are distance 1 apart.

noncomputable def unitDistNum (s : Finset X) : ℕ := #{p ∈ s.sym2 | dist p.out.1 p.out.2 = 1}

The set of distances determined by a finite set of points in a metric space.

noncomputable def distanceSet (points : Finset X) : Finset ℝ :=
  points.offDiag.image fun (pair : X × X) => dist pair.1 pair.2

Given a finite set of points in a metric space, we define the number of distinct distances between pairs of points.

noncomputable def distinctDistances (points : Finset X) : ℕ :=
  #(distanceSet points)

The multiplicity of the distance d determined by points, that is, the number of unordered pairs of distinct points at distance d apart.

noncomputable def distanceMultiplicity (points : Finset X) (d : ℝ) : ℕ :=
  #(points.offDiag.filter fun (pair : X × X) => dist pair.1 pair.2 = d) / 2

open Classical in

Given a finite set of points in a metric space, we define the number of distinct distances between a given point and all other points.

noncomputable def distinctDistancesFrom (points : Finset X) (pt : X) : ℕ :=
  #((points.erase pt).image fun x => dist x pt)

open Classical in

The number of unit-distance pairs of a finite set of n points is at most $\binom{n}{2}$, the total number of unordered pairs of distinct points.


theorem unitDistNum_le_choose_two (s : Finset X) : unitDistNum s ≤ (#s).choose 2 := byX:Type u_1inst✝:MetricSpace Xs:Finset X⊢ unitDistNum s ≤ (#s).choose 2
  rw [unitDistNum,X:Type u_1inst✝:MetricSpace Xs:Finset X⊢ #({p ∈ s.sym2 | dist (Quot.out p).1 (Quot.out p).2 = 1}) ≤ (#s).choose 2X:Type u_1inst✝:MetricSpace Xs:Finset X⊢ #({p ∈ s.sym2 | dist (Quot.out p).1 (Quot.out p).2 = 1}) ≤ #(Finset.image (Function.uncurry Sym2.mk) s.offDiag) ← Sym2.card_image_offDiagX:Type u_1inst✝:MetricSpace Xs:Finset X⊢ #({p ∈ s.sym2 | dist (Quot.out p).1 (Quot.out p).2 = 1}) ≤ #(Finset.image (Function.uncurry Sym2.mk) s.offDiag)X:Type u_1inst✝:MetricSpace Xs:Finset X⊢ #({p ∈ s.sym2 | dist (Quot.out p).1 (Quot.out p).2 = 1}) ≤ #(Finset.image (Function.uncurry Sym2.mk) s.offDiag)]X:Type u_1inst✝:MetricSpace Xs:Finset X⊢ #({p ∈ s.sym2 | dist (Quot.out p).1 (Quot.out p).2 = 1}) ≤ #(Finset.image (Function.uncurry Sym2.mk) s.offDiag)
  refine Finset.card_le_card fun p hp => ?_X:Type u_1inst✝:MetricSpace Xs:Finset Xp:Sym2 Xhp:p ∈ {p ∈ s.sym2 | dist (Quot.out p).1 (Quot.out p).2 = 1}⊢ p ∈ Finset.image (Function.uncurry Sym2.mk) s.offDiag
  obtain ⟨hps, hpd⟩ := Finset.mem_filter.mp hpX:Type u_1inst✝:MetricSpace Xs:Finset Xp:Sym2 Xhp:p ∈ {p ∈ s.sym2 | dist (Quot.out p).1 (Quot.out p).2 = 1}hps:p ∈ s.sym2hpd:dist (Quot.out p).1 (Quot.out p).2 = 1⊢ p ∈ Finset.image (Function.uncurry Sym2.mk) s.offDiag
  rw [← Finset.image_diag_union_image_offDiag (s := s),X:Type u_1inst✝:MetricSpace Xs:Finset Xp:Sym2 Xhp:p ∈ {p ∈ s.sym2 | dist (Quot.out p).1 (Quot.out p).2 = 1}hps:p ∈ Finset.image (Function.uncurry Sym2.mk) s.diag ∪ Finset.image (Function.uncurry Sym2.mk) s.offDiaghpd:dist (Quot.out p).1 (Quot.out p).2 = 1⊢ p ∈ Finset.image (Function.uncurry Sym2.mk) s.offDiagX:Type u_1inst✝:MetricSpace Xs:Finset Xp:Sym2 Xhp:p ∈ {p ∈ s.sym2 | dist (Quot.out p).1 (Quot.out p).2 = 1}hps:p ∈ Finset.image (Function.uncurry Sym2.mk) s.diag ∨ p ∈ Finset.image (Function.uncurry Sym2.mk) s.offDiaghpd:dist (Quot.out p).1 (Quot.out p).2 = 1⊢ p ∈ Finset.image (Function.uncurry Sym2.mk) s.offDiag Finset.mem_unionX:Type u_1inst✝:MetricSpace Xs:Finset Xp:Sym2 Xhp:p ∈ {p ∈ s.sym2 | dist (Quot.out p).1 (Quot.out p).2 = 1}hps:p ∈ Finset.image (Function.uncurry Sym2.mk) s.diag ∨ p ∈ Finset.image (Function.uncurry Sym2.mk) s.offDiaghpd:dist (Quot.out p).1 (Quot.out p).2 = 1⊢ p ∈ Finset.image (Function.uncurry Sym2.mk) s.offDiagX:Type u_1inst✝:MetricSpace Xs:Finset Xp:Sym2 Xhp:p ∈ {p ∈ s.sym2 | dist (Quot.out p).1 (Quot.out p).2 = 1}hps:p ∈ Finset.image (Function.uncurry Sym2.mk) s.diag ∨ p ∈ Finset.image (Function.uncurry Sym2.mk) s.offDiaghpd:dist (Quot.out p).1 (Quot.out p).2 = 1⊢ p ∈ Finset.image (Function.uncurry Sym2.mk) s.offDiag] at hpsX:Type u_1inst✝:MetricSpace Xs:Finset Xp:Sym2 Xhp:p ∈ {p ∈ s.sym2 | dist (Quot.out p).1 (Quot.out p).2 = 1}hps:p ∈ Finset.image (Function.uncurry Sym2.mk) s.diag ∨ p ∈ Finset.image (Function.uncurry Sym2.mk) s.offDiaghpd:dist (Quot.out p).1 (Quot.out p).2 = 1⊢ p ∈ Finset.image (Function.uncurry Sym2.mk) s.offDiag
  rcases hps with h | hinlX:Type u_1inst✝:MetricSpace Xs:Finset Xp:Sym2 Xhp:p ∈ {p ∈ s.sym2 | dist (Quot.out p).1 (Quot.out p).2 = 1}hpd:dist (Quot.out p).1 (Quot.out p).2 = 1h:p ∈ Finset.image (Function.uncurry Sym2.mk) s.diag⊢ p ∈ Finset.image (Function.uncurry Sym2.mk) s.offDiaginrX:Type u_1inst✝:MetricSpace Xs:Finset Xp:Sym2 Xhp:p ∈ {p ∈ s.sym2 | dist (Quot.out p).1 (Quot.out p).2 = 1}hpd:dist (Quot.out p).1 (Quot.out p).2 = 1h:p ∈ Finset.image (Function.uncurry Sym2.mk) s.offDiag⊢ p ∈ Finset.image (Function.uncurry Sym2.mk) s.offDiag
  ·inlX:Type u_1inst✝:MetricSpace Xs:Finset Xp:Sym2 Xhp:p ∈ {p ∈ s.sym2 | dist (Quot.out p).1 (Quot.out p).2 = 1}hpd:dist (Quot.out p).1 (Quot.out p).2 = 1h:p ∈ Finset.image (Function.uncurry Sym2.mk) s.diag⊢ p ∈ Finset.image (Function.uncurry Sym2.mk) s.offDiag obtain ⟨⟨x, y⟩, hxy, rfl⟩ := Finset.mem_image.mp hinlX:Type u_1inst✝:MetricSpace Xs:Finset Xx:Xy:Xhxy:(x, y) ∈ s.diaghp:Function.uncurry Sym2.mk (x, y) ∈ {p ∈ s.sym2 | dist (Quot.out p).1 (Quot.out p).2 = 1}hpd:dist (Quot.out (Function.uncurry Sym2.mk (x, y))).1 (Quot.out (Function.uncurry Sym2.mk (x, y))).2 = 1h:Function.uncurry Sym2.mk (x, y) ∈ Finset.image (Function.uncurry Sym2.mk) s.diag⊢ Function.uncurry Sym2.mk (x, y) ∈ Finset.image (Function.uncurry Sym2.mk) s.offDiag
    obtain ⟨-, rfl⟩ : _ ∧ x = y := Finset.mem_diag.mp hxyinlX:Type u_1inst✝:MetricSpace Xs:Finset Xx:Xhxy:(x, x) ∈ s.diaghp:Function.uncurry Sym2.mk (x, x) ∈ {p ∈ s.sym2 | dist (Quot.out p).1 (Quot.out p).2 = 1}hpd:dist (Quot.out (Function.uncurry Sym2.mk (x, x))).1 (Quot.out (Function.uncurry Sym2.mk (x, x))).2 = 1h:Function.uncurry Sym2.mk (x, x) ∈ Finset.image (Function.uncurry Sym2.mk) s.diag⊢ Function.uncurry Sym2.mk (x, x) ∈ Finset.image (Function.uncurry Sym2.mk) s.offDiag
    simp at hpdAll goals completed! 🐙
  ·inrX:Type u_1inst✝:MetricSpace Xs:Finset Xp:Sym2 Xhp:p ∈ {p ∈ s.sym2 | dist (Quot.out p).1 (Quot.out p).2 = 1}hpd:dist (Quot.out p).1 (Quot.out p).2 = 1h:p ∈ Finset.image (Function.uncurry Sym2.mk) s.offDiag⊢ p ∈ Finset.image (Function.uncurry Sym2.mk) s.offDiag exact hAll goals completed! 🐙