Erdős problem 96

/-!
# Superlinearly many unit distances in convex position
Authors: Liam Kruer <kruerl@purdue.edu>
         Jensen Kohlmeyer <jenwin@purdue.edu>

OpenAI Codex provided substantial assistance with the mathematical exploration,
construction, proofs, formalization, verification, and manuscript preparation.
The authors are responsible for the content.

Complete proof declarations for the supplied counterexample target.
The task provides the imports and enclosing Bounty namespace.
-/

open _root_.Erdos96

/- ## Angle -/

section OriginalAngle

/- Calculus of the angle subtended by a unit chord at the origin. -/

namespace Proof


noncomputable def chordCos (r s : ℝ) : ℝ := (r ^ 2 + s ^ 2 - 1) / (2 * r * s)
noncomputable def chordCosLeft (r s : ℝ) : ℝ := (r ^ 2 - s ^ 2 + 1) / (2 * r ^ 2 * s)
noncomputable def chordCosMixed (r s : ℝ) : ℝ := -(r ^ 2 + s ^ 2 + 1) / (2 * r ^ 2 * s ^ 2)
noncomputable def chordAngle (r s : ℝ) : ℝ := Real.arccos (chordCos r s)

theorem chordCos_comm (r s : ℝ) : chordCos r s = chordCos s r := by
  unfold chordCos
  congr 1 <;> ring

theorem hasDerivAt_chordCos_left {r s : ℝ} (hr : r ≠ 0) (hs : s ≠ 0) :
    HasDerivAt (fun x => chordCos x s) (chordCosLeft r s) r := by
  have hnum := (((hasDerivAt_id r).pow 2).add_const (s ^ 2)).sub_const 1
  have hden := ((hasDerivAt_id r).const_mul 2).mul_const s
  convert! hnum.div hden (mul_ne_zero (mul_ne_zero two_ne_zero hr) hs) using 1
  dsimp only [id_eq, Pi.pow_apply]
  unfold chordCosLeft
  field_simp [hr, hs]
  ring

theorem hasDerivAt_chordCos_right {r s : ℝ} (hr : r ≠ 0) (hs : s ≠ 0) :
    HasDerivAt (chordCos r) (chordCosLeft s r) s := by
  simpa only [chordCos_comm] using hasDerivAt_chordCos_left hs hr

theorem hasDerivAt_chordCosLeft_right {r s : ℝ} (hr : r ≠ 0) (hs : s ≠ 0) :
    HasDerivAt (chordCosLeft r) (chordCosMixed r s) s := by
  have hnum := (((hasDerivAt_id s).pow 2).const_sub (r ^ 2)).add_const 1
  have hden := (hasDerivAt_id s).const_mul (2 * r ^ 2)
  convert! hnum.div hden (mul_ne_zero (mul_ne_zero two_ne_zero (pow_ne_zero 2 hr)) hs) using 1
  dsimp only [id_eq, Pi.pow_apply]
  unfold chordCosMixed
  field_simp [hr, hs]
  ring

theorem chordCos_mixed_identity {r s : ℝ} (hr : r ≠ 0) (hs : s ≠ 0) :
    -(chordCosMixed r s * (1 - chordCos r s ^ 2) +
      chordCos r s * chordCosLeft r s * chordCosLeft s r) = 1 / (r ^ 2 * s ^ 2) := by
  unfold chordCosMixed chordCos chordCosLeft
  field_simp [hr, hs]
  ring

noncomputable def chordAngleLeft (r s : ℝ) : ℝ :=
  -chordCosLeft r s / Real.sqrt (1 - chordCos r s ^ 2)

theorem chord_discriminant_pos {r s : ℝ}
    (hl : -1 < chordCos r s) (hu : chordCos r s < 1) :
    0 < 1 - chordCos r s ^ 2 := by
  nlinarith

theorem hasDerivAt_chordAngle_left {r s : ℝ} (hr : r ≠ 0) (hs : s ≠ 0)
    (hl : -1 < chordCos r s) (hu : chordCos r s < 1) :
    HasDerivAt (fun x => chordAngle x s) (chordAngleLeft r s) r := by
  convert! (Real.hasDerivAt_arccos (ne_of_gt hl) (ne_of_lt hu)).comp r
    (hasDerivAt_chordCos_left hr hs) using 1
  unfold chordAngleLeft
  ring

