Lean4
/-- The induction step for the existence and uniqueness of the
circumcenter. Given a nonempty set of points in a nonempty affine
subspace whose direction is complete, such that there is a unique
(circumcenter, circumradius) pair for those points in that subspace,
and a point `p` not in that subspace, there is a unique (circumcenter,
circumradius) pair for the set with `p` added, in the span of the
subspace with `p` added. -/
theorem existsUnique_dist_eq_of_insert {s : AffineSubspace ℝ P} [s.direction.HasOrthogonalProjection] {ps : Set P}
(hnps : ps.Nonempty) {p : P} (hps : ps ⊆ s) (hp : p ∉ s)
(hu : ∃! cs : Sphere P, cs.center ∈ s ∧ ps ⊆ (cs : Set P)) :
∃! cs₂ : Sphere P, cs₂.center ∈ affineSpan ℝ (insert p (s : Set P)) ∧ insert p ps ⊆ (cs₂ : Set P) :=
by
haveI : Nonempty s := Set.Nonempty.to_subtype (hnps.mono hps)
rcases hu with ⟨⟨cc, cr⟩, ⟨hcc, hcr⟩, hcccru⟩
simp only at hcc hcr hcccru
let x := dist cc (orthogonalProjection s p)
let y := dist p (orthogonalProjection s p)
have hy0 : y ≠ 0 := dist_orthogonalProjection_ne_zero_of_notMem hp
let ycc₂ := (x * x + y * y - cr * cr) / (2 * y)
let cc₂ := (ycc₂ / y) • (p -ᵥ orthogonalProjection s p : V) +ᵥ cc
let cr₂ := √(cr * cr + ycc₂ * ycc₂)
use ⟨cc₂, cr₂⟩
simp -zeta -proj only
have hpo : p = (1 : ℝ) • (p -ᵥ orthogonalProjection s p : V) +ᵥ (orthogonalProjection s p : P) := by simp
constructor
· constructor
· refine vadd_mem_of_mem_direction ?_ (mem_affineSpan ℝ (Set.mem_insert_of_mem _ hcc))
rw [direction_affineSpan]
exact
Submodule.smul_mem _ _
(vsub_mem_vectorSpan ℝ (Set.mem_insert _ _) (Set.mem_insert_of_mem _ (orthogonalProjection_mem _)))
· intro p₁ hp₁
rw [Sphere.mem_coe, mem_sphere, ← mul_self_inj_of_nonneg dist_nonneg (Real.sqrt_nonneg _),
Real.mul_self_sqrt (add_nonneg (mul_self_nonneg _) (mul_self_nonneg _))]
rcases hp₁ with hp₁ | hp₁
· rw [hp₁, hpo,
dist_sq_smul_orthogonal_vadd_smul_orthogonal_vadd (orthogonalProjection_mem p) hcc _ _
(vsub_orthogonalProjection_mem_direction_orthogonal s p),
← dist_eq_norm_vsub V p, dist_comm _ cc]
simp only [ycc₂]
field_simp
ring
·
rw [dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq _ (hps hp₁),
orthogonalProjection_vadd_smul_vsub_orthogonalProjection _ _ hcc, Subtype.coe_mk,
dist_of_mem_subset_mk_sphere hp₁ hcr, dist_eq_norm_vsub V cc₂ cc, vadd_vsub, norm_smul, ← dist_eq_norm_vsub V,
Real.norm_eq_abs, abs_div, abs_of_nonneg dist_nonneg, div_mul_cancel₀ _ hy0, abs_mul_abs_self]
· rintro ⟨cc₃, cr₃⟩ ⟨hcc₃, hcr₃⟩
simp only at hcc₃ hcr₃
obtain ⟨t₃, cc₃', hcc₃', hcc₃''⟩ : ∃ r : ℝ, ∃ p0 ∈ s, cc₃ = r • (p -ᵥ ↑((orthogonalProjection s) p)) +ᵥ p0 := by
rwa [mem_affineSpan_insert_iff (orthogonalProjection_mem p)] at hcc₃
have hcr₃' : ∃ r, ∀ p₁ ∈ ps, dist p₁ cc₃ = r :=
⟨cr₃, fun p₁ hp₁ => dist_of_mem_subset_mk_sphere (Set.mem_insert_of_mem _ hp₁) hcr₃⟩
rw [exists_dist_eq_iff_exists_dist_orthogonalProjection_eq hps cc₃, hcc₃'',
orthogonalProjection_vadd_smul_vsub_orthogonalProjection _ _ hcc₃'] at hcr₃'
obtain ⟨cr₃', hcr₃'⟩ := hcr₃'
have hu := hcccru ⟨cc₃', cr₃'⟩
simp only at hu
replace hu := hu ⟨hcc₃', hcr₃'⟩
cases hu
have hcr₃val : cr₃ = √(cr * cr + t₃ * y * (t₃ * y)) :=
by
obtain ⟨p0, hp0⟩ := hnps
have h' : ↑(⟨cc, hcc₃'⟩ : s) = cc := rfl
rw [← dist_of_mem_subset_mk_sphere (Set.mem_insert_of_mem _ hp0) hcr₃, hcc₃'', ←
mul_self_inj_of_nonneg dist_nonneg (Real.sqrt_nonneg _),
Real.mul_self_sqrt (add_nonneg (mul_self_nonneg _) (mul_self_nonneg _)),
dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq _ (hps hp0),
orthogonalProjection_vadd_smul_vsub_orthogonalProjection _ _ hcc₃', h', dist_of_mem_subset_mk_sphere hp0 hcr,
dist_eq_norm_vsub V _ cc, vadd_vsub, norm_smul, ← dist_eq_norm_vsub V p, Real.norm_eq_abs, ← mul_assoc,
mul_comm _ |t₃|, ← mul_assoc, abs_mul_abs_self]
ring
replace hcr₃ := dist_of_mem_subset_mk_sphere (Set.mem_insert _ _) hcr₃
rw [hpo, hcc₃'', hcr₃val, ← mul_self_inj_of_nonneg dist_nonneg (Real.sqrt_nonneg _),
dist_sq_smul_orthogonal_vadd_smul_orthogonal_vadd (orthogonalProjection_mem p) hcc₃' _ _
(vsub_orthogonalProjection_mem_direction_orthogonal s p),
dist_comm, ← dist_eq_norm_vsub V p,
Real.mul_self_sqrt (add_nonneg (mul_self_nonneg _) (mul_self_nonneg _))] at hcr₃
change x * x + _ * (y * y) = _ at hcr₃
rw [show x * x + (1 - t₃) * (1 - t₃) * (y * y) = x * x + y * y - 2 * y * (t₃ * y) + t₃ * y * (t₃ * y) by ring,
add_left_inj] at hcr₃
have ht₃ : t₃ = ycc₂ / y := by simp [ycc₂, ← hcr₃, hy0]
subst ht₃
change cc₃ = cc₂ at hcc₃''
congr
rw [hcr₃val]
congr 2
field_simp
