Counting transfer definition Erdos9796Counting_IsoscelesCount

/- Generated by exact skeleton subtraction from Erdos9796Proof.P97.IsoscelesCount; source SHA-256 207564b11a38e9270192c8e5de3202b113b7f89c7ece5af3bc12954928d3013c -/
import Definitions.Def_Erdos9796Counting_Adapter
import Mathlib.Algebra.BigOperators.Group.Finset.Basic
import Mathlib.Algebra.Order.BigOperators.Group.Finset
import Mathlib.Data.Finset.Powerset


/-!
# Isosceles count for Erdős Problem 97 (Dumitrescu lower bound, Milestone 3)

Defines the per-vertex and total isosceles count of a finite point set,
in the Dumitrescu 2006 / Nivasch–Pach–Pinchasi–Zerbib 2013 convention
(equilaterals counted three times), and proves the easy lower bound:

  Per-vertex `K4` ⇒ each vertex contributes `≥ C(4,2) = 6` isosceles pairs.
  Summing: `6 · |A| ≤ I(A)`.

The matching upper bound `I(A) ≤ (11·|A|²−18·|A|)/12` for convex point
sets is Dumitrescu 2006 eq. (5), still open
(`p97-isosceles-count-upper-bound`).

References: doc slug `p97-isosceles-obstruction`.
-/

set_option linter.style.openClassical false

open scoped EuclideanGeometry
open Finset Classical

namespace Problem97

/-- Unordered pairs of points in `A.erase p` at common distance from `p`.
Each such pair witnesses one isosceles triangle with apex `p`. -/
noncomputable def IsoscelesPairsAt (A : Finset ℝ²) (p : ℝ²) : Finset (Finset ℝ²) :=
  ((A.erase p).powersetCard 2).filter (fun s => ∃ r : ℝ, ∀ q ∈ s, dist p q = r)

/-- The number of isosceles triangles with apex `p`. -/
noncomputable def iCountAt (A : Finset ℝ²) (p : ℝ²) : ℕ := (IsoscelesPairsAt A p).card

/-- Total isosceles count of `A`, equilaterals counted 3× (Dumitrescu 2006). -/
noncomputable def iCount (A : Finset ℝ²) : ℕ := ∑ p ∈ A, iCountAt A p





















end Problem97