theorem hasDerivAt_chordAngleLeft_right {r s : ℝ} (hr : r ≠ 0) (hs : s ≠ 0)
    (hl : -1 < chordCos r s) (hu : chordCos r s < 1) :
    HasDerivAt (chordAngleLeft r)
      (1 / (r ^ 2 * s ^ 2 * Real.sqrt (1 - chordCos r s ^ 2) ^ 3)) s := by
  have hq := chord_discriminant_pos hl hu
  have hsqrt : Real.sqrt (1 - chordCos r s ^ 2) ≠ 0 := ne_of_gt (Real.sqrt_pos.mpr hq)
  have hsquare := Real.sq_sqrt hq.le
  have hnum := (hasDerivAt_chordCosLeft_right hr hs).neg
  have hden := (((hasDerivAt_chordCos_right hr hs).pow 2).const_sub 1).sqrt (ne_of_gt hq)
  convert! hnum.div hden hsqrt using 1
  have hid := chordCos_mixed_identity hr hs
  dsimp only [id_eq, Pi.pow_apply, Pi.neg_apply, Nat.cast_ofNat, Nat.reduceSub, pow_one, one_mul, mul_one]
  field_simp [hr, hs, hsqrt] at hid ⊢
  rw [hsquare]
  linear_combination -hid

theorem chordAngle_mixed_positive {r s : ℝ} (hr : r ≠ 0) (hs : s ≠ 0)
    (hl : -1 < chordCos r s) (hu : chordCos r s < 1) :
    0 < deriv (chordAngleLeft r) s := by
  rw [(hasDerivAt_chordAngleLeft_right hr hs hl hu).deriv]
  have := Real.sqrt_pos.mpr (chord_discriminant_pos hl hu)
  positivity

end Proof

end OriginalAngle

/- ## GenericAngles -/

section OriginalGenericAngles

/- Local separation of finite linear combinations of edge angles. -/

namespace Proof

open Set Filter
open scoped Topology


def ChordFeasible (r s : ℝ) : Prop :=
  r ≠ 0 ∧ s ≠ 0 ∧ -1 < chordCos r s ∧ chordCos r s < 1

theorem chordAngle_rectangle_strict {a b c d : ℝ} (hab : a < b) (hcd : c < d)
    (hf : ∀ x ∈ Icc a b, ∀ y ∈ Icc c d, ChordFeasible x y) :
    0 < chordAngle b d - chordAngle a d - chordAngle b c + chordAngle a c := by
  have hm : ∀ x ∈ Icc a b, chordAngleLeft x c < chordAngleLeft x d := by
    intro x hx
    have hmono : StrictMonoOn (chordAngleLeft x) (Icc c d) := by
      apply strictMonoOn_of_deriv_pos (convex_Icc c d)
      · intro y hy
        obtain ⟨hr, hs, hl, hu⟩ := hf x hx y hy
        exact (hasDerivAt_chordAngleLeft_right hr hs hl hu).continuousAt.continuousWithinAt
      · intro y hy
        obtain ⟨hr, hs, hl, hu⟩ := hf x hx y (interior_subset hy)
        exact chordAngle_mixed_positive hr hs hl hu
    exact hmono ⟨le_rfl, hcd.le⟩ ⟨hcd.le, le_rfl⟩ hcd
  have hder : ∀ x ∈ Icc a b,
      HasDerivAt (fun t => chordAngle t d - chordAngle t c)
        (chordAngleLeft x d - chordAngleLeft x c) x := by
    intro x hx
    obtain ⟨hrd, hsd, hld, hud⟩ := hf x hx d ⟨hcd.le, le_rfl⟩
    obtain ⟨hrc, hsc, hlc, huc⟩ := hf x hx c ⟨le_rfl, hcd.le⟩
    exact (hasDerivAt_chordAngle_left hrd hsd hld hud).sub
      (hasDerivAt_chordAngle_left hrc hsc hlc huc)
  have hmono : StrictMonoOn (fun t => chordAngle t d - chordAngle t c) (Icc a b) := by
    apply strictMonoOn_of_deriv_pos (convex_Icc a b)
    · intro x hx
      exact (hder x hx).continuousAt.continuousWithinAt
    · intro x hx
      rw [(hder x (interior_subset hx)).deriv]
      exact sub_pos.mpr (hm x (interior_subset hx))
  have hh := hmono ⟨le_rfl, hab.le⟩ ⟨hab.le, le_rfl⟩ hab
  linarith

