Is this formula a thing?

Stream: maths

[Ilmārs Cīrulis]

Has it a name or maybe some proof? (Decided to ask here, but, if necessary, the topic can be moved to some other place.)

import Mathlib

open InnerProductGeometry
open scoped RealInnerProductSpace

variable {V : Type*}
variable [NormedAddCommGroup V]
variable [InnerProductSpace ℝ V]

lemma aux12 {x y z : V} (Hx : ‖x‖ = 1) (Hy : ‖y‖ = 1) (Hz : ‖z‖ = 1) :
    angle x z ≠ 0 → angle x z ≠ Real.pi →
    angle x z = angle x y + angle y z →
    Real.sin (angle x z) • y = Real.sin (angle y z) • x + Real.sin (angle x y) • z := by
  sorry

[Aaron Liu]

where did this come from?

[Ilmārs Cīrulis]

Kinda found it when tinkering with math from #new members > Criterion for equality in the triangle inequality for angles.

[Aaron Liu]

well an informal proof shouldn't be too hard

[Aaron Liu]

basically I think this is the formula for circumcenter in barycentric coordinates

[Ilmārs Cīrulis]

Would be grateful, at this moment my brain doesn't cooperate. :sweat_smile:

[Aaron Liu]

which for a triangle ABC the circumcenter is (sin 2A, sin 2B, sin 2C) where A B C are the angles

[Aaron Liu]

so let ABC be a triangle and let α β γ be its angles then the circumcenter O is given by O = (A*sin 2α + B*sin 2β + C*sin2γ) / (sin 2α + sin 2β + sin 2γ)

[Aaron Liu]

in this case of course the circumcenter is 0

[Aaron Liu]

and you apply the intercepted arc double angle thing to get angles in the triangle

[Ilmārs Cīrulis]

Ok, will try to understand this. :sweat_smile:

[Ilmārs Cīrulis]

Thank you!

[Violeta Hernández]

This is a really cool result! But no, I don't think I've seen it before.

[Ilmārs Cīrulis]

Woop, I proved that! :partying_face: