Theorems · Theorem · functional analysis

Orientation.abs_volumeForm_apply_le

∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {n : ℕ}
  [_i : Fact (Module.finrank ℝ E = n)] (o : Orientation ℝ E (Fin n)) (v : Fin n → E), |o.volumeForm v| ≤ ∏ i, ‖v i‖

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.

Defined in

Mathlib.Analysis.InnerProductSpace.Orientation

Cited by

2 results in Mathlib

Foundations

Depth 250 from the axioms · uses propext, Classical.choice, Quot.sound

Assumes

NormedAddCommGroupInnerProductSpaceFact