noncomputable def matrixSum {L P : Type*} [Fintype L] [Fintype P]
    (f : L → P → ℝ → ℝ → ℝ) (r : L → ℝ) (s : P → ℝ) : ℝ :=
  ∑ i, ∑ j, f i j (r i) (s j)

theorem matrix_rectangle {L P : Type*} [Fintype L] [Fintype P]
    [DecidableEq L] [DecidableEq P] (f : L → P → ℝ → ℝ → ℝ)
    (r : L → ℝ) (s : P → ℝ) (i : L) (j : P) (x y : ℝ) :
    matrixSum f (Function.update r i x) (Function.update s j y) -
      matrixSum f r (Function.update s j y) -
      matrixSum f (Function.update r i x) s + matrixSum f r s =
    f i j x y - f i j (r i) y - f i j x (s j) + f i j (r i) (s j) := by
  let g := fun a b => f a b (Function.update r i x a) (Function.update s j y b) -
    f a b (r a) (Function.update s j y b) -
    f a b (Function.update r i x a) (s b) + f a b (r a) (s b)
  have he : matrixSum f (Function.update r i x) (Function.update s j y) -
      matrixSum f r (Function.update s j y) -
      matrixSum f (Function.update r i x) s + matrixSum f r s = ∑ a, ∑ b, g a b := by
    simp only [matrixSum, g, Finset.sum_add_distrib, Finset.sum_sub_distrib]
  rw [he, Finset.sum_eq_single i]
  · rw [Finset.sum_eq_single j]
    · simp [g]
    · intro b _ hbj
      simp [g, Function.update_of_ne hbj]
    · simp
  · intro a _ hai
    apply Finset.sum_eq_zero
    intro b _
    simp [g, Function.update_of_ne hai]
  · simp

theorem finite_avoidance {X K Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] [T1Space Y] [Zero Y]
    (f : K → X → Y) (U : Set X) (hU : IsOpen U) (hne : U.Nonempty)
    (hc : ∀ k, ContinuousOn (f k) U)
    (hnc : ∀ k, ∀ V : Set X, V ⊆ U → IsOpen V → V.Nonempty → ∃ x ∈ V, f k x ≠ 0)
    (s : Finset K) : ∃ x ∈ U, ∀ k ∈ s, f k x ≠ 0 := by
  classical
  suffices ∃ V : Set X, V ⊆ U ∧ IsOpen V ∧ V.Nonempty ∧
      ∀ x ∈ V, ∀ k ∈ s, f k x ≠ 0 by
    obtain ⟨V, hVU, hVo, ⟨x, hx⟩, hv⟩ := this
    exact ⟨x, hVU hx, hv x hx⟩
  induction s using Finset.induction_on with
  | empty => exact ⟨U, subset_rfl, hU, hne, by simp⟩
  | @insert k s hks ih =>
    obtain ⟨V, hVU, hVo, hVne, hV⟩ := ih
    obtain ⟨x, hx, hkx⟩ := hnc k V hVU hVo hVne
    refine ⟨V ∩ (f k) ⁻¹' ({0}ᶜ), inter_subset_left.trans hVU,
      (hc k |>.mono hVU).isOpen_inter_preimage hVo isClosed_singleton.isOpen_compl,
      ⟨x, hx, hkx⟩, ?_⟩
    intro y hy j hj
    rcases Finset.mem_insert.mp hj with rfl | hj
    · exact hy.2
    · exact hV y hy.1 j hj

