Finite planar distance configurations

This module defines unordered index pairs, realized distances, their multiplicities, and the low-multiplicity distances in Erdős Problem 132. The definitions work on a selected finite subset of a labelled configuration, which makes deletion and insertion statements literal finset identities.

structure LeanPool.Erdos132N14.Configuration (ι : Type u_1) : Type u_1

A labelled finite planar configuration.

• point : ι → ℂ

  The planar point carrying a label.

• injective : Function.Injective self.point

def LeanPool.Erdos132N14.pairs {ι : Type u_1} [LinearOrder ι] (S : Finset ι) : Finset (ι × ι)

The unordered pairs in S, represented by their increasing orientation.

Equations

• LeanPool.Erdos132N14.pairs S = {e ∈ S ×ˢ S | e.1 < e.2}

def LeanPool.Erdos132N14.pairWith {ι : Type u_1} [LinearOrder ι] (v w : ι) : ι × ι

The increasing representative of the unordered pair containing v and w.

Equations

• LeanPool.Erdos132N14.pairWith v w = if w < v then (w, v) else (v, w)

def LeanPool.Erdos132N14.insertionPairs {ι : Type u_1} [LinearOrder ι] (v : ι) (S : Finset ι) : Finset (ι × ι)

The new unordered pairs created by inserting v into S.

Equations

• LeanPool.Erdos132N14.insertionPairs v S = Finset.image (LeanPool.Erdos132N14.pairWith v) S

theorem LeanPool.Erdos132N14.pairWith_injective {ι : Type u_1} [LinearOrder ι] (v : ι) : Function.Injective (pairWith v)

theorem LeanPool.Erdos132N14.pairs_insert {ι : Type u_1} [LinearOrder ι] {v : ι} {S : Finset ι} (hv : v ∉ S) : pairs (insert v S) = pairs S ∪ insertionPairs v S

theorem LeanPool.Erdos132N14.pairs_disjoint_insertionPairs {ι : Type u_1} [LinearOrder ι] {v : ι} {S : Finset ι} (hv : v ∉ S) : Disjoint (pairs S) (insertionPairs v S)

theorem LeanPool.Erdos132N14.pairWith_mem_pairs {ι : Type u_1} [LinearOrder ι] {S : Finset ι} {a b : ι} (ha : a ∈ S) (hb : b ∈ S) (hab : a ≠ b) : pairWith a b ∈ pairs S

theorem LeanPool.Erdos132N14.pairWith_map_injectiveOn_orderedPairs {ι : Type u_1} {κ : Type u_2} [LinearOrder ι] [LinearOrder κ] (f : κ → ι) (hf : Function.Injective f) : Set.InjOn (fun (e : κ × κ) => pairWith (f e.1) (f e.2)) {e : κ × κ | e.1 < e.2}

noncomputable def LeanPool.Erdos132N14.Configuration.pairDistance {ι : Type u_1} (P : Configuration ι) (e : ι × ι) : ℝ

The Euclidean length belonging to an indexed pair.

Equations

• P.pairDistance e = dist (P.point e.1) (P.point e.2)

noncomputable def LeanPool.Erdos132N14.Configuration.realizedDistances {ι : Type u_1} [LinearOrder ι] (P : Configuration ι) (S : Finset ι) : Finset ℝ

The positive distances realized inside S.

Equations

• P.realizedDistances S = Finset.image P.pairDistance (LeanPool.Erdos132N14.pairs S)

noncomputable def LeanPool.Erdos132N14.Configuration.distanceMultiplicity {ι : Type u_1} [LinearOrder ι] (P : Configuration ι) (S : Finset ι) (d : ℝ) : ℕ

The number of unordered pairs in S at distance d.

Equations

• P.distanceMultiplicity S d = {e ∈ LeanPool.Erdos132N14.pairs S | P.pairDistance e = d}.card

noncomputable def LeanPool.Erdos132N14.Configuration.lowMultiplicityDistances {ι : Type u_1} [LinearOrder ι] (P : Configuration ι) (S : Finset ι) (threshold : ℕ) : Finset ℝ

Realized distances represented by at most threshold unordered pairs.

Equations

• P.lowMultiplicityDistances S threshold = {d ∈ P.realizedDistances S | P.distanceMultiplicity S d ≤ threshold}

theorem LeanPool.Erdos132N14.Configuration.mem_realizedDistances_iff {ι : Type u_1} [LinearOrder ι] (P : Configuration ι) (S : Finset ι) (d : ℝ) : d ∈ P.realizedDistances S ↔ ∃ e ∈ pairs S, P.pairDistance e = d

theorem LeanPool.Erdos132N14.Configuration.distanceMultiplicity_pos_iff {ι : Type u_1} [LinearOrder ι] (P : Configuration ι) (S : Finset ι) (d : ℝ) : 0 < P.distanceMultiplicity S d ↔ d ∈ P.realizedDistances S

theorem LeanPool.Erdos132N14.Configuration.pairDistance_pos {ι : Type u_1} [LinearOrder ι] (P : Configuration ι) {S : Finset ι} {e : ι × ι} (he : e ∈ pairs S) : 0 < P.pairDistance e

theorem LeanPool.Erdos132N14.Configuration.realizedDistance_pos {ι : Type u_1} [LinearOrder ι] (P : Configuration ι) {S : Finset ι} {d : ℝ} (hd : d ∈ P.realizedDistances S) : 0 < d

