-- Mathlib/Analysis/InnerProductSpace/Orientation.lean
theorem abs_volumeForm_apply_le (v : Fin n → E) : |o.volumeForm v| ≤ ∏ i : Fin n, ‖v i‖

Proof state:
case succ.h1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
this✝ : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin n.succ)
b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis this v
hb : b.toBasis.det v = ∏ i : Fin n.succ, inner (b i) (v i)
⊢ ∀ i ∈ Finset.univ, |inner (b i) (v i)| ≤ ‖v i‖

Tactic:
intro i _

Result:
case succ.h1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
this✝ : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin n.succ)
b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis this v
hb : b.toBasis.det v = ∏ i : Fin n.succ, inner (b i) (v i)
i : Fin n.succ
a✝ : i ∈ Finset.univ
⊢ |inner (b i) (v i)| ≤ ‖v i‖

Proof state:
case succ.h0
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
this✝ : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin n.succ)
b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis this v
hb : b.toBasis.det v = ∏ i : Fin n.succ, inner (b i) (v i)
⊢ ∀ i ∈ Finset.univ, 0 ≤ |inner (b i) (v i)|

Tactic:
intro i _

Result:
case succ.h0
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
this✝ : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin n.succ)
b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis this v
hb : b.toBasis.det v = ∏ i : Fin n.succ, inner (b i) (v i)
i : Fin n.succ
a✝ : i ∈ Finset.univ
⊢ 0 ≤ |inner (b i) (v i)|

Proof state:
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
this✝ : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin n.succ)
b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis this v
⊢ |o.volumeForm v| ≤ ∏ i : Fin (n + 1), ‖v i‖

Tactic:
have hb : b.toBasis.det v = ∏ i, ⟪b i, v i⟫ := gramSchmidtOrthonormalBasis_det this v

Result:
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
this✝ : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin n.succ)
b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis this v
hb : b.toBasis.det v = ∏ i : Fin n.succ, inner (b i) (v i)
⊢ |o.volumeForm v| ≤ ∏ i : Fin (n + 1), ‖v i‖

Proof state:
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
⊢ |o.volumeForm v| ≤ ∏ i : Fin (n + 1), ‖v i‖

Tactic:
haveI : FiniteDimensional ℝ E := .of_fact_finrank_eq_succ n

Result:
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
this : FiniteDimensional ℝ E
⊢ |o.volumeForm v| ≤ ∏ i : Fin (n + 1), ‖v i‖

Proof state:
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
this : FiniteDimensional ℝ E
⊢ |o.volumeForm v| ≤ ∏ i : Fin (n + 1), ‖v i‖

Tactic:
have : finrank ℝ E = Fintype.card (Fin n.succ) := by simpa using _i.out

Result:
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
this✝ : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin n.succ)
⊢ |o.volumeForm v| ≤ ∏ i : Fin (n + 1), ‖v i‖

Proof state:
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
this✝ : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin n.succ)
b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis this v
hb : b.toBasis.det v = ∏ i : Fin n.succ, inner (b i) (v i)
⊢ ∏ x : Fin n.succ, |inner (b x) (v x)| ≤ ∏ i : Fin (n + 1), ‖v i‖

Tactic:
apply Finset.prod_le_prod

Result:
case succ.h0
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
this✝ : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin n.succ)
b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis this v
hb : b.toBasis.det v = ∏ i : Fin n.succ, inner (b i) (v i)
⊢ ∀ i ∈ Finset.univ, 0 ≤ |inner (b i) (v i)|

case succ.h1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
this✝ : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin n.succ)
b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis this v
hb : b.toBasis.det v = ∏ i : Fin n.succ, inner (b i) (v i)
⊢ ∀ i ∈ Finset.univ, |inner (b i) (v i)| ≤ ‖v i‖

Proof state:
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
this✝ : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin n.succ)
b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis this v
hb : b.toBasis.det v = ∏ i : Fin n.succ, inner (b i) (v i)
⊢ |o.volumeForm v| ≤ ∏ i : Fin (n + 1), ‖v i‖

Tactic:
rw [o.volumeForm_robust' b, hb, Finset.abs_prod]

Result:
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
this✝ : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin n.succ)
b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis this v
hb : b.toBasis.det v = ∏ i : Fin n.succ, inner (b i) (v i)
⊢ ∏ x : Fin n.succ, |inner (b x) (v x)| ≤ ∏ i : Fin (n + 1), ‖v i‖

Proof state:
case succ.h0
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
this✝ : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin n.succ)
b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis this v
hb : b.toBasis.det v = ∏ i : Fin n.succ, inner (b i) (v i)
i : Fin n.succ
a✝ : i ∈ Finset.univ
⊢ 0 ≤ |inner (b i) (v i)|

Tactic:
positivity

Result:
no goals

Proof state:
case h.e'_4
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n + 1)
o : Orientation ℝ E (Fin (n + 1))
v : Fin (n + 1) → E
this✝ : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin n.succ)
b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis this v
hb : b.toBasis.det v = ∏ i : Fin n.succ, inner (b i) (v i)
i : Fin n.succ
a✝ : i ∈ Finset.univ
⊢ ‖v i‖ = ‖b i‖ * ‖v i‖

Tactic:
simp [b.orthonormal.1 i]

Result:
no goals

Proof state:
case zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = 0)
o : Orientation ℝ E (Fin 0)
v : Fin 0 → E
⊢ |o.volumeForm v| ≤ ∏ i : Fin 0, ‖v i‖

Tactic:
refine o.eq_or_eq_neg_of_isEmpty.elim ?_ ?_ <;> rintro rfl <;> simp

Result:
no goals