theorem coordinate_rectangle {L P : Type*} [DecidableEq L] [DecidableEq P]
    {U : Set ((L → ℝ) × (P → ℝ))} (hU : IsOpen U) {z : (L → ℝ) × (P → ℝ)}
    (hz : z ∈ U) (i : L) (j : P) :
    ∃ b d : ℝ, z.1 i < b ∧ z.2 j < d ∧
      ∀ x ∈ Icc (z.1 i) b, ∀ y ∈ Icc (z.2 j) d,
        (Function.update z.1 i x, Function.update z.2 j y) ∈ U := by
  let F := fun xy : ℝ × ℝ => (Function.update z.1 i xy.1, Function.update z.2 j xy.2)
  have hF : Continuous F := by unfold F; fun_prop
  have hmem : (z.1 i, z.2 j) ∈ F ⁻¹' U := by simpa [F] using hz
  obtain ⟨A, hA, B, hB, hAB⟩ := mem_nhds_prod_iff.mp ((hU.preimage hF).mem_nhds hmem)
  obtain ⟨a, b, hab, hAsub⟩ := mem_nhds_iff_exists_Ioo_subset.mp hA
  obtain ⟨c, d, hcd, hBsub⟩ := mem_nhds_iff_exists_Ioo_subset.mp hB
  refine ⟨(z.1 i + b) / 2, (z.2 j + d) / 2, by linarith [hab.2], by linarith [hcd.2], ?_⟩
  intro x hx y hy
  change (x, y) ∈ F ⁻¹' U
  apply hAB
  constructor
  · apply hAsub
    constructor <;> linarith [hab.1, hab.2, hx.1, hx.2]
  · apply hBsub
    constructor <;> linarith [hcd.1, hcd.2, hy.1, hy.2]

theorem angle_sum_not_constant {L P : Type*} [Fintype L] [Fintype P]
    [DecidableEq L] [DecidableEq P] (c : L → P → ℝ) (i : L) (j : P) (hc : c i j ≠ 0)
    (U : Set ((L → ℝ) × (P → ℝ))) (hU : IsOpen U) (hne : U.Nonempty)
    (hf : ∀ z ∈ U, ChordFeasible (z.1 i) (z.2 j)) (k : ℝ) :
    ∃ z ∈ U, matrixSum (fun a b x y => c a b * chordAngle x y) z.1 z.2 ≠ k := by
  by_contra hnone
  push Not at hnone
  obtain ⟨z, hz⟩ := hne
  obtain ⟨b, d, hb, hd, hrect⟩ := coordinate_rectangle hU hz i j
  have hfeas : ∀ x ∈ Icc (z.1 i) b, ∀ y ∈ Icc (z.2 j) d, ChordFeasible x y := by
    intro x hx y hy
    simpa using hf _ (hrect x hx y hy)
  have hpositive := chordAngle_rectangle_strict hb hd hfeas
  have h00 := hnone z hz
  have h11 := hnone _ (hrect b ⟨hb.le, le_rfl⟩ d ⟨hd.le, le_rfl⟩)
  have h01 := hnone _ (hrect (z.1 i) ⟨le_rfl, hb.le⟩ d ⟨hd.le, le_rfl⟩)
  have h10 := hnone _ (hrect b ⟨hb.le, le_rfl⟩ (z.2 j) ⟨le_rfl, hd.le⟩)
  simp only [Function.update_eq_self] at h01 h10
  have hid := matrix_rectangle (fun a b x y => c a b * chordAngle x y) z.1 z.2 i j b d
  rw [h00, h11, h01, h10] at hid
  have hzero : c i j * (chordAngle b d - chordAngle (z.1 i) d -
      chordAngle b (z.2 j) + chordAngle (z.1 i) (z.2 j)) = 0 := by linear_combination -hid
  exact (mul_ne_zero hc (ne_of_gt hpositive)) hzero

theorem weighted_angles_continuousAt {L P : Type*} [Fintype L] [Fintype P]
    (c : L → P → ℝ) (z : (L → ℝ) × (P → ℝ))
    (hr : ∀ i, z.1 i ≠ 0) (hs : ∀ j, z.2 j ≠ 0) :
    ContinuousAt (fun u => matrixSum (fun i j x y => c i j * chordAngle x y) u.1 u.2) z := by
  unfold matrixSum chordAngle chordCos
  fun_prop (disch := aesop)

