-
Notifications
You must be signed in to change notification settings - Fork 10
/
CrossProduct.lean
128 lines (106 loc) · 6.4 KB
/
CrossProduct.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
/-
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 to_mathlib.analysis.inner_product_space.cross_product
-/
import Mathlib.Analysis.InnerProductSpace.Dual
import Mathlib.Analysis.InnerProductSpace.Orientation
/-! # The cross-product on an oriented real inner product space of dimension three -/
noncomputable section
open scoped RealInnerProductSpace
open FiniteDimensional
set_option synthInstance.checkSynthOrder false
attribute [local instance] fact_finiteDimensional_of_finrank_eq_succ
set_option synthInstance.checkSynthOrder true
variable (E : Type _) [NormedAddCommGroup E] [InnerProductSpace ℝ E]
/-- The identification of a finite-dimensional inner product space with its algebraic dual. -/
private def to_dual [FiniteDimensional ℝ E] : E ≃ₗ[ℝ] E →ₗ[ℝ] ℝ :=
(InnerProductSpace.toDual ℝ E).toLinearEquiv ≪≫ₗ LinearMap.toContinuousLinearMap.symm
namespace Orientation
variable {E}
variable [Fact (finrank ℝ E = 3)] (ω : Orientation ℝ E (Fin 3))
/-- Linear map from `E` to `E →ₗ[ℝ] E` constructed from a 3-form `Ω` on `E` and an identification of
`E` with its dual. Effectively, the Hodge star operation. (Under appropriate hypotheses it turns
out that the image of this map is in `𝔰𝔬(E)`, the skew-symmetric operators, which can be identified
with `Λ²E`.) -/
def crossProduct : E →ₗ[ℝ] 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
let y' : AlternatingMap ℝ E ℝ (Fin 1) →ₗ[ℝ] E :=
(LinearMap.llcomp ℝ (AlternatingMap ℝ E ℝ (Fin 1)) (E →ₗ[ℝ] ℝ) E (to_dual E).symm) y
let u : AlternatingMap ℝ E ℝ (Fin 2) →ₗ[ℝ] E →ₗ[ℝ] E :=
LinearMap.llcomp ℝ E (AlternatingMap ℝ E ℝ (Fin 1)) _ y' ∘ₗ AlternatingMap.curryLeftLinearMap
exact u ∘ₗ AlternatingMap.curryLeftLinearMap (n := 2) ω.volumeForm
local infixl:100 "×₃" => ω.crossProduct
theorem crossProduct_apply_self (v : E) : v×₃v = 0 := by simp [crossProduct]
theorem inner_crossProduct_apply (u v w : E) : ⟪u×₃v, w⟫ = ω.volumeForm ![u, v, w] := by
simp only [crossProduct, to_dual, LinearEquiv.trans_symm, LinearEquiv.symm_symm,
LinearIsometryEquiv.toLinearEquiv_symm, AlternatingMap.curryLeftLinearMap_apply,
LinearMap.coe_comp, Function.comp_apply, LinearMap.llcomp_apply, LinearEquiv.coe_coe,
LinearEquiv.trans_apply, LinearIsometryEquiv.coe_toLinearEquiv, LinearMap.coe_comp]
rw [InnerProductSpace.toDual_symm_apply]
simp only [LinearMap.coe_toContinuousLinearMap', Function.comp_apply, LinearMap.llcomp_apply,
LinearEquiv.coe_coe, AlternatingMap.constLinearEquivOfIsEmpty_symm_apply,
Matrix.zero_empty, AlternatingMap.curryLeftLinearMap_apply,
AlternatingMap.curryLeft_apply_apply]
theorem inner_crossProduct_apply_self (u : E) (v : (ℝ ∙ u)ᗮ) : ⟪u×₃v, u⟫ = 0 := by
rw [ω.inner_crossProduct_apply u v u]
refine' ω.volumeForm.map_eq_zero_of_eq ![u, v, u] _ (by norm_num : (0 : Fin 3) ≠ 2)
simp
theorem inner_crossProduct_apply_apply_self (u : E) (v : (ℝ ∙ u)ᗮ) : ⟪u×₃v, v⟫ = 0 := by
rw [ω.inner_crossProduct_apply u v v]
refine' ω.volumeForm.map_eq_zero_of_eq ![u, v, v] _ (by norm_num : (1 : Fin 3) ≠ 2)
simp
/-- The map `cross_product`, upgraded from linear to continuous-linear; useful for calculus. -/
def crossProduct' : E →L[ℝ] E →L[ℝ] E :=
LinearMap.toContinuousLinearMap
(↑(LinearMap.toContinuousLinearMap : (E →ₗ[ℝ] E) ≃ₗ[ℝ] E →L[ℝ] E) ∘ₗ ω.crossProduct)
@[simp]
theorem crossProduct'_apply (v : E) :
ω.crossProduct' v = LinearMap.toContinuousLinearMap (ω.crossProduct v) :=
rfl
theorem norm_crossProduct (u : E) (v : (ℝ ∙ u)ᗮ) : ‖u×₃v‖ = ‖u‖ * ‖v‖ := by
classical
refine' le_antisymm _ _
· cases' eq_or_lt_of_le (norm_nonneg (u×₃v)) with h h
· rw [← h]
positivity
refine' le_of_mul_le_mul_right _ h
rw [← real_inner_self_eq_norm_mul_norm]
simpa only [inner_crossProduct_apply, Fin.mk_zero, Fin.prod_univ_succ, Finset.card_singleton,
Finset.prod_const, Fintype.univ_ofSubsingleton, Matrix.cons_val_fin_one, Matrix.cons_val_succ,
Matrix.cons_val_zero, mul_assoc, Nat.zero_eq, pow_one, Submodule.coe_norm] using
ω.volumeForm_apply_le ![u, v, u×₃v]
let K : Submodule ℝ E := Submodule.span ℝ ({u, ↑v} : Set E)
have : Nontrivial Kᗮ :=
by
apply @FiniteDimensional.nontrivial_of_finrank_pos ℝ
have : finrank ℝ K ≤ Finset.card {u, (v : E)} := by
simpa [Set.toFinset_singleton] using finrank_span_le_card ({u, ↑v} : Set E)
have : Finset.card {u, (v : E)} ≤ Finset.card {(v : E)} + 1 := Finset.card_insert_le u {↑v}
have : Finset.card {(v : E)} = 1 := Finset.card_singleton (v : E)
have : finrank ℝ K + finrank ℝ Kᗮ = finrank ℝ E := K.finrank_add_finrank_orthogonal
have : finrank ℝ E = 3 := Fact.out
linarith
obtain ⟨w, hw⟩ : ∃ w : Kᗮ, w ≠ 0 := exists_ne 0
have H : Pairwise fun i j => ⟪![u, v, w] i, ![u, v, w] j⟫ = 0 :=
by
intro i j hij
have h1 : ⟪u, v⟫ = 0 := v.2 _ (Submodule.mem_span_singleton_self _)
have h2 : ⟪(v : E), w⟫ = 0 := w.2 _ (Submodule.subset_span (by simp))
have h3 : ⟪u, w⟫ = 0 := w.2 _ (Submodule.subset_span (by simp))
fin_cases i <;> fin_cases j <;> norm_num at hij <;> simp [h1, h2, h3] <;>
rw [real_inner_comm] <;>
assumption
refine' le_of_mul_le_mul_right _ (by rwa [norm_pos_iff] : 0 < ‖w‖)
-- Cauchy-Schwarz inequality for `u ×₃ v` and `w`
simpa only [inner_crossProduct_apply, ω.abs_volumeForm_apply_of_pairwise_orthogonal H,
inner_crossProduct_apply, Fin.mk_zero, Fin.prod_univ_succ, Finset.card_singleton,
Finset.prod_const, Fintype.univ_ofSubsingleton, Matrix.cons_val_fin_one, Matrix.cons_val_succ,
Matrix.cons_val_zero, Nat.zero_eq, pow_one, mul_assoc] using abs_real_inner_le_norm (u×₃v) w
theorem isometry_on_crossProduct (u : Metric.sphere (0 : E) 1) (v : (ℝ ∙ (u : E))ᗮ) :
‖u×₃v‖ = ‖v‖ := by simp [norm_crossProduct]
end Orientation