English
If the vectors v_i are pairwise orthogonal, the absolute value of the volume form equals the product of their norms.
Русский
Если векторы v_i попарно ортогональны, модуль объемной формы равен произведению их норм.
LaTeX
$$$$ |o.volumeForm(v)| = \prod_{i=1}^n \|v_i\| \quad\text{when } \langle v_i, v_j \rangle = 0 \ (i \neq j). $$$$
Lean4
/-- Let `v` be an indexed family of `n` orthogonal vectors in an oriented `n`-dimensional
real inner product space `E`. The output of the volume form of `E` when evaluated on `v` is, up to
sign, the product of the norms of the vectors `v i`. -/
theorem abs_volumeForm_apply_of_pairwise_orthogonal {v : Fin n → E} (hv : Pairwise fun i j => ⟪v i, v j⟫ = 0) :
|o.volumeForm v| = ∏ i : Fin n, ‖v i‖ := by
rcases n with - | n
· refine o.eq_or_eq_neg_of_isEmpty.elim ?_ ?_ <;> rintro rfl <;> simp
haveI : FiniteDimensional ℝ E := .of_fact_finrank_eq_succ n
have hdim : finrank ℝ E = Fintype.card (Fin n.succ) := by simpa using _i.out
let b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis hdim v
have hb : b.toBasis.det v = ∏ i, ⟪b i, v i⟫ := gramSchmidtOrthonormalBasis_det hdim v
rw [o.volumeForm_robust' b, hb, Finset.abs_prod]
by_cases h : ∃ i, v i = 0
· obtain ⟨i, hi⟩ := h
rw [Finset.prod_eq_zero (Finset.mem_univ i), Finset.prod_eq_zero (Finset.mem_univ i)] <;> simp [hi]
push_neg at h
congr
ext i
have hb : b i = ‖v i‖⁻¹ • v i := gramSchmidtOrthonormalBasis_apply_of_orthogonal hdim hv (h i)
simp only [hb, inner_smul_left, real_inner_self_eq_norm_mul_norm, RCLike.conj_to_real]
rw [abs_of_nonneg]
· field_simp
· positivity