theorem finite_angle_avoidance {L P K : Type*} [Fintype L] [Fintype P]
    [DecidableEq L] [DecidableEq P]
    (c : K → L → P → ℝ) (offset : K → ℝ) (U : Set ((L → ℝ) × (P → ℝ)))
    (hU : IsOpen U) (hne : U.Nonempty)
    (hnz : ∀ z ∈ U, (∀ i, z.1 i ≠ 0) ∧ (∀ j, z.2 j ≠ 0))
    (hc : ∀ k, ∃ i j, c k i j ≠ 0)
    (hfeas : ∀ k i j, c k i j ≠ 0 → ∀ z ∈ U, ChordFeasible (z.1 i) (z.2 j))
    (s : Finset K) : ∃ z ∈ U, ∀ k ∈ s,
      matrixSum (fun i j x y => c k i j * chordAngle x y) z.1 z.2 ≠ offset k := by
  let f := fun (k : K) (z : (L → ℝ) × (P → ℝ)) =>
    matrixSum (fun i j x y => c k i j * chordAngle x y) z.1 z.2 - offset k
  have hcont : ∀ k, ContinuousOn (f k) U := by
    intro k z hz
    exact ((weighted_angles_continuousAt (c k) z (hnz z hz).1 (hnz z hz).2).sub
      continuousAt_const).continuousWithinAt
  have hnc : ∀ k, ∀ V : Set ((L → ℝ) × (P → ℝ)),
      V ⊆ U → IsOpen V → V.Nonempty → ∃ z ∈ V, f k z ≠ 0 := by
    intro k V hVU hVo hVne
    obtain ⟨i, j, hij⟩ := hc k
    obtain ⟨z, hz, hh⟩ := angle_sum_not_constant (c k) i j hij V hVo hVne
      (fun z hz => hfeas k i j hij z (hVU hz)) (offset k)
    exact ⟨z, hz, sub_ne_zero.mpr hh⟩
  obtain ⟨z, hz, hh⟩ := finite_avoidance f U hU hne hcont hnc s
  exact ⟨z, hz, fun k hk => sub_ne_zero.mp (hh k hk)⟩

end Proof

end OriginalGenericAngles

/- ## SeedAlgebra -/

section OriginalSeedAlgebra

/- Polynomial identities for the two classes of incidence seeds. -/

namespace Proof

noncomputable section

def lineC (x t : ℝ) : ℝ := x ^ 2 + t / 2
def pointD (x t : ℝ) : ℝ := -x ^ 2 + t / 2

def lineSeed (ε x t : ℝ) : ℂ := ⟨ε * x, -1 / 2 + ε ^ 2 * lineC x t⟩
def pointSeed (ε x t : ℝ) : ℂ := ⟨-ε * x, 1 / 2 + ε ^ 2 * pointD x t⟩

def support (a b : ℂ) : ℝ := a.re * (b.re - a.re) + a.im * (b.im - a.im)

theorem line_support_identity (ε x t y u : ℝ) :
    support (lineSeed ε x t) (lineSeed ε y u) =
      ε ^ 2 * (-(y - x) ^ 2 / 2 - (u - t) / 4) +
      ε ^ 4 * lineC x t * (lineC y u - lineC x t) := by
  simp only [support, lineSeed, lineC]
  ring

theorem point_support_identity (ε x t y u : ℝ) :
    support (pointSeed ε x t) (pointSeed ε y u) =
      ε ^ 2 * (-(y - x) ^ 2 / 2 + (u - t) / 4) +
      ε ^ 4 * pointD x t * (pointD y u - pointD x t) := by
  simp only [support, pointSeed, pointD]
  ring

theorem line_normSq (ε x t : ℝ) :
    Complex.normSq (lineSeed ε x t) =
      1 / 4 - ε ^ 2 * t / 2 + ε ^ 4 * (lineC x t) ^ 2 := by
  simp only [Complex.normSq_apply, lineSeed, lineC]
  ring

theorem point_normSq (ε x t : ℝ) :
    Complex.normSq (pointSeed ε x t) =
      1 / 4 + ε ^ 2 * t / 2 + ε ^ 4 * (pointD x t) ^ 2 := by
  simp only [Complex.normSq_apply, pointSeed, pointD]
  ring

theorem incidence_distance_identity (ε x t y u : ℝ)
    (h : u - t = (y - x) ^ 2) :
    Complex.normSq (pointSeed ε y u - lineSeed ε x t) =
      1 + ε ^ 4 * (pointD y u - lineC x t) ^ 2 := by
  simp only [Complex.normSq_apply, Complex.sub_re, Complex.sub_im,
    pointSeed, lineSeed, pointD, lineC]
  linear_combination ε ^ 2 * h

theorem signed_digit_margin {x t : ℝ}
    (h : |t| < (50 / 27 : ℝ) * x ^ 2) :
    -x ^ 2 / 2 - t / 4 < -x ^ 2 / 27 ∧
      -x ^ 2 / 2 + t / 4 < -x ^ 2 / 27 := by
  rcases abs_lt.mp h with ⟨hl, hu⟩
  constructor <;> linarith

end
end Proof

end OriginalSeedAlgebra

/- ## RadialGeometry -/

section OriginalRadialGeometry

