From 53fdc5a6349ad967a5d19f3b38ddf9c61da52da1 Mon Sep 17 00:00:00 2001 From: Parcly Taxel Date: Sun, 11 Jun 2023 17:25:05 +0800 Subject: [PATCH 1/5] feat: port Geometry.Euclidean.Angle.Oriented.Basic From d53e4279eb87b50c3fb738b15c5084d1e0b29ffb Mon Sep 17 00:00:00 2001 From: Parcly Taxel Date: Sun, 11 Jun 2023 17:25:05 +0800 Subject: [PATCH 2/5] Initial file copy from mathport --- .../Euclidean/Angle/Oriented/Basic.lean | 1144 +++++++++++++++++ 1 file changed, 1144 insertions(+) create mode 100644 Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean diff --git a/Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean b/Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean new file mode 100644 index 0000000000000..bf588bf8a7579 --- /dev/null +++ b/Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean @@ -0,0 +1,1144 @@ +/- +Copyright (c) 2022 Joseph Myers. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Joseph Myers, Heather Macbeth + +! This file was ported from Lean 3 source module geometry.euclidean.angle.oriented.basic +! leanprover-community/mathlib commit f0c8bf9245297a541f468be517f1bde6195105e9 +! Please do not edit these lines, except to modify the commit id +! if you have ported upstream changes. +-/ +import Mathbin.Analysis.InnerProductSpace.TwoDim +import Mathbin.Geometry.Euclidean.Angle.Unoriented.Basic + +/-! +# Oriented angles. + +This file defines oriented angles in real inner product spaces. + +## Main definitions + +* `orientation.oangle` is the oriented angle between two vectors with respect to an orientation. + +## Implementation notes + +The definitions here use the `real.angle` type, angles modulo `2 * π`. For some purposes, +angles modulo `π` are more convenient, because results are true for such angles with less +configuration dependence. Results that are only equalities modulo `π` can be represented +modulo `2 * π` as equalities of `(2 : ℤ) • θ`. + +## References + +* Evan Chen, Euclidean Geometry in Mathematical Olympiads. + +-/ + + +noncomputable section + +open FiniteDimensional Complex + +open scoped Real RealInnerProductSpace ComplexConjugate + +namespace Orientation + +attribute [local instance] fact_finite_dimensional_of_finrank_eq_succ + +attribute [local instance] Complex.finrank_real_complex_fact + +variable {V V' : Type _} + +variable [NormedAddCommGroup V] [NormedAddCommGroup V'] + +variable [InnerProductSpace ℝ V] [InnerProductSpace ℝ V'] + +variable [Fact (finrank ℝ V = 2)] [Fact (finrank ℝ V' = 2)] (o : Orientation ℝ V (Fin 2)) + +-- mathport name: exprω +local notation "ω" => o.areaForm + +/-- The oriented angle from `x` to `y`, modulo `2 * π`. If either vector is 0, this is 0. +See `inner_product_geometry.angle` for the corresponding unoriented angle definition. -/ +def oangle (x y : V) : Real.Angle := + Complex.arg (o.kahler x y) +#align orientation.oangle Orientation.oangle + +/-- Oriented angles are continuous when the vectors involved are nonzero. -/ +theorem continuousAt_oangle {x : V × V} (hx1 : x.1 ≠ 0) (hx2 : x.2 ≠ 0) : + ContinuousAt (fun y : V × V => o.oangle y.1 y.2) x := + by + refine' (Complex.continuousAt_arg_coe_angle _).comp _ + · exact o.kahler_ne_zero hx1 hx2 + exact + ((continuous_of_real.comp continuous_inner).add + ((continuous_of_real.comp o.area_form'.continuous₂).mul continuous_const)).ContinuousAt +#align orientation.continuous_at_oangle Orientation.continuousAt_oangle + +/-- If the first vector passed to `oangle` is 0, the result is 0. -/ +@[simp] +theorem oangle_zero_left (x : V) : o.oangle 0 x = 0 := by simp [oangle] +#align orientation.oangle_zero_left Orientation.oangle_zero_left + +/-- If the second vector passed to `oangle` is 0, the result is 0. -/ +@[simp] +theorem oangle_zero_right (x : V) : o.oangle x 0 = 0 := by simp [oangle] +#align orientation.oangle_zero_right Orientation.oangle_zero_right + +/-- If the two vectors passed to `oangle` are the same, the result is 0. -/ +@[simp] +theorem oangle_self (x : V) : o.oangle x x = 0 := + by + simp only [oangle, kahler_apply_self, ← Complex.ofReal_pow] + convert QuotientAddGroup.mk_zero _ + apply arg_of_real_of_nonneg + positivity +#align orientation.oangle_self Orientation.oangle_self + +/-- If the angle between two vectors is nonzero, the first vector is nonzero. -/ +theorem left_ne_zero_of_oangle_ne_zero {x y : V} (h : o.oangle x y ≠ 0) : x ≠ 0 := by rintro rfl; + simpa using h +#align orientation.left_ne_zero_of_oangle_ne_zero Orientation.left_ne_zero_of_oangle_ne_zero + +/-- If the angle between two vectors is nonzero, the second vector is nonzero. -/ +theorem right_ne_zero_of_oangle_ne_zero {x y : V} (h : o.oangle x y ≠ 0) : y ≠ 0 := by rintro rfl; + simpa using h +#align orientation.right_ne_zero_of_oangle_ne_zero Orientation.right_ne_zero_of_oangle_ne_zero + +/-- If the angle between two vectors is nonzero, the vectors are not equal. -/ +theorem ne_of_oangle_ne_zero {x y : V} (h : o.oangle x y ≠ 0) : x ≠ y := by rintro rfl; + simpa using h +#align orientation.ne_of_oangle_ne_zero Orientation.ne_of_oangle_ne_zero + +/-- If the angle between two vectors is `π`, the first vector is nonzero. -/ +theorem left_ne_zero_of_oangle_eq_pi {x y : V} (h : o.oangle x y = π) : x ≠ 0 := + o.left_ne_zero_of_oangle_ne_zero (h.symm ▸ Real.Angle.pi_ne_zero : o.oangle x y ≠ 0) +#align orientation.left_ne_zero_of_oangle_eq_pi Orientation.left_ne_zero_of_oangle_eq_pi + +/-- If the angle between two vectors is `π`, the second vector is nonzero. -/ +theorem right_ne_zero_of_oangle_eq_pi {x y : V} (h : o.oangle x y = π) : y ≠ 0 := + o.right_ne_zero_of_oangle_ne_zero (h.symm ▸ Real.Angle.pi_ne_zero : o.oangle x y ≠ 0) +#align orientation.right_ne_zero_of_oangle_eq_pi Orientation.right_ne_zero_of_oangle_eq_pi + +/-- If the angle between two vectors is `π`, the vectors are not equal. -/ +theorem ne_of_oangle_eq_pi {x y : V} (h : o.oangle x y = π) : x ≠ y := + o.ne_of_oangle_ne_zero (h.symm ▸ Real.Angle.pi_ne_zero : o.oangle x y ≠ 0) +#align orientation.ne_of_oangle_eq_pi Orientation.ne_of_oangle_eq_pi + +/-- If the angle between two vectors is `π / 2`, the first vector is nonzero. -/ +theorem left_ne_zero_of_oangle_eq_pi_div_two {x y : V} (h : o.oangle x y = (π / 2 : ℝ)) : x ≠ 0 := + o.left_ne_zero_of_oangle_ne_zero (h.symm ▸ Real.Angle.pi_div_two_ne_zero : o.oangle x y ≠ 0) +#align orientation.left_ne_zero_of_oangle_eq_pi_div_two Orientation.left_ne_zero_of_oangle_eq_pi_div_two + +/-- If the angle between two vectors is `π / 2`, the second vector is nonzero. -/ +theorem right_ne_zero_of_oangle_eq_pi_div_two {x y : V} (h : o.oangle x y = (π / 2 : ℝ)) : y ≠ 0 := + o.right_ne_zero_of_oangle_ne_zero (h.symm ▸ Real.Angle.pi_div_two_ne_zero : o.oangle x y ≠ 0) +#align orientation.right_ne_zero_of_oangle_eq_pi_div_two Orientation.right_ne_zero_of_oangle_eq_pi_div_two + +/-- If the angle between two vectors is `π / 2`, the vectors are not equal. -/ +theorem ne_of_oangle_eq_pi_div_two {x y : V} (h : o.oangle x y = (π / 2 : ℝ)) : x ≠ y := + o.ne_of_oangle_ne_zero (h.symm ▸ Real.Angle.pi_div_two_ne_zero : o.oangle x y ≠ 0) +#align orientation.ne_of_oangle_eq_pi_div_two Orientation.ne_of_oangle_eq_pi_div_two + +/-- If the angle between two vectors is `-π / 2`, the first vector is nonzero. -/ +theorem left_ne_zero_of_oangle_eq_neg_pi_div_two {x y : V} (h : o.oangle x y = (-π / 2 : ℝ)) : + x ≠ 0 := + o.left_ne_zero_of_oangle_ne_zero (h.symm ▸ Real.Angle.neg_pi_div_two_ne_zero : o.oangle x y ≠ 0) +#align orientation.left_ne_zero_of_oangle_eq_neg_pi_div_two Orientation.left_ne_zero_of_oangle_eq_neg_pi_div_two + +/-- If the angle between two vectors is `-π / 2`, the second vector is nonzero. -/ +theorem right_ne_zero_of_oangle_eq_neg_pi_div_two {x y : V} (h : o.oangle x y = (-π / 2 : ℝ)) : + y ≠ 0 := + o.right_ne_zero_of_oangle_ne_zero (h.symm ▸ Real.Angle.neg_pi_div_two_ne_zero : o.oangle x y ≠ 0) +#align orientation.right_ne_zero_of_oangle_eq_neg_pi_div_two Orientation.right_ne_zero_of_oangle_eq_neg_pi_div_two + +/-- If the angle between two vectors is `-π / 2`, the vectors are not equal. -/ +theorem ne_of_oangle_eq_neg_pi_div_two {x y : V} (h : o.oangle x y = (-π / 2 : ℝ)) : x ≠ y := + o.ne_of_oangle_ne_zero (h.symm ▸ Real.Angle.neg_pi_div_two_ne_zero : o.oangle x y ≠ 0) +#align orientation.ne_of_oangle_eq_neg_pi_div_two Orientation.ne_of_oangle_eq_neg_pi_div_two + +/-- If the sign of the angle between two vectors is nonzero, the first vector is nonzero. -/ +theorem left_ne_zero_of_oangle_sign_ne_zero {x y : V} (h : (o.oangle x y).sign ≠ 0) : x ≠ 0 := + o.left_ne_zero_of_oangle_ne_zero (Real.Angle.sign_ne_zero_iff.1 h).1 +#align orientation.left_ne_zero_of_oangle_sign_ne_zero Orientation.left_ne_zero_of_oangle_sign_ne_zero + +/-- If the sign of the angle between two vectors is nonzero, the second vector is nonzero. -/ +theorem right_ne_zero_of_oangle_sign_ne_zero {x y : V} (h : (o.oangle x y).sign ≠ 0) : y ≠ 0 := + o.right_ne_zero_of_oangle_ne_zero (Real.Angle.sign_ne_zero_iff.1 h).1 +#align orientation.right_ne_zero_of_oangle_sign_ne_zero Orientation.right_ne_zero_of_oangle_sign_ne_zero + +/-- If the sign of the angle between two vectors is nonzero, the vectors are not equal. -/ +theorem ne_of_oangle_sign_ne_zero {x y : V} (h : (o.oangle x y).sign ≠ 0) : x ≠ y := + o.ne_of_oangle_ne_zero (Real.Angle.sign_ne_zero_iff.1 h).1 +#align orientation.ne_of_oangle_sign_ne_zero Orientation.ne_of_oangle_sign_ne_zero + +/-- If the sign of the angle between two vectors is positive, the first vector is nonzero. -/ +theorem left_ne_zero_of_oangle_sign_eq_one {x y : V} (h : (o.oangle x y).sign = 1) : x ≠ 0 := + o.left_ne_zero_of_oangle_sign_ne_zero (h.symm ▸ by decide : (o.oangle x y).sign ≠ 0) +#align orientation.left_ne_zero_of_oangle_sign_eq_one Orientation.left_ne_zero_of_oangle_sign_eq_one + +/-- If the sign of the angle between two vectors is positive, the second vector is nonzero. -/ +theorem right_ne_zero_of_oangle_sign_eq_one {x y : V} (h : (o.oangle x y).sign = 1) : y ≠ 0 := + o.right_ne_zero_of_oangle_sign_ne_zero (h.symm ▸ by decide : (o.oangle x y).sign ≠ 0) +#align orientation.right_ne_zero_of_oangle_sign_eq_one Orientation.right_ne_zero_of_oangle_sign_eq_one + +/-- If the sign of the angle between two vectors is positive, the vectors are not equal. -/ +theorem ne_of_oangle_sign_eq_one {x y : V} (h : (o.oangle x y).sign = 1) : x ≠ y := + o.ne_of_oangle_sign_ne_zero (h.symm ▸ by decide : (o.oangle x y).sign ≠ 0) +#align orientation.ne_of_oangle_sign_eq_one Orientation.ne_of_oangle_sign_eq_one + +/-- If the sign of the angle between two vectors is negative, the first vector is nonzero. -/ +theorem left_ne_zero_of_oangle_sign_eq_neg_one {x y : V} (h : (o.oangle x y).sign = -1) : x ≠ 0 := + o.left_ne_zero_of_oangle_sign_ne_zero (h.symm ▸ by decide : (o.oangle x y).sign ≠ 0) +#align orientation.left_ne_zero_of_oangle_sign_eq_neg_one Orientation.left_ne_zero_of_oangle_sign_eq_neg_one + +/-- If the sign of the angle between two vectors is negative, the second vector is nonzero. -/ +theorem right_ne_zero_of_oangle_sign_eq_neg_one {x y : V} (h : (o.oangle x y).sign = -1) : y ≠ 0 := + o.right_ne_zero_of_oangle_sign_ne_zero (h.symm ▸ by decide : (o.oangle x y).sign ≠ 0) +#align orientation.right_ne_zero_of_oangle_sign_eq_neg_one Orientation.right_ne_zero_of_oangle_sign_eq_neg_one + +/-- If the sign of the angle between two vectors is negative, the vectors are not equal. -/ +theorem ne_of_oangle_sign_eq_neg_one {x y : V} (h : (o.oangle x y).sign = -1) : x ≠ y := + o.ne_of_oangle_sign_ne_zero (h.symm ▸ by decide : (o.oangle x y).sign ≠ 0) +#align orientation.ne_of_oangle_sign_eq_neg_one Orientation.ne_of_oangle_sign_eq_neg_one + +/-- Swapping the two vectors passed to `oangle` negates the angle. -/ +theorem oangle_rev (x y : V) : o.oangle y x = -o.oangle x y := by + simp only [oangle, o.kahler_swap y x, Complex.arg_conj_coe_angle] +#align orientation.oangle_rev Orientation.oangle_rev + +/-- Adding the angles between two vectors in each order results in 0. -/ +@[simp] +theorem oangle_add_oangle_rev (x y : V) : o.oangle x y + o.oangle y x = 0 := by + simp [o.oangle_rev y x] +#align orientation.oangle_add_oangle_rev Orientation.oangle_add_oangle_rev + +/-- Negating the first vector passed to `oangle` adds `π` to the angle. -/ +theorem oangle_neg_left {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) : o.oangle (-x) y = o.oangle x y + π := + by + simp only [oangle, map_neg] + convert Complex.arg_neg_coe_angle _ + exact o.kahler_ne_zero hx hy +#align orientation.oangle_neg_left Orientation.oangle_neg_left + +/-- Negating the second vector passed to `oangle` adds `π` to the angle. -/ +theorem oangle_neg_right {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) : o.oangle x (-y) = o.oangle x y + π := + by + simp only [oangle, map_neg] + convert Complex.arg_neg_coe_angle _ + exact o.kahler_ne_zero hx hy +#align orientation.oangle_neg_right Orientation.oangle_neg_right + +/-- Negating the first vector passed to `oangle` does not change twice the angle. -/ +@[simp] +theorem two_zsmul_oangle_neg_left (x y : V) : (2 : ℤ) • o.oangle (-x) y = (2 : ℤ) • o.oangle x y := + by + by_cases hx : x = 0 + · simp [hx] + · by_cases hy : y = 0 + · simp [hy] + · simp [o.oangle_neg_left hx hy] +#align orientation.two_zsmul_oangle_neg_left Orientation.two_zsmul_oangle_neg_left + +/-- Negating the second vector passed to `oangle` does not change twice the angle. -/ +@[simp] +theorem two_zsmul_oangle_neg_right (x y : V) : (2 : ℤ) • o.oangle x (-y) = (2 : ℤ) • o.oangle x y := + by + by_cases hx : x = 0 + · simp [hx] + · by_cases hy : y = 0 + · simp [hy] + · simp [o.oangle_neg_right hx hy] +#align orientation.two_zsmul_oangle_neg_right Orientation.two_zsmul_oangle_neg_right + +/-- Negating both vectors passed to `oangle` does not change the angle. -/ +@[simp] +theorem oangle_neg_neg (x y : V) : o.oangle (-x) (-y) = o.oangle x y := by simp [oangle] +#align orientation.oangle_neg_neg Orientation.oangle_neg_neg + +/-- Negating the first vector produces the same angle as negating the second vector. -/ +theorem oangle_neg_left_eq_neg_right (x y : V) : o.oangle (-x) y = o.oangle x (-y) := by + rw [← neg_neg y, oangle_neg_neg, neg_neg] +#align orientation.oangle_neg_left_eq_neg_right Orientation.oangle_neg_left_eq_neg_right + +/-- The angle between the negation of a nonzero vector and that vector is `π`. -/ +@[simp] +theorem oangle_neg_self_left {x : V} (hx : x ≠ 0) : o.oangle (-x) x = π := by + simp [oangle_neg_left, hx] +#align orientation.oangle_neg_self_left Orientation.oangle_neg_self_left + +/-- The angle between a nonzero vector and its negation is `π`. -/ +@[simp] +theorem oangle_neg_self_right {x : V} (hx : x ≠ 0) : o.oangle x (-x) = π := by + simp [oangle_neg_right, hx] +#align orientation.oangle_neg_self_right Orientation.oangle_neg_self_right + +/-- Twice the angle between the negation of a vector and that vector is 0. -/ +@[simp] +theorem two_zsmul_oangle_neg_self_left (x : V) : (2 : ℤ) • o.oangle (-x) x = 0 := by + by_cases hx : x = 0 <;> simp [hx] +#align orientation.two_zsmul_oangle_neg_self_left Orientation.two_zsmul_oangle_neg_self_left + +/-- Twice the angle between a vector and its negation is 0. -/ +@[simp] +theorem two_zsmul_oangle_neg_self_right (x : V) : (2 : ℤ) • o.oangle x (-x) = 0 := by + by_cases hx : x = 0 <;> simp [hx] +#align orientation.two_zsmul_oangle_neg_self_right Orientation.two_zsmul_oangle_neg_self_right + +/-- Adding the angles between two vectors in each order, with the first vector in each angle +negated, results in 0. -/ +@[simp] +theorem oangle_add_oangle_rev_neg_left (x y : V) : o.oangle (-x) y + o.oangle (-y) x = 0 := by + rw [oangle_neg_left_eq_neg_right, oangle_rev, add_left_neg] +#align orientation.oangle_add_oangle_rev_neg_left Orientation.oangle_add_oangle_rev_neg_left + +/-- Adding the angles between two vectors in each order, with the second vector in each angle +negated, results in 0. -/ +@[simp] +theorem oangle_add_oangle_rev_neg_right (x y : V) : o.oangle x (-y) + o.oangle y (-x) = 0 := by + rw [o.oangle_rev (-x), oangle_neg_left_eq_neg_right, add_neg_self] +#align orientation.oangle_add_oangle_rev_neg_right Orientation.oangle_add_oangle_rev_neg_right + +/-- Multiplying the first vector passed to `oangle` by a positive real does not change the +angle. -/ +@[simp] +theorem oangle_smul_left_of_pos (x y : V) {r : ℝ} (hr : 0 < r) : + o.oangle (r • x) y = o.oangle x y := by simp [oangle, Complex.arg_real_mul _ hr] +#align orientation.oangle_smul_left_of_pos Orientation.oangle_smul_left_of_pos + +/-- Multiplying the second vector passed to `oangle` by a positive real does not change the +angle. -/ +@[simp] +theorem oangle_smul_right_of_pos (x y : V) {r : ℝ} (hr : 0 < r) : + o.oangle x (r • y) = o.oangle x y := by simp [oangle, Complex.arg_real_mul _ hr] +#align orientation.oangle_smul_right_of_pos Orientation.oangle_smul_right_of_pos + +/-- Multiplying the first vector passed to `oangle` by a negative real produces the same angle +as negating that vector. -/ +@[simp] +theorem oangle_smul_left_of_neg (x y : V) {r : ℝ} (hr : r < 0) : + o.oangle (r • x) y = o.oangle (-x) y := by + rw [← neg_neg r, neg_smul, ← smul_neg, o.oangle_smul_left_of_pos _ _ (neg_pos_of_neg hr)] +#align orientation.oangle_smul_left_of_neg Orientation.oangle_smul_left_of_neg + +/-- Multiplying the second vector passed to `oangle` by a negative real produces the same angle +as negating that vector. -/ +@[simp] +theorem oangle_smul_right_of_neg (x y : V) {r : ℝ} (hr : r < 0) : + o.oangle x (r • y) = o.oangle x (-y) := by + rw [← neg_neg r, neg_smul, ← smul_neg, o.oangle_smul_right_of_pos _ _ (neg_pos_of_neg hr)] +#align orientation.oangle_smul_right_of_neg Orientation.oangle_smul_right_of_neg + +/-- The angle between a nonnegative multiple of a vector and that vector is 0. -/ +@[simp] +theorem oangle_smul_left_self_of_nonneg (x : V) {r : ℝ} (hr : 0 ≤ r) : o.oangle (r • x) x = 0 := + by + rcases hr.lt_or_eq with (h | h) + · simp [h] + · simp [h.symm] +#align orientation.oangle_smul_left_self_of_nonneg Orientation.oangle_smul_left_self_of_nonneg + +/-- The angle between a vector and a nonnegative multiple of that vector is 0. -/ +@[simp] +theorem oangle_smul_right_self_of_nonneg (x : V) {r : ℝ} (hr : 0 ≤ r) : o.oangle x (r • x) = 0 := + by + rcases hr.lt_or_eq with (h | h) + · simp [h] + · simp [h.symm] +#align orientation.oangle_smul_right_self_of_nonneg Orientation.oangle_smul_right_self_of_nonneg + +/-- The angle between two nonnegative multiples of the same vector is 0. -/ +@[simp] +theorem oangle_smul_smul_self_of_nonneg (x : V) {r₁ r₂ : ℝ} (hr₁ : 0 ≤ r₁) (hr₂ : 0 ≤ r₂) : + o.oangle (r₁ • x) (r₂ • x) = 0 := + by + rcases hr₁.lt_or_eq with (h | h) + · simp [h, hr₂] + · simp [h.symm] +#align orientation.oangle_smul_smul_self_of_nonneg Orientation.oangle_smul_smul_self_of_nonneg + +/-- Multiplying the first vector passed to `oangle` by a nonzero real does not change twice the +angle. -/ +@[simp] +theorem two_zsmul_oangle_smul_left_of_ne_zero (x y : V) {r : ℝ} (hr : r ≠ 0) : + (2 : ℤ) • o.oangle (r • x) y = (2 : ℤ) • o.oangle x y := by + rcases hr.lt_or_lt with (h | h) <;> simp [h] +#align orientation.two_zsmul_oangle_smul_left_of_ne_zero Orientation.two_zsmul_oangle_smul_left_of_ne_zero + +/-- Multiplying the second vector passed to `oangle` by a nonzero real does not change twice the +angle. -/ +@[simp] +theorem two_zsmul_oangle_smul_right_of_ne_zero (x y : V) {r : ℝ} (hr : r ≠ 0) : + (2 : ℤ) • o.oangle x (r • y) = (2 : ℤ) • o.oangle x y := by + rcases hr.lt_or_lt with (h | h) <;> simp [h] +#align orientation.two_zsmul_oangle_smul_right_of_ne_zero Orientation.two_zsmul_oangle_smul_right_of_ne_zero + +/-- Twice the angle between a multiple of a vector and that vector is 0. -/ +@[simp] +theorem two_zsmul_oangle_smul_left_self (x : V) {r : ℝ} : (2 : ℤ) • o.oangle (r • x) x = 0 := by + rcases lt_or_le r 0 with (h | h) <;> simp [h] +#align orientation.two_zsmul_oangle_smul_left_self Orientation.two_zsmul_oangle_smul_left_self + +/-- Twice the angle between a vector and a multiple of that vector is 0. -/ +@[simp] +theorem two_zsmul_oangle_smul_right_self (x : V) {r : ℝ} : (2 : ℤ) • o.oangle x (r • x) = 0 := by + rcases lt_or_le r 0 with (h | h) <;> simp [h] +#align orientation.two_zsmul_oangle_smul_right_self Orientation.two_zsmul_oangle_smul_right_self + +/-- Twice the angle between two multiples of a vector is 0. -/ +@[simp] +theorem two_zsmul_oangle_smul_smul_self (x : V) {r₁ r₂ : ℝ} : + (2 : ℤ) • o.oangle (r₁ • x) (r₂ • x) = 0 := by by_cases h : r₁ = 0 <;> simp [h] +#align orientation.two_zsmul_oangle_smul_smul_self Orientation.two_zsmul_oangle_smul_smul_self + +/-- If the spans of two vectors are equal, twice angles with those vectors on the left are +equal. -/ +theorem two_zsmul_oangle_left_of_span_eq {x y : V} (z : V) (h : (ℝ ∙ x) = ℝ ∙ y) : + (2 : ℤ) • o.oangle x z = (2 : ℤ) • o.oangle y z := + by + rw [Submodule.span_singleton_eq_span_singleton] at h + rcases h with ⟨r, rfl⟩ + exact (o.two_zsmul_oangle_smul_left_of_ne_zero _ _ (Units.ne_zero _)).symm +#align orientation.two_zsmul_oangle_left_of_span_eq Orientation.two_zsmul_oangle_left_of_span_eq + +/-- If the spans of two vectors are equal, twice angles with those vectors on the right are +equal. -/ +theorem two_zsmul_oangle_right_of_span_eq (x : V) {y z : V} (h : (ℝ ∙ y) = ℝ ∙ z) : + (2 : ℤ) • o.oangle x y = (2 : ℤ) • o.oangle x z := + by + rw [Submodule.span_singleton_eq_span_singleton] at h + rcases h with ⟨r, rfl⟩ + exact (o.two_zsmul_oangle_smul_right_of_ne_zero _ _ (Units.ne_zero _)).symm +#align orientation.two_zsmul_oangle_right_of_span_eq Orientation.two_zsmul_oangle_right_of_span_eq + +/-- If the spans of two pairs of vectors are equal, twice angles between those vectors are +equal. -/ +theorem two_zsmul_oangle_of_span_eq_of_span_eq {w x y z : V} (hwx : (ℝ ∙ w) = ℝ ∙ x) + (hyz : (ℝ ∙ y) = ℝ ∙ z) : (2 : ℤ) • o.oangle w y = (2 : ℤ) • o.oangle x z := by + rw [o.two_zsmul_oangle_left_of_span_eq y hwx, o.two_zsmul_oangle_right_of_span_eq x hyz] +#align orientation.two_zsmul_oangle_of_span_eq_of_span_eq Orientation.two_zsmul_oangle_of_span_eq_of_span_eq + +/-- The oriented angle between two vectors is zero if and only if the angle with the vectors +swapped is zero. -/ +theorem oangle_eq_zero_iff_oangle_rev_eq_zero {x y : V} : o.oangle x y = 0 ↔ o.oangle y x = 0 := by + rw [oangle_rev, neg_eq_zero] +#align orientation.oangle_eq_zero_iff_oangle_rev_eq_zero Orientation.oangle_eq_zero_iff_oangle_rev_eq_zero + +/-- The oriented angle between two vectors is zero if and only if they are on the same ray. -/ +theorem oangle_eq_zero_iff_sameRay {x y : V} : o.oangle x y = 0 ↔ SameRay ℝ x y := + by + rw [oangle, kahler_apply_apply, Complex.arg_coe_angle_eq_iff_eq_toReal, Real.Angle.toReal_zero, + Complex.arg_eq_zero_iff] + simpa using o.nonneg_inner_and_area_form_eq_zero_iff_same_ray x y +#align orientation.oangle_eq_zero_iff_same_ray Orientation.oangle_eq_zero_iff_sameRay + +/-- The oriented angle between two vectors is `π` if and only if the angle with the vectors +swapped is `π`. -/ +theorem oangle_eq_pi_iff_oangle_rev_eq_pi {x y : V} : o.oangle x y = π ↔ o.oangle y x = π := by + rw [oangle_rev, neg_eq_iff_eq_neg, Real.Angle.neg_coe_pi] +#align orientation.oangle_eq_pi_iff_oangle_rev_eq_pi Orientation.oangle_eq_pi_iff_oangle_rev_eq_pi + +/-- The oriented angle between two vectors is `π` if and only they are nonzero and the first is +on the same ray as the negation of the second. -/ +theorem oangle_eq_pi_iff_sameRay_neg {x y : V} : + o.oangle x y = π ↔ x ≠ 0 ∧ y ≠ 0 ∧ SameRay ℝ x (-y) := + by + rw [← o.oangle_eq_zero_iff_same_ray] + constructor + · intro h + by_cases hx : x = 0; · simpa [hx, real.angle.pi_ne_zero.symm] using h + by_cases hy : y = 0; · simpa [hy, real.angle.pi_ne_zero.symm] using h + refine' ⟨hx, hy, _⟩ + rw [o.oangle_neg_right hx hy, h, Real.Angle.coe_pi_add_coe_pi] + · rintro ⟨hx, hy, h⟩ + rwa [o.oangle_neg_right hx hy, ← Real.Angle.sub_coe_pi_eq_add_coe_pi, sub_eq_zero] at h +#align orientation.oangle_eq_pi_iff_same_ray_neg Orientation.oangle_eq_pi_iff_sameRay_neg + +/-- The oriented angle between two vectors is zero or `π` if and only if those two vectors are +not linearly independent. -/ +theorem oangle_eq_zero_or_eq_pi_iff_not_linearIndependent {x y : V} : + o.oangle x y = 0 ∨ o.oangle x y = π ↔ ¬LinearIndependent ℝ ![x, y] := by + rw [oangle_eq_zero_iff_same_ray, oangle_eq_pi_iff_same_ray_neg, + sameRay_or_ne_zero_and_sameRay_neg_iff_not_linearIndependent] +#align orientation.oangle_eq_zero_or_eq_pi_iff_not_linear_independent Orientation.oangle_eq_zero_or_eq_pi_iff_not_linearIndependent + +/-- The oriented angle between two vectors is zero or `π` if and only if the first vector is zero +or the second is a multiple of the first. -/ +theorem oangle_eq_zero_or_eq_pi_iff_right_eq_smul {x y : V} : + o.oangle x y = 0 ∨ o.oangle x y = π ↔ x = 0 ∨ ∃ r : ℝ, y = r • x := + by + rw [oangle_eq_zero_iff_same_ray, oangle_eq_pi_iff_same_ray_neg] + refine' ⟨fun h => _, fun h => _⟩ + · rcases h with (h | ⟨-, -, h⟩) + · by_cases hx : x = 0; · simp [hx] + obtain ⟨r, -, rfl⟩ := h.exists_nonneg_left hx + exact Or.inr ⟨r, rfl⟩ + · by_cases hx : x = 0; · simp [hx] + obtain ⟨r, -, hy⟩ := h.exists_nonneg_left hx + refine' Or.inr ⟨-r, _⟩ + simp [hy] + · rcases h with (rfl | ⟨r, rfl⟩); · simp + by_cases hx : x = 0; · simp [hx] + rcases lt_trichotomy r 0 with (hr | hr | hr) + · rw [← neg_smul] + exact + Or.inr ⟨hx, smul_ne_zero hr.ne hx, SameRay.sameRay_pos_smul_right x (Left.neg_pos_iff.2 hr)⟩ + · simp [hr] + · exact Or.inl (SameRay.sameRay_pos_smul_right x hr) +#align orientation.oangle_eq_zero_or_eq_pi_iff_right_eq_smul Orientation.oangle_eq_zero_or_eq_pi_iff_right_eq_smul + +/-- The oriented angle between two vectors is not zero or `π` if and only if those two vectors +are linearly independent. -/ +theorem oangle_ne_zero_and_ne_pi_iff_linearIndependent {x y : V} : + o.oangle x y ≠ 0 ∧ o.oangle x y ≠ π ↔ LinearIndependent ℝ ![x, y] := by + rw [← not_or, ← not_iff_not, Classical.not_not, + oangle_eq_zero_or_eq_pi_iff_not_linear_independent] +#align orientation.oangle_ne_zero_and_ne_pi_iff_linear_independent Orientation.oangle_ne_zero_and_ne_pi_iff_linearIndependent + +/-- Two vectors are equal if and only if they have equal norms and zero angle between them. -/ +theorem eq_iff_norm_eq_and_oangle_eq_zero (x y : V) : x = y ↔ ‖x‖ = ‖y‖ ∧ o.oangle x y = 0 := + by + rw [oangle_eq_zero_iff_same_ray] + constructor + · rintro rfl + simp + · rcases eq_or_ne y 0 with (rfl | hy) + · simp + rintro ⟨h₁, h₂⟩ + obtain ⟨r, hr, rfl⟩ := h₂.exists_nonneg_right hy + have : ‖y‖ ≠ 0 := by simpa using hy + obtain rfl : r = 1 := by + apply mul_right_cancel₀ this + simpa [norm_smul, _root_.abs_of_nonneg hr] using h₁ + simp +#align orientation.eq_iff_norm_eq_and_oangle_eq_zero Orientation.eq_iff_norm_eq_and_oangle_eq_zero + +/-- Two vectors with equal norms are equal if and only if they have zero angle between them. -/ +theorem eq_iff_oangle_eq_zero_of_norm_eq {x y : V} (h : ‖x‖ = ‖y‖) : x = y ↔ o.oangle x y = 0 := + ⟨fun he => ((o.eq_iff_norm_eq_and_oangle_eq_zero x y).1 he).2, fun ha => + (o.eq_iff_norm_eq_and_oangle_eq_zero x y).2 ⟨h, ha⟩⟩ +#align orientation.eq_iff_oangle_eq_zero_of_norm_eq Orientation.eq_iff_oangle_eq_zero_of_norm_eq + +/-- Two vectors with zero angle between them are equal if and only if they have equal norms. -/ +theorem eq_iff_norm_eq_of_oangle_eq_zero {x y : V} (h : o.oangle x y = 0) : x = y ↔ ‖x‖ = ‖y‖ := + ⟨fun he => ((o.eq_iff_norm_eq_and_oangle_eq_zero x y).1 he).1, fun hn => + (o.eq_iff_norm_eq_and_oangle_eq_zero x y).2 ⟨hn, h⟩⟩ +#align orientation.eq_iff_norm_eq_of_oangle_eq_zero Orientation.eq_iff_norm_eq_of_oangle_eq_zero + +/-- Given three nonzero vectors, the angle between the first and the second plus the angle +between the second and the third equals the angle between the first and the third. -/ +@[simp] +theorem oangle_add {x y z : V} (hx : x ≠ 0) (hy : y ≠ 0) (hz : z ≠ 0) : + o.oangle x y + o.oangle y z = o.oangle x z := + by + simp_rw [oangle] + rw [← Complex.arg_mul_coe_angle, o.kahler_mul y x z] + congr 1 + convert Complex.arg_real_mul _ (_ : 0 < ‖y‖ ^ 2) using 2 + · norm_cast + · have : 0 < ‖y‖ := by simpa using hy + positivity + · exact o.kahler_ne_zero hx hy + · exact o.kahler_ne_zero hy hz +#align orientation.oangle_add Orientation.oangle_add + +/-- Given three nonzero vectors, the angle between the second and the third plus the angle +between the first and the second equals the angle between the first and the third. -/ +@[simp] +theorem oangle_add_swap {x y z : V} (hx : x ≠ 0) (hy : y ≠ 0) (hz : z ≠ 0) : + o.oangle y z + o.oangle x y = o.oangle x z := by rw [add_comm, o.oangle_add hx hy hz] +#align orientation.oangle_add_swap Orientation.oangle_add_swap + +/-- Given three nonzero vectors, the angle between the first and the third minus the angle +between the first and the second equals the angle between the second and the third. -/ +@[simp] +theorem oangle_sub_left {x y z : V} (hx : x ≠ 0) (hy : y ≠ 0) (hz : z ≠ 0) : + o.oangle x z - o.oangle x y = o.oangle y z := by + rw [sub_eq_iff_eq_add, o.oangle_add_swap hx hy hz] +#align orientation.oangle_sub_left Orientation.oangle_sub_left + +/-- Given three nonzero vectors, the angle between the first and the third minus the angle +between the second and the third equals the angle between the first and the second. -/ +@[simp] +theorem oangle_sub_right {x y z : V} (hx : x ≠ 0) (hy : y ≠ 0) (hz : z ≠ 0) : + o.oangle x z - o.oangle y z = o.oangle x y := by rw [sub_eq_iff_eq_add, o.oangle_add hx hy hz] +#align orientation.oangle_sub_right Orientation.oangle_sub_right + +/-- Given three nonzero vectors, adding the angles between them in cyclic order results in 0. -/ +@[simp] +theorem oangle_add_cyc3 {x y z : V} (hx : x ≠ 0) (hy : y ≠ 0) (hz : z ≠ 0) : + o.oangle x y + o.oangle y z + o.oangle z x = 0 := by simp [hx, hy, hz] +#align orientation.oangle_add_cyc3 Orientation.oangle_add_cyc3 + +/-- Given three nonzero vectors, adding the angles between them in cyclic order, with the first +vector in each angle negated, results in π. If the vectors add to 0, this is a version of the +sum of the angles of a triangle. -/ +@[simp] +theorem oangle_add_cyc3_neg_left {x y z : V} (hx : x ≠ 0) (hy : y ≠ 0) (hz : z ≠ 0) : + o.oangle (-x) y + o.oangle (-y) z + o.oangle (-z) x = π := by + rw [o.oangle_neg_left hx hy, o.oangle_neg_left hy hz, o.oangle_neg_left hz hx, + show + o.oangle x y + π + (o.oangle y z + π) + (o.oangle z x + π) = + o.oangle x y + o.oangle y z + o.oangle z x + (π + π + π : Real.Angle) + by abel, + o.oangle_add_cyc3 hx hy hz, Real.Angle.coe_pi_add_coe_pi, zero_add, zero_add] +#align orientation.oangle_add_cyc3_neg_left Orientation.oangle_add_cyc3_neg_left + +/-- Given three nonzero vectors, adding the angles between them in cyclic order, with the second +vector in each angle negated, results in π. If the vectors add to 0, this is a version of the +sum of the angles of a triangle. -/ +@[simp] +theorem oangle_add_cyc3_neg_right {x y z : V} (hx : x ≠ 0) (hy : y ≠ 0) (hz : z ≠ 0) : + o.oangle x (-y) + o.oangle y (-z) + o.oangle z (-x) = π := by + simp_rw [← oangle_neg_left_eq_neg_right, o.oangle_add_cyc3_neg_left hx hy hz] +#align orientation.oangle_add_cyc3_neg_right Orientation.oangle_add_cyc3_neg_right + +/-- Pons asinorum, oriented vector angle form. -/ +theorem oangle_sub_eq_oangle_sub_rev_of_norm_eq {x y : V} (h : ‖x‖ = ‖y‖) : + o.oangle x (x - y) = o.oangle (y - x) y := by simp [oangle, h] +#align orientation.oangle_sub_eq_oangle_sub_rev_of_norm_eq Orientation.oangle_sub_eq_oangle_sub_rev_of_norm_eq + +/- ./././Mathport/Syntax/Translate/Tactic/Lean3.lean:132:4: warning: unsupported: rw with cfg: { occs := occurrences.pos[occurrences.pos] «expr[ ,]»([1]) } -/ +/-- The angle at the apex of an isosceles triangle is `π` minus twice a base angle, oriented +vector angle form. -/ +theorem oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq {x y : V} (hn : x ≠ y) (h : ‖x‖ = ‖y‖) : + o.oangle y x = π - (2 : ℤ) • o.oangle (y - x) y := + by + rw [two_zsmul] + rw [← o.oangle_sub_eq_oangle_sub_rev_of_norm_eq h] + rw [eq_sub_iff_add_eq, ← oangle_neg_neg, ← add_assoc] + have hy : y ≠ 0 := by + rintro rfl + rw [norm_zero, norm_eq_zero] at h + exact hn h + have hx : x ≠ 0 := norm_ne_zero_iff.1 (h.symm ▸ norm_ne_zero_iff.2 hy) + convert o.oangle_add_cyc3_neg_right (neg_ne_zero.2 hy) hx (sub_ne_zero_of_ne hn.symm) <;> simp +#align orientation.oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq Orientation.oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq + +/-- The angle between two vectors, with respect to an orientation given by `orientation.map` +with a linear isometric equivalence, equals the angle between those two vectors, transformed by +the inverse of that equivalence, with respect to the original orientation. -/ +@[simp] +theorem oangle_map (x y : V') (f : V ≃ₗᵢ[ℝ] V') : + (Orientation.map (Fin 2) f.toLinearEquiv o).oangle x y = o.oangle (f.symm x) (f.symm y) := by + simp [oangle, o.kahler_map] +#align orientation.oangle_map Orientation.oangle_map + +@[simp] +protected theorem Complex.oangle (w z : ℂ) : + Complex.orientation.oangle w z = Complex.arg (conj w * z) := by simp [oangle] +#align complex.oangle Complex.oangle + +/-- The oriented angle on an oriented real inner product space of dimension 2 can be evaluated in +terms of a complex-number representation of the space. -/ +theorem oangle_map_complex (f : V ≃ₗᵢ[ℝ] ℂ) + (hf : Orientation.map (Fin 2) f.toLinearEquiv o = Complex.orientation) (x y : V) : + o.oangle x y = Complex.arg (conj (f x) * f y) := + by + rw [← Complex.oangle, ← hf, o.oangle_map] + simp +#align orientation.oangle_map_complex Orientation.oangle_map_complex + +/-- Negating the orientation negates the value of `oangle`. -/ +theorem oangle_neg_orientation_eq_neg (x y : V) : (-o).oangle x y = -o.oangle x y := by + simp [oangle] +#align orientation.oangle_neg_orientation_eq_neg Orientation.oangle_neg_orientation_eq_neg + +/-- The inner product of two vectors is the product of the norms and the cosine of the oriented +angle between the vectors. -/ +theorem inner_eq_norm_mul_norm_mul_cos_oangle (x y : V) : + ⟪x, y⟫ = ‖x‖ * ‖y‖ * Real.Angle.cos (o.oangle x y) := + by + by_cases hx : x = 0; · simp [hx] + by_cases hy : y = 0; · simp [hy] + have : ‖x‖ ≠ 0 := by simpa using hx + have : ‖y‖ ≠ 0 := by simpa using hy + rw [oangle, Real.Angle.cos_coe, Complex.cos_arg, o.abs_kahler] + · simp only [kahler_apply_apply, real_smul, add_re, of_real_re, mul_re, I_re, of_real_im] + field_simp + ring + · exact o.kahler_ne_zero hx hy +#align orientation.inner_eq_norm_mul_norm_mul_cos_oangle Orientation.inner_eq_norm_mul_norm_mul_cos_oangle + +/-- The cosine of the oriented angle between two nonzero vectors is the inner product divided by +the product of the norms. -/ +theorem cos_oangle_eq_inner_div_norm_mul_norm {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) : + Real.Angle.cos (o.oangle x y) = ⟪x, y⟫ / (‖x‖ * ‖y‖) := + by + rw [o.inner_eq_norm_mul_norm_mul_cos_oangle] + field_simp [norm_ne_zero_iff.2 hx, norm_ne_zero_iff.2 hy] + ring +#align orientation.cos_oangle_eq_inner_div_norm_mul_norm Orientation.cos_oangle_eq_inner_div_norm_mul_norm + +/-- The cosine of the oriented angle between two nonzero vectors equals that of the unoriented +angle. -/ +theorem cos_oangle_eq_cos_angle {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) : + Real.Angle.cos (o.oangle x y) = Real.cos (InnerProductGeometry.angle x y) := by + rw [o.cos_oangle_eq_inner_div_norm_mul_norm hx hy, InnerProductGeometry.cos_angle] +#align orientation.cos_oangle_eq_cos_angle Orientation.cos_oangle_eq_cos_angle + +/-- The oriented angle between two nonzero vectors is plus or minus the unoriented angle. -/ +theorem oangle_eq_angle_or_eq_neg_angle {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) : + o.oangle x y = InnerProductGeometry.angle x y ∨ + o.oangle x y = -InnerProductGeometry.angle x y := + Real.Angle.cos_eq_real_cos_iff_eq_or_eq_neg.1 <| o.cos_oangle_eq_cos_angle hx hy +#align orientation.oangle_eq_angle_or_eq_neg_angle Orientation.oangle_eq_angle_or_eq_neg_angle + +/-- The unoriented angle between two nonzero vectors is the absolute value of the oriented angle, +converted to a real. -/ +theorem angle_eq_abs_oangle_toReal {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) : + InnerProductGeometry.angle x y = |(o.oangle x y).toReal| := + by + have h0 := InnerProductGeometry.angle_nonneg x y + have hpi := InnerProductGeometry.angle_le_pi x y + rcases o.oangle_eq_angle_or_eq_neg_angle hx hy with (h | h) + · rw [h, eq_comm, Real.Angle.abs_toReal_coe_eq_self_iff] + exact ⟨h0, hpi⟩ + · rw [h, eq_comm, Real.Angle.abs_toReal_neg_coe_eq_self_iff] + exact ⟨h0, hpi⟩ +#align orientation.angle_eq_abs_oangle_to_real Orientation.angle_eq_abs_oangle_toReal + +/-- If the sign of the oriented angle between two vectors is zero, either one of the vectors is +zero or the unoriented angle is 0 or π. -/ +theorem eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero {x y : V} + (h : (o.oangle x y).sign = 0) : + x = 0 ∨ y = 0 ∨ InnerProductGeometry.angle x y = 0 ∨ InnerProductGeometry.angle x y = π := + by + by_cases hx : x = 0; · simp [hx] + by_cases hy : y = 0; · simp [hy] + rw [o.angle_eq_abs_oangle_to_real hx hy] + rw [Real.Angle.sign_eq_zero_iff] at h + rcases h with (h | h) <;> simp [h, real.pi_pos.le] +#align orientation.eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero Orientation.eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero + +/-- If two unoriented angles are equal, and the signs of the corresponding oriented angles are +equal, then the oriented angles are equal (even in degenerate cases). -/ +theorem oangle_eq_of_angle_eq_of_sign_eq {w x y z : V} + (h : InnerProductGeometry.angle w x = InnerProductGeometry.angle y z) + (hs : (o.oangle w x).sign = (o.oangle y z).sign) : o.oangle w x = o.oangle y z := + by + by_cases h0 : (w = 0 ∨ x = 0) ∨ y = 0 ∨ z = 0 + · have hs' : (o.oangle w x).sign = 0 ∧ (o.oangle y z).sign = 0 := + by + rcases h0 with ((rfl | rfl) | rfl | rfl) + · simpa using hs.symm + · simpa using hs.symm + · simpa using hs + · simpa using hs + rcases hs' with ⟨hswx, hsyz⟩ + have h' : InnerProductGeometry.angle w x = π / 2 ∧ InnerProductGeometry.angle y z = π / 2 := + by + rcases h0 with ((rfl | rfl) | rfl | rfl) + · simpa using h.symm + · simpa using h.symm + · simpa using h + · simpa using h + rcases h' with ⟨hwx, hyz⟩ + have hpi : π / 2 ≠ π := by + intro hpi + rw [div_eq_iff, eq_comm, ← sub_eq_zero, mul_two, add_sub_cancel] at hpi + · exact real.pi_pos.ne.symm hpi + · exact two_ne_zero + have h0wx : w = 0 ∨ x = 0 := + by + have h0' := o.eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero hswx + simpa [hwx, real.pi_pos.ne.symm, hpi] using h0' + have h0yz : y = 0 ∨ z = 0 := + by + have h0' := o.eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero hsyz + simpa [hyz, real.pi_pos.ne.symm, hpi] using h0' + rcases h0wx with (h0wx | h0wx) <;> rcases h0yz with (h0yz | h0yz) <;> simp [h0wx, h0yz] + · push_neg at h0 + rw [Real.Angle.eq_iff_abs_toReal_eq_of_sign_eq hs] + rwa [o.angle_eq_abs_oangle_to_real h0.1.1 h0.1.2, + o.angle_eq_abs_oangle_to_real h0.2.1 h0.2.2] at h +#align orientation.oangle_eq_of_angle_eq_of_sign_eq Orientation.oangle_eq_of_angle_eq_of_sign_eq + +/-- If the signs of two oriented angles between nonzero vectors are equal, the oriented angles are +equal if and only if the unoriented angles are equal. -/ +theorem angle_eq_iff_oangle_eq_of_sign_eq {w x y z : V} (hw : w ≠ 0) (hx : x ≠ 0) (hy : y ≠ 0) + (hz : z ≠ 0) (hs : (o.oangle w x).sign = (o.oangle y z).sign) : + InnerProductGeometry.angle w x = InnerProductGeometry.angle y z ↔ o.oangle w x = o.oangle y z := + by + refine' ⟨fun h => o.oangle_eq_of_angle_eq_of_sign_eq h hs, fun h => _⟩ + rw [o.angle_eq_abs_oangle_to_real hw hx, o.angle_eq_abs_oangle_to_real hy hz, h] +#align orientation.angle_eq_iff_oangle_eq_of_sign_eq Orientation.angle_eq_iff_oangle_eq_of_sign_eq + +/-- The oriented angle between two vectors equals the unoriented angle if the sign is positive. -/ +theorem oangle_eq_angle_of_sign_eq_one {x y : V} (h : (o.oangle x y).sign = 1) : + o.oangle x y = InnerProductGeometry.angle x y := + by + by_cases hx : x = 0; · exfalso; simpa [hx] using h + by_cases hy : y = 0; · exfalso; simpa [hy] using h + refine' (o.oangle_eq_angle_or_eq_neg_angle hx hy).resolve_right _ + intro hxy + rw [hxy, Real.Angle.sign_neg, neg_eq_iff_eq_neg, ← SignType.neg_iff, ← not_le] at h + exact + h + (Real.Angle.sign_coe_nonneg_of_nonneg_of_le_pi (InnerProductGeometry.angle_nonneg _ _) + (InnerProductGeometry.angle_le_pi _ _)) +#align orientation.oangle_eq_angle_of_sign_eq_one Orientation.oangle_eq_angle_of_sign_eq_one + +/-- The oriented angle between two vectors equals minus the unoriented angle if the sign is +negative. -/ +theorem oangle_eq_neg_angle_of_sign_eq_neg_one {x y : V} (h : (o.oangle x y).sign = -1) : + o.oangle x y = -InnerProductGeometry.angle x y := + by + by_cases hx : x = 0; · exfalso; simpa [hx] using h + by_cases hy : y = 0; · exfalso; simpa [hy] using h + refine' (o.oangle_eq_angle_or_eq_neg_angle hx hy).resolve_left _ + intro hxy + rw [hxy, ← SignType.neg_iff, ← not_le] at h + exact + h + (Real.Angle.sign_coe_nonneg_of_nonneg_of_le_pi (InnerProductGeometry.angle_nonneg _ _) + (InnerProductGeometry.angle_le_pi _ _)) +#align orientation.oangle_eq_neg_angle_of_sign_eq_neg_one Orientation.oangle_eq_neg_angle_of_sign_eq_neg_one + +/-- The oriented angle between two nonzero vectors is zero if and only if the unoriented angle +is zero. -/ +theorem oangle_eq_zero_iff_angle_eq_zero {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) : + o.oangle x y = 0 ↔ InnerProductGeometry.angle x y = 0 := + by + refine' ⟨fun h => _, fun h => _⟩ + · simpa [o.angle_eq_abs_oangle_to_real hx hy] + · have ha := o.oangle_eq_angle_or_eq_neg_angle hx hy + rw [h] at ha + simpa using ha +#align orientation.oangle_eq_zero_iff_angle_eq_zero Orientation.oangle_eq_zero_iff_angle_eq_zero + +/-- The oriented angle between two vectors is `π` if and only if the unoriented angle is `π`. -/ +theorem oangle_eq_pi_iff_angle_eq_pi {x y : V} : + o.oangle x y = π ↔ InnerProductGeometry.angle x y = π := + by + by_cases hx : x = 0; + · simp [hx, real.angle.pi_ne_zero.symm, div_eq_mul_inv, mul_right_eq_self₀, not_or, + Real.pi_ne_zero] + norm_num + by_cases hy : y = 0; + · simp [hy, real.angle.pi_ne_zero.symm, div_eq_mul_inv, mul_right_eq_self₀, not_or, + Real.pi_ne_zero] + norm_num + refine' ⟨fun h => _, fun h => _⟩ + · rw [o.angle_eq_abs_oangle_to_real hx hy, h] + simp [real.pi_pos.le] + · have ha := o.oangle_eq_angle_or_eq_neg_angle hx hy + rw [h] at ha + simpa using ha +#align orientation.oangle_eq_pi_iff_angle_eq_pi Orientation.oangle_eq_pi_iff_angle_eq_pi + +/-- One of two vectors is zero or the oriented angle between them is plus or minus `π / 2` if +and only if the inner product of those vectors is zero. -/ +theorem eq_zero_or_oangle_eq_iff_inner_eq_zero {x y : V} : + x = 0 ∨ y = 0 ∨ o.oangle x y = (π / 2 : ℝ) ∨ o.oangle x y = (-π / 2 : ℝ) ↔ ⟪x, y⟫ = 0 := + by + by_cases hx : x = 0; · simp [hx] + by_cases hy : y = 0; · simp [hy] + rw [InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two, or_iff_right hx, or_iff_right hy] + refine' ⟨fun h => _, fun h => _⟩ + · rwa [o.angle_eq_abs_oangle_to_real hx hy, Real.Angle.abs_toReal_eq_pi_div_two_iff] + · convert o.oangle_eq_angle_or_eq_neg_angle hx hy <;> rw [h] + exact neg_div _ _ +#align orientation.eq_zero_or_oangle_eq_iff_inner_eq_zero Orientation.eq_zero_or_oangle_eq_iff_inner_eq_zero + +/-- If the oriented angle between two vectors is `π / 2`, the inner product of those vectors +is zero. -/ +theorem inner_eq_zero_of_oangle_eq_pi_div_two {x y : V} (h : o.oangle x y = (π / 2 : ℝ)) : + ⟪x, y⟫ = 0 := + o.eq_zero_or_oangle_eq_iff_inner_eq_zero.1 <| Or.inr <| Or.inr <| Or.inl h +#align orientation.inner_eq_zero_of_oangle_eq_pi_div_two Orientation.inner_eq_zero_of_oangle_eq_pi_div_two + +/-- If the oriented angle between two vectors is `π / 2`, the inner product of those vectors +(reversed) is zero. -/ +theorem inner_rev_eq_zero_of_oangle_eq_pi_div_two {x y : V} (h : o.oangle x y = (π / 2 : ℝ)) : + ⟪y, x⟫ = 0 := by rw [real_inner_comm, o.inner_eq_zero_of_oangle_eq_pi_div_two h] +#align orientation.inner_rev_eq_zero_of_oangle_eq_pi_div_two Orientation.inner_rev_eq_zero_of_oangle_eq_pi_div_two + +/-- If the oriented angle between two vectors is `-π / 2`, the inner product of those vectors +is zero. -/ +theorem inner_eq_zero_of_oangle_eq_neg_pi_div_two {x y : V} (h : o.oangle x y = (-π / 2 : ℝ)) : + ⟪x, y⟫ = 0 := + o.eq_zero_or_oangle_eq_iff_inner_eq_zero.1 <| Or.inr <| Or.inr <| Or.inr h +#align orientation.inner_eq_zero_of_oangle_eq_neg_pi_div_two Orientation.inner_eq_zero_of_oangle_eq_neg_pi_div_two + +/-- If the oriented angle between two vectors is `-π / 2`, the inner product of those vectors +(reversed) is zero. -/ +theorem inner_rev_eq_zero_of_oangle_eq_neg_pi_div_two {x y : V} (h : o.oangle x y = (-π / 2 : ℝ)) : + ⟪y, x⟫ = 0 := by rw [real_inner_comm, o.inner_eq_zero_of_oangle_eq_neg_pi_div_two h] +#align orientation.inner_rev_eq_zero_of_oangle_eq_neg_pi_div_two Orientation.inner_rev_eq_zero_of_oangle_eq_neg_pi_div_two + +/-- Negating the first vector passed to `oangle` negates the sign of the angle. -/ +@[simp] +theorem oangle_sign_neg_left (x y : V) : (o.oangle (-x) y).sign = -(o.oangle x y).sign := + by + by_cases hx : x = 0; · simp [hx] + by_cases hy : y = 0; · simp [hy] + rw [o.oangle_neg_left hx hy, Real.Angle.sign_add_pi] +#align orientation.oangle_sign_neg_left Orientation.oangle_sign_neg_left + +/-- Negating the second vector passed to `oangle` negates the sign of the angle. -/ +@[simp] +theorem oangle_sign_neg_right (x y : V) : (o.oangle x (-y)).sign = -(o.oangle x y).sign := + by + by_cases hx : x = 0; · simp [hx] + by_cases hy : y = 0; · simp [hy] + rw [o.oangle_neg_right hx hy, Real.Angle.sign_add_pi] +#align orientation.oangle_sign_neg_right Orientation.oangle_sign_neg_right + +/-- Multiplying the first vector passed to `oangle` by a real multiplies the sign of the angle by +the sign of the real. -/ +@[simp] +theorem oangle_sign_smul_left (x y : V) (r : ℝ) : + (o.oangle (r • x) y).sign = SignType.sign r * (o.oangle x y).sign := by + rcases lt_trichotomy r 0 with (h | h | h) <;> simp [h] +#align orientation.oangle_sign_smul_left Orientation.oangle_sign_smul_left + +/-- Multiplying the second vector passed to `oangle` by a real multiplies the sign of the angle by +the sign of the real. -/ +@[simp] +theorem oangle_sign_smul_right (x y : V) (r : ℝ) : + (o.oangle x (r • y)).sign = SignType.sign r * (o.oangle x y).sign := by + rcases lt_trichotomy r 0 with (h | h | h) <;> simp [h] +#align orientation.oangle_sign_smul_right Orientation.oangle_sign_smul_right + +/-- Auxiliary lemma for the proof of `oangle_sign_smul_add_right`; not intended to be used +outside of that proof. -/ +theorem oangle_smul_add_right_eq_zero_or_eq_pi_iff {x y : V} (r : ℝ) : + o.oangle x (r • x + y) = 0 ∨ o.oangle x (r • x + y) = π ↔ o.oangle x y = 0 ∨ o.oangle x y = π := + by + simp_rw [oangle_eq_zero_or_eq_pi_iff_not_linear_independent, Fintype.not_linearIndependent_iff, + Fin.sum_univ_two, Fin.exists_fin_two] + refine' ⟨fun h => _, fun h => _⟩ + · rcases h with ⟨m, h, hm⟩ + change m 0 • x + m 1 • (r • x + y) = 0 at h + refine' ⟨![m 0 + m 1 * r, m 1], _⟩ + change (m 0 + m 1 * r) • x + m 1 • y = 0 ∧ (m 0 + m 1 * r ≠ 0 ∨ m 1 ≠ 0) + rw [smul_add, smul_smul, ← add_assoc, ← add_smul] at h + refine' ⟨h, not_and_or.1 fun h0 => _⟩ + obtain ⟨h0, h1⟩ := h0 + rw [h1] at h0 hm + rw [MulZeroClass.zero_mul, add_zero] at h0 + simpa [h0] using hm + · rcases h with ⟨m, h, hm⟩ + change m 0 • x + m 1 • y = 0 at h + refine' ⟨![m 0 - m 1 * r, m 1], _⟩ + change (m 0 - m 1 * r) • x + m 1 • (r • x + y) = 0 ∧ (m 0 - m 1 * r ≠ 0 ∨ m 1 ≠ 0) + rw [sub_smul, smul_add, smul_smul, ← add_assoc, sub_add_cancel] + refine' ⟨h, not_and_or.1 fun h0 => _⟩ + obtain ⟨h0, h1⟩ := h0 + rw [h1] at h0 hm + rw [MulZeroClass.zero_mul, sub_zero] at h0 + simpa [h0] using hm +#align orientation.oangle_smul_add_right_eq_zero_or_eq_pi_iff Orientation.oangle_smul_add_right_eq_zero_or_eq_pi_iff + +/-- Adding a multiple of the first vector passed to `oangle` to the second vector does not change +the sign of the angle. -/ +@[simp] +theorem oangle_sign_smul_add_right (x y : V) (r : ℝ) : + (o.oangle x (r • x + y)).sign = (o.oangle x y).sign := + by + by_cases h : o.oangle x y = 0 ∨ o.oangle x y = π + · + rwa [Real.Angle.sign_eq_zero_iff.2 h, Real.Angle.sign_eq_zero_iff, + oangle_smul_add_right_eq_zero_or_eq_pi_iff] + have h' : ∀ r' : ℝ, o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ π := + by + intro r' + rwa [← o.oangle_smul_add_right_eq_zero_or_eq_pi_iff r', not_or] at h + let s : Set (V × V) := (fun r' : ℝ => (x, r' • x + y)) '' Set.univ + have hc : IsConnected s := + is_connected_univ.image _ + (continuous_const.prod_mk + ((continuous_id.smul continuous_const).add continuous_const)).ContinuousOn + have hf : ContinuousOn (fun z : V × V => o.oangle z.1 z.2) s := + by + refine' ContinuousAt.continuousOn fun z hz => o.continuous_at_oangle _ _ + all_goals + simp_rw [s, Set.mem_image] at hz + obtain ⟨r', -, rfl⟩ := hz + simp only [Prod.fst, Prod.snd] + intro hz + · simpa [hz] using (h' 0).1 + · simpa [hz] using (h' r').1 + have hs : ∀ z : V × V, z ∈ s → o.oangle z.1 z.2 ≠ 0 ∧ o.oangle z.1 z.2 ≠ π := + by + intro z hz + simp_rw [s, Set.mem_image] at hz + obtain ⟨r', -, rfl⟩ := hz + exact h' r' + have hx : (x, y) ∈ s := + by + convert Set.mem_image_of_mem (fun r' : ℝ => (x, r' • x + y)) (Set.mem_univ 0) + simp + have hy : (x, r • x + y) ∈ s := Set.mem_image_of_mem _ (Set.mem_univ _) + convert Real.Angle.sign_eq_of_continuousOn hc hf hs hx hy +#align orientation.oangle_sign_smul_add_right Orientation.oangle_sign_smul_add_right + +/-- Adding a multiple of the second vector passed to `oangle` to the first vector does not change +the sign of the angle. -/ +@[simp] +theorem oangle_sign_add_smul_left (x y : V) (r : ℝ) : + (o.oangle (x + r • y) y).sign = (o.oangle x y).sign := by + simp_rw [o.oangle_rev y, Real.Angle.sign_neg, add_comm x, oangle_sign_smul_add_right] +#align orientation.oangle_sign_add_smul_left Orientation.oangle_sign_add_smul_left + +/-- Subtracting a multiple of the first vector passed to `oangle` from the second vector does +not change the sign of the angle. -/ +@[simp] +theorem oangle_sign_sub_smul_right (x y : V) (r : ℝ) : + (o.oangle x (y - r • x)).sign = (o.oangle x y).sign := by + rw [sub_eq_add_neg, ← neg_smul, add_comm, oangle_sign_smul_add_right] +#align orientation.oangle_sign_sub_smul_right Orientation.oangle_sign_sub_smul_right + +/-- Subtracting a multiple of the second vector passed to `oangle` from the first vector does +not change the sign of the angle. -/ +@[simp] +theorem oangle_sign_sub_smul_left (x y : V) (r : ℝ) : + (o.oangle (x - r • y) y).sign = (o.oangle x y).sign := by + rw [sub_eq_add_neg, ← neg_smul, oangle_sign_add_smul_left] +#align orientation.oangle_sign_sub_smul_left Orientation.oangle_sign_sub_smul_left + +/-- Adding the first vector passed to `oangle` to the second vector does not change the sign of +the angle. -/ +@[simp] +theorem oangle_sign_add_right (x y : V) : (o.oangle x (x + y)).sign = (o.oangle x y).sign := by + rw [← o.oangle_sign_smul_add_right x y 1, one_smul] +#align orientation.oangle_sign_add_right Orientation.oangle_sign_add_right + +/-- Adding the second vector passed to `oangle` to the first vector does not change the sign of +the angle. -/ +@[simp] +theorem oangle_sign_add_left (x y : V) : (o.oangle (x + y) y).sign = (o.oangle x y).sign := by + rw [← o.oangle_sign_add_smul_left x y 1, one_smul] +#align orientation.oangle_sign_add_left Orientation.oangle_sign_add_left + +/-- Subtracting the first vector passed to `oangle` from the second vector does not change the +sign of the angle. -/ +@[simp] +theorem oangle_sign_sub_right (x y : V) : (o.oangle x (y - x)).sign = (o.oangle x y).sign := by + rw [← o.oangle_sign_sub_smul_right x y 1, one_smul] +#align orientation.oangle_sign_sub_right Orientation.oangle_sign_sub_right + +/-- Subtracting the second vector passed to `oangle` from the first vector does not change the +sign of the angle. -/ +@[simp] +theorem oangle_sign_sub_left (x y : V) : (o.oangle (x - y) y).sign = (o.oangle x y).sign := by + rw [← o.oangle_sign_sub_smul_left x y 1, one_smul] +#align orientation.oangle_sign_sub_left Orientation.oangle_sign_sub_left + +/-- Subtracting the second vector passed to `oangle` from a multiple of the first vector negates +the sign of the angle. -/ +@[simp] +theorem oangle_sign_smul_sub_right (x y : V) (r : ℝ) : + (o.oangle x (r • x - y)).sign = -(o.oangle x y).sign := by + rw [← oangle_sign_neg_right, sub_eq_add_neg, oangle_sign_smul_add_right] +#align orientation.oangle_sign_smul_sub_right Orientation.oangle_sign_smul_sub_right + +/-- Subtracting the first vector passed to `oangle` from a multiple of the second vector negates +the sign of the angle. -/ +@[simp] +theorem oangle_sign_smul_sub_left (x y : V) (r : ℝ) : + (o.oangle (r • y - x) y).sign = -(o.oangle x y).sign := by + rw [← oangle_sign_neg_left, sub_eq_neg_add, oangle_sign_add_smul_left] +#align orientation.oangle_sign_smul_sub_left Orientation.oangle_sign_smul_sub_left + +/-- Subtracting the second vector passed to `oangle` from the first vector negates the sign of +the angle. -/ +theorem oangle_sign_sub_right_eq_neg (x y : V) : (o.oangle x (x - y)).sign = -(o.oangle x y).sign := + by rw [← o.oangle_sign_smul_sub_right x y 1, one_smul] +#align orientation.oangle_sign_sub_right_eq_neg Orientation.oangle_sign_sub_right_eq_neg + +/-- Subtracting the first vector passed to `oangle` from the second vector negates the sign of +the angle. -/ +theorem oangle_sign_sub_left_eq_neg (x y : V) : (o.oangle (y - x) y).sign = -(o.oangle x y).sign := + by rw [← o.oangle_sign_smul_sub_left x y 1, one_smul] +#align orientation.oangle_sign_sub_left_eq_neg Orientation.oangle_sign_sub_left_eq_neg + +/-- Subtracting the first vector passed to `oangle` from the second vector then swapping the +vectors does not change the sign of the angle. -/ +@[simp] +theorem oangle_sign_sub_right_swap (x y : V) : (o.oangle y (y - x)).sign = (o.oangle x y).sign := by + rw [oangle_sign_sub_right_eq_neg, o.oangle_rev y x, Real.Angle.sign_neg] +#align orientation.oangle_sign_sub_right_swap Orientation.oangle_sign_sub_right_swap + +/-- Subtracting the second vector passed to `oangle` from the first vector then swapping the +vectors does not change the sign of the angle. -/ +@[simp] +theorem oangle_sign_sub_left_swap (x y : V) : (o.oangle (x - y) x).sign = (o.oangle x y).sign := by + rw [oangle_sign_sub_left_eq_neg, o.oangle_rev y x, Real.Angle.sign_neg] +#align orientation.oangle_sign_sub_left_swap Orientation.oangle_sign_sub_left_swap + +/-- The sign of the angle between a vector, and a linear combination of that vector with a second +vector, is the sign of the factor by which the second vector is multiplied in that combination +multiplied by the sign of the angle between the two vectors. -/ +@[simp] +theorem oangle_sign_smul_add_smul_right (x y : V) (r₁ r₂ : ℝ) : + (o.oangle x (r₁ • x + r₂ • y)).sign = SignType.sign r₂ * (o.oangle x y).sign := + by + rw [← o.oangle_sign_smul_add_right x (r₁ • x + r₂ • y) (-r₁)] + simp +#align orientation.oangle_sign_smul_add_smul_right Orientation.oangle_sign_smul_add_smul_right + +/-- The sign of the angle between a linear combination of two vectors and the second vector is +the sign of the factor by which the first vector is multiplied in that combination multiplied by +the sign of the angle between the two vectors. -/ +@[simp] +theorem oangle_sign_smul_add_smul_left (x y : V) (r₁ r₂ : ℝ) : + (o.oangle (r₁ • x + r₂ • y) y).sign = SignType.sign r₁ * (o.oangle x y).sign := by + simp_rw [o.oangle_rev y, Real.Angle.sign_neg, add_comm (r₁ • x), oangle_sign_smul_add_smul_right, + mul_neg] +#align orientation.oangle_sign_smul_add_smul_left Orientation.oangle_sign_smul_add_smul_left + +/-- The sign of the angle between two linear combinations of two vectors is the sign of the +determinant of the factors in those combinations multiplied by the sign of the angle between the +two vectors. -/ +theorem oangle_sign_smul_add_smul_smul_add_smul (x y : V) (r₁ r₂ r₃ r₄ : ℝ) : + (o.oangle (r₁ • x + r₂ • y) (r₃ • x + r₄ • y)).sign = + SignType.sign (r₁ * r₄ - r₂ * r₃) * (o.oangle x y).sign := + by + by_cases hr₁ : r₁ = 0 + · + rw [hr₁, zero_smul, MulZeroClass.zero_mul, zero_add, zero_sub, Left.sign_neg, + oangle_sign_smul_left, add_comm, oangle_sign_smul_add_smul_right, oangle_rev, + Real.Angle.sign_neg, sign_mul, mul_neg, mul_neg, neg_mul, mul_assoc] + · + rw [← o.oangle_sign_smul_add_right (r₁ • x + r₂ • y) (r₃ • x + r₄ • y) (-r₃ / r₁), smul_add, + smul_smul, smul_smul, div_mul_cancel _ hr₁, neg_smul, ← add_assoc, add_comm (-(r₃ • x)), ← + sub_eq_add_neg, sub_add_cancel, ← add_smul, oangle_sign_smul_right, + oangle_sign_smul_add_smul_left, ← mul_assoc, ← sign_mul, add_mul, mul_assoc, mul_comm r₂ r₁, ← + mul_assoc, div_mul_cancel _ hr₁, add_comm, neg_mul, ← sub_eq_add_neg, mul_comm r₄, + mul_comm r₃] +#align orientation.oangle_sign_smul_add_smul_smul_add_smul Orientation.oangle_sign_smul_add_smul_smul_add_smul + +/-- A base angle of an isosceles triangle is acute, oriented vector angle form. -/ +theorem abs_oangle_sub_left_toReal_lt_pi_div_two {x y : V} (h : ‖x‖ = ‖y‖) : + |(o.oangle (y - x) y).toReal| < π / 2 := + by + by_cases hn : x = y; · simp [hn, div_pos, Real.pi_pos] + have hs : ((2 : ℤ) • o.oangle (y - x) y).sign = (o.oangle (y - x) y).sign := + by + conv_rhs => rw [oangle_sign_sub_left_swap] + rw [o.oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq hn h, Real.Angle.sign_pi_sub] + rw [Real.Angle.sign_two_zsmul_eq_sign_iff] at hs + rcases hs with (hs | hs) + · rw [oangle_eq_pi_iff_oangle_rev_eq_pi, oangle_eq_pi_iff_same_ray_neg, neg_sub] at hs + rcases hs with ⟨hy, -, hr⟩ + rw [← exists_nonneg_left_iff_sameRay hy] at hr + rcases hr with ⟨r, hr0, hr⟩ + rw [eq_sub_iff_add_eq] at hr + nth_rw 2 [← one_smul ℝ y] at hr + rw [← add_smul] at hr + rw [← hr, norm_smul, Real.norm_eq_abs, abs_of_pos (Left.add_pos_of_nonneg_of_pos hr0 one_pos), + mul_left_eq_self₀, or_iff_left (norm_ne_zero_iff.2 hy), add_left_eq_self] at h + rw [h, zero_add, one_smul] at hr + exact False.elim (hn hr.symm) + · exact hs +#align orientation.abs_oangle_sub_left_to_real_lt_pi_div_two Orientation.abs_oangle_sub_left_toReal_lt_pi_div_two + +/-- A base angle of an isosceles triangle is acute, oriented vector angle form. -/ +theorem abs_oangle_sub_right_toReal_lt_pi_div_two {x y : V} (h : ‖x‖ = ‖y‖) : + |(o.oangle x (x - y)).toReal| < π / 2 := + (o.oangle_sub_eq_oangle_sub_rev_of_norm_eq h).symm ▸ o.abs_oangle_sub_left_toReal_lt_pi_div_two h +#align orientation.abs_oangle_sub_right_to_real_lt_pi_div_two Orientation.abs_oangle_sub_right_toReal_lt_pi_div_two + +end Orientation + From 29f4e102ec91f063178e24b6a7a094a2e80fedbe Mon Sep 17 00:00:00 2001 From: Parcly Taxel Date: Sun, 11 Jun 2023 17:25:05 +0800 Subject: [PATCH 3/5] automated fixes Mathbin -> Mathlib fix certain import statements move "by" to end of line add import to Mathlib.lean --- Mathlib.lean | 1 + .../Euclidean/Angle/Oriented/Basic.lean | 121 ++++++------------ 2 files changed, 42 insertions(+), 80 deletions(-) diff --git a/Mathlib.lean b/Mathlib.lean index d2e258e60e569..003c52876beb5 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -1716,6 +1716,7 @@ import Mathlib.FieldTheory.SeparableDegree import Mathlib.FieldTheory.SplittingField.IsSplittingField import Mathlib.FieldTheory.Subfield import Mathlib.FieldTheory.Tower +import Mathlib.Geometry.Euclidean.Angle.Oriented.Basic import Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine import Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic import Mathlib.Geometry.Euclidean.Angle.Unoriented.Conformal diff --git a/Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean b/Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean index bf588bf8a7579..fb18fee4e2f50 100644 --- a/Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean +++ b/Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean @@ -8,8 +8,8 @@ Authors: Joseph Myers, Heather Macbeth ! Please do not edit these lines, except to modify the commit id ! if you have ported upstream changes. -/ -import Mathbin.Analysis.InnerProductSpace.TwoDim -import Mathbin.Geometry.Euclidean.Angle.Unoriented.Basic +import Mathlib.Analysis.InnerProductSpace.TwoDim +import Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic /-! # Oriented angles. @@ -65,8 +65,7 @@ def oangle (x y : V) : Real.Angle := /-- Oriented angles are continuous when the vectors involved are nonzero. -/ theorem continuousAt_oangle {x : V × V} (hx1 : x.1 ≠ 0) (hx2 : x.2 ≠ 0) : - ContinuousAt (fun y : V × V => o.oangle y.1 y.2) x := - by + ContinuousAt (fun y : V × V => o.oangle y.1 y.2) x := by refine' (Complex.continuousAt_arg_coe_angle _).comp _ · exact o.kahler_ne_zero hx1 hx2 exact @@ -86,8 +85,7 @@ theorem oangle_zero_right (x : V) : o.oangle x 0 = 0 := by simp [oangle] /-- If the two vectors passed to `oangle` are the same, the result is 0. -/ @[simp] -theorem oangle_self (x : V) : o.oangle x x = 0 := - by +theorem oangle_self (x : V) : o.oangle x x = 0 := by simp only [oangle, kahler_apply_self, ← Complex.ofReal_pow] convert QuotientAddGroup.mk_zero _ apply arg_of_real_of_nonneg @@ -330,8 +328,7 @@ theorem oangle_smul_right_of_neg (x y : V) {r : ℝ} (hr : r < 0) : /-- The angle between a nonnegative multiple of a vector and that vector is 0. -/ @[simp] -theorem oangle_smul_left_self_of_nonneg (x : V) {r : ℝ} (hr : 0 ≤ r) : o.oangle (r • x) x = 0 := - by +theorem oangle_smul_left_self_of_nonneg (x : V) {r : ℝ} (hr : 0 ≤ r) : o.oangle (r • x) x = 0 := by rcases hr.lt_or_eq with (h | h) · simp [h] · simp [h.symm] @@ -339,8 +336,7 @@ theorem oangle_smul_left_self_of_nonneg (x : V) {r : ℝ} (hr : 0 ≤ r) : o.oan /-- The angle between a vector and a nonnegative multiple of that vector is 0. -/ @[simp] -theorem oangle_smul_right_self_of_nonneg (x : V) {r : ℝ} (hr : 0 ≤ r) : o.oangle x (r • x) = 0 := - by +theorem oangle_smul_right_self_of_nonneg (x : V) {r : ℝ} (hr : 0 ≤ r) : o.oangle x (r • x) = 0 := by rcases hr.lt_or_eq with (h | h) · simp [h] · simp [h.symm] @@ -349,8 +345,7 @@ theorem oangle_smul_right_self_of_nonneg (x : V) {r : ℝ} (hr : 0 ≤ r) : o.oa /-- The angle between two nonnegative multiples of the same vector is 0. -/ @[simp] theorem oangle_smul_smul_self_of_nonneg (x : V) {r₁ r₂ : ℝ} (hr₁ : 0 ≤ r₁) (hr₂ : 0 ≤ r₂) : - o.oangle (r₁ • x) (r₂ • x) = 0 := - by + o.oangle (r₁ • x) (r₂ • x) = 0 := by rcases hr₁.lt_or_eq with (h | h) · simp [h, hr₂] · simp [h.symm] @@ -393,8 +388,7 @@ theorem two_zsmul_oangle_smul_smul_self (x : V) {r₁ r₂ : ℝ} : /-- If the spans of two vectors are equal, twice angles with those vectors on the left are equal. -/ theorem two_zsmul_oangle_left_of_span_eq {x y : V} (z : V) (h : (ℝ ∙ x) = ℝ ∙ y) : - (2 : ℤ) • o.oangle x z = (2 : ℤ) • o.oangle y z := - by + (2 : ℤ) • o.oangle x z = (2 : ℤ) • o.oangle y z := by rw [Submodule.span_singleton_eq_span_singleton] at h rcases h with ⟨r, rfl⟩ exact (o.two_zsmul_oangle_smul_left_of_ne_zero _ _ (Units.ne_zero _)).symm @@ -403,8 +397,7 @@ theorem two_zsmul_oangle_left_of_span_eq {x y : V} (z : V) (h : (ℝ ∙ x) = /-- If the spans of two vectors are equal, twice angles with those vectors on the right are equal. -/ theorem two_zsmul_oangle_right_of_span_eq (x : V) {y z : V} (h : (ℝ ∙ y) = ℝ ∙ z) : - (2 : ℤ) • o.oangle x y = (2 : ℤ) • o.oangle x z := - by + (2 : ℤ) • o.oangle x y = (2 : ℤ) • o.oangle x z := by rw [Submodule.span_singleton_eq_span_singleton] at h rcases h with ⟨r, rfl⟩ exact (o.two_zsmul_oangle_smul_right_of_ne_zero _ _ (Units.ne_zero _)).symm @@ -424,8 +417,7 @@ theorem oangle_eq_zero_iff_oangle_rev_eq_zero {x y : V} : o.oangle x y = 0 ↔ o #align orientation.oangle_eq_zero_iff_oangle_rev_eq_zero Orientation.oangle_eq_zero_iff_oangle_rev_eq_zero /-- The oriented angle between two vectors is zero if and only if they are on the same ray. -/ -theorem oangle_eq_zero_iff_sameRay {x y : V} : o.oangle x y = 0 ↔ SameRay ℝ x y := - by +theorem oangle_eq_zero_iff_sameRay {x y : V} : o.oangle x y = 0 ↔ SameRay ℝ x y := by rw [oangle, kahler_apply_apply, Complex.arg_coe_angle_eq_iff_eq_toReal, Real.Angle.toReal_zero, Complex.arg_eq_zero_iff] simpa using o.nonneg_inner_and_area_form_eq_zero_iff_same_ray x y @@ -440,8 +432,7 @@ theorem oangle_eq_pi_iff_oangle_rev_eq_pi {x y : V} : o.oangle x y = π ↔ o.oa /-- The oriented angle between two vectors is `π` if and only they are nonzero and the first is on the same ray as the negation of the second. -/ theorem oangle_eq_pi_iff_sameRay_neg {x y : V} : - o.oangle x y = π ↔ x ≠ 0 ∧ y ≠ 0 ∧ SameRay ℝ x (-y) := - by + o.oangle x y = π ↔ x ≠ 0 ∧ y ≠ 0 ∧ SameRay ℝ x (-y) := by rw [← o.oangle_eq_zero_iff_same_ray] constructor · intro h @@ -464,8 +455,7 @@ theorem oangle_eq_zero_or_eq_pi_iff_not_linearIndependent {x y : V} : /-- The oriented angle between two vectors is zero or `π` if and only if the first vector is zero or the second is a multiple of the first. -/ theorem oangle_eq_zero_or_eq_pi_iff_right_eq_smul {x y : V} : - o.oangle x y = 0 ∨ o.oangle x y = π ↔ x = 0 ∨ ∃ r : ℝ, y = r • x := - by + o.oangle x y = 0 ∨ o.oangle x y = π ↔ x = 0 ∨ ∃ r : ℝ, y = r • x := by rw [oangle_eq_zero_iff_same_ray, oangle_eq_pi_iff_same_ray_neg] refine' ⟨fun h => _, fun h => _⟩ · rcases h with (h | ⟨-, -, h⟩) @@ -495,8 +485,7 @@ theorem oangle_ne_zero_and_ne_pi_iff_linearIndependent {x y : V} : #align orientation.oangle_ne_zero_and_ne_pi_iff_linear_independent Orientation.oangle_ne_zero_and_ne_pi_iff_linearIndependent /-- Two vectors are equal if and only if they have equal norms and zero angle between them. -/ -theorem eq_iff_norm_eq_and_oangle_eq_zero (x y : V) : x = y ↔ ‖x‖ = ‖y‖ ∧ o.oangle x y = 0 := - by +theorem eq_iff_norm_eq_and_oangle_eq_zero (x y : V) : x = y ↔ ‖x‖ = ‖y‖ ∧ o.oangle x y = 0 := by rw [oangle_eq_zero_iff_same_ray] constructor · rintro rfl @@ -528,8 +517,7 @@ theorem eq_iff_norm_eq_of_oangle_eq_zero {x y : V} (h : o.oangle x y = 0) : x = between the second and the third equals the angle between the first and the third. -/ @[simp] theorem oangle_add {x y z : V} (hx : x ≠ 0) (hy : y ≠ 0) (hz : z ≠ 0) : - o.oangle x y + o.oangle y z = o.oangle x z := - by + o.oangle x y + o.oangle y z = o.oangle x z := by simp_rw [oangle] rw [← Complex.arg_mul_coe_angle, o.kahler_mul y x z] congr 1 @@ -601,8 +589,7 @@ theorem oangle_sub_eq_oangle_sub_rev_of_norm_eq {x y : V} (h : ‖x‖ = ‖y‖ /-- The angle at the apex of an isosceles triangle is `π` minus twice a base angle, oriented vector angle form. -/ theorem oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq {x y : V} (hn : x ≠ y) (h : ‖x‖ = ‖y‖) : - o.oangle y x = π - (2 : ℤ) • o.oangle (y - x) y := - by + o.oangle y x = π - (2 : ℤ) • o.oangle (y - x) y := by rw [two_zsmul] rw [← o.oangle_sub_eq_oangle_sub_rev_of_norm_eq h] rw [eq_sub_iff_add_eq, ← oangle_neg_neg, ← add_assoc] @@ -632,8 +619,7 @@ protected theorem Complex.oangle (w z : ℂ) : terms of a complex-number representation of the space. -/ theorem oangle_map_complex (f : V ≃ₗᵢ[ℝ] ℂ) (hf : Orientation.map (Fin 2) f.toLinearEquiv o = Complex.orientation) (x y : V) : - o.oangle x y = Complex.arg (conj (f x) * f y) := - by + o.oangle x y = Complex.arg (conj (f x) * f y) := by rw [← Complex.oangle, ← hf, o.oangle_map] simp #align orientation.oangle_map_complex Orientation.oangle_map_complex @@ -646,8 +632,7 @@ theorem oangle_neg_orientation_eq_neg (x y : V) : (-o).oangle x y = -o.oangle x /-- The inner product of two vectors is the product of the norms and the cosine of the oriented angle between the vectors. -/ theorem inner_eq_norm_mul_norm_mul_cos_oangle (x y : V) : - ⟪x, y⟫ = ‖x‖ * ‖y‖ * Real.Angle.cos (o.oangle x y) := - by + ⟪x, y⟫ = ‖x‖ * ‖y‖ * Real.Angle.cos (o.oangle x y) := by by_cases hx : x = 0; · simp [hx] by_cases hy : y = 0; · simp [hy] have : ‖x‖ ≠ 0 := by simpa using hx @@ -662,8 +647,7 @@ theorem inner_eq_norm_mul_norm_mul_cos_oangle (x y : V) : /-- The cosine of the oriented angle between two nonzero vectors is the inner product divided by the product of the norms. -/ theorem cos_oangle_eq_inner_div_norm_mul_norm {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) : - Real.Angle.cos (o.oangle x y) = ⟪x, y⟫ / (‖x‖ * ‖y‖) := - by + Real.Angle.cos (o.oangle x y) = ⟪x, y⟫ / (‖x‖ * ‖y‖) := by rw [o.inner_eq_norm_mul_norm_mul_cos_oangle] field_simp [norm_ne_zero_iff.2 hx, norm_ne_zero_iff.2 hy] ring @@ -686,8 +670,7 @@ theorem oangle_eq_angle_or_eq_neg_angle {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) /-- The unoriented angle between two nonzero vectors is the absolute value of the oriented angle, converted to a real. -/ theorem angle_eq_abs_oangle_toReal {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) : - InnerProductGeometry.angle x y = |(o.oangle x y).toReal| := - by + InnerProductGeometry.angle x y = |(o.oangle x y).toReal| := by have h0 := InnerProductGeometry.angle_nonneg x y have hpi := InnerProductGeometry.angle_le_pi x y rcases o.oangle_eq_angle_or_eq_neg_angle hx hy with (h | h) @@ -701,8 +684,7 @@ theorem angle_eq_abs_oangle_toReal {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) : zero or the unoriented angle is 0 or π. -/ theorem eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero {x y : V} (h : (o.oangle x y).sign = 0) : - x = 0 ∨ y = 0 ∨ InnerProductGeometry.angle x y = 0 ∨ InnerProductGeometry.angle x y = π := - by + x = 0 ∨ y = 0 ∨ InnerProductGeometry.angle x y = 0 ∨ InnerProductGeometry.angle x y = π := by by_cases hx : x = 0; · simp [hx] by_cases hy : y = 0; · simp [hy] rw [o.angle_eq_abs_oangle_to_real hx hy] @@ -714,19 +696,16 @@ theorem eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero {x y : V} equal, then the oriented angles are equal (even in degenerate cases). -/ theorem oangle_eq_of_angle_eq_of_sign_eq {w x y z : V} (h : InnerProductGeometry.angle w x = InnerProductGeometry.angle y z) - (hs : (o.oangle w x).sign = (o.oangle y z).sign) : o.oangle w x = o.oangle y z := - by + (hs : (o.oangle w x).sign = (o.oangle y z).sign) : o.oangle w x = o.oangle y z := by by_cases h0 : (w = 0 ∨ x = 0) ∨ y = 0 ∨ z = 0 - · have hs' : (o.oangle w x).sign = 0 ∧ (o.oangle y z).sign = 0 := - by + · have hs' : (o.oangle w x).sign = 0 ∧ (o.oangle y z).sign = 0 := by rcases h0 with ((rfl | rfl) | rfl | rfl) · simpa using hs.symm · simpa using hs.symm · simpa using hs · simpa using hs rcases hs' with ⟨hswx, hsyz⟩ - have h' : InnerProductGeometry.angle w x = π / 2 ∧ InnerProductGeometry.angle y z = π / 2 := - by + have h' : InnerProductGeometry.angle w x = π / 2 ∧ InnerProductGeometry.angle y z = π / 2 := by rcases h0 with ((rfl | rfl) | rfl | rfl) · simpa using h.symm · simpa using h.symm @@ -738,12 +717,10 @@ theorem oangle_eq_of_angle_eq_of_sign_eq {w x y z : V} rw [div_eq_iff, eq_comm, ← sub_eq_zero, mul_two, add_sub_cancel] at hpi · exact real.pi_pos.ne.symm hpi · exact two_ne_zero - have h0wx : w = 0 ∨ x = 0 := - by + have h0wx : w = 0 ∨ x = 0 := by have h0' := o.eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero hswx simpa [hwx, real.pi_pos.ne.symm, hpi] using h0' - have h0yz : y = 0 ∨ z = 0 := - by + have h0yz : y = 0 ∨ z = 0 := by have h0' := o.eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero hsyz simpa [hyz, real.pi_pos.ne.symm, hpi] using h0' rcases h0wx with (h0wx | h0wx) <;> rcases h0yz with (h0yz | h0yz) <;> simp [h0wx, h0yz] @@ -765,8 +742,7 @@ theorem angle_eq_iff_oangle_eq_of_sign_eq {w x y z : V} (hw : w ≠ 0) (hx : x /-- The oriented angle between two vectors equals the unoriented angle if the sign is positive. -/ theorem oangle_eq_angle_of_sign_eq_one {x y : V} (h : (o.oangle x y).sign = 1) : - o.oangle x y = InnerProductGeometry.angle x y := - by + o.oangle x y = InnerProductGeometry.angle x y := by by_cases hx : x = 0; · exfalso; simpa [hx] using h by_cases hy : y = 0; · exfalso; simpa [hy] using h refine' (o.oangle_eq_angle_or_eq_neg_angle hx hy).resolve_right _ @@ -781,8 +757,7 @@ theorem oangle_eq_angle_of_sign_eq_one {x y : V} (h : (o.oangle x y).sign = 1) : /-- The oriented angle between two vectors equals minus the unoriented angle if the sign is negative. -/ theorem oangle_eq_neg_angle_of_sign_eq_neg_one {x y : V} (h : (o.oangle x y).sign = -1) : - o.oangle x y = -InnerProductGeometry.angle x y := - by + o.oangle x y = -InnerProductGeometry.angle x y := by by_cases hx : x = 0; · exfalso; simpa [hx] using h by_cases hy : y = 0; · exfalso; simpa [hy] using h refine' (o.oangle_eq_angle_or_eq_neg_angle hx hy).resolve_left _ @@ -797,8 +772,7 @@ theorem oangle_eq_neg_angle_of_sign_eq_neg_one {x y : V} (h : (o.oangle x y).sig /-- The oriented angle between two nonzero vectors is zero if and only if the unoriented angle is zero. -/ theorem oangle_eq_zero_iff_angle_eq_zero {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) : - o.oangle x y = 0 ↔ InnerProductGeometry.angle x y = 0 := - by + o.oangle x y = 0 ↔ InnerProductGeometry.angle x y = 0 := by refine' ⟨fun h => _, fun h => _⟩ · simpa [o.angle_eq_abs_oangle_to_real hx hy] · have ha := o.oangle_eq_angle_or_eq_neg_angle hx hy @@ -808,8 +782,7 @@ theorem oangle_eq_zero_iff_angle_eq_zero {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) /-- The oriented angle between two vectors is `π` if and only if the unoriented angle is `π`. -/ theorem oangle_eq_pi_iff_angle_eq_pi {x y : V} : - o.oangle x y = π ↔ InnerProductGeometry.angle x y = π := - by + o.oangle x y = π ↔ InnerProductGeometry.angle x y = π := by by_cases hx : x = 0; · simp [hx, real.angle.pi_ne_zero.symm, div_eq_mul_inv, mul_right_eq_self₀, not_or, Real.pi_ne_zero] @@ -829,8 +802,7 @@ theorem oangle_eq_pi_iff_angle_eq_pi {x y : V} : /-- One of two vectors is zero or the oriented angle between them is plus or minus `π / 2` if and only if the inner product of those vectors is zero. -/ theorem eq_zero_or_oangle_eq_iff_inner_eq_zero {x y : V} : - x = 0 ∨ y = 0 ∨ o.oangle x y = (π / 2 : ℝ) ∨ o.oangle x y = (-π / 2 : ℝ) ↔ ⟪x, y⟫ = 0 := - by + x = 0 ∨ y = 0 ∨ o.oangle x y = (π / 2 : ℝ) ∨ o.oangle x y = (-π / 2 : ℝ) ↔ ⟪x, y⟫ = 0 := by by_cases hx : x = 0; · simp [hx] by_cases hy : y = 0; · simp [hy] rw [InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two, or_iff_right hx, or_iff_right hy] @@ -868,8 +840,7 @@ theorem inner_rev_eq_zero_of_oangle_eq_neg_pi_div_two {x y : V} (h : o.oangle x /-- Negating the first vector passed to `oangle` negates the sign of the angle. -/ @[simp] -theorem oangle_sign_neg_left (x y : V) : (o.oangle (-x) y).sign = -(o.oangle x y).sign := - by +theorem oangle_sign_neg_left (x y : V) : (o.oangle (-x) y).sign = -(o.oangle x y).sign := by by_cases hx : x = 0; · simp [hx] by_cases hy : y = 0; · simp [hy] rw [o.oangle_neg_left hx hy, Real.Angle.sign_add_pi] @@ -877,8 +848,7 @@ theorem oangle_sign_neg_left (x y : V) : (o.oangle (-x) y).sign = -(o.oangle x y /-- Negating the second vector passed to `oangle` negates the sign of the angle. -/ @[simp] -theorem oangle_sign_neg_right (x y : V) : (o.oangle x (-y)).sign = -(o.oangle x y).sign := - by +theorem oangle_sign_neg_right (x y : V) : (o.oangle x (-y)).sign = -(o.oangle x y).sign := by by_cases hx : x = 0; · simp [hx] by_cases hy : y = 0; · simp [hy] rw [o.oangle_neg_right hx hy, Real.Angle.sign_add_pi] @@ -934,14 +904,12 @@ theorem oangle_smul_add_right_eq_zero_or_eq_pi_iff {x y : V} (r : ℝ) : the sign of the angle. -/ @[simp] theorem oangle_sign_smul_add_right (x y : V) (r : ℝ) : - (o.oangle x (r • x + y)).sign = (o.oangle x y).sign := - by + (o.oangle x (r • x + y)).sign = (o.oangle x y).sign := by by_cases h : o.oangle x y = 0 ∨ o.oangle x y = π · rwa [Real.Angle.sign_eq_zero_iff.2 h, Real.Angle.sign_eq_zero_iff, oangle_smul_add_right_eq_zero_or_eq_pi_iff] - have h' : ∀ r' : ℝ, o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ π := - by + have h' : ∀ r' : ℝ, o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ π := by intro r' rwa [← o.oangle_smul_add_right_eq_zero_or_eq_pi_iff r', not_or] at h let s : Set (V × V) := (fun r' : ℝ => (x, r' • x + y)) '' Set.univ @@ -949,8 +917,7 @@ theorem oangle_sign_smul_add_right (x y : V) (r : ℝ) : is_connected_univ.image _ (continuous_const.prod_mk ((continuous_id.smul continuous_const).add continuous_const)).ContinuousOn - have hf : ContinuousOn (fun z : V × V => o.oangle z.1 z.2) s := - by + have hf : ContinuousOn (fun z : V × V => o.oangle z.1 z.2) s := by refine' ContinuousAt.continuousOn fun z hz => o.continuous_at_oangle _ _ all_goals simp_rw [s, Set.mem_image] at hz @@ -959,14 +926,12 @@ theorem oangle_sign_smul_add_right (x y : V) (r : ℝ) : intro hz · simpa [hz] using (h' 0).1 · simpa [hz] using (h' r').1 - have hs : ∀ z : V × V, z ∈ s → o.oangle z.1 z.2 ≠ 0 ∧ o.oangle z.1 z.2 ≠ π := - by + have hs : ∀ z : V × V, z ∈ s → o.oangle z.1 z.2 ≠ 0 ∧ o.oangle z.1 z.2 ≠ π := by intro z hz simp_rw [s, Set.mem_image] at hz obtain ⟨r', -, rfl⟩ := hz exact h' r' - have hx : (x, y) ∈ s := - by + have hx : (x, y) ∈ s := by convert Set.mem_image_of_mem (fun r' : ℝ => (x, r' • x + y)) (Set.mem_univ 0) simp have hy : (x, r • x + y) ∈ s := Set.mem_image_of_mem _ (Set.mem_univ _) @@ -1072,8 +1037,7 @@ vector, is the sign of the factor by which the second vector is multiplied in th multiplied by the sign of the angle between the two vectors. -/ @[simp] theorem oangle_sign_smul_add_smul_right (x y : V) (r₁ r₂ : ℝ) : - (o.oangle x (r₁ • x + r₂ • y)).sign = SignType.sign r₂ * (o.oangle x y).sign := - by + (o.oangle x (r₁ • x + r₂ • y)).sign = SignType.sign r₂ * (o.oangle x y).sign := by rw [← o.oangle_sign_smul_add_right x (r₁ • x + r₂ • y) (-r₁)] simp #align orientation.oangle_sign_smul_add_smul_right Orientation.oangle_sign_smul_add_smul_right @@ -1093,8 +1057,7 @@ determinant of the factors in those combinations multiplied by the sign of the a two vectors. -/ theorem oangle_sign_smul_add_smul_smul_add_smul (x y : V) (r₁ r₂ r₃ r₄ : ℝ) : (o.oangle (r₁ • x + r₂ • y) (r₃ • x + r₄ • y)).sign = - SignType.sign (r₁ * r₄ - r₂ * r₃) * (o.oangle x y).sign := - by + SignType.sign (r₁ * r₄ - r₂ * r₃) * (o.oangle x y).sign := by by_cases hr₁ : r₁ = 0 · rw [hr₁, zero_smul, MulZeroClass.zero_mul, zero_add, zero_sub, Left.sign_neg, @@ -1111,11 +1074,9 @@ theorem oangle_sign_smul_add_smul_smul_add_smul (x y : V) (r₁ r₂ r₃ r₄ : /-- A base angle of an isosceles triangle is acute, oriented vector angle form. -/ theorem abs_oangle_sub_left_toReal_lt_pi_div_two {x y : V} (h : ‖x‖ = ‖y‖) : - |(o.oangle (y - x) y).toReal| < π / 2 := - by + |(o.oangle (y - x) y).toReal| < π / 2 := by by_cases hn : x = y; · simp [hn, div_pos, Real.pi_pos] - have hs : ((2 : ℤ) • o.oangle (y - x) y).sign = (o.oangle (y - x) y).sign := - by + have hs : ((2 : ℤ) • o.oangle (y - x) y).sign = (o.oangle (y - x) y).sign := by conv_rhs => rw [oangle_sign_sub_left_swap] rw [o.oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq hn h, Real.Angle.sign_pi_sub] rw [Real.Angle.sign_two_zsmul_eq_sign_iff] at hs From 1828e91917dd108a8ff5f9404e5459e9773acd35 Mon Sep 17 00:00:00 2001 From: Parcly Taxel Date: Sun, 11 Jun 2023 17:28:00 +0800 Subject: [PATCH 4/5] pilfer #4602 --- Mathlib.lean | 1 + .../Analysis/InnerProductSpace/TwoDim.lean | 676 ++++++++++++++++++ 2 files changed, 677 insertions(+) create mode 100644 Mathlib/Analysis/InnerProductSpace/TwoDim.lean diff --git a/Mathlib.lean b/Mathlib.lean index 003c52876beb5..552fdb1677c8d 100644 --- a/Mathlib.lean +++ b/Mathlib.lean @@ -581,6 +581,7 @@ import Mathlib.Analysis.InnerProductSpace.PiL2 import Mathlib.Analysis.InnerProductSpace.Positive import Mathlib.Analysis.InnerProductSpace.Projection import Mathlib.Analysis.InnerProductSpace.Symmetric +import Mathlib.Analysis.InnerProductSpace.TwoDim import Mathlib.Analysis.InnerProductSpace.l2Space import Mathlib.Analysis.LocallyConvex.AbsConvex import Mathlib.Analysis.LocallyConvex.BalancedCoreHull diff --git a/Mathlib/Analysis/InnerProductSpace/TwoDim.lean b/Mathlib/Analysis/InnerProductSpace/TwoDim.lean new file mode 100644 index 0000000000000..2c1ac56d2dfd8 --- /dev/null +++ b/Mathlib/Analysis/InnerProductSpace/TwoDim.lean @@ -0,0 +1,676 @@ +/- +Copyright (c) 2022 Heather Macbeth. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Heather Macbeth + +! This file was ported from Lean 3 source module analysis.inner_product_space.two_dim +! leanprover-community/mathlib commit cd8fafa2fac98e1a67097e8a91ad9901cfde48af +! Please do not edit these lines, except to modify the commit id +! if you have ported upstream changes. +-/ +import Mathlib.Analysis.InnerProductSpace.Dual +import Mathlib.Analysis.InnerProductSpace.Orientation +import Mathlib.Data.Complex.Orientation +import Mathlib.Tactic.LinearCombination + +/-! +# Oriented two-dimensional real inner product spaces + +This file defines constructions specific to the geometry of an oriented two-dimensional real inner +product space `E`. + +## Main declarations + +* `Orientation.areaForm`: an antisymmetric bilinear form `E →ₗ[ℝ] E →ₗ[ℝ] ℝ` (usual notation `ω`). + Morally, when `ω` is evaluated on two vectors, it gives the oriented area of the parallelogram + they span. (But mathlib does not yet have a construction of oriented area, and in fact the + construction of oriented area should pass through `ω`.) + +* `Orientation.rightAngleRotation`: an isometric automorphism `E ≃ₗᵢ[ℝ] E` (usual notation `J`). + This automorphism squares to -1. In a later file, rotations (`Orientation.rotation`) are defined, + in such a way that this automorphism is equal to rotation by 90 degrees. + +* `Orientation.basisRightAngleRotation`: for a nonzero vector `x` in `E`, the basis `![x, J x]` + for `E`. + +* `Orientation.kahler`: a complex-valued real-bilinear map `E →ₗ[ℝ] E →ₗ[ℝ] ℂ`. Its real part is the + inner product and its imaginary part is `Orientation.areaForm`. For vectors `x` and `y` in `E`, + the complex number `o.kahler x y` has modulus `‖x‖ * ‖y‖`. In a later file, oriented angles + (`Orientation.oangle`) are defined, in such a way that the argument of `o.kahler x y` is the + oriented angle from `x` to `y`. + +## Main results + +* `Orientation.rightAngleRotation_rightAngleRotation`: the identity `J (J x) = - x` + +* `Orientation.nonneg_inner_and_areaForm_eq_zero_iff_sameRay`: `x`, `y` are in the same ray, if + and only if `0 ≤ ⟪x, y⟫` and `ω x y = 0` + +* `Orientation.kahler_mul`: the identity `o.kahler x a * o.kahler a y = ‖a‖ ^ 2 * o.kahler x y` + +* `Complex.areaForm`, `Complex.rightAngleRotation`, `Complex.kahler`: the concrete + interpretations of `areaForm`, `rightAngleRotation`, `kahler` for the oriented real inner + product space `ℂ` + +* `Orientation.areaForm_map_complex`, `Orientation.rightAngleRotation_map_complex`, + `Orientation.kahler_map_complex`: given an orientation-preserving isometry from `E` to `ℂ`, + expressions for `areaForm`, `rightAngleRotation`, `kahler` as the pullback of their concrete + interpretations on `ℂ` + +## Implementation notes + +Notation `ω` for `Orientation.areaForm` and `J` for `Orientation.rightAngleRotation` should be +defined locally in each file which uses them, since otherwise one would need a more cumbersome +notation which mentions the orientation explicitly (something like `ω[o]`). Write + +``` +local notation `ω` := o.areaForm +local notation `J` := o.rightAngleRotation +``` + +-/ + + +noncomputable section + +open scoped RealInnerProductSpace ComplexConjugate + +open FiniteDimensional + +lemma FiniteDimensional.fact_finiteDimensional_of_finrank_eq_two {K V : Type _} [DivisionRing K] + [AddCommGroup V] [Module K V] [Fact (finrank K V = 2)] : FiniteDimensional K V := + fact_finiteDimensional_of_finrank_eq_succ 1 + +attribute [local instance] FiniteDimensional.fact_finiteDimensional_of_finrank_eq_two + +variable {E : Type _} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [Fact (finrank ℝ E = 2)] + (o : Orientation ℝ E (Fin 2)) + +namespace Orientation + +/-- An antisymmetric bilinear form on an oriented real inner product space of dimension 2 (usual +notation `ω`). When evaluated on two vectors, it gives the oriented area of the parallelogram they +span. -/ +irreducible_def areaForm : E →ₗ[ℝ] E →ₗ[ℝ] ℝ := by + let z : AlternatingMap ℝ E ℝ (Fin 0) ≃ₗ[ℝ] ℝ := + AlternatingMap.constLinearEquivOfIsEmpty.symm + let y : AlternatingMap ℝ E ℝ (Fin 1) →ₗ[ℝ] E →ₗ[ℝ] ℝ := + LinearMap.llcomp ℝ E (AlternatingMap ℝ E ℝ (Fin 0)) ℝ z ∘ₗ AlternatingMap.curryLeftLinearMap + exact y ∘ₗ AlternatingMap.curryLeftLinearMap (R' := ℝ) o.volumeForm +#align orientation.area_form Orientation.areaForm + +local notation "ω" => o.areaForm + +theorem areaForm_to_volumeForm (x y : E) : ω x y = o.volumeForm ![x, y] := by simp [areaForm] +#align orientation.area_form_to_volume_form Orientation.areaForm_to_volumeForm + +@[simp] +theorem areaForm_apply_self (x : E) : ω x x = 0 := by + rw [areaForm_to_volumeForm] + refine' o.volumeForm.map_eq_zero_of_eq ![x, x] _ (_ : (0 : Fin 2) ≠ 1) + · simp + · norm_num +#align orientation.area_form_apply_self Orientation.areaForm_apply_self + +theorem areaForm_swap (x y : E) : ω x y = -ω y x := by + simp only [areaForm_to_volumeForm] + convert o.volumeForm.map_swap ![y, x] (_ : (0 : Fin 2) ≠ 1) + · ext i + fin_cases i <;> rfl + · norm_num +#align orientation.area_form_swap Orientation.areaForm_swap + +@[simp] +theorem areaForm_neg_orientation : (-o).areaForm = -o.areaForm := by + ext (x y) + simp [areaForm_to_volumeForm] +#align orientation.area_form_neg_orientation Orientation.areaForm_neg_orientation + +/-- Continuous linear map version of `Orientation.areaForm`, useful for calculus. -/ +def areaForm' : E →L[ℝ] E →L[ℝ] ℝ := + LinearMap.toContinuousLinearMap + (↑(LinearMap.toContinuousLinearMap : (E →ₗ[ℝ] ℝ) ≃ₗ[ℝ] E →L[ℝ] ℝ) ∘ₗ o.areaForm) +#align orientation.area_form' Orientation.areaForm' + +@[simp] +theorem areaForm'_apply (x : E) : + o.areaForm' x = LinearMap.toContinuousLinearMap (o.areaForm x) := + rfl +#align orientation.area_form'_apply Orientation.areaForm'_apply + +theorem abs_areaForm_le (x y : E) : |ω x y| ≤ ‖x‖ * ‖y‖ := by + simpa [areaForm_to_volumeForm, Fin.prod_univ_succ] using o.abs_volumeForm_apply_le ![x, y] +#align orientation.abs_area_form_le Orientation.abs_areaForm_le + +theorem areaForm_le (x y : E) : ω x y ≤ ‖x‖ * ‖y‖ := by + simpa [areaForm_to_volumeForm, Fin.prod_univ_succ] using o.volumeForm_apply_le ![x, y] +#align orientation.area_form_le Orientation.areaForm_le + +theorem abs_areaForm_of_orthogonal {x y : E} (h : ⟪x, y⟫ = 0) : |ω x y| = ‖x‖ * ‖y‖ := by + rw [o.areaForm_to_volumeForm, o.abs_volumeForm_apply_of_pairwise_orthogonal] + · simp [Fin.prod_univ_succ] + intro i j hij + fin_cases i <;> fin_cases j + · simp_all + · simpa using h + · simpa [real_inner_comm] using h + · simp_all +#align orientation.abs_area_form_of_orthogonal Orientation.abs_areaForm_of_orthogonal + +theorem areaForm_map {F : Type _} [NormedAddCommGroup F] [InnerProductSpace ℝ F] + [Fact (finrank ℝ F = 2)] (φ : E ≃ₗᵢ[ℝ] F) (x y : F) : + (Orientation.map (Fin 2) φ.toLinearEquiv o).areaForm x y = + o.areaForm (φ.symm x) (φ.symm y) := by + have : φ.symm ∘ ![x, y] = ![φ.symm x, φ.symm y] := by + ext i + fin_cases i <;> rfl + simp [areaForm_to_volumeForm, volumeForm_map, this] +#align orientation.area_form_map Orientation.areaForm_map + +/-- The area form is invariant under pullback by a positively-oriented isometric automorphism. -/ +theorem areaForm_comp_linearIsometryEquiv (φ : E ≃ₗᵢ[ℝ] E) + (hφ : 0 < LinearMap.det (φ.toLinearEquiv : E →ₗ[ℝ] E)) (x y : E) : + o.areaForm (φ x) (φ y) = o.areaForm x y := by + convert o.areaForm_map φ (φ x) (φ y) + · symm + rwa [← o.map_eq_iff_det_pos φ.toLinearEquiv] at hφ + rw [@Fact.out (finrank ℝ E = 2), Fintype.card_fin] + · simp + · simp +#align orientation.area_form_comp_linear_isometry_equiv Orientation.areaForm_comp_linearIsometryEquiv + +/-- Auxiliary construction for `Orientation.rightAngleRotation`, rotation by 90 degrees in an +oriented real inner product space of dimension 2. -/ +irreducible_def rightAngleRotationAux₁ : E →ₗ[ℝ] E := + let to_dual : E ≃ₗ[ℝ] E →ₗ[ℝ] ℝ := + (InnerProductSpace.toDual ℝ E).toLinearEquiv ≪≫ₗ LinearMap.toContinuousLinearMap.symm + ↑to_dual.symm ∘ₗ ω +#align orientation.right_angle_rotation_aux₁ Orientation.rightAngleRotationAux₁ + +@[simp] +theorem inner_rightAngleRotationAux₁_left (x y : E) : ⟪o.rightAngleRotationAux₁ x, y⟫ = ω x y := by + -- Porting note: split `simp only` for greater proof control + simp only [rightAngleRotationAux₁, LinearEquiv.trans_symm, LinearIsometryEquiv.toLinearEquiv_symm, + LinearMap.coe_comp, LinearEquiv.coe_coe, Function.comp_apply, LinearEquiv.trans_apply, + LinearIsometryEquiv.coe_toLinearEquiv] + rw [InnerProductSpace.toDual_symm_apply] + norm_cast +#align orientation.inner_right_angle_rotation_aux₁_left Orientation.inner_rightAngleRotationAux₁_left + +@[simp] +theorem inner_rightAngleRotationAux₁_right (x y : E) : + ⟪x, o.rightAngleRotationAux₁ y⟫ = -ω x y := by + rw [real_inner_comm] + simp [o.areaForm_swap y x] +#align orientation.inner_right_angle_rotation_aux₁_right Orientation.inner_rightAngleRotationAux₁_right + +/-- Auxiliary construction for `Orientation.rightAngleRotation`, rotation by 90 degrees in an +oriented real inner product space of dimension 2. -/ +def rightAngleRotationAux₂ : E →ₗᵢ[ℝ] E := + { o.rightAngleRotationAux₁ with + norm_map' := fun x => by + dsimp + refine' le_antisymm _ _ + · cases' eq_or_lt_of_le (norm_nonneg (o.rightAngleRotationAux₁ x)) with h h + · rw [← h] + positivity + refine' le_of_mul_le_mul_right _ h + rw [← real_inner_self_eq_norm_mul_norm, o.inner_rightAngleRotationAux₁_left] + exact o.areaForm_le x (o.rightAngleRotationAux₁ x) + · let K : Submodule ℝ E := ℝ ∙ x + have : Nontrivial Kᗮ := by + apply @FiniteDimensional.nontrivial_of_finrank_pos ℝ + have : finrank ℝ K ≤ Finset.card {x} := by + rw [← Set.toFinset_singleton] + exact finrank_span_le_card ({x} : Set E) + have : Finset.card {x} = 1 := Finset.card_singleton x + have : finrank ℝ K + finrank ℝ Kᗮ = finrank ℝ E := K.finrank_add_finrank_orthogonal + have : finrank ℝ E = 2 := Fact.out + linarith + obtain ⟨w, hw₀⟩ : ∃ w : Kᗮ, w ≠ 0 := exists_ne 0 + have hw' : ⟪x, (w : E)⟫ = 0 := Submodule.mem_orthogonal_singleton_iff_inner_right.mp w.2 + have hw : (w : E) ≠ 0 := fun h => hw₀ (Submodule.coe_eq_zero.mp h) + refine' le_of_mul_le_mul_right _ (by rwa [norm_pos_iff] : 0 < ‖(w : E)‖) + rw [← o.abs_areaForm_of_orthogonal hw'] + rw [← o.inner_rightAngleRotationAux₁_left x w] + exact abs_real_inner_le_norm (o.rightAngleRotationAux₁ x) w } +#align orientation.right_angle_rotation_aux₂ Orientation.rightAngleRotationAux₂ + +@[simp] +theorem rightAngleRotationAux₁_rightAngleRotationAux₁ (x : E) : + o.rightAngleRotationAux₁ (o.rightAngleRotationAux₁ x) = -x := by + apply ext_inner_left ℝ + intro y + have : ⟪o.rightAngleRotationAux₁ y, o.rightAngleRotationAux₁ x⟫ = ⟪y, x⟫ := + LinearIsometry.inner_map_map o.rightAngleRotationAux₂ y x + rw [o.inner_rightAngleRotationAux₁_right, ← o.inner_rightAngleRotationAux₁_left, this, + inner_neg_right] +#align orientation.right_angle_rotation_aux₁_right_angle_rotation_aux₁ Orientation.rightAngleRotationAux₁_rightAngleRotationAux₁ + +/-- An isometric automorphism of an oriented real inner product space of dimension 2 (usual notation +`J`). This automorphism squares to -1. We will define rotations in such a way that this +automorphism is equal to rotation by 90 degrees. -/ +irreducible_def rightAngleRotation : E ≃ₗᵢ[ℝ] E := + LinearIsometryEquiv.ofLinearIsometry o.rightAngleRotationAux₂ (-o.rightAngleRotationAux₁) + (by ext; simp [rightAngleRotationAux₂]) (by ext; simp [rightAngleRotationAux₂]) +#align orientation.right_angle_rotation Orientation.rightAngleRotation + +local notation "J" => o.rightAngleRotation + +@[simp] +theorem inner_rightAngleRotation_left (x y : E) : ⟪J x, y⟫ = ω x y := by + rw [rightAngleRotation] + exact o.inner_rightAngleRotationAux₁_left x y +#align orientation.inner_right_angle_rotation_left Orientation.inner_rightAngleRotation_left + +@[simp] +theorem inner_rightAngleRotation_right (x y : E) : ⟪x, J y⟫ = -ω x y := by + rw [rightAngleRotation] + exact o.inner_rightAngleRotationAux₁_right x y +#align orientation.inner_right_angle_rotation_right Orientation.inner_rightAngleRotation_right + +@[simp] +theorem rightAngleRotation_rightAngleRotation (x : E) : J (J x) = -x := by + rw [rightAngleRotation] + exact o.rightAngleRotationAux₁_rightAngleRotationAux₁ x +#align orientation.right_angle_rotation_right_angle_rotation Orientation.rightAngleRotation_rightAngleRotation + +@[simp] +theorem rightAngleRotation_symm : + LinearIsometryEquiv.symm J = LinearIsometryEquiv.trans J (LinearIsometryEquiv.neg ℝ) := by + rw [rightAngleRotation] + exact LinearIsometryEquiv.toLinearIsometry_injective rfl +#align orientation.right_angle_rotation_symm Orientation.rightAngleRotation_symm + +-- @[simp] -- Porting note: simp already proves this +theorem inner_rightAngleRotation_self (x : E) : ⟪J x, x⟫ = 0 := by simp +#align orientation.inner_right_angle_rotation_self Orientation.inner_rightAngleRotation_self + +theorem inner_rightAngleRotation_swap (x y : E) : ⟪x, J y⟫ = -⟪J x, y⟫ := by simp +#align orientation.inner_right_angle_rotation_swap Orientation.inner_rightAngleRotation_swap + +theorem inner_rightAngleRotation_swap' (x y : E) : ⟪J x, y⟫ = -⟪x, J y⟫ := by + simp [o.inner_rightAngleRotation_swap x y] +#align orientation.inner_right_angle_rotation_swap' Orientation.inner_rightAngleRotation_swap' + +theorem inner_comp_rightAngleRotation (x y : E) : ⟪J x, J y⟫ = ⟪x, y⟫ := + LinearIsometryEquiv.inner_map_map J x y +#align orientation.inner_comp_right_angle_rotation Orientation.inner_comp_rightAngleRotation + +@[simp] +theorem areaForm_rightAngleRotation_left (x y : E) : ω (J x) y = -⟪x, y⟫ := by + rw [← o.inner_comp_rightAngleRotation, o.inner_rightAngleRotation_right, neg_neg] +#align orientation.area_form_right_angle_rotation_left Orientation.areaForm_rightAngleRotation_left + +@[simp] +theorem areaForm_rightAngleRotation_right (x y : E) : ω x (J y) = ⟪x, y⟫ := by + rw [← o.inner_rightAngleRotation_left, o.inner_comp_rightAngleRotation] +#align orientation.area_form_right_angle_rotation_right Orientation.areaForm_rightAngleRotation_right + +-- @[simp] -- Porting note: simp already proves this +theorem areaForm_comp_rightAngleRotation (x y : E) : ω (J x) (J y) = ω x y := by simp +#align orientation.area_form_comp_right_angle_rotation Orientation.areaForm_comp_rightAngleRotation + +@[simp] +theorem rightAngleRotation_trans_rightAngleRotation : + LinearIsometryEquiv.trans J J = LinearIsometryEquiv.neg ℝ := by ext; simp +#align orientation.right_angle_rotation_trans_right_angle_rotation Orientation.rightAngleRotation_trans_rightAngleRotation + +theorem rightAngleRotation_neg_orientation (x : E) : + (-o).rightAngleRotation x = -o.rightAngleRotation x := by + apply ext_inner_right ℝ + intro y + rw [inner_rightAngleRotation_left] + simp +#align orientation.right_angle_rotation_neg_orientation Orientation.rightAngleRotation_neg_orientation + +@[simp] +theorem rightAngleRotation_trans_neg_orientation : + (-o).rightAngleRotation = o.rightAngleRotation.trans (LinearIsometryEquiv.neg ℝ) := + LinearIsometryEquiv.ext <| o.rightAngleRotation_neg_orientation +#align orientation.right_angle_rotation_trans_neg_orientation Orientation.rightAngleRotation_trans_neg_orientation + +theorem rightAngleRotation_map {F : Type _} [NormedAddCommGroup F] [InnerProductSpace ℝ F] + [Fact (finrank ℝ F = 2)] (φ : E ≃ₗᵢ[ℝ] F) (x : F) : + (Orientation.map (Fin 2) φ.toLinearEquiv o).rightAngleRotation x = + φ (o.rightAngleRotation (φ.symm x)) := by + apply ext_inner_right ℝ + intro y + rw [inner_rightAngleRotation_left] + trans ⟪J (φ.symm x), φ.symm y⟫ + · simp [o.areaForm_map] + trans ⟪φ (J (φ.symm x)), φ (φ.symm y)⟫ + · rw [φ.inner_map_map] + · simp +#align orientation.right_angle_rotation_map Orientation.rightAngleRotation_map + +/-- `J` commutes with any positively-oriented isometric automorphism. -/ +theorem linearIsometryEquiv_comp_rightAngleRotation (φ : E ≃ₗᵢ[ℝ] E) + (hφ : 0 < LinearMap.det (φ.toLinearEquiv : E →ₗ[ℝ] E)) (x : E) : φ (J x) = J (φ x) := by + convert(o.rightAngleRotation_map φ (φ x)).symm + · simp + · symm + rwa [← o.map_eq_iff_det_pos φ.toLinearEquiv] at hφ + rw [@Fact.out (finrank ℝ E = 2), Fintype.card_fin] +#align orientation.linear_isometry_equiv_comp_right_angle_rotation Orientation.linearIsometryEquiv_comp_rightAngleRotation + +theorem rightAngleRotation_map' {F : Type _} [NormedAddCommGroup F] [InnerProductSpace ℝ F] + [Fact (finrank ℝ F = 2)] (φ : E ≃ₗᵢ[ℝ] F) : + (Orientation.map (Fin 2) φ.toLinearEquiv o).rightAngleRotation = + (φ.symm.trans o.rightAngleRotation).trans φ := + LinearIsometryEquiv.ext <| o.rightAngleRotation_map φ +#align orientation.right_angle_rotation_map' Orientation.rightAngleRotation_map' + +/-- `J` commutes with any positively-oriented isometric automorphism. -/ +theorem linearIsometryEquiv_comp_rightAngleRotation' (φ : E ≃ₗᵢ[ℝ] E) + (hφ : 0 < LinearMap.det (φ.toLinearEquiv : E →ₗ[ℝ] E)) : + LinearIsometryEquiv.trans J φ = φ.trans J := + LinearIsometryEquiv.ext <| o.linearIsometryEquiv_comp_rightAngleRotation φ hφ +#align orientation.linear_isometry_equiv_comp_right_angle_rotation' Orientation.linearIsometryEquiv_comp_rightAngleRotation' + +/-- For a nonzero vector `x` in an oriented two-dimensional real inner product space `E`, +`![x, J x]` forms an (orthogonal) basis for `E`. -/ +def basisRightAngleRotation (x : E) (hx : x ≠ 0) : Basis (Fin 2) ℝ E := + @basisOfLinearIndependentOfCardEqFinrank ℝ _ _ _ _ _ _ _ ![x, J x] + (linearIndependent_of_ne_zero_of_inner_eq_zero (fun i => by fin_cases i <;> simp [hx]) + (by + intro i j hij + fin_cases i <;> fin_cases j <;> simp_all)) + (@Fact.out (finrank ℝ E = 2)).symm +#align orientation.basis_right_angle_rotation Orientation.basisRightAngleRotation + +@[simp] +theorem coe_basisRightAngleRotation (x : E) (hx : x ≠ 0) : + ⇑(o.basisRightAngleRotation x hx) = ![x, J x] := + coe_basisOfLinearIndependentOfCardEqFinrank _ _ +#align orientation.coe_basis_right_angle_rotation Orientation.coe_basisRightAngleRotation + +/-- For vectors `a x y : E`, the identity `⟪a, x⟫ * ⟪a, y⟫ + ω a x * ω a y = ‖a‖ ^ 2 * ⟪x, y⟫`. (See +`Orientation.inner_mul_inner_add_areaForm_mul_areaForm` for the "applied" form.)-/ +theorem inner_mul_inner_add_areaForm_mul_areaForm' (a x : E) : + ⟪a, x⟫ • innerₛₗ ℝ a + ω a x • ω a = ‖a‖ ^ 2 • innerₛₗ ℝ x := by + by_cases ha : a = 0 + · simp [ha] + apply (o.basisRightAngleRotation a ha).ext + intro i + fin_cases i + · simp only [Fin.mk_zero, coe_basisRightAngleRotation, Matrix.cons_val_zero, LinearMap.add_apply, + LinearMap.smul_apply, innerₛₗ_apply, real_inner_self_eq_norm_sq, smul_eq_mul, + areaForm_apply_self, mul_zero, add_zero, Real.rpow_two, real_inner_comm] + ring + · simp only [Fin.mk_one, coe_basisRightAngleRotation, Matrix.cons_val_one, Matrix.head_cons, + LinearMap.add_apply, LinearMap.smul_apply, innerₛₗ_apply, inner_rightAngleRotation_right, + areaForm_apply_self, neg_zero, smul_eq_mul, mul_zero, areaForm_rightAngleRotation_right, + real_inner_self_eq_norm_sq, zero_add, Real.rpow_two, mul_neg] + rw [o.areaForm_swap] + ring +#align orientation.inner_mul_inner_add_area_form_mul_area_form' Orientation.inner_mul_inner_add_areaForm_mul_areaForm' + +/-- For vectors `a x y : E`, the identity `⟪a, x⟫ * ⟪a, y⟫ + ω a x * ω a y = ‖a‖ ^ 2 * ⟪x, y⟫`. -/ +theorem inner_mul_inner_add_areaForm_mul_areaForm (a x y : E) : + ⟪a, x⟫ * ⟪a, y⟫ + ω a x * ω a y = ‖a‖ ^ 2 * ⟪x, y⟫ := + congr_arg (fun f : E →ₗ[ℝ] ℝ => f y) (o.inner_mul_inner_add_areaForm_mul_areaForm' a x) +#align orientation.inner_mul_inner_add_area_form_mul_area_form Orientation.inner_mul_inner_add_areaForm_mul_areaForm + +theorem inner_sq_add_areaForm_sq (a b : E) : ⟪a, b⟫ ^ 2 + ω a b ^ 2 = ‖a‖ ^ 2 * ‖b‖ ^ 2 := by + simpa [sq, real_inner_self_eq_norm_sq] using o.inner_mul_inner_add_areaForm_mul_areaForm a b b +#align orientation.inner_sq_add_area_form_sq Orientation.inner_sq_add_areaForm_sq + +/-- For vectors `a x y : E`, the identity `⟪a, x⟫ * ω a y - ω a x * ⟪a, y⟫ = ‖a‖ ^ 2 * ω x y`. (See +`Orientation.inner_mul_areaForm_sub` for the "applied" form.) -/ +theorem inner_mul_areaForm_sub' (a x : E) : ⟪a, x⟫ • ω a - ω a x • innerₛₗ ℝ a = ‖a‖ ^ 2 • ω x := by + by_cases ha : a = 0 + · simp [ha] + apply (o.basisRightAngleRotation a ha).ext + intro i + fin_cases i + · simp only [o.areaForm_swap a x, neg_smul, sub_neg_eq_add, Fin.mk_zero, + coe_basisRightAngleRotation, Matrix.cons_val_zero, LinearMap.add_apply, LinearMap.smul_apply, + areaForm_apply_self, smul_eq_mul, mul_zero, innerₛₗ_apply, real_inner_self_eq_norm_sq, + zero_add, Real.rpow_two] + ring + · simp only [Fin.mk_one, coe_basisRightAngleRotation, Matrix.cons_val_one, Matrix.head_cons, + LinearMap.sub_apply, LinearMap.smul_apply, areaForm_rightAngleRotation_right, + real_inner_self_eq_norm_sq, smul_eq_mul, innerₛₗ_apply, inner_rightAngleRotation_right, + areaForm_apply_self, neg_zero, mul_zero, sub_zero, Real.rpow_two, real_inner_comm] + ring +#align orientation.inner_mul_area_form_sub' Orientation.inner_mul_areaForm_sub' + +/-- For vectors `a x y : E`, the identity `⟪a, x⟫ * ω a y - ω a x * ⟪a, y⟫ = ‖a‖ ^ 2 * ω x y`. -/ +theorem inner_mul_areaForm_sub (a x y : E) : ⟪a, x⟫ * ω a y - ω a x * ⟪a, y⟫ = ‖a‖ ^ 2 * ω x y := + congr_arg (fun f : E →ₗ[ℝ] ℝ => f y) (o.inner_mul_areaForm_sub' a x) +#align orientation.inner_mul_area_form_sub Orientation.inner_mul_areaForm_sub + +theorem nonneg_inner_and_areaForm_eq_zero_iff_sameRay (x y : E) : + 0 ≤ ⟪x, y⟫ ∧ ω x y = 0 ↔ SameRay ℝ x y := by + by_cases hx : x = 0 + · simp [hx] + constructor + · let a : ℝ := (o.basisRightAngleRotation x hx).repr y 0 + let b : ℝ := (o.basisRightAngleRotation x hx).repr y 1 + suffices 0 ≤ a * ‖x‖ ^ 2 ∧ b * ‖x‖ ^ 2 = 0 → SameRay ℝ x (a • x + b • J x) by + -- Porting note: `simp only` rewritten as `rw` + rw [← (o.basisRightAngleRotation x hx).sum_repr y, + Fin.sum_univ_succ, coe_basisRightAngleRotation, Matrix.cons_val_zero, + Finset.univ_unique, Fin.default_eq_zero, Finset.sum_singleton, Fin.succ_zero_eq_one, + Matrix.cons_val_one, Matrix.head_cons, + inner_add_right, real_inner_smul_right, real_inner_smul_right, + real_inner_self_eq_norm_sq, inner_rightAngleRotation_right, + areaForm_apply_self, neg_zero, mul_zero, add_zero, + map_add, map_smul, map_smul, areaForm_rightAngleRotation_right, real_inner_self_eq_norm_sq, + areaForm_apply_self, smul_eq_mul, mul_zero, zero_add, smul_eq_mul, ← Real.rpow_two] + exact this + rintro ⟨ha, hb⟩ + rw [Real.rpow_two] at hb + have hx' : 0 < ‖x‖ := by simpa using hx + have ha' : 0 ≤ a := nonneg_of_mul_nonneg_left ha (by positivity) + have hb' : b = 0 := eq_zero_of_ne_zero_of_mul_right_eq_zero (pow_ne_zero 2 hx'.ne') hb + simpa [hb'] using SameRay.sameRay_nonneg_smul_right x ha' + · intro h + obtain ⟨r, hr, rfl⟩ := h.exists_nonneg_left hx + simp only [inner_smul_right, real_inner_self_eq_norm_sq, LinearMap.map_smulₛₗ, + areaForm_apply_self, Algebra.id.smul_eq_mul, MulZeroClass.mul_zero, eq_self_iff_true, + and_true_iff] + positivity +#align orientation.nonneg_inner_and_area_form_eq_zero_iff_same_ray Orientation.nonneg_inner_and_areaForm_eq_zero_iff_sameRay + +/-- A complex-valued real-bilinear map on an oriented real inner product space of dimension 2. Its +real part is the inner product and its imaginary part is `Orientation.areaForm`. + +On `ℂ` with the standard orientation, `kahler w z = conj w * z`; see `Complex.kahler`. -/ +def kahler : E →ₗ[ℝ] E →ₗ[ℝ] ℂ := + LinearMap.llcomp ℝ E ℝ ℂ Complex.ofRealClm ∘ₗ innerₛₗ ℝ + + LinearMap.llcomp ℝ E ℝ ℂ ((LinearMap.lsmul ℝ ℂ).flip Complex.I) ∘ₗ ω +#align orientation.kahler Orientation.kahler + +theorem kahler_apply_apply (x y : E) : o.kahler x y = ⟪x, y⟫ + ω x y • Complex.I := + rfl +#align orientation.kahler_apply_apply Orientation.kahler_apply_apply + +theorem kahler_swap (x y : E) : o.kahler x y = conj (o.kahler y x) := by + have : ∀ r : ℝ, Complex.ofReal' r = @IsROrC.ofReal ℂ _ r := fun r => rfl + simp only [kahler_apply_apply] + rw [real_inner_comm, areaForm_swap] + simp [this] +#align orientation.kahler_swap Orientation.kahler_swap + +@[simp] +theorem kahler_apply_self (x : E) : o.kahler x x = ‖x‖ ^ 2 := by + simp [kahler_apply_apply, real_inner_self_eq_norm_sq] +#align orientation.kahler_apply_self Orientation.kahler_apply_self + +@[simp] +theorem kahler_rightAngleRotation_left (x y : E) : + o.kahler (J x) y = -Complex.I * o.kahler x y := by + simp only [o.areaForm_rightAngleRotation_left, o.inner_rightAngleRotation_left, + o.kahler_apply_apply, Complex.ofReal_neg, Complex.real_smul] + linear_combination ω x y * Complex.I_sq +#align orientation.kahler_right_angle_rotation_left Orientation.kahler_rightAngleRotation_left + +@[simp] +theorem kahler_rightAngleRotation_right (x y : E) : + o.kahler x (J y) = Complex.I * o.kahler x y := by + simp only [o.areaForm_rightAngleRotation_right, o.inner_rightAngleRotation_right, + o.kahler_apply_apply, Complex.ofReal_neg, Complex.real_smul] + linear_combination -ω x y * Complex.I_sq +#align orientation.kahler_right_angle_rotation_right Orientation.kahler_rightAngleRotation_right + +-- @[simp] -- Porting note: simp normal form is `kahler_comp_rightAngleRotation'` +theorem kahler_comp_rightAngleRotation (x y : E) : o.kahler (J x) (J y) = o.kahler x y := by + simp only [kahler_rightAngleRotation_left, kahler_rightAngleRotation_right] + linear_combination -o.kahler x y * Complex.I_sq +#align orientation.kahler_comp_right_angle_rotation Orientation.kahler_comp_rightAngleRotation + +theorem kahler_comp_rightAngleRotation' (x y : E) : + -(Complex.I * (Complex.I * o.kahler x y)) = o.kahler x y := by + linear_combination -o.kahler x y * Complex.I_sq + +@[simp] +theorem kahler_neg_orientation (x y : E) : (-o).kahler x y = conj (o.kahler x y) := by + have : ∀ r : ℝ, Complex.ofReal' r = @IsROrC.ofReal ℂ _ r := fun r => rfl + simp [kahler_apply_apply, this] +#align orientation.kahler_neg_orientation Orientation.kahler_neg_orientation + +theorem kahler_mul (a x y : E) : o.kahler x a * o.kahler a y = ‖a‖ ^ 2 * o.kahler x y := by + trans (↑(‖a‖ ^ 2) : ℂ) * o.kahler x y + · ext + · simp only [o.kahler_apply_apply, Complex.add_im, Complex.add_re, Complex.I_im, Complex.I_re, + Complex.mul_im, Complex.mul_re, Complex.ofReal_im, Complex.ofReal_re, Complex.real_smul] + rw [real_inner_comm a x, o.areaForm_swap x a] + linear_combination o.inner_mul_inner_add_areaForm_mul_areaForm a x y + · simp only [o.kahler_apply_apply, Complex.add_im, Complex.add_re, Complex.I_im, Complex.I_re, + Complex.mul_im, Complex.mul_re, Complex.ofReal_im, Complex.ofReal_re, Complex.real_smul] + rw [real_inner_comm a x, o.areaForm_swap x a] + linear_combination o.inner_mul_areaForm_sub a x y + · norm_cast +#align orientation.kahler_mul Orientation.kahler_mul + +theorem normSq_kahler (x y : E) : Complex.normSq (o.kahler x y) = ‖x‖ ^ 2 * ‖y‖ ^ 2 := by + simpa [kahler_apply_apply, Complex.normSq, sq] using o.inner_sq_add_areaForm_sq x y +#align orientation.norm_sq_kahler Orientation.normSq_kahler + +theorem abs_kahler (x y : E) : Complex.abs (o.kahler x y) = ‖x‖ * ‖y‖ := by + rw [← sq_eq_sq, Complex.sq_abs] + · linear_combination (norm := ring_nf) o.normSq_kahler x y; simp + · positivity + · positivity +#align orientation.abs_kahler Orientation.abs_kahler + +theorem norm_kahler (x y : E) : ‖o.kahler x y‖ = ‖x‖ * ‖y‖ := by simpa using o.abs_kahler x y +#align orientation.norm_kahler Orientation.norm_kahler + +theorem eq_zero_or_eq_zero_of_kahler_eq_zero {x y : E} (hx : o.kahler x y = 0) : x = 0 ∨ y = 0 := by + have : ‖x‖ * ‖y‖ = 0 := by simpa [hx] using (o.norm_kahler x y).symm + cases' eq_zero_or_eq_zero_of_mul_eq_zero this with h h + · left + simpa using h + · right + simpa using h +#align orientation.eq_zero_or_eq_zero_of_kahler_eq_zero Orientation.eq_zero_or_eq_zero_of_kahler_eq_zero + +theorem kahler_eq_zero_iff (x y : E) : o.kahler x y = 0 ↔ x = 0 ∨ y = 0 := by + refine' ⟨o.eq_zero_or_eq_zero_of_kahler_eq_zero, _⟩ + rintro (rfl | rfl) <;> simp +#align orientation.kahler_eq_zero_iff Orientation.kahler_eq_zero_iff + +theorem kahler_ne_zero {x y : E} (hx : x ≠ 0) (hy : y ≠ 0) : o.kahler x y ≠ 0 := by + apply mt o.eq_zero_or_eq_zero_of_kahler_eq_zero + tauto +#align orientation.kahler_ne_zero Orientation.kahler_ne_zero + +theorem kahler_ne_zero_iff (x y : E) : o.kahler x y ≠ 0 ↔ x ≠ 0 ∧ y ≠ 0 := by + refine' ⟨_, fun h => o.kahler_ne_zero h.1 h.2⟩ + contrapose + simp only [not_and_or, Classical.not_not, kahler_apply_apply, Complex.real_smul] + rintro (rfl | rfl) <;> simp +#align orientation.kahler_ne_zero_iff Orientation.kahler_ne_zero_iff + +theorem kahler_map {F : Type _} [NormedAddCommGroup F] [InnerProductSpace ℝ F] + [Fact (finrank ℝ F = 2)] (φ : E ≃ₗᵢ[ℝ] F) (x y : F) : + (Orientation.map (Fin 2) φ.toLinearEquiv o).kahler x y = o.kahler (φ.symm x) (φ.symm y) := by + simp [kahler_apply_apply, areaForm_map] +#align orientation.kahler_map Orientation.kahler_map + +/-- The bilinear map `kahler` is invariant under pullback by a positively-oriented isometric +automorphism. -/ +theorem kahler_comp_linearIsometryEquiv (φ : E ≃ₗᵢ[ℝ] E) + (hφ : 0 < LinearMap.det (φ.toLinearEquiv : E →ₗ[ℝ] E)) (x y : E) : + o.kahler (φ x) (φ y) = o.kahler x y := + by simp [kahler_apply_apply, o.areaForm_comp_linearIsometryEquiv φ hφ] +#align orientation.kahler_comp_linear_isometry_equiv Orientation.kahler_comp_linearIsometryEquiv + +end Orientation + +namespace Complex + +attribute [local instance] Complex.finrank_real_complex_fact + +@[simp] +protected theorem areaForm (w z : ℂ) : Complex.orientation.areaForm w z = (conj w * z).im := by + let o := Complex.orientation + -- Porting note: split `simp only` for greater proof control + rw [o.areaForm_to_volumeForm, o.volumeForm_robust Complex.orthonormalBasisOneI rfl, + Basis.det_apply, Matrix.det_fin_two] + repeat rw [Basis.toMatrix_apply] + simp only [toBasis_orthonormalBasisOneI, Matrix.cons_val_zero, Matrix.cons_val_one, + Matrix.head_cons, coe_basisOneI_repr, mul_im, conj_re, conj_im, neg_mul] + ring +#align complex.area_form Complex.areaForm + +@[simp] +protected theorem rightAngleRotation (z : ℂ) : + Complex.orientation.rightAngleRotation z = I * z := by + apply ext_inner_right ℝ + intro w + rw [Orientation.inner_rightAngleRotation_left] + simp only [Complex.areaForm, Complex.inner, mul_re, mul_im, conj_re, conj_im, map_mul, conj_I, + neg_re, neg_im, I_re, I_im] + ring +#align complex.right_angle_rotation Complex.rightAngleRotation + +@[simp] +protected theorem kahler (w z : ℂ) : Complex.orientation.kahler w z = conj w * z := by + rw [Orientation.kahler_apply_apply] + ext1 <;> simp +#align complex.kahler Complex.kahler + +end Complex + +namespace Orientation + +local notation "ω" => o.areaForm + +local notation "J" => o.rightAngleRotation + +open Complex + +attribute [local instance] finrank_real_complex_fact -- Porting note: this instance is needed + +/-- The area form on an oriented real inner product space of dimension 2 can be evaluated in terms +of a complex-number representation of the space. -/ +theorem areaForm_map_complex (f : E ≃ₗᵢ[ℝ] ℂ) + (hf : Orientation.map (Fin 2) f.toLinearEquiv o = Complex.orientation) (x y : E) : + ω x y = (conj (f x) * f y).im := by + rw [← Complex.areaForm, ← hf, areaForm_map] + iterate 2 rw [LinearIsometryEquiv.symm_apply_apply] +#align orientation.area_form_map_complex Orientation.areaForm_map_complex + +/-- The rotation by 90 degrees on an oriented real inner product space of dimension 2 can be +evaluated in terms of a complex-number representation of the space. -/ +theorem rightAngleRotation_map_complex (f : E ≃ₗᵢ[ℝ] ℂ) + (hf : Orientation.map (Fin 2) f.toLinearEquiv o = Complex.orientation) (x : E) : + f (J x) = I * f x := by + rw [← Complex.rightAngleRotation, ← hf, o.rightAngleRotation_map, + LinearIsometryEquiv.symm_apply_apply] +#align orientation.right_angle_rotation_map_complex Orientation.rightAngleRotation_map_complex + +/-- The Kahler form on an oriented real inner product space of dimension 2 can be evaluated in terms +of a complex-number representation of the space. -/ +theorem kahler_map_complex (f : E ≃ₗᵢ[ℝ] ℂ) + (hf : Orientation.map (Fin 2) f.toLinearEquiv o = Complex.orientation) (x y : E) : + o.kahler x y = conj (f x) * f y := by + rw [← Complex.kahler, ← hf, o.kahler_map] + iterate 2 rw [LinearIsometryEquiv.symm_apply_apply] +#align orientation.kahler_map_complex Orientation.kahler_map_complex + +end Orientation From 90843f2237b30cb562142946532c01620ab1c0cc Mon Sep 17 00:00:00 2001 From: Parcly Taxel Date: Sun, 11 Jun 2023 17:28:45 +0800 Subject: [PATCH 5/5] fix the actual file --- .../Euclidean/Angle/Oriented/Basic.lean | 270 +++++++++--------- 1 file changed, 133 insertions(+), 137 deletions(-) diff --git a/Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean b/Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean index fb18fee4e2f50..c1f2fb1d6bf6a 100644 --- a/Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean +++ b/Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean @@ -18,11 +18,11 @@ This file defines oriented angles in real inner product spaces. ## Main definitions -* `orientation.oangle` is the oriented angle between two vectors with respect to an orientation. +* `Orientation.oangle` is the oriented angle between two vectors with respect to an orientation. ## Implementation notes -The definitions here use the `real.angle` type, angles modulo `2 * π`. For some purposes, +The definitions here use the `Real.angle` type, angles modulo `2 * π`. For some purposes, angles modulo `π` are more convenient, because results are true for such angles with less configuration dependence. Results that are only equalities modulo `π` can be represented modulo `2 * π` as equalities of `(2 : ℤ) • θ`. @@ -42,8 +42,6 @@ open scoped Real RealInnerProductSpace ComplexConjugate namespace Orientation -attribute [local instance] fact_finite_dimensional_of_finrank_eq_succ - attribute [local instance] Complex.finrank_real_complex_fact variable {V V' : Type _} @@ -54,11 +52,10 @@ variable [InnerProductSpace ℝ V] [InnerProductSpace ℝ V'] variable [Fact (finrank ℝ V = 2)] [Fact (finrank ℝ V' = 2)] (o : Orientation ℝ V (Fin 2)) --- mathport name: exprω local notation "ω" => o.areaForm /-- The oriented angle from `x` to `y`, modulo `2 * π`. If either vector is 0, this is 0. -See `inner_product_geometry.angle` for the corresponding unoriented angle definition. -/ +See `InnerProductGeometry.angle` for the corresponding unoriented angle definition. -/ def oangle (x y : V) : Real.Angle := Complex.arg (o.kahler x y) #align orientation.oangle Orientation.oangle @@ -68,9 +65,8 @@ theorem continuousAt_oangle {x : V × V} (hx1 : x.1 ≠ 0) (hx2 : x.2 ≠ 0) : ContinuousAt (fun y : V × V => o.oangle y.1 y.2) x := by refine' (Complex.continuousAt_arg_coe_angle _).comp _ · exact o.kahler_ne_zero hx1 hx2 - exact - ((continuous_of_real.comp continuous_inner).add - ((continuous_of_real.comp o.area_form'.continuous₂).mul continuous_const)).ContinuousAt + exact ((continuous_ofReal.comp continuous_inner).add + ((continuous_ofReal.comp o.areaForm'.continuous₂).mul continuous_const)).continuousAt #align orientation.continuous_at_oangle Orientation.continuousAt_oangle /-- If the first vector passed to `oangle` is 0, the result is 0. -/ @@ -86,25 +82,25 @@ theorem oangle_zero_right (x : V) : o.oangle x 0 = 0 := by simp [oangle] /-- If the two vectors passed to `oangle` are the same, the result is 0. -/ @[simp] theorem oangle_self (x : V) : o.oangle x x = 0 := by - simp only [oangle, kahler_apply_self, ← Complex.ofReal_pow] - convert QuotientAddGroup.mk_zero _ - apply arg_of_real_of_nonneg + rw [oangle, kahler_apply_self]; norm_cast + convert QuotientAddGroup.mk_zero (AddSubgroup.zmultiples (2 * π)) + apply arg_ofReal_of_nonneg positivity #align orientation.oangle_self Orientation.oangle_self /-- If the angle between two vectors is nonzero, the first vector is nonzero. -/ -theorem left_ne_zero_of_oangle_ne_zero {x y : V} (h : o.oangle x y ≠ 0) : x ≠ 0 := by rintro rfl; - simpa using h +theorem left_ne_zero_of_oangle_ne_zero {x y : V} (h : o.oangle x y ≠ 0) : x ≠ 0 := by + rintro rfl; simp at h #align orientation.left_ne_zero_of_oangle_ne_zero Orientation.left_ne_zero_of_oangle_ne_zero /-- If the angle between two vectors is nonzero, the second vector is nonzero. -/ -theorem right_ne_zero_of_oangle_ne_zero {x y : V} (h : o.oangle x y ≠ 0) : y ≠ 0 := by rintro rfl; - simpa using h +theorem right_ne_zero_of_oangle_ne_zero {x y : V} (h : o.oangle x y ≠ 0) : y ≠ 0 := by + rintro rfl; simp at h #align orientation.right_ne_zero_of_oangle_ne_zero Orientation.right_ne_zero_of_oangle_ne_zero /-- If the angle between two vectors is nonzero, the vectors are not equal. -/ -theorem ne_of_oangle_ne_zero {x y : V} (h : o.oangle x y ≠ 0) : x ≠ y := by rintro rfl; - simpa using h +theorem ne_of_oangle_ne_zero {x y : V} (h : o.oangle x y ≠ 0) : x ≠ y := by + rintro rfl; simp at h #align orientation.ne_of_oangle_ne_zero Orientation.ne_of_oangle_ne_zero /-- If the angle between two vectors is `π`, the first vector is nonzero. -/ @@ -211,16 +207,16 @@ theorem oangle_add_oangle_rev (x y : V) : o.oangle x y + o.oangle y x = 0 := by #align orientation.oangle_add_oangle_rev Orientation.oangle_add_oangle_rev /-- Negating the first vector passed to `oangle` adds `π` to the angle. -/ -theorem oangle_neg_left {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) : o.oangle (-x) y = o.oangle x y + π := - by +theorem oangle_neg_left {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) : + o.oangle (-x) y = o.oangle x y + π := by simp only [oangle, map_neg] convert Complex.arg_neg_coe_angle _ exact o.kahler_ne_zero hx hy #align orientation.oangle_neg_left Orientation.oangle_neg_left /-- Negating the second vector passed to `oangle` adds `π` to the angle. -/ -theorem oangle_neg_right {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) : o.oangle x (-y) = o.oangle x y + π := - by +theorem oangle_neg_right {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) : + o.oangle x (-y) = o.oangle x y + π := by simp only [oangle, map_neg] convert Complex.arg_neg_coe_angle _ exact o.kahler_ne_zero hx hy @@ -228,8 +224,8 @@ theorem oangle_neg_right {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) : o.oangle x (- /-- Negating the first vector passed to `oangle` does not change twice the angle. -/ @[simp] -theorem two_zsmul_oangle_neg_left (x y : V) : (2 : ℤ) • o.oangle (-x) y = (2 : ℤ) • o.oangle x y := - by +theorem two_zsmul_oangle_neg_left (x y : V) : + (2 : ℤ) • o.oangle (-x) y = (2 : ℤ) • o.oangle x y := by by_cases hx : x = 0 · simp [hx] · by_cases hy : y = 0 @@ -239,8 +235,8 @@ theorem two_zsmul_oangle_neg_left (x y : V) : (2 : ℤ) • o.oangle (-x) y = (2 /-- Negating the second vector passed to `oangle` does not change twice the angle. -/ @[simp] -theorem two_zsmul_oangle_neg_right (x y : V) : (2 : ℤ) • o.oangle x (-y) = (2 : ℤ) • o.oangle x y := - by +theorem two_zsmul_oangle_neg_right (x y : V) : + (2 : ℤ) • o.oangle x (-y) = (2 : ℤ) • o.oangle x y := by by_cases hx : x = 0 · simp [hx] · by_cases hy : y = 0 @@ -271,13 +267,13 @@ theorem oangle_neg_self_right {x : V} (hx : x ≠ 0) : o.oangle x (-x) = π := b #align orientation.oangle_neg_self_right Orientation.oangle_neg_self_right /-- Twice the angle between the negation of a vector and that vector is 0. -/ -@[simp] +-- @[simp] -- Porting note: simp can prove this theorem two_zsmul_oangle_neg_self_left (x : V) : (2 : ℤ) • o.oangle (-x) x = 0 := by by_cases hx : x = 0 <;> simp [hx] #align orientation.two_zsmul_oangle_neg_self_left Orientation.two_zsmul_oangle_neg_self_left /-- Twice the angle between a vector and its negation is 0. -/ -@[simp] +-- @[simp] -- Porting note: simp can prove this theorem two_zsmul_oangle_neg_self_right (x : V) : (2 : ℤ) • o.oangle x (-x) = 0 := by by_cases hx : x = 0 <;> simp [hx] #align orientation.two_zsmul_oangle_neg_self_right Orientation.two_zsmul_oangle_neg_self_right @@ -389,7 +385,7 @@ theorem two_zsmul_oangle_smul_smul_self (x : V) {r₁ r₂ : ℝ} : equal. -/ theorem two_zsmul_oangle_left_of_span_eq {x y : V} (z : V) (h : (ℝ ∙ x) = ℝ ∙ y) : (2 : ℤ) • o.oangle x z = (2 : ℤ) • o.oangle y z := by - rw [Submodule.span_singleton_eq_span_singleton] at h + rw [Submodule.span_singleton_eq_span_singleton] at h rcases h with ⟨r, rfl⟩ exact (o.two_zsmul_oangle_smul_left_of_ne_zero _ _ (Units.ne_zero _)).symm #align orientation.two_zsmul_oangle_left_of_span_eq Orientation.two_zsmul_oangle_left_of_span_eq @@ -398,7 +394,7 @@ theorem two_zsmul_oangle_left_of_span_eq {x y : V} (z : V) (h : (ℝ ∙ x) = equal. -/ theorem two_zsmul_oangle_right_of_span_eq (x : V) {y z : V} (h : (ℝ ∙ y) = ℝ ∙ z) : (2 : ℤ) • o.oangle x y = (2 : ℤ) • o.oangle x z := by - rw [Submodule.span_singleton_eq_span_singleton] at h + rw [Submodule.span_singleton_eq_span_singleton] at h rcases h with ⟨r, rfl⟩ exact (o.two_zsmul_oangle_smul_right_of_ne_zero _ _ (Units.ne_zero _)).symm #align orientation.two_zsmul_oangle_right_of_span_eq Orientation.two_zsmul_oangle_right_of_span_eq @@ -420,7 +416,7 @@ theorem oangle_eq_zero_iff_oangle_rev_eq_zero {x y : V} : o.oangle x y = 0 ↔ o theorem oangle_eq_zero_iff_sameRay {x y : V} : o.oangle x y = 0 ↔ SameRay ℝ x y := by rw [oangle, kahler_apply_apply, Complex.arg_coe_angle_eq_iff_eq_toReal, Real.Angle.toReal_zero, Complex.arg_eq_zero_iff] - simpa using o.nonneg_inner_and_area_form_eq_zero_iff_same_ray x y + simpa using o.nonneg_inner_and_areaForm_eq_zero_iff_sameRay x y #align orientation.oangle_eq_zero_iff_same_ray Orientation.oangle_eq_zero_iff_sameRay /-- The oriented angle between two vectors is `π` if and only if the angle with the vectors @@ -433,22 +429,22 @@ theorem oangle_eq_pi_iff_oangle_rev_eq_pi {x y : V} : o.oangle x y = π ↔ o.oa on the same ray as the negation of the second. -/ theorem oangle_eq_pi_iff_sameRay_neg {x y : V} : o.oangle x y = π ↔ x ≠ 0 ∧ y ≠ 0 ∧ SameRay ℝ x (-y) := by - rw [← o.oangle_eq_zero_iff_same_ray] + rw [← o.oangle_eq_zero_iff_sameRay] constructor · intro h - by_cases hx : x = 0; · simpa [hx, real.angle.pi_ne_zero.symm] using h - by_cases hy : y = 0; · simpa [hy, real.angle.pi_ne_zero.symm] using h + by_cases hx : x = 0; · simp [hx, Real.Angle.pi_ne_zero.symm] at h + by_cases hy : y = 0; · simp [hy, Real.Angle.pi_ne_zero.symm] at h refine' ⟨hx, hy, _⟩ rw [o.oangle_neg_right hx hy, h, Real.Angle.coe_pi_add_coe_pi] · rintro ⟨hx, hy, h⟩ - rwa [o.oangle_neg_right hx hy, ← Real.Angle.sub_coe_pi_eq_add_coe_pi, sub_eq_zero] at h + rwa [o.oangle_neg_right hx hy, ← Real.Angle.sub_coe_pi_eq_add_coe_pi, sub_eq_zero] at h #align orientation.oangle_eq_pi_iff_same_ray_neg Orientation.oangle_eq_pi_iff_sameRay_neg /-- The oriented angle between two vectors is zero or `π` if and only if those two vectors are not linearly independent. -/ theorem oangle_eq_zero_or_eq_pi_iff_not_linearIndependent {x y : V} : o.oangle x y = 0 ∨ o.oangle x y = π ↔ ¬LinearIndependent ℝ ![x, y] := by - rw [oangle_eq_zero_iff_same_ray, oangle_eq_pi_iff_same_ray_neg, + rw [oangle_eq_zero_iff_sameRay, oangle_eq_pi_iff_sameRay_neg, sameRay_or_ne_zero_and_sameRay_neg_iff_not_linearIndependent] #align orientation.oangle_eq_zero_or_eq_pi_iff_not_linear_independent Orientation.oangle_eq_zero_or_eq_pi_iff_not_linearIndependent @@ -456,7 +452,7 @@ theorem oangle_eq_zero_or_eq_pi_iff_not_linearIndependent {x y : V} : or the second is a multiple of the first. -/ theorem oangle_eq_zero_or_eq_pi_iff_right_eq_smul {x y : V} : o.oangle x y = 0 ∨ o.oangle x y = π ↔ x = 0 ∨ ∃ r : ℝ, y = r • x := by - rw [oangle_eq_zero_iff_same_ray, oangle_eq_pi_iff_same_ray_neg] + rw [oangle_eq_zero_iff_sameRay, oangle_eq_pi_iff_sameRay_neg] refine' ⟨fun h => _, fun h => _⟩ · rcases h with (h | ⟨-, -, h⟩) · by_cases hx : x = 0; · simp [hx] @@ -470,8 +466,8 @@ theorem oangle_eq_zero_or_eq_pi_iff_right_eq_smul {x y : V} : by_cases hx : x = 0; · simp [hx] rcases lt_trichotomy r 0 with (hr | hr | hr) · rw [← neg_smul] - exact - Or.inr ⟨hx, smul_ne_zero hr.ne hx, SameRay.sameRay_pos_smul_right x (Left.neg_pos_iff.2 hr)⟩ + exact Or.inr ⟨hx, smul_ne_zero hr.ne hx, + SameRay.sameRay_pos_smul_right x (Left.neg_pos_iff.2 hr)⟩ · simp [hr] · exact Or.inl (SameRay.sameRay_pos_smul_right x hr) #align orientation.oangle_eq_zero_or_eq_pi_iff_right_eq_smul Orientation.oangle_eq_zero_or_eq_pi_iff_right_eq_smul @@ -481,15 +477,15 @@ are linearly independent. -/ theorem oangle_ne_zero_and_ne_pi_iff_linearIndependent {x y : V} : o.oangle x y ≠ 0 ∧ o.oangle x y ≠ π ↔ LinearIndependent ℝ ![x, y] := by rw [← not_or, ← not_iff_not, Classical.not_not, - oangle_eq_zero_or_eq_pi_iff_not_linear_independent] + oangle_eq_zero_or_eq_pi_iff_not_linearIndependent] #align orientation.oangle_ne_zero_and_ne_pi_iff_linear_independent Orientation.oangle_ne_zero_and_ne_pi_iff_linearIndependent /-- Two vectors are equal if and only if they have equal norms and zero angle between them. -/ theorem eq_iff_norm_eq_and_oangle_eq_zero (x y : V) : x = y ↔ ‖x‖ = ‖y‖ ∧ o.oangle x y = 0 := by - rw [oangle_eq_zero_iff_same_ray] + rw [oangle_eq_zero_iff_sameRay] constructor · rintro rfl - simp + simp; rfl · rcases eq_or_ne y 0 with (rfl | hy) · simp rintro ⟨h₁, h₂⟩ @@ -564,10 +560,8 @@ sum of the angles of a triangle. -/ theorem oangle_add_cyc3_neg_left {x y z : V} (hx : x ≠ 0) (hy : y ≠ 0) (hz : z ≠ 0) : o.oangle (-x) y + o.oangle (-y) z + o.oangle (-z) x = π := by rw [o.oangle_neg_left hx hy, o.oangle_neg_left hy hz, o.oangle_neg_left hz hx, - show - o.oangle x y + π + (o.oangle y z + π) + (o.oangle z x + π) = - o.oangle x y + o.oangle y z + o.oangle z x + (π + π + π : Real.Angle) - by abel, + show o.oangle x y + π + (o.oangle y z + π) + (o.oangle z x + π) = + o.oangle x y + o.oangle y z + o.oangle z x + (π + π + π : Real.Angle) by abel, o.oangle_add_cyc3 hx hy hz, Real.Angle.coe_pi_add_coe_pi, zero_add, zero_add] #align orientation.oangle_add_cyc3_neg_left Orientation.oangle_add_cyc3_neg_left @@ -585,23 +579,23 @@ theorem oangle_sub_eq_oangle_sub_rev_of_norm_eq {x y : V} (h : ‖x‖ = ‖y‖ o.oangle x (x - y) = o.oangle (y - x) y := by simp [oangle, h] #align orientation.oangle_sub_eq_oangle_sub_rev_of_norm_eq Orientation.oangle_sub_eq_oangle_sub_rev_of_norm_eq -/- ./././Mathport/Syntax/Translate/Tactic/Lean3.lean:132:4: warning: unsupported: rw with cfg: { occs := occurrences.pos[occurrences.pos] «expr[ ,]»([1]) } -/ /-- The angle at the apex of an isosceles triangle is `π` minus twice a base angle, oriented vector angle form. -/ theorem oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq {x y : V} (hn : x ≠ y) (h : ‖x‖ = ‖y‖) : o.oangle y x = π - (2 : ℤ) • o.oangle (y - x) y := by rw [two_zsmul] - rw [← o.oangle_sub_eq_oangle_sub_rev_of_norm_eq h] + nth_rw 1 [← o.oangle_sub_eq_oangle_sub_rev_of_norm_eq h] rw [eq_sub_iff_add_eq, ← oangle_neg_neg, ← add_assoc] have hy : y ≠ 0 := by rintro rfl - rw [norm_zero, norm_eq_zero] at h + rw [norm_zero, norm_eq_zero] at h exact hn h have hx : x ≠ 0 := norm_ne_zero_iff.1 (h.symm ▸ norm_ne_zero_iff.2 hy) - convert o.oangle_add_cyc3_neg_right (neg_ne_zero.2 hy) hx (sub_ne_zero_of_ne hn.symm) <;> simp + convert o.oangle_add_cyc3_neg_right (neg_ne_zero.2 hy) hx (sub_ne_zero_of_ne hn.symm) using 1 + simp #align orientation.oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq Orientation.oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq -/-- The angle between two vectors, with respect to an orientation given by `orientation.map` +/-- The angle between two vectors, with respect to an orientation given by `Orientation.map` with a linear isometric equivalence, equals the angle between those two vectors, transformed by the inverse of that equivalence, with respect to the original orientation. -/ @[simp] @@ -611,7 +605,7 @@ theorem oangle_map (x y : V') (f : V ≃ₗᵢ[ℝ] V') : #align orientation.oangle_map Orientation.oangle_map @[simp] -protected theorem Complex.oangle (w z : ℂ) : +protected theorem _root_.Complex.oangle (w z : ℂ) : Complex.orientation.oangle w z = Complex.arg (conj w * z) := by simp [oangle] #align complex.oangle Complex.oangle @@ -621,7 +615,7 @@ theorem oangle_map_complex (f : V ≃ₗᵢ[ℝ] ℂ) (hf : Orientation.map (Fin 2) f.toLinearEquiv o = Complex.orientation) (x y : V) : o.oangle x y = Complex.arg (conj (f x) * f y) := by rw [← Complex.oangle, ← hf, o.oangle_map] - simp + iterate 2 rw [LinearIsometryEquiv.symm_apply_apply] #align orientation.oangle_map_complex Orientation.oangle_map_complex /-- Negating the orientation negates the value of `oangle`. -/ @@ -638,7 +632,7 @@ theorem inner_eq_norm_mul_norm_mul_cos_oangle (x y : V) : have : ‖x‖ ≠ 0 := by simpa using hx have : ‖y‖ ≠ 0 := by simpa using hy rw [oangle, Real.Angle.cos_coe, Complex.cos_arg, o.abs_kahler] - · simp only [kahler_apply_apply, real_smul, add_re, of_real_re, mul_re, I_re, of_real_im] + · simp only [kahler_apply_apply, real_smul, add_re, ofReal_re, mul_re, I_re, ofReal_im] field_simp ring · exact o.kahler_ne_zero hx hy @@ -687,9 +681,9 @@ theorem eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero {x y : V} x = 0 ∨ y = 0 ∨ InnerProductGeometry.angle x y = 0 ∨ InnerProductGeometry.angle x y = π := by by_cases hx : x = 0; · simp [hx] by_cases hy : y = 0; · simp [hy] - rw [o.angle_eq_abs_oangle_to_real hx hy] - rw [Real.Angle.sign_eq_zero_iff] at h - rcases h with (h | h) <;> simp [h, real.pi_pos.le] + rw [o.angle_eq_abs_oangle_toReal hx hy] + rw [Real.Angle.sign_eq_zero_iff] at h + rcases h with (h | h) <;> simp [h, Real.pi_pos.le] #align orientation.eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero Orientation.eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero /-- If two unoriented angles are equal, and the signs of the corresponding oriented angles are @@ -714,59 +708,55 @@ theorem oangle_eq_of_angle_eq_of_sign_eq {w x y z : V} rcases h' with ⟨hwx, hyz⟩ have hpi : π / 2 ≠ π := by intro hpi - rw [div_eq_iff, eq_comm, ← sub_eq_zero, mul_two, add_sub_cancel] at hpi - · exact real.pi_pos.ne.symm hpi + rw [div_eq_iff, eq_comm, ← sub_eq_zero, mul_two, add_sub_cancel] at hpi + · exact Real.pi_pos.ne.symm hpi · exact two_ne_zero have h0wx : w = 0 ∨ x = 0 := by have h0' := o.eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero hswx - simpa [hwx, real.pi_pos.ne.symm, hpi] using h0' + simpa [hwx, Real.pi_pos.ne.symm, hpi] using h0' have h0yz : y = 0 ∨ z = 0 := by have h0' := o.eq_zero_or_angle_eq_zero_or_pi_of_sign_oangle_eq_zero hsyz - simpa [hyz, real.pi_pos.ne.symm, hpi] using h0' + simpa [hyz, Real.pi_pos.ne.symm, hpi] using h0' rcases h0wx with (h0wx | h0wx) <;> rcases h0yz with (h0yz | h0yz) <;> simp [h0wx, h0yz] - · push_neg at h0 + · push_neg at h0 rw [Real.Angle.eq_iff_abs_toReal_eq_of_sign_eq hs] - rwa [o.angle_eq_abs_oangle_to_real h0.1.1 h0.1.2, - o.angle_eq_abs_oangle_to_real h0.2.1 h0.2.2] at h + rwa [o.angle_eq_abs_oangle_toReal h0.1.1 h0.1.2, + o.angle_eq_abs_oangle_toReal h0.2.1 h0.2.2] at h #align orientation.oangle_eq_of_angle_eq_of_sign_eq Orientation.oangle_eq_of_angle_eq_of_sign_eq /-- If the signs of two oriented angles between nonzero vectors are equal, the oriented angles are equal if and only if the unoriented angles are equal. -/ theorem angle_eq_iff_oangle_eq_of_sign_eq {w x y z : V} (hw : w ≠ 0) (hx : x ≠ 0) (hy : y ≠ 0) (hz : z ≠ 0) (hs : (o.oangle w x).sign = (o.oangle y z).sign) : - InnerProductGeometry.angle w x = InnerProductGeometry.angle y z ↔ o.oangle w x = o.oangle y z := - by + InnerProductGeometry.angle w x = InnerProductGeometry.angle y z ↔ + o.oangle w x = o.oangle y z := by refine' ⟨fun h => o.oangle_eq_of_angle_eq_of_sign_eq h hs, fun h => _⟩ - rw [o.angle_eq_abs_oangle_to_real hw hx, o.angle_eq_abs_oangle_to_real hy hz, h] + rw [o.angle_eq_abs_oangle_toReal hw hx, o.angle_eq_abs_oangle_toReal hy hz, h] #align orientation.angle_eq_iff_oangle_eq_of_sign_eq Orientation.angle_eq_iff_oangle_eq_of_sign_eq /-- The oriented angle between two vectors equals the unoriented angle if the sign is positive. -/ theorem oangle_eq_angle_of_sign_eq_one {x y : V} (h : (o.oangle x y).sign = 1) : o.oangle x y = InnerProductGeometry.angle x y := by - by_cases hx : x = 0; · exfalso; simpa [hx] using h - by_cases hy : y = 0; · exfalso; simpa [hy] using h + by_cases hx : x = 0; · exfalso; simp [hx] at h + by_cases hy : y = 0; · exfalso; simp [hy] at h refine' (o.oangle_eq_angle_or_eq_neg_angle hx hy).resolve_right _ intro hxy - rw [hxy, Real.Angle.sign_neg, neg_eq_iff_eq_neg, ← SignType.neg_iff, ← not_le] at h - exact - h - (Real.Angle.sign_coe_nonneg_of_nonneg_of_le_pi (InnerProductGeometry.angle_nonneg _ _) - (InnerProductGeometry.angle_le_pi _ _)) + rw [hxy, Real.Angle.sign_neg, neg_eq_iff_eq_neg, ← SignType.neg_iff, ← not_le] at h + exact h (Real.Angle.sign_coe_nonneg_of_nonneg_of_le_pi (InnerProductGeometry.angle_nonneg _ _) + (InnerProductGeometry.angle_le_pi _ _)) #align orientation.oangle_eq_angle_of_sign_eq_one Orientation.oangle_eq_angle_of_sign_eq_one /-- The oriented angle between two vectors equals minus the unoriented angle if the sign is negative. -/ theorem oangle_eq_neg_angle_of_sign_eq_neg_one {x y : V} (h : (o.oangle x y).sign = -1) : o.oangle x y = -InnerProductGeometry.angle x y := by - by_cases hx : x = 0; · exfalso; simpa [hx] using h - by_cases hy : y = 0; · exfalso; simpa [hy] using h + by_cases hx : x = 0; · exfalso; simp [hx] at h + by_cases hy : y = 0; · exfalso; simp [hy] at h refine' (o.oangle_eq_angle_or_eq_neg_angle hx hy).resolve_left _ intro hxy - rw [hxy, ← SignType.neg_iff, ← not_le] at h - exact - h - (Real.Angle.sign_coe_nonneg_of_nonneg_of_le_pi (InnerProductGeometry.angle_nonneg _ _) - (InnerProductGeometry.angle_le_pi _ _)) + rw [hxy, ← SignType.neg_iff, ← not_le] at h + exact h (Real.Angle.sign_coe_nonneg_of_nonneg_of_le_pi (InnerProductGeometry.angle_nonneg _ _) + (InnerProductGeometry.angle_le_pi _ _)) #align orientation.oangle_eq_neg_angle_of_sign_eq_neg_one Orientation.oangle_eq_neg_angle_of_sign_eq_neg_one /-- The oriented angle between two nonzero vectors is zero if and only if the unoriented angle @@ -774,28 +764,26 @@ is zero. -/ theorem oangle_eq_zero_iff_angle_eq_zero {x y : V} (hx : x ≠ 0) (hy : y ≠ 0) : o.oangle x y = 0 ↔ InnerProductGeometry.angle x y = 0 := by refine' ⟨fun h => _, fun h => _⟩ - · simpa [o.angle_eq_abs_oangle_to_real hx hy] + · simpa [o.angle_eq_abs_oangle_toReal hx hy] · have ha := o.oangle_eq_angle_or_eq_neg_angle hx hy - rw [h] at ha + rw [h] at ha simpa using ha #align orientation.oangle_eq_zero_iff_angle_eq_zero Orientation.oangle_eq_zero_iff_angle_eq_zero /-- The oriented angle between two vectors is `π` if and only if the unoriented angle is `π`. -/ theorem oangle_eq_pi_iff_angle_eq_pi {x y : V} : o.oangle x y = π ↔ InnerProductGeometry.angle x y = π := by - by_cases hx : x = 0; - · simp [hx, real.angle.pi_ne_zero.symm, div_eq_mul_inv, mul_right_eq_self₀, not_or, + by_cases hx : x = 0 + · simp [hx, Real.Angle.pi_ne_zero.symm, div_eq_mul_inv, mul_right_eq_self₀, not_or, Real.pi_ne_zero] - norm_num - by_cases hy : y = 0; - · simp [hy, real.angle.pi_ne_zero.symm, div_eq_mul_inv, mul_right_eq_self₀, not_or, + by_cases hy : y = 0 + · simp [hy, Real.Angle.pi_ne_zero.symm, div_eq_mul_inv, mul_right_eq_self₀, not_or, Real.pi_ne_zero] - norm_num refine' ⟨fun h => _, fun h => _⟩ - · rw [o.angle_eq_abs_oangle_to_real hx hy, h] - simp [real.pi_pos.le] + · rw [o.angle_eq_abs_oangle_toReal hx hy, h] + simp [Real.pi_pos.le] · have ha := o.oangle_eq_angle_or_eq_neg_angle hx hy - rw [h] at ha + rw [h] at ha simpa using ha #align orientation.oangle_eq_pi_iff_angle_eq_pi Orientation.oangle_eq_pi_iff_angle_eq_pi @@ -807,9 +795,9 @@ theorem eq_zero_or_oangle_eq_iff_inner_eq_zero {x y : V} : by_cases hy : y = 0; · simp [hy] rw [InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two, or_iff_right hx, or_iff_right hy] refine' ⟨fun h => _, fun h => _⟩ - · rwa [o.angle_eq_abs_oangle_to_real hx hy, Real.Angle.abs_toReal_eq_pi_div_two_iff] - · convert o.oangle_eq_angle_or_eq_neg_angle hx hy <;> rw [h] - exact neg_div _ _ + · rwa [o.angle_eq_abs_oangle_toReal hx hy, Real.Angle.abs_toReal_eq_pi_div_two_iff] + · convert o.oangle_eq_angle_or_eq_neg_angle hx hy using 2 <;> rw [h] + simp only [neg_div, Real.Angle.coe_neg] #align orientation.eq_zero_or_oangle_eq_iff_inner_eq_zero Orientation.eq_zero_or_oangle_eq_iff_inner_eq_zero /-- If the oriented angle between two vectors is `π / 2`, the inner product of those vectors @@ -873,31 +861,42 @@ theorem oangle_sign_smul_right (x y : V) (r : ℝ) : /-- Auxiliary lemma for the proof of `oangle_sign_smul_add_right`; not intended to be used outside of that proof. -/ theorem oangle_smul_add_right_eq_zero_or_eq_pi_iff {x y : V} (r : ℝ) : - o.oangle x (r • x + y) = 0 ∨ o.oangle x (r • x + y) = π ↔ o.oangle x y = 0 ∨ o.oangle x y = π := - by - simp_rw [oangle_eq_zero_or_eq_pi_iff_not_linear_independent, Fintype.not_linearIndependent_iff, - Fin.sum_univ_two, Fin.exists_fin_two] + o.oangle x (r • x + y) = 0 ∨ o.oangle x (r • x + y) = π ↔ + o.oangle x y = 0 ∨ o.oangle x y = π := by + simp_rw [oangle_eq_zero_or_eq_pi_iff_not_linearIndependent, Fintype.not_linearIndependent_iff] + -- Porting note: at this point all occurences of the bound variable `i` are of type + -- `Fin (Nat.succ (Nat.succ 0))`, but `Fin.sum_univ_two` and `Fin.exists_fin_two` expect it to be + -- `Fin 2` instead. Hence all the `conv`s. + -- Was `simp_rw [Fin.sum_univ_two, Fin.exists_fin_two]` + conv_lhs => enter [1, g, 1, 1, 2, i]; tactic => change Fin 2 at i + conv_lhs => enter [1, g]; rw [Fin.sum_univ_two] + conv_rhs => enter [1, g, 1, 1, 2, i]; tactic => change Fin 2 at i + conv_rhs => enter [1, g]; rw [Fin.sum_univ_two] + conv_lhs => enter [1, g, 2, 1, i]; tactic => change Fin 2 at i + conv_lhs => enter [1, g]; rw [Fin.exists_fin_two] + conv_rhs => enter [1, g, 2, 1, i]; tactic => change Fin 2 at i + conv_rhs => enter [1, g]; rw [Fin.exists_fin_two] refine' ⟨fun h => _, fun h => _⟩ · rcases h with ⟨m, h, hm⟩ - change m 0 • x + m 1 • (r • x + y) = 0 at h + change m 0 • x + m 1 • (r • x + y) = 0 at h refine' ⟨![m 0 + m 1 * r, m 1], _⟩ change (m 0 + m 1 * r) • x + m 1 • y = 0 ∧ (m 0 + m 1 * r ≠ 0 ∨ m 1 ≠ 0) - rw [smul_add, smul_smul, ← add_assoc, ← add_smul] at h + rw [smul_add, smul_smul, ← add_assoc, ← add_smul] at h refine' ⟨h, not_and_or.1 fun h0 => _⟩ obtain ⟨h0, h1⟩ := h0 - rw [h1] at h0 hm - rw [MulZeroClass.zero_mul, add_zero] at h0 - simpa [h0] using hm + rw [h1] at h0 hm + rw [MulZeroClass.zero_mul, add_zero] at h0 + simp [h0] at hm · rcases h with ⟨m, h, hm⟩ - change m 0 • x + m 1 • y = 0 at h + change m 0 • x + m 1 • y = 0 at h refine' ⟨![m 0 - m 1 * r, m 1], _⟩ change (m 0 - m 1 * r) • x + m 1 • (r • x + y) = 0 ∧ (m 0 - m 1 * r ≠ 0 ∨ m 1 ≠ 0) rw [sub_smul, smul_add, smul_smul, ← add_assoc, sub_add_cancel] refine' ⟨h, not_and_or.1 fun h0 => _⟩ obtain ⟨h0, h1⟩ := h0 - rw [h1] at h0 hm - rw [MulZeroClass.zero_mul, sub_zero] at h0 - simpa [h0] using hm + rw [h1] at h0 hm + rw [MulZeroClass.zero_mul, sub_zero] at h0 + simp [h0] at hm #align orientation.oangle_smul_add_right_eq_zero_or_eq_pi_iff Orientation.oangle_smul_add_right_eq_zero_or_eq_pi_iff /-- Adding a multiple of the first vector passed to `oangle` to the second vector does not change @@ -906,21 +905,18 @@ the sign of the angle. -/ theorem oangle_sign_smul_add_right (x y : V) (r : ℝ) : (o.oangle x (r • x + y)).sign = (o.oangle x y).sign := by by_cases h : o.oangle x y = 0 ∨ o.oangle x y = π - · - rwa [Real.Angle.sign_eq_zero_iff.2 h, Real.Angle.sign_eq_zero_iff, + · rwa [Real.Angle.sign_eq_zero_iff.2 h, Real.Angle.sign_eq_zero_iff, oangle_smul_add_right_eq_zero_or_eq_pi_iff] have h' : ∀ r' : ℝ, o.oangle x (r' • x + y) ≠ 0 ∧ o.oangle x (r' • x + y) ≠ π := by intro r' - rwa [← o.oangle_smul_add_right_eq_zero_or_eq_pi_iff r', not_or] at h + rwa [← o.oangle_smul_add_right_eq_zero_or_eq_pi_iff r', not_or] at h let s : Set (V × V) := (fun r' : ℝ => (x, r' • x + y)) '' Set.univ - have hc : IsConnected s := - is_connected_univ.image _ - (continuous_const.prod_mk - ((continuous_id.smul continuous_const).add continuous_const)).ContinuousOn + have hc : IsConnected s := isConnected_univ.image _ (continuous_const.prod_mk + ((continuous_id.smul continuous_const).add continuous_const)).continuousOn have hf : ContinuousOn (fun z : V × V => o.oangle z.1 z.2) s := by - refine' ContinuousAt.continuousOn fun z hz => o.continuous_at_oangle _ _ + refine' ContinuousAt.continuousOn fun z hz => o.continuousAt_oangle _ _ all_goals - simp_rw [s, Set.mem_image] at hz + simp_rw [Set.mem_image] at hz obtain ⟨r', -, rfl⟩ := hz simp only [Prod.fst, Prod.snd] intro hz @@ -928,7 +924,7 @@ theorem oangle_sign_smul_add_right (x y : V) (r : ℝ) : · simpa [hz] using (h' r').1 have hs : ∀ z : V × V, z ∈ s → o.oangle z.1 z.2 ≠ 0 ∧ o.oangle z.1 z.2 ≠ π := by intro z hz - simp_rw [s, Set.mem_image] at hz + simp_rw [Set.mem_image] at hz obtain ⟨r', -, rfl⟩ := hz exact h' r' have hx : (x, y) ∈ s := by @@ -1008,14 +1004,16 @@ theorem oangle_sign_smul_sub_left (x y : V) (r : ℝ) : /-- Subtracting the second vector passed to `oangle` from the first vector negates the sign of the angle. -/ -theorem oangle_sign_sub_right_eq_neg (x y : V) : (o.oangle x (x - y)).sign = -(o.oangle x y).sign := - by rw [← o.oangle_sign_smul_sub_right x y 1, one_smul] +theorem oangle_sign_sub_right_eq_neg (x y : V) : + (o.oangle x (x - y)).sign = -(o.oangle x y).sign := by + rw [← o.oangle_sign_smul_sub_right x y 1, one_smul] #align orientation.oangle_sign_sub_right_eq_neg Orientation.oangle_sign_sub_right_eq_neg /-- Subtracting the first vector passed to `oangle` from the second vector negates the sign of the angle. -/ -theorem oangle_sign_sub_left_eq_neg (x y : V) : (o.oangle (y - x) y).sign = -(o.oangle x y).sign := - by rw [← o.oangle_sign_smul_sub_left x y 1, one_smul] +theorem oangle_sign_sub_left_eq_neg (x y : V) : + (o.oangle (y - x) y).sign = -(o.oangle x y).sign := by + rw [← o.oangle_sign_smul_sub_left x y 1, one_smul] #align orientation.oangle_sign_sub_left_eq_neg Orientation.oangle_sign_sub_left_eq_neg /-- Subtracting the first vector passed to `oangle` from the second vector then swapping the @@ -1035,7 +1033,7 @@ theorem oangle_sign_sub_left_swap (x y : V) : (o.oangle (x - y) x).sign = (o.oan /-- The sign of the angle between a vector, and a linear combination of that vector with a second vector, is the sign of the factor by which the second vector is multiplied in that combination multiplied by the sign of the angle between the two vectors. -/ -@[simp] +-- @[simp] -- Porting note: simp can prove this theorem oangle_sign_smul_add_smul_right (x y : V) (r₁ r₂ : ℝ) : (o.oangle x (r₁ • x + r₂ • y)).sign = SignType.sign r₂ * (o.oangle x y).sign := by rw [← o.oangle_sign_smul_add_right x (r₁ • x + r₂ • y) (-r₁)] @@ -1045,7 +1043,7 @@ theorem oangle_sign_smul_add_smul_right (x y : V) (r₁ r₂ : ℝ) : /-- The sign of the angle between a linear combination of two vectors and the second vector is the sign of the factor by which the first vector is multiplied in that combination multiplied by the sign of the angle between the two vectors. -/ -@[simp] +-- @[simp] -- Porting note: simp can prove this theorem oangle_sign_smul_add_smul_left (x y : V) (r₁ r₂ : ℝ) : (o.oangle (r₁ • x + r₂ • y) y).sign = SignType.sign r₁ * (o.oangle x y).sign := by simp_rw [o.oangle_rev y, Real.Angle.sign_neg, add_comm (r₁ • x), oangle_sign_smul_add_smul_right, @@ -1059,12 +1057,10 @@ theorem oangle_sign_smul_add_smul_smul_add_smul (x y : V) (r₁ r₂ r₃ r₄ : (o.oangle (r₁ • x + r₂ • y) (r₃ • x + r₄ • y)).sign = SignType.sign (r₁ * r₄ - r₂ * r₃) * (o.oangle x y).sign := by by_cases hr₁ : r₁ = 0 - · - rw [hr₁, zero_smul, MulZeroClass.zero_mul, zero_add, zero_sub, Left.sign_neg, + · rw [hr₁, zero_smul, MulZeroClass.zero_mul, zero_add, zero_sub, Left.sign_neg, oangle_sign_smul_left, add_comm, oangle_sign_smul_add_smul_right, oangle_rev, Real.Angle.sign_neg, sign_mul, mul_neg, mul_neg, neg_mul, mul_assoc] - · - rw [← o.oangle_sign_smul_add_right (r₁ • x + r₂ • y) (r₃ • x + r₄ • y) (-r₃ / r₁), smul_add, + · rw [← o.oangle_sign_smul_add_right (r₁ • x + r₂ • y) (r₃ • x + r₄ • y) (-r₃ / r₁), smul_add, smul_smul, smul_smul, div_mul_cancel _ hr₁, neg_smul, ← add_assoc, add_comm (-(r₃ • x)), ← sub_eq_add_neg, sub_add_cancel, ← add_smul, oangle_sign_smul_right, oangle_sign_smul_add_smul_left, ← mul_assoc, ← sign_mul, add_mul, mul_assoc, mul_comm r₂ r₁, ← @@ -1072,6 +1068,7 @@ theorem oangle_sign_smul_add_smul_smul_add_smul (x y : V) (r₁ r₂ r₃ r₄ : mul_comm r₃] #align orientation.oangle_sign_smul_add_smul_smul_add_smul Orientation.oangle_sign_smul_add_smul_smul_add_smul +set_option maxHeartbeats 350000 in /-- A base angle of an isosceles triangle is acute, oriented vector angle form. -/ theorem abs_oangle_sub_left_toReal_lt_pi_div_two {x y : V} (h : ‖x‖ = ‖y‖) : |(o.oangle (y - x) y).toReal| < π / 2 := by @@ -1079,18 +1076,18 @@ theorem abs_oangle_sub_left_toReal_lt_pi_div_two {x y : V} (h : ‖x‖ = ‖y have hs : ((2 : ℤ) • o.oangle (y - x) y).sign = (o.oangle (y - x) y).sign := by conv_rhs => rw [oangle_sign_sub_left_swap] rw [o.oangle_eq_pi_sub_two_zsmul_oangle_sub_of_norm_eq hn h, Real.Angle.sign_pi_sub] - rw [Real.Angle.sign_two_zsmul_eq_sign_iff] at hs + rw [Real.Angle.sign_two_zsmul_eq_sign_iff] at hs rcases hs with (hs | hs) - · rw [oangle_eq_pi_iff_oangle_rev_eq_pi, oangle_eq_pi_iff_same_ray_neg, neg_sub] at hs + · rw [oangle_eq_pi_iff_oangle_rev_eq_pi, oangle_eq_pi_iff_sameRay_neg, neg_sub] at hs rcases hs with ⟨hy, -, hr⟩ - rw [← exists_nonneg_left_iff_sameRay hy] at hr + rw [← exists_nonneg_left_iff_sameRay hy] at hr rcases hr with ⟨r, hr0, hr⟩ - rw [eq_sub_iff_add_eq] at hr - nth_rw 2 [← one_smul ℝ y] at hr - rw [← add_smul] at hr + rw [eq_sub_iff_add_eq] at hr + nth_rw 2 [← one_smul ℝ y] at hr + rw [← add_smul] at hr rw [← hr, norm_smul, Real.norm_eq_abs, abs_of_pos (Left.add_pos_of_nonneg_of_pos hr0 one_pos), - mul_left_eq_self₀, or_iff_left (norm_ne_zero_iff.2 hy), add_left_eq_self] at h - rw [h, zero_add, one_smul] at hr + mul_left_eq_self₀, or_iff_left (norm_ne_zero_iff.2 hy), add_left_eq_self] at h + rw [h, zero_add, one_smul] at hr exact False.elim (hn hr.symm) · exact hs #align orientation.abs_oangle_sub_left_to_real_lt_pi_div_two Orientation.abs_oangle_sub_left_toReal_lt_pi_div_two @@ -1102,4 +1099,3 @@ theorem abs_oangle_sub_right_toReal_lt_pi_div_two {x y : V} (h : ‖x‖ = ‖y #align orientation.abs_oangle_sub_right_to_real_lt_pi_div_two Orientation.abs_oangle_sub_right_toReal_lt_pi_div_two end Orientation -