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

case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
v : Fin (Nat.succ n) → E
⊢ abs (↑(volumeForm o) v) ≤ ∏ i : Fin (Nat.succ n), ‖v i‖
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = n)
o : Orientation ℝ E (Fin n)
v : Fin n → E
⊢ abs (↑(volumeForm o) v) ≤ ∏ i : Fin n, ‖v i‖
cases' n with n
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
v : Fin (Nat.succ n) → E
this : FiniteDimensional ℝ E
⊢ abs (↑(volumeForm o) v) ≤ ∏ i : Fin (Nat.succ n), ‖v i‖
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
v : Fin (Nat.succ n) → E
⊢ abs (↑(volumeForm o) v) ≤ ∏ i : Fin (Nat.succ n), ‖v i‖
haveI : FiniteDimensional ℝ E := fact_finiteDimensional_of_finrank_eq_succ n
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
v : Fin (Nat.succ n) → E
this✝ : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
⊢ abs (↑(volumeForm o) v) ≤ ∏ i : Fin (Nat.succ n), ‖v i‖
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
v : Fin (Nat.succ n) → E
this : FiniteDimensional ℝ E
⊢ abs (↑(volumeForm o) v) ≤ ∏ i : Fin (Nat.succ n), ‖v i‖
have : finrank ℝ E = Fintype.card (Fin n.succ) := by simpa using _i.out
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
v : Fin (Nat.succ n) → E
this✝ : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E := gramSchmidtOrthonormalBasis this v
⊢ abs (↑(volumeForm o) v) ≤ ∏ i : Fin (Nat.succ n), ‖v i‖
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
v : Fin (Nat.succ n) → E
this✝ : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
⊢ abs (↑(volumeForm o) v) ≤ ∏ i : Fin (Nat.succ n), ‖v i‖
let b : OrthonormalBasis (Fin n.succ) ℝ E := gramSchmidtOrthonormalBasis this v
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
v : Fin (Nat.succ n) → E
this✝ : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E := gramSchmidtOrthonormalBasis this v
hb : ↑(Basis.det (OrthonormalBasis.toBasis b)) v = ∏ i : Fin (Nat.succ n), inner (↑b i) (v i)
⊢ abs (↑(volumeForm o) v) ≤ ∏ i : Fin (Nat.succ n), ‖v i‖
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
v : Fin (Nat.succ n) → E
this✝ : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E := gramSchmidtOrthonormalBasis this v
⊢ abs (↑(volumeForm o) v) ≤ ∏ i : Fin (Nat.succ n), ‖v i‖
have hb : b.toBasis.det v = ∏ i, ⟪b i, v i⟫ := gramSchmidtOrthonormalBasis_det this v
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
v : Fin (Nat.succ n) → E
this✝ : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E := gramSchmidtOrthonormalBasis this v
hb : ↑(Basis.det (OrthonormalBasis.toBasis b)) v = ∏ i : Fin (Nat.succ n), inner (↑b i) (v i)
⊢ ∏ x : Fin (Nat.succ n), abs (inner (↑b x) (v x)) ≤ ∏ i : Fin (Nat.succ n), ‖v i‖
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
v : Fin (Nat.succ n) → E
this✝ : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E := gramSchmidtOrthonormalBasis this v
hb : ↑(Basis.det (OrthonormalBasis.toBasis b)) v = ∏ i : Fin (Nat.succ n), inner (↑b i) (v i)
⊢ abs (↑(volumeForm o) v) ≤ ∏ i : Fin (Nat.succ n), ‖v i‖
rw [o.volumeForm_robust' b, hb, Finset.abs_prod]
case succ.h0
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
v : Fin (Nat.succ n) → E
this✝ : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E := gramSchmidtOrthonormalBasis this v
hb : ↑(Basis.det (OrthonormalBasis.toBasis b)) v = ∏ i : Fin (Nat.succ n), inner (↑b i) (v i)
⊢ ∀ (i : Fin (Nat.succ n)), i ∈ Finset.univ → 0 ≤ abs (inner (↑b i) (v i))

case succ.h1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
v : Fin (Nat.succ n) → E
this✝ : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E := gramSchmidtOrthonormalBasis this v
hb : ↑(Basis.det (OrthonormalBasis.toBasis b)) v = ∏ i : Fin (Nat.succ n), inner (↑b i) (v i)
⊢ ∀ (i : Fin (Nat.succ n)), i ∈ Finset.univ → abs (inner (↑b i) (v i)) ≤ ‖v i‖
case succ
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
v : Fin (Nat.succ n) → E
this✝ : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E := gramSchmidtOrthonormalBasis this v
hb : ↑(Basis.det (OrthonormalBasis.toBasis b)) v = ∏ i : Fin (Nat.succ n), inner (↑b i) (v i)
⊢ ∏ x : Fin (Nat.succ n), abs (inner (↑b x) (v x)) ≤ ∏ i : Fin (Nat.succ n), ‖v i‖
apply Finset.prod_le_prod
case succ.h1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
v : Fin (Nat.succ n) → E
this✝ : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E := gramSchmidtOrthonormalBasis this v
hb : ↑(Basis.det (OrthonormalBasis.toBasis b)) v = ∏ i : Fin (Nat.succ n), inner (↑b i) (v i)
i : Fin (Nat.succ n)
a✝ : i ∈ Finset.univ
⊢ abs (inner (↑b i) (v i)) ≤ ‖v i‖
case succ.h1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
v : Fin (Nat.succ n) → E
this✝ : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E := gramSchmidtOrthonormalBasis this v
hb : ↑(Basis.det (OrthonormalBasis.toBasis b)) v = ∏ i : Fin (Nat.succ n), inner (↑b i) (v i)
⊢ ∀ (i : Fin (Nat.succ n)), i ∈ Finset.univ → abs (inner (↑b i) (v i)) ≤ ‖v i‖
intro i _
case h.e'_4
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
v : Fin (Nat.succ n) → E
this✝ : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E := gramSchmidtOrthonormalBasis this v
hb : ↑(Basis.det (OrthonormalBasis.toBasis b)) v = ∏ i : Fin (Nat.succ n), inner (↑b i) (v i)
i : Fin (Nat.succ n)
a✝ : i ∈ Finset.univ
⊢ ‖v i‖ = ‖↑b i‖ * ‖v i‖
case succ.h1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
v : Fin (Nat.succ n) → E
this✝ : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E := gramSchmidtOrthonormalBasis this v
hb : ↑(Basis.det (OrthonormalBasis.toBasis b)) v = ∏ i : Fin (Nat.succ n), inner (↑b i) (v i)
i : Fin (Nat.succ n)
a✝ : i ∈ Finset.univ
⊢ abs (inner (↑b i) (v i)) ≤ ‖v i‖
convert abs_real_inner_le_norm (b i) (v i)
no goals
case h.e'_4
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
v : Fin (Nat.succ n) → E
this✝ : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E := gramSchmidtOrthonormalBasis this v
hb : ↑(Basis.det (OrthonormalBasis.toBasis b)) v = ∏ i : Fin (Nat.succ n), inner (↑b i) (v i)
i : Fin (Nat.succ n)
a✝ : i ∈ Finset.univ
⊢ ‖v i‖ = ‖↑b i‖ * ‖v i‖
simp [b.orthonormal.1 i]
no goals
case zero
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
_i : Fact (finrank ℝ E = Nat.zero)
o : Orientation ℝ E (Fin Nat.zero)
v : Fin Nat.zero → E
⊢ abs (↑(volumeForm o) v) ≤ ∏ i : Fin Nat.zero, ‖v i‖
refine' o.eq_or_eq_neg_of_isEmpty.elim _ _ <;> rintro rfl <;> simp
no goals
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
v : Fin (Nat.succ n) → E
this : FiniteDimensional ℝ E
⊢ finrank ℝ E = Fintype.card (Fin (Nat.succ n))
simpa using _i.out
case succ.h0
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
v : Fin (Nat.succ n) → E
this✝ : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E := gramSchmidtOrthonormalBasis this v
hb : ↑(Basis.det (OrthonormalBasis.toBasis b)) v = ∏ i : Fin (Nat.succ n), inner (↑b i) (v i)
i : Fin (Nat.succ n)
a✝ : i ∈ Finset.univ
⊢ 0 ≤ abs (inner (↑b i) (v i))
case succ.h0
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
v : Fin (Nat.succ n) → E
this✝ : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E := gramSchmidtOrthonormalBasis this v
hb : ↑(Basis.det (OrthonormalBasis.toBasis b)) v = ∏ i : Fin (Nat.succ n), inner (↑b i) (v i)
⊢ ∀ (i : Fin (Nat.succ n)), i ∈ Finset.univ → 0 ≤ abs (inner (↑b i) (v i))
intro i _
no goals
case succ.h0
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
_i : Fact (finrank ℝ E = Nat.succ n)
o : Orientation ℝ E (Fin (Nat.succ n))
v : Fin (Nat.succ n) → E
this✝ : FiniteDimensional ℝ E
this : finrank ℝ E = Fintype.card (Fin (Nat.succ n))
b : OrthonormalBasis (Fin (Nat.succ n)) ℝ E := gramSchmidtOrthonormalBasis this v
hb : ↑(Basis.det (OrthonormalBasis.toBasis b)) v = ∏ i : Fin (Nat.succ n), inner (↑b i) (v i)
i : Fin (Nat.succ n)
a✝ : i ∈ Finset.univ
⊢ 0 ≤ abs (inner (↑b i) (v i))
positivity