/- Strict radial support, rotations, and their convexity consequences. -/

namespace Proof

open scoped InnerProductSpace

theorem support_eq_inner (a b : ℂ) : support a b = ⟪a, b - a⟫_ℝ := by
  simp only [support, Complex.inner, Complex.mul_re, Complex.sub_re,
    Complex.sub_im, Complex.conj_re, Complex.conj_im]
  ring

theorem support_eq_normSq (a b : ℂ) :
    2 * support a b = Complex.normSq b - Complex.normSq a - Complex.normSq (b - a) := by
  simp only [support, Complex.normSq_apply, Complex.sub_re, Complex.sub_im]
  ring

theorem support_negative_of_equal_norm {a b : ℂ} (hne : a ≠ b)
    (hnorm : ‖a‖ = ‖b‖) : support a b < 0 := by
  have heq : Complex.normSq a = Complex.normSq b := by
    simpa only [Complex.normSq_eq_norm_sq] using congrArg (fun r : ℝ => r ^ 2) hnorm
  have hp : 0 < Complex.normSq (b - a) := Complex.normSq_pos.mpr (sub_ne_zero.mpr hne.symm)
  have := support_eq_normSq a b
  linarith

theorem convexIndependent_of_support {ι : Type*} (p : ι → ℂ)
    (h : ∀ i j, i ≠ j → support (p i) (p j) < 0) : ConvexIndependent ℝ p := by
  intro s i hi
  by_contra hnot
  have hs : p '' s ⊆ {z : ℂ | ⟪p i, z⟫_ℝ < ⟪p i, p i⟫_ℝ} := by
    rintro z ⟨j, hj, rfl⟩
    have hij : i ≠ j := fun he => hnot (he.symm ▸ hj)
    have hh := h i j hij
    rw [support_eq_inner, inner_sub_right] at hh
    exact sub_neg.mp hh
  have hc : Convex ℝ {z : ℂ | ⟪p i, z⟫_ℝ < ⟪p i, p i⟫_ℝ} :=
    convex_halfSpace_lt ((innerₗ ℂ) (p i)).isLinear _
  have hz := (convexHull_min hs hc) hi
  exact lt_irrefl _ (show ⟪p i, p i⟫_ℝ < ⟪p i, p i⟫_ℝ from hz)

theorem support_mul (a b w : ℂ) :
    support (a * w) (b * w) = Complex.normSq w * support a b := by
  simp only [support, Complex.mul_re, Complex.mul_im, Complex.normSq_apply]
  ring

theorem norm_subset_prod {ι : Type*} (s : Finset ι) (w : ι → ℂ)
    (hw : ∀ i ∈ s, ‖w i‖ = 1) : ‖∏ i ∈ s, w i‖ = 1 := by
  rw [norm_prod]
  exact Finset.prod_eq_one hw

theorem norm_prod_sub_one_le {ι : Type*} (s : Finset ι) (w : ι → ℂ)
    (hw : ∀ i ∈ s, ‖w i‖ = 1) :
    ‖(∏ i ∈ s, w i) - 1‖ ≤ ∑ i ∈ s, ‖w i - 1‖ := by
  classical
  induction s using Finset.induction_on with
  | empty => simp
  | @insert i s hi ih =>
    rw [Finset.prod_insert hi, Finset.sum_insert hi]
    have hwi := hw i (Finset.mem_insert_self i s)
    have hws : ∀ j ∈ s, ‖w j‖ = 1 := fun j hj => hw j (Finset.mem_insert_of_mem hj)
    calc
      ‖w i * (∏ j ∈ s, w j) - 1‖ =
          ‖w i * ((∏ j ∈ s, w j) - 1) + (w i - 1)‖ := by congr 1; ring
      _ ≤ ‖w i * ((∏ j ∈ s, w j) - 1)‖ + ‖w i - 1‖ := norm_add_le _ _
      _ = ‖(∏ j ∈ s, w j) - 1‖ + ‖w i - 1‖ := by rw [norm_mul, hwi, one_mul]
      _ ≤ ‖w i - 1‖ + ∑ j ∈ s, ‖w j - 1‖ := by linarith [ih hws]

