English
The absolute value of the volume form applied to a vector-valued n-tuple is bounded by the product of the norms of the vectors.
Русский
Абсолютное значение объемной формы, примененной к набору векторов, не превышает произведение норм этих векторов.
LaTeX
$$$$ |o.volumeForm(v)| \le \prod_{i=1}^n \|v_i\|. $$$$
Lean4
/-- Let `v` be an indexed family of `n` vectors in an oriented `n`-dimensional real inner
product space `E`. The output of the volume form of `E` when evaluated on `v` is bounded in absolute
value by the product of the norms of the vectors `v i`. -/
theorem abs_volumeForm_apply_le (v : Fin n → E) : |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 : finrank ℝ E = Fintype.card (Fin n.succ) := by simpa using _i.out
let b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis this v
have hb : b.toBasis.det v = ∏ i, ⟪b i, v i⟫ := gramSchmidtOrthonormalBasis_det this v
rw [o.volumeForm_robust' b, hb, Finset.abs_prod]
apply Finset.prod_le_prod
· intro i _
positivity
intro i _
convert abs_real_inner_le_norm (b i) (v i)
simp [b.orthonormal.1 i]
