Calculating angles

Stream: new members

[Bjørn Kjos-Hanssen]

How can I calculate the angle between two concrete vectors as below? The second example does not even typecheck even though it's supposed to be identical to the first.

import Mathlib

instance : Fact (Module.finrank ℝ (EuclideanSpace ℝ (Fin 2)) = 2) := { out := finrank_euclideanSpace_fin }
instance :  Fact (Module.finrank ℝ (Fin (Nat.succ 1) → ℝ) = 2) := { out := finrank_euclideanSpace_fin }

noncomputable instance (n : Type*) [Fintype n] [DecidableEq n] :
  Module.Oriented ℝ (EuclideanSpace ℝ n) n :=
  ⟨Basis.orientation <| Pi.basisFun _ _⟩

open EuclideanGeometry

def e₁ : EuclideanSpace ℝ (Fin 2) := ![1,0]

example : ∡ e₁ 0 ![0,1] = Real.pi /(2:ℝ):= by
  sorry

example : ∡ (![1,0] : EuclideanSpace ℝ (Fin 2)) 0 ![0,1] = Real.pi /(2:ℝ):= by
  sorry

[Junyan Xu]

It doesn't typecheck because you didn't use WithLp.equiv

[Bjørn Kjos-Hanssen]

Oh... how?

[Aaron Liu]

def e₁ : EuclideanSpace ℝ (Fin 2) := !₂[1,0]

example : ∡ e₁ 0 !₂[0,1] = Real.pi /(2:ℝ):= by
  sorry

example : ∡ (!₂[1,0] : EuclideanSpace ℝ (Fin 2)) 0 !₂[0,1] = Real.pi /(2:ℝ):= by
  sorry

[Bjørn Kjos-Hanssen]

Oh thanks @Aaron Liu & @Junyan Xu , so the point is to write !₂. But then to finish the example I feel like we need to access the orientation somehow to make sure the answer is not negative pi/2?

[Bjørn Kjos-Hanssen]

OK I guess I figured it out... can post if anyone is curious :sweat_smile:

[Kenny Lau]

@Bjørn Kjos-Hanssen yeah I'd like to see it thanks

[Bjørn Kjos-Hanssen]

@Kenny Lau here you go, probably not the simplest solution but it works:

import Mathlib.Geometry.Euclidean.Angle.Oriented.Affine

instance : Fact (Module.finrank ℝ (EuclideanSpace ℝ (Fin 2)) = 2) :=
  { out := finrank_euclideanSpace_fin }

noncomputable instance (n : Type*) [Fintype n] [DecidableEq n] :
    Module.Oriented ℝ (EuclideanSpace ℝ n) n :=
  ⟨Basis.orientation <| Pi.basisFun _ _⟩

open EuclideanGeometry Orientation

theorem calculate_angle :
    (oangle (V := (WithLp 2 (Fin 2 → ℝ))) o !₂[1, 0] !₂[0, 1]).toReal
    = Real.pi / 2 := by
  simp [Orientation.oangle, Orientation.kahler, innerₛₗ]
  rw [
    Orientation.areaForm_to_volumeForm,
    Orientation.volumeForm_robust,
    Basis.det_apply, Matrix.det_fin_two]
  rw [show (EuclideanSpace.basisFun (Fin 2) ℝ).toBasis.toMatrix
      ![!₂[1, 0], !₂[0, 1]] = ![!₂[1, 0], !₂[0, 1]] by
          ext i j;fin_cases i <;> fin_cases j <;> rfl]
  simp
  exact rfl

[Bjørn Kjos-Hanssen]

By the way, the docs have a confusing typo when explaining the notation !₂ so I made #26188 to fix it.