English
There exists a single radius r so that all signed distances equal r; this happens exactly when p is the incenter.
Русский
Для фиксированного p внутри аффинного пространства существование общего величины подпорогового расстояния r ко всем вершинам эквивалентно тому, что p является инцентром.
LaTeX
$$$ \exists r \in \mathbb{R}, \forall i, s.signedInfDist(i,p) = r \quad\iff\quad p = s.incenter $$$
Lean4
theorem exists_forall_signedInfDist_eq_iff_excenterExists_and_eq_excenter {p : P}
(hp : p ∈ affineSpan ℝ (Set.range s.points)) {signs : Finset (Fin (n + 1))} :
(∃ r : ℝ, ∀ i, s.signedInfDist i p = (if i ∈ signs then -1 else 1) * r) ↔
s.ExcenterExists signs ∧ p = s.excenter signs :=
by
refine ⟨?_, ?_⟩
· rintro ⟨r, h⟩
obtain ⟨w, h1, rfl⟩ := eq_affineCombination_of_mem_affineSpan_of_fintype hp
have h' : ∀ i, w i * ‖s.points i -ᵥ s.altitudeFoot i‖ = (if i ∈ signs then -1 else 1) * r :=
by
intro i
rw [altitudeFoot, ← s.signedInfDist_affineCombination i h1]
exact h i
simp_rw [← dist_eq_norm_vsub] at h'
have h'' : ∀ i, w i = r * s.excenterWeightsUnnorm signs i :=
by
simp_rw [excenterWeightsUnnorm]
intro i
replace h' := h' i
rw [← height, ← eq_div_iff (s.height_pos i).ne'] at h'
rw [h', mul_comm, div_eq_mul_inv, mul_assoc, height, altitudeFoot, orthogonalProjectionSpan]
have hw : w = s.excenterWeights signs :=
by
simp_rw [h'', ← Finset.mul_sum] at h1
ext j
rw [h'', eq_inv_of_mul_eq_one_left h1]
simp [excenterWeights]
subst hw
exact ⟨s.sum_excenterWeights_eq_one_iff.1 h1, rfl⟩
· rintro ⟨h, rfl⟩
refine ⟨SignType.sign (∑ j, s.excenterWeightsUnnorm signs j) * (s.exradius signs), fun i ↦ ?_⟩
rw [h.signedInfDist_excenter]
simp
