1. FormalConjecturesForMathlib
  2. Geometry
  3. 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.Algebra.BigOperators.Ring.Finset public import Mathlib.Data.Finset.Sym public import Mathlib.Data.Nat.Choose.Basic public import Mathlib.Data.Sym.Card public import Mathlib.Data.ZMod.Basic public import Mathlib.Order.Lattice.Nat 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)variable (X) in

The minimum number of distinct distances determined by a set of n points in X.

noncomputable def minimalDistinctDistances (n : ℕ) : ℕ := sInf {m : ℕ | ∃ points : Finset X, #points = n ∧ distinctDistances points = m}

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) / 2open 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.

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 ∨ 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 X: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.offDiagX: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 X: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 X: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 X: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 All goals completed! 🐙 X: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 All goals completed! 🐙

The ordered pairs of distinct points of points at distance d come in swapped pairs, so there are evenly many of them.

X:Type u_1inst✝:MetricSpace Xpoints:Finset Xd:ℝF:Finset (X × X) := {pair ∈ points.offDiag | dist pair.1 pair.2 = d}hF:F = {pair ∈ points.offDiag | dist pair.1 pair.2 = d}h:∑ _a ∈ F, 1 = 0⊢ ↑(#F) = 0 All goals completed! 🐙

The multiplicities of the distances determined by points add up to the number of unordered pairs of distinct points.

All goals completed! 🐙