feat(analysis/inner_product_space/two_dim): volume/area form of negat…

…ed orientation (#16939)

src/analysis/inner_product_space/orientation.lean

@@ -57,6 +57,17 @@ begin
   linarith,
 end
 
+/-- The change-of-basis matrix between two orthonormal bases with the opposite orientations has
+determinant -1. -/
+lemma det_to_matrix_orthonormal_basis_of_opposite_orientation
+  (h : e.to_basis.orientation ≠ f.to_basis.orientation) :
+  e.to_basis.det f = -1 :=
+begin
+  contrapose! h,
+  simp [e.to_basis.orientation_eq_iff_det_pos,
+    (e.det_to_matrix_orthonormal_basis_real f).resolve_right h],
+end
+
 variables {e f}
 
 /-- Two orthonormal bases with the same orientation determine the same "determinant" top-dimensional
@@ -73,7 +84,17 @@ begin
     simp [e.det_to_matrix_orthonormal_basis_of_same_orientation f h], },
 end
 
-variables (e)
+variables (e f)
+
+/-- Two orthonormal bases with opposite orientations determine opposite "determinant"
+top-dimensional forms on `E`. -/
+lemma det_eq_neg_det_of_opposite_orientation
+  (h : e.to_basis.orientation ≠ f.to_basis.orientation) :
+  e.to_basis.det = -f.to_basis.det :=
+begin
+  rw e.to_basis.det.eq_smul_basis_det f.to_basis,
+  simp [e.det_to_matrix_orthonormal_basis_of_opposite_orientation f h],
+end
 
 section adjust_to_orientation
 include ne
@@ -161,8 +182,7 @@ begin
   classical,
   unfreezingI { cases n },
   { let opos : alternating_map ℝ E ℝ (fin 0) := alternating_map.const_of_is_empty ℝ E (1:ℝ),
-    let oneg : alternating_map ℝ E ℝ (fin 0) := alternating_map.const_of_is_empty ℝ E (-1:ℝ),
-    exact o.eq_or_eq_neg_of_is_empty.by_cases (λ _, opos) (λ _, oneg) },
+    exact o.eq_or_eq_neg_of_is_empty.by_cases (λ _, opos) (λ _, -opos) },
   { exact (o.fin_orthonormal_basis n.succ_pos _i.out).to_basis.det }
 end
 
@@ -171,11 +191,11 @@ omit _i o
 @[simp] lemma volume_form_zero_pos [_i : fact (finrank ℝ E = 0)] :
   orientation.volume_form (positive_orientation : orientation ℝ E (fin 0))
   = alternating_map.const_linear_equiv_of_is_empty 1 :=
-by simp [volume_form, or.by_cases, dif_pos]
+by simp [volume_form, or.by_cases, if_pos]
 
-@[simp] lemma volume_form_zero_neg [_i : fact (finrank ℝ E = 0)] :
+lemma volume_form_zero_neg [_i : fact (finrank ℝ E = 0)] :
   orientation.volume_form (-positive_orientation : orientation ℝ E (fin 0))
-  = alternating_map.const_linear_equiv_of_is_empty (-1) :=
+  = - alternating_map.const_linear_equiv_of_is_empty 1 :=
 begin
   dsimp [volume_form, or.by_cases, positive_orientation],
   apply if_neg,
@@ -200,6 +220,34 @@ begin
     exact o.fin_orthonormal_basis_orientation _ _ },
 end
 
+/-- The volume form on an oriented real inner product space can be evaluated as the determinant with
+respect to any orthonormal basis of the space compatible with the orientation. -/
+lemma volume_form_robust_neg (b : orthonormal_basis (fin n) ℝ E)
+  (hb : b.to_basis.orientation ≠ o) :
+  o.volume_form = - b.to_basis.det :=
+begin
+  unfreezingI { cases n },
+  { have : positive_orientation ≠ o := by rwa b.to_basis.orientation_is_empty at hb,
+    simp [volume_form, or.by_cases, dif_neg this.symm] },
+  let e : orthonormal_basis (fin n.succ) ℝ E := o.fin_orthonormal_basis n.succ_pos (fact.out _),
+  dsimp [volume_form],
+  apply e.det_eq_neg_det_of_opposite_orientation b,
+  convert hb.symm,
+  exact o.fin_orthonormal_basis_orientation _ _,
+end
+
+@[simp] lemma volume_form_neg_orientation : (-o).volume_form = - o.volume_form :=
+begin
+  unfreezingI { cases n },
+  { refine o.eq_or_eq_neg_of_is_empty.by_cases _ _; rintros rfl; simp [volume_form_zero_neg] },
+  let e : orthonormal_basis (fin n.succ) ℝ E := o.fin_orthonormal_basis n.succ_pos (fact.out _),
+  have h₁ : e.to_basis.orientation = o := o.fin_orthonormal_basis_orientation _ _,
+  have h₂ : e.to_basis.orientation ≠ -o,
+  { symmetry,
+    rw [e.to_basis.orientation_ne_iff_eq_neg, h₁] },
+  rw [o.volume_form_robust e h₁, (-o).volume_form_robust_neg e h₂],
+end
+
 lemma volume_form_robust' (b : orthonormal_basis (fin n) ℝ E) (v : fin n → E) :
   |o.volume_form v| = |b.to_basis.det v| :=
 begin

src/analysis/inner_product_space/two_dim.lean

@@ -95,6 +95,12 @@ begin
   { norm_num }
 end
 
+@[simp] lemma area_form_neg_orientation : (-o).area_form = -o.area_form :=
+begin
+  ext x y,
+  simp [area_form_to_volume_form]
+end
+
 /-- Continuous linear map version of `orientation.area_form`, useful for calculus. -/
 def area_form' : E →L[ℝ] (E →L[ℝ] ℝ) :=
 ((↑(linear_map.to_continuous_linear_map : (E →ₗ[ℝ] ℝ) ≃ₗ[ℝ] (E →L[ℝ] ℝ)))
@@ -243,6 +249,19 @@ by simp
   linear_isometry_equiv.trans J J = linear_isometry_equiv.neg ℝ :=
 by ext; simp
 
+lemma right_angle_rotation_neg_orientation (x : E) :
+  (-o).right_angle_rotation x = - o.right_angle_rotation x :=
+begin
+  apply ext_inner_right ℝ,
+  intros y,
+  rw inner_right_angle_rotation_left,
+  simp
+end
+
+@[simp] lemma right_angle_rotation_trans_neg_orientation :
+  (-o).right_angle_rotation = o.right_angle_rotation.trans (linear_isometry_equiv.neg ℝ) :=
+linear_isometry_equiv.ext $ o.right_angle_rotation_neg_orientation
+
 /-- 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 basis_right_angle_rotation (x : E) (hx : x ≠ 0) : basis (fin 2) ℝ E :=
@@ -391,6 +410,9 @@ begin
   linear_combination - o.kahler x y * complex.I_sq,
 end
 
+@[simp] lemma kahler_neg_orientation (x y : E) : (-o).kahler x y = conj (o.kahler x y) :=
+by simp [kahler_apply_apply]
+
 lemma kahler_mul (a x y : E) : o.kahler x a * o.kahler a y = ∥a∥ ^ 2 * o.kahler x y :=
 begin
   transitivity (↑(∥a∥ ^ 2) : ℂ) * o.kahler x y,