theorem support_change_same_norm (a b a' b' : ℂ) (hn : ‖a'‖ = ‖a‖) :
    |support a' b' - support a b| ≤
      ‖a' - a‖ * ‖b'‖ + ‖a‖ * ‖b' - b‖ := by
  have he : support a' b' - support a b =
      ⟪a' - a, b'⟫_ℝ + ⟪a, b' - b⟫_ℝ := by
    simp only [support_eq_inner, inner_sub_left, inner_sub_right,
      real_inner_self_eq_norm_sq, hn]
    ring
  rw [he]
  exact (abs_add_le _ _).trans (add_le_add (abs_real_inner_le_norm _ _) (abs_real_inner_le_norm _ _))

theorem rotated_support_bound {a b u v : ℂ} {H : ℝ}
    (ha : ‖a‖ ≤ 1) (hb : ‖b‖ ≤ 1) (hu : ‖u‖ = 1) (hv : ‖v‖ = 1)
    (hU : ‖u - 1‖ ≤ H) (hV : ‖v - 1‖ ≤ H) :
    support (a * u) (b * v) ≤ support a b + 2 * H := by
  have hH : 0 ≤ H := (norm_nonneg _).trans hU
  have hau : ‖a * u‖ = ‖a‖ := by rw [norm_mul, hu, mul_one]
  have hbv : ‖b * v‖ = ‖b‖ := by rw [norm_mul, hv, mul_one]
  have hdiffa : ‖a * u - a‖ ≤ H := by
    rw [← mul_sub_one, norm_mul]
    exact (mul_le_mul ha hU (norm_nonneg _) (by norm_num)).trans_eq (one_mul H)
  have hdiffb : ‖b * v - b‖ ≤ H := by
    rw [← mul_sub_one, norm_mul]
    exact (mul_le_mul hb hV (norm_nonneg _) (by norm_num)).trans_eq (one_mul H)
  have hh := support_change_same_norm a b (a * u) (b * v) hau
  rw [hbv] at hh
  have h1 : ‖a * u - a‖ * ‖b‖ ≤ H := by
    exact (mul_le_mul hdiffa hb (norm_nonneg _) hH).trans_eq (mul_one H)
  have h2 : ‖a‖ * ‖b * v - b‖ ≤ H := by
    exact (mul_le_mul ha hdiffb (norm_nonneg _) (by norm_num)).trans_eq (one_mul H)
  have := le_abs_self (support (a * u) (b * v) - support a b)
  linarith

end Proof

end OriginalRadialGeometry

/- ## Amplification -/

section OriginalAmplification

/- Amplification by products of unit complex numbers. -/

namespace Proof

noncomputable section

def subsetProduct {E : Type*} (w : E → ℂ) (S : Finset E) : ℂ := ∏ e ∈ S, w e

def rotatedCopy {I E : Type*} (b : I → ℂ) (w : E → ℂ) (x : I × Finset E) : ℂ :=
  b x.1 * subsetProduct w x.2

theorem subsetProduct_norm {E : Type*} (w : E → ℂ) (hw : ∀ e, ‖w e‖ = 1)
    (S : Finset E) : ‖subsetProduct w S‖ = 1 :=
  norm_subset_prod S w (fun e _ => hw e)

theorem subsetProduct_close {E : Type*} [Fintype E] (w : E → ℂ)
    (hw : ∀ e, ‖w e‖ = 1) (S : Finset E) :
    ‖subsetProduct w S - 1‖ ≤ ∑ e, ‖w e - 1‖ := by
  classical
  refine (norm_prod_sub_one_le S w (fun e _ => hw e)).trans ?_
  exact Finset.sum_le_sum_of_subset_of_nonneg (Finset.subset_univ S)
    (fun e _ _ => norm_nonneg (w e - 1))

theorem rotatedCopy_injective {I E : Type*} (b : I → ℂ) (w : E → ℂ)
    (hb : ∀ i, b i ≠ 0) (hn : Function.Injective (fun i => ‖b i‖))
    (hw : ∀ e, ‖w e‖ = 1) (hprod : Function.Injective (subsetProduct w)) :
    Function.Injective (rotatedCopy b w) := by
  rintro ⟨i, S⟩ ⟨j, T⟩ he
  have hnorm := congrArg norm he
  simp only [rotatedCopy, norm_mul, subsetProduct_norm w hw, mul_one] at hnorm
  have hij := hn hnorm
  subst j
  have hST := hprod (mul_left_cancel₀ (hb i) he)
  exact Prod.ext rfl hST

theorem rotatedCopy_convexIndependent {I E : Type*} [Fintype E]