theorem LeanPool.Erdos132N14.Configuration.pairs_mono {ι : Type u_1} [LinearOrder ι] {S T : Finset ι} (hST : S ⊆ T) : pairs S ⊆ pairs T

theorem LeanPool.Erdos132N14.Configuration.realizedDistances_mono {ι : Type u_1} [LinearOrder ι] (P : Configuration ι) {S T : Finset ι} (hST : S ⊆ T) : P.realizedDistances S ⊆ P.realizedDistances T

theorem LeanPool.Erdos132N14.Configuration.distanceMultiplicity_mono {ι : Type u_1} [LinearOrder ι] (P : Configuration ι) {S T : Finset ι} (hST : S ⊆ T) (d : ℝ) : P.distanceMultiplicity S d ≤ P.distanceMultiplicity T d

theorem LeanPool.Erdos132N14.Configuration.sum_distanceMultiplicity {ι : Type u_1} [LinearOrder ι] (P : Configuration ι) (S : Finset ι) : ∑ d ∈ P.realizedDistances S, P.distanceMultiplicity S d = (pairs S).card

Multiplicities partition the unordered pairs.

noncomputable def LeanPool.Erdos132N14.Configuration.insertionMultiplicity {ι : Type u_1} (P : Configuration ι) (v : ι) (S : Finset ι) (d : ℝ) : ℕ

Number of new edges of length d created by inserting v into S.

Equations

• P.insertionMultiplicity v S d = {w ∈ S | dist (P.point v) (P.point w) = d}.card

theorem LeanPool.Erdos132N14.Configuration.pairDistance_pairWith {ι : Type u_1} [LinearOrder ι] (P : Configuration ι) (v w : ι) : P.pairDistance (pairWith v w) = dist (P.point v) (P.point w)

theorem LeanPool.Erdos132N14.Configuration.filter_insertionPairs {ι : Type u_1} [LinearOrder ι] (P : Configuration ι) (v : ι) (S : Finset ι) (d : ℝ) : {e ∈ insertionPairs v S | P.pairDistance e = d} = Finset.image (pairWith v) ({w ∈ S | dist (P.point v) (P.point w) = d})

theorem LeanPool.Erdos132N14.Configuration.distanceMultiplicity_insert {ι : Type u_1} [LinearOrder ι] (P : Configuration ι) {v : ι} {S : Finset ι} (hv : v ∉ S) (d : ℝ) : P.distanceMultiplicity (insert v S) d = P.distanceMultiplicity S d + P.insertionMultiplicity v S d

Exact insertion formula for distance multiplicity.

structure LeanPool.Erdos132N14.PlaneSimilarity : Type

A distance-scaling equivalence of the Euclidean plane.

• toEquiv : ℂ ≃ ℂ

  The underlying bijection of the plane.

• ratio : ℝ

  The positive distance scale factor.

• ratio_pos : 0 < self.ratio
• map_dist (x y : ℂ) : dist (self.toEquiv x) (self.toEquiv y) = self.ratio * dist x y

@[implicit_reducible]

instance LeanPool.Erdos132N14.instCoeFunPlaneSimilarityForallComplex : CoeFun PlaneSimilarity fun (x : PlaneSimilarity) => ℂ → ℂ

Equations

• LeanPool.Erdos132N14.instCoeFunPlaneSimilarityForallComplex = { coe := fun (f : LeanPool.Erdos132N14.PlaneSimilarity) => ⇑f.toEquiv }

structure LeanPool.Erdos132N14.SimilarTo {ι : Type u_1} (P : Configuration ι) (S : Finset ι) {κ : Type u_3} (template : κ → ℂ) : Type (max u_1 u_3)

A selected configuration is a relabelled Euclidean similarity image of a template.

• reindex : κ ≃ ↥S

  A relabelling from the template onto the selected points.

• similarity : PlaneSimilarity

  The Euclidean similarity carrying the template to the selection.

• point_eq (i : κ) : P.point ↑(self.reindex i) = self.similarity.toEquiv (template i)

theorem LeanPool.Erdos132N14.PlaneSimilarity.injective (f : PlaneSimilarity) : Function.Injective ⇑f.toEquiv

theorem LeanPool.Erdos132N14.SimilarTo.distance_eq {ι : Type u_1} {κ : Type u_2} {P : Configuration ι} {S : Finset ι} {template : κ → ℂ} (h : SimilarTo P S template) (i j : κ) : dist (P.point ↑(h.reindex i)) (P.point ↑(h.reindex j)) = h.similarity.ratio * dist (template i) (template j)

theorem LeanPool.Erdos132N14.SimilarTo.distanceMultiplicity_le {ι : Type u_1} {κ : Type u_2} [LinearOrder ι] {P : Configuration ι} [Fintype κ] [LinearOrder κ] {S : Finset ι} (Q : Configuration κ) (h : SimilarTo P S Q.point) (d : ℝ) : Q.distanceMultiplicity Finset.univ d ≤ P.distanceMultiplicity S (h.similarity.ratio * d)

A Euclidean similarity injects every template distance class into the corresponding scaled class of the selected configuration.

theorem LeanPool.Erdos132N14.SimilarTo.distanceMultiplicity_eq {ι : Type u_1} {κ : Type u_2} [LinearOrder ι] {P : Configuration ι} [Fintype κ] [LinearOrder κ] {S : Finset ι} (Q : Configuration κ) (h : SimilarTo P S Q.point) (d : ℝ) : P.distanceMultiplicity S (h.similarity.ratio * d) = Q.distanceMultiplicity Finset.univ d

Euclidean similarities preserve every distance multiplicity exactly.