Theorem: smulCmmap_norm (Ray/Misc/Multilinear.lean)

State before:
n : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : NormedAddCommGroup B
inst✝ : NormedSpace 𝕜 B
x : ContinuousMultilinearMap 𝕜 (fun x => A) 𝕜
xs : ContinuousMultilinearMap 𝕜 (fun x => A) B
⊢ ‖smulCmmap 𝕜 A B x xs‖ ≤ ‖x‖ * ‖xs‖
Tactic:
apply ContinuousMultilinearMap.opNorm_le_bound
State after:
case hMp
n : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : NormedAddCommGroup B
inst✝ : NormedSpace 𝕜 B
x : ContinuousMultilinearMap 𝕜 (fun x => A) 𝕜
xs : ContinuousMultilinearMap 𝕜 (fun x => A) B
⊢ 0 ≤ ‖x‖ * ‖xs‖

case hM
n : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : NormedAddCommGroup B
inst✝ : NormedSpace 𝕜 B
x : ContinuousMultilinearMap 𝕜 (fun x => A) 𝕜
xs : ContinuousMultilinearMap 𝕜 (fun x => A) B
⊢ ∀ (m : Fin (n + 1) → A), ‖(smulCmmap 𝕜 A B x xs) m‖ ≤ ‖x‖ * ‖xs‖ * Finset.univ.prod fun i => ‖m i‖

State before:
case hMp
n : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : NormedAddCommGroup B
inst✝ : NormedSpace 𝕜 B
x : ContinuousMultilinearMap 𝕜 (fun x => A) 𝕜
xs : ContinuousMultilinearMap 𝕜 (fun x => A) B
⊢ 0 ≤ ‖x‖ * ‖xs‖

case hM
n : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : NormedAddCommGroup B
inst✝ : NormedSpace 𝕜 B
x : ContinuousMultilinearMap 𝕜 (fun x => A) 𝕜
xs : ContinuousMultilinearMap 𝕜 (fun x => A) B
⊢ ∀ (m : Fin (n + 1) → A), ‖(smulCmmap 𝕜 A B x xs) m‖ ≤ ‖x‖ * ‖xs‖ * Finset.univ.prod fun i => ‖m i‖
Tactic:
bound
State after:
case hM
n : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : NormedAddCommGroup B
inst✝ : NormedSpace 𝕜 B
x : ContinuousMultilinearMap 𝕜 (fun x => A) 𝕜
xs : ContinuousMultilinearMap 𝕜 (fun x => A) B
⊢ ∀ (m : Fin (n + 1) → A), ‖(smulCmmap 𝕜 A B x xs) m‖ ≤ ‖x‖ * ‖xs‖ * Finset.univ.prod fun i => ‖m i‖

State before:
case hM
n : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : NormedAddCommGroup B
inst✝ : NormedSpace 𝕜 B
x : ContinuousMultilinearMap 𝕜 (fun x => A) 𝕜
xs : ContinuousMultilinearMap 𝕜 (fun x => A) B
⊢ ∀ (m : Fin (n + 1) → A), ‖(smulCmmap 𝕜 A B x xs) m‖ ≤ ‖x‖ * ‖xs‖ * Finset.univ.prod fun i => ‖m i‖
Tactic:
intro z
State after:
case hM
n : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : NormedAddCommGroup B
inst✝ : NormedSpace 𝕜 B
x : ContinuousMultilinearMap 𝕜 (fun x => A) 𝕜
xs : ContinuousMultilinearMap 𝕜 (fun x => A) B
z : Fin (n + 1) → A
⊢ ‖(smulCmmap 𝕜 A B x xs) z‖ ≤ ‖x‖ * ‖xs‖ * Finset.univ.prod fun i => ‖z i‖

State before:
case hM
n : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : NormedAddCommGroup B
inst✝ : NormedSpace 𝕜 B
x : ContinuousMultilinearMap 𝕜 (fun x => A) 𝕜
xs : ContinuousMultilinearMap 𝕜 (fun x => A) B
z : Fin (n + 1) → A
⊢ ‖(smulCmmap 𝕜 A B x xs) z‖ ≤ ‖x‖ * ‖xs‖ * Finset.univ.prod fun i => ‖z i‖
Tactic:
rw [smulCmmap_apply]
State after:
case hM
n : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : NormedAddCommGroup B
inst✝ : NormedSpace 𝕜 B
x : ContinuousMultilinearMap 𝕜 (fun x => A) 𝕜
xs : ContinuousMultilinearMap 𝕜 (fun x => A) B
z : Fin (n + 1) → A
⊢ ‖(x fun x => z 0) • xs fun i => z i.succ‖ ≤ ‖x‖ * ‖xs‖ * Finset.univ.prod fun i => ‖z i‖

State before:
case hM
n : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : NormedAddCommGroup B
inst✝ : NormedSpace 𝕜 B
x : ContinuousMultilinearMap 𝕜 (fun x => A) 𝕜
xs : ContinuousMultilinearMap 𝕜 (fun x => A) B
z : Fin (n + 1) → A
⊢ ‖(x fun x => z 0) • xs fun i => z i.succ‖ ≤ ‖x‖ * ‖xs‖ * Finset.univ.prod fun i => ‖z i‖
Tactic:
have xb := ContinuousMultilinearMap.le_opNorm x fun _ : Fin 1 ↦ z 0
State after:
case hM
n : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : NormedAddCommGroup B
inst✝ : NormedSpace 𝕜 B
x : ContinuousMultilinearMap 𝕜 (fun x => A) 𝕜
xs : ContinuousMultilinearMap 𝕜 (fun x => A) B
z : Fin (n + 1) → A
xb : ‖x fun x => z 0‖ ≤ ‖x‖ * Finset.univ.prod fun i => ‖z 0‖
⊢ ‖(x fun x => z 0) • xs fun i => z i.succ‖ ≤ ‖x‖ * ‖xs‖ * Finset.univ.prod fun i => ‖z i‖

State before:
case hM
n : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : NormedAddCommGroup B
inst✝ : NormedSpace 𝕜 B
x : ContinuousMultilinearMap 𝕜 (fun x => A) 𝕜
xs : ContinuousMultilinearMap 𝕜 (fun x => A) B
z : Fin (n + 1) → A
xb : ‖x fun x => z 0‖ ≤ ‖x‖ * Finset.univ.prod fun i => ‖z 0‖
⊢ ‖(x fun x => z 0) • xs fun i => z i.succ‖ ≤ ‖x‖ * ‖xs‖ * Finset.univ.prod fun i => ‖z i‖
Tactic:
have xsb := ContinuousMultilinearMap.le_opNorm xs fun i : Fin n ↦ z i.succ
State after:
case hM
n : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : NormedAddCommGroup B
inst✝ : NormedSpace 𝕜 B
x : ContinuousMultilinearMap 𝕜 (fun x => A) 𝕜
xs : ContinuousMultilinearMap 𝕜 (fun x => A) B
z : Fin (n + 1) → A
xb : ‖x fun x => z 0‖ ≤ ‖x‖ * Finset.univ.prod fun i => ‖z 0‖
xsb : ‖xs fun i => z i.succ‖ ≤ ‖xs‖ * Finset.univ.prod fun i => ‖z i.succ‖
⊢ ‖(x fun x => z 0) • xs fun i => z i.succ‖ ≤ ‖x‖ * ‖xs‖ * Finset.univ.prod fun i => ‖z i‖

State before:
case hM
n : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : NormedAddCommGroup B
inst✝ : NormedSpace 𝕜 B
x : ContinuousMultilinearMap 𝕜 (fun x => A) 𝕜
xs : ContinuousMultilinearMap 𝕜 (fun x => A) B
z : Fin (n + 1) → A
xb : ‖x fun x => z 0‖ ≤ ‖x‖ * Finset.univ.prod fun i => ‖z 0‖
xsb : ‖xs fun i => z i.succ‖ ≤ ‖xs‖ * Finset.univ.prod fun i => ‖z i.succ‖
⊢ ‖(x fun x => z 0) • xs fun i => z i.succ‖ ≤ ‖x‖ * ‖xs‖ * Finset.univ.prod fun i => ‖z i‖
Tactic:
simp only [Finset.univ_unique, Fin.default_eq_zero, Finset.prod_const, Finset.card_singleton,
  pow_one] at xb xsb
State after:
case hM
n : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : NormedAddCommGroup B
inst✝ : NormedSpace 𝕜 B
x : ContinuousMultilinearMap 𝕜 (fun x => A) 𝕜
xs : ContinuousMultilinearMap 𝕜 (fun x => A) B
z : Fin (n + 1) → A
xsb : ‖xs fun i => z i.succ‖ ≤ ‖xs‖ * Finset.univ.prod fun i => ‖z i.succ‖
xb : ‖x fun x => z 0‖ ≤ ‖x‖ * ‖z 0‖
⊢ ‖(x fun x => z 0) • xs fun i => z i.succ‖ ≤ ‖x‖ * ‖xs‖ * Finset.univ.prod fun i => ‖z i‖

State before:
case hM
n : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : NormedAddCommGroup B
inst✝ : NormedSpace 𝕜 B
x : ContinuousMultilinearMap 𝕜 (fun x => A) 𝕜
xs : ContinuousMultilinearMap 𝕜 (fun x => A) B
z : Fin (n + 1) → A
xsb : ‖xs fun i => z i.succ‖ ≤ ‖xs‖ * Finset.univ.prod fun i => ‖z i.succ‖
xb : ‖x fun x => z 0‖ ≤ ‖x‖ * ‖z 0‖
⊢ ‖(x fun x => z 0) • xs fun i => z i.succ‖ ≤ ‖x‖ * ‖xs‖ * Finset.univ.prod fun i => ‖z i‖
Tactic:
have e0 := Fin.prod_cons ‖z 0‖ fun i : Fin n ↦ ‖z i.succ‖
State after:
case hM
n : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : NormedAddCommGroup B
inst✝ : NormedSpace 𝕜 B
x : ContinuousMultilinearMap 𝕜 (fun x => A) 𝕜
xs : ContinuousMultilinearMap 𝕜 (fun x => A) B
z : Fin (n + 1) → A
xsb : ‖xs fun i => z i.succ‖ ≤ ‖xs‖ * Finset.univ.prod fun i => ‖z i.succ‖
xb : ‖x fun x => z 0‖ ≤ ‖x‖ * ‖z 0‖
e0 : (Finset.univ.prod fun i => Fin.cons ‖z 0‖ (fun i => ‖z i.succ‖) i) = ‖z 0‖ * Finset.univ.prod fun i => ‖z i.succ‖
⊢ ‖(x fun x => z 0) • xs fun i => z i.succ‖ ≤ ‖x‖ * ‖xs‖ * Finset.univ.prod fun i => ‖z i‖

State before:
case hM
n : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : NormedAddCommGroup B
inst✝ : NormedSpace 𝕜 B
x : ContinuousMultilinearMap 𝕜 (fun x => A) 𝕜
xs : ContinuousMultilinearMap 𝕜 (fun x => A) B
z : Fin (n + 1) → A
xsb : ‖xs fun i => z i.succ‖ ≤ ‖xs‖ * Finset.univ.prod fun i => ‖z i.succ‖
xb : ‖x fun x => z 0‖ ≤ ‖x‖ * ‖z 0‖
e0 : (Finset.univ.prod fun i => Fin.cons ‖z 0‖ (fun i => ‖z i.succ‖) i) = ‖z 0‖ * Finset.univ.prod fun i => ‖z i.succ‖
⊢ ‖(x fun x => z 0) • xs fun i => z i.succ‖ ≤ ‖x‖ * ‖xs‖ * Finset.univ.prod fun i => ‖z i‖
Tactic:
have e1 : ‖z 0‖ = (fun i : Fin (n + 1) ↦ ‖z i‖) 0 := rfl
State after:
case hM
n : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : NormedAddCommGroup B
inst✝ : NormedSpace 𝕜 B
x : ContinuousMultilinearMap 𝕜 (fun x => A) 𝕜
xs : ContinuousMultilinearMap 𝕜 (fun x => A) B
z : Fin (n + 1) → A
xsb : ‖xs fun i => z i.succ‖ ≤ ‖xs‖ * Finset.univ.prod fun i => ‖z i.succ‖
xb : ‖x fun x => z 0‖ ≤ ‖x‖ * ‖z 0‖
e0 : (Finset.univ.prod fun i => Fin.cons ‖z 0‖ (fun i => ‖z i.succ‖) i) = ‖z 0‖ * Finset.univ.prod fun i => ‖z i.succ‖
e1 : ‖z 0‖ = (fun i => ‖z i‖) 0
⊢ ‖(x fun x => z 0) • xs fun i => z i.succ‖ ≤ ‖x‖ * ‖xs‖ * Finset.univ.prod fun i => ‖z i‖

State before:
case hM
n : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : NormedAddCommGroup B
inst✝ : NormedSpace 𝕜 B
x : ContinuousMultilinearMap 𝕜 (fun x => A) 𝕜
xs : ContinuousMultilinearMap 𝕜 (fun x => A) B
z : Fin (n + 1) → A
xsb : ‖xs fun i => z i.succ‖ ≤ ‖xs‖ * Finset.univ.prod fun i => ‖z i.succ‖
xb : ‖x fun x => z 0‖ ≤ ‖x‖ * ‖z 0‖
e0 : (Finset.univ.prod fun i => Fin.cons ‖z 0‖ (fun i => ‖z i.succ‖) i) = ‖z 0‖ * Finset.univ.prod fun i => ‖z i.succ‖
e1 : ‖z 0‖ = (fun i => ‖z i‖) 0
⊢ ‖(x fun x => z 0) • xs fun i => z i.succ‖ ≤ ‖x‖ * ‖xs‖ * Finset.univ.prod fun i => ‖z i‖
Tactic:
have e2 : (fun i : Fin n ↦ ‖z i.succ‖) = Fin.tail fun i : Fin (n + 1) ↦ ‖z i‖ := rfl
State after:
case hM
n : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : NormedAddCommGroup B
inst✝ : NormedSpace 𝕜 B
x : ContinuousMultilinearMap 𝕜 (fun x => A) 𝕜
xs : ContinuousMultilinearMap 𝕜 (fun x => A) B
z : Fin (n + 1) → A
xsb : ‖xs fun i => z i.succ‖ ≤ ‖xs‖ * Finset.univ.prod fun i => ‖z i.succ‖
xb : ‖x fun x => z 0‖ ≤ ‖x‖ * ‖z 0‖
e0 : (Finset.univ.prod fun i => Fin.cons ‖z 0‖ (fun i => ‖z i.succ‖) i) = ‖z 0‖ * Finset.univ.prod fun i => ‖z i.succ‖
e1 : ‖z 0‖ = (fun i => ‖z i‖) 0
e2 : (fun i => ‖z i.succ‖) = Fin.tail fun i => ‖z i‖
⊢ ‖(x fun x => z 0) • xs fun i => z i.succ‖ ≤ ‖x‖ * ‖xs‖ * Finset.univ.prod fun i => ‖z i‖

State before:
case hM
n : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : NormedAddCommGroup B
inst✝ : NormedSpace 𝕜 B
x : ContinuousMultilinearMap 𝕜 (fun x => A) 𝕜
xs : ContinuousMultilinearMap 𝕜 (fun x => A) B
z : Fin (n + 1) → A
xsb : ‖xs fun i => z i.succ‖ ≤ ‖xs‖ * Finset.univ.prod fun i => ‖z i.succ‖
xb : ‖x fun x => z 0‖ ≤ ‖x‖ * ‖z 0‖
e0 : (Finset.univ.prod fun i => Fin.cons ‖z 0‖ (fun i => ‖z i.succ‖) i) = ‖z 0‖ * Finset.univ.prod fun i => ‖z i.succ‖
e1 : ‖z 0‖ = (fun i => ‖z i‖) 0
e2 : (fun i => ‖z i.succ‖) = Fin.tail fun i => ‖z i‖
⊢ ‖(x fun x => z 0) • xs fun i => z i.succ‖ ≤ ‖x‖ * ‖xs‖ * Finset.univ.prod fun i => ‖z i‖
Tactic:
nth_rw 1 [e1] at e0
State after:
case hM
n : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : NormedAddCommGroup B
inst✝ : NormedSpace 𝕜 B
x : ContinuousMultilinearMap 𝕜 (fun x => A) 𝕜
xs : ContinuousMultilinearMap 𝕜 (fun x => A) B
z : Fin (n + 1) → A
xsb : ‖xs fun i => z i.succ‖ ≤ ‖xs‖ * Finset.univ.prod fun i => ‖z i.succ‖
xb : ‖x fun x => z 0‖ ≤ ‖x‖ * ‖z 0‖
e0 :
  (Finset.univ.prod fun i => Fin.cons ((fun i => ‖z i‖) 0) (fun i => ‖z i.succ‖) i) =
    ‖z 0‖ * Finset.univ.prod fun i => ‖z i.succ‖
e1 : ‖z 0‖ = (fun i => ‖z i‖) 0
e2 : (fun i => ‖z i.succ‖) = Fin.tail fun i => ‖z i‖
⊢ ‖(x fun x => z 0) • xs fun i => z i.succ‖ ≤ ‖x‖ * ‖xs‖ * Finset.univ.prod fun i => ‖z i‖

State before:
case hM
n : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : NormedAddCommGroup B
inst✝ : NormedSpace 𝕜 B
x : ContinuousMultilinearMap 𝕜 (fun x => A) 𝕜
xs : ContinuousMultilinearMap 𝕜 (fun x => A) B
z : Fin (n + 1) → A
xsb : ‖xs fun i => z i.succ‖ ≤ ‖xs‖ * Finset.univ.prod fun i => ‖z i.succ‖
xb : ‖x fun x => z 0‖ ≤ ‖x‖ * ‖z 0‖
e0 :
  (Finset.univ.prod fun i => Fin.cons ((fun i => ‖z i‖) 0) (fun i => ‖z i.succ‖) i) =
    ‖z 0‖ * Finset.univ.prod fun i => ‖z i.succ‖
e1 : ‖z 0‖ = (fun i => ‖z i‖) 0
e2 : (fun i => ‖z i.succ‖) = Fin.tail fun i => ‖z i‖
⊢ ‖(x fun x => z 0) • xs fun i => z i.succ‖ ≤ ‖x‖ * ‖xs‖ * Finset.univ.prod fun i => ‖z i‖
Tactic:
nth_rw 1 [e2] at e0
State after:
case hM
n : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : NormedAddCommGroup B
inst✝ : NormedSpace 𝕜 B
x : ContinuousMultilinearMap 𝕜 (fun x => A) 𝕜
xs : ContinuousMultilinearMap 𝕜 (fun x => A) B
z : Fin (n + 1) → A
xsb : ‖xs fun i => z i.succ‖ ≤ ‖xs‖ * Finset.univ.prod fun i => ‖z i.succ‖
xb : ‖x fun x => z 0‖ ≤ ‖x‖ * ‖z 0‖
e0 :
  (Finset.univ.prod fun i => Fin.cons ((fun i => ‖z i‖) 0) (Fin.tail fun i => ‖z i‖) i) =
    ‖z 0‖ * Finset.univ.prod fun i => ‖z i.succ‖
e1 : ‖z 0‖ = (fun i => ‖z i‖) 0
e2 : (fun i => ‖z i.succ‖) = Fin.tail fun i => ‖z i‖
⊢ ‖(x fun x => z 0) • xs fun i => z i.succ‖ ≤ ‖x‖ * ‖xs‖ * Finset.univ.prod fun i => ‖z i‖

State before:
case hM
n : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : NormedAddCommGroup B
inst✝ : NormedSpace 𝕜 B
x : ContinuousMultilinearMap 𝕜 (fun x => A) 𝕜
xs : ContinuousMultilinearMap 𝕜 (fun x => A) B
z : Fin (n + 1) → A
xsb : ‖xs fun i => z i.succ‖ ≤ ‖xs‖ * Finset.univ.prod fun i => ‖z i.succ‖
xb : ‖x fun x => z 0‖ ≤ ‖x‖ * ‖z 0‖
e0 :
  (Finset.univ.prod fun i => Fin.cons ((fun i => ‖z i‖) 0) (Fin.tail fun i => ‖z i‖) i) =
    ‖z 0‖ * Finset.univ.prod fun i => ‖z i.succ‖
e1 : ‖z 0‖ = (fun i => ‖z i‖) 0
e2 : (fun i => ‖z i.succ‖) = Fin.tail fun i => ‖z i‖
⊢ ‖(x fun x => z 0) • xs fun i => z i.succ‖ ≤ ‖x‖ * ‖xs‖ * Finset.univ.prod fun i => ‖z i‖
Tactic:
rw [Fin.cons_self_tail (fun i ↦ ‖z i‖)] at e0
State after:
case hM
n : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : NormedAddCommGroup B
inst✝ : NormedSpace 𝕜 B
x : ContinuousMultilinearMap 𝕜 (fun x => A) 𝕜
xs : ContinuousMultilinearMap 𝕜 (fun x => A) B
z : Fin (n + 1) → A
xsb : ‖xs fun i => z i.succ‖ ≤ ‖xs‖ * Finset.univ.prod fun i => ‖z i.succ‖
xb : ‖x fun x => z 0‖ ≤ ‖x‖ * ‖z 0‖
e0 : (Finset.univ.prod fun i => (fun i => ‖z i‖) i) = ‖z 0‖ * Finset.univ.prod fun i => ‖z i.succ‖
e1 : ‖z 0‖ = (fun i => ‖z i‖) 0
e2 : (fun i => ‖z i.succ‖) = Fin.tail fun i => ‖z i‖
⊢ ‖(x fun x => z 0) • xs fun i => z i.succ‖ ≤ ‖x‖ * ‖xs‖ * Finset.univ.prod fun i => ‖z i‖

State before:
case hM
n : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : NormedAddCommGroup B
inst✝ : NormedSpace 𝕜 B
x : ContinuousMultilinearMap 𝕜 (fun x => A) 𝕜
xs : ContinuousMultilinearMap 𝕜 (fun x => A) B
z : Fin (n + 1) → A
xsb : ‖xs fun i => z i.succ‖ ≤ ‖xs‖ * Finset.univ.prod fun i => ‖z i.succ‖
xb : ‖x fun x => z 0‖ ≤ ‖x‖ * ‖z 0‖
e0 : (Finset.univ.prod fun i => (fun i => ‖z i‖) i) = ‖z 0‖ * Finset.univ.prod fun i => ‖z i.succ‖
e1 : ‖z 0‖ = (fun i => ‖z i‖) 0
e2 : (fun i => ‖z i.succ‖) = Fin.tail fun i => ‖z i‖
⊢ ‖(x fun x => z 0) • xs fun i => z i.succ‖ ≤ ‖x‖ * ‖xs‖ * Finset.univ.prod fun i => ‖z i‖
Tactic:
calc ‖(x fun _ : Fin 1 ↦ z 0) • xs fun i : Fin n ↦ z i.succ‖
  _ ≤ ‖x‖ * ‖z 0‖ * (‖xs‖ * Finset.univ.prod fun i : Fin n ↦ ‖z i.succ‖) := by
    rw [norm_smul]; bound
  _ = ‖x‖ * ‖xs‖ * (‖z 0‖ * Finset.univ.prod fun i : Fin n ↦ ‖z i.succ‖) := by ring
  _ = ‖x‖ * ‖xs‖ * Finset.univ.prod fun i : Fin (n + 1) ↦ ‖z i‖ := by rw [←e0]
State after:
no goals

State before:
n : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : NormedAddCommGroup B
inst✝ : NormedSpace 𝕜 B
x : ContinuousMultilinearMap 𝕜 (fun x => A) 𝕜
xs : ContinuousMultilinearMap 𝕜 (fun x => A) B
z : Fin (n + 1) → A
xsb : ‖xs fun i => z i.succ‖ ≤ ‖xs‖ * Finset.univ.prod fun i => ‖z i.succ‖
xb : ‖x fun x => z 0‖ ≤ ‖x‖ * ‖z 0‖
e0 : (Finset.univ.prod fun i => (fun i => ‖z i‖) i) = ‖z 0‖ * Finset.univ.prod fun i => ‖z i.succ‖
e1 : ‖z 0‖ = (fun i => ‖z i‖) 0
e2 : (fun i => ‖z i.succ‖) = Fin.tail fun i => ‖z i‖
⊢ ‖(x fun x => z 0) • xs fun i => z i.succ‖ ≤ ‖x‖ * ‖z 0‖ * (‖xs‖ * Finset.univ.prod fun i => ‖z i.succ‖)
Tactic:
rw [norm_smul]
State after:
n : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : NormedAddCommGroup B
inst✝ : NormedSpace 𝕜 B
x : ContinuousMultilinearMap 𝕜 (fun x => A) 𝕜
xs : ContinuousMultilinearMap 𝕜 (fun x => A) B
z : Fin (n + 1) → A
xsb : ‖xs fun i => z i.succ‖ ≤ ‖xs‖ * Finset.univ.prod fun i => ‖z i.succ‖
xb : ‖x fun x => z 0‖ ≤ ‖x‖ * ‖z 0‖
e0 : (Finset.univ.prod fun i => (fun i => ‖z i‖) i) = ‖z 0‖ * Finset.univ.prod fun i => ‖z i.succ‖
e1 : ‖z 0‖ = (fun i => ‖z i‖) 0
e2 : (fun i => ‖z i.succ‖) = Fin.tail fun i => ‖z i‖
⊢ ‖x fun x => z 0‖ * ‖xs fun i => z i.succ‖ ≤ ‖x‖ * ‖z 0‖ * (‖xs‖ * Finset.univ.prod fun i => ‖z i.succ‖)

State before:
n : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : NormedAddCommGroup B
inst✝ : NormedSpace 𝕜 B
x : ContinuousMultilinearMap 𝕜 (fun x => A) 𝕜
xs : ContinuousMultilinearMap 𝕜 (fun x => A) B
z : Fin (n + 1) → A
xsb : ‖xs fun i => z i.succ‖ ≤ ‖xs‖ * Finset.univ.prod fun i => ‖z i.succ‖
xb : ‖x fun x => z 0‖ ≤ ‖x‖ * ‖z 0‖
e0 : (Finset.univ.prod fun i => (fun i => ‖z i‖) i) = ‖z 0‖ * Finset.univ.prod fun i => ‖z i.succ‖
e1 : ‖z 0‖ = (fun i => ‖z i‖) 0
e2 : (fun i => ‖z i.succ‖) = Fin.tail fun i => ‖z i‖
⊢ ‖x fun x => z 0‖ * ‖xs fun i => z i.succ‖ ≤ ‖x‖ * ‖z 0‖ * (‖xs‖ * Finset.univ.prod fun i => ‖z i.succ‖)
Tactic:
bound
State after:
no goals

State before:
n : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : NormedAddCommGroup B
inst✝ : NormedSpace 𝕜 B
x : ContinuousMultilinearMap 𝕜 (fun x => A) 𝕜
xs : ContinuousMultilinearMap 𝕜 (fun x => A) B
z : Fin (n + 1) → A
xsb : ‖xs fun i => z i.succ‖ ≤ ‖xs‖ * Finset.univ.prod fun i => ‖z i.succ‖
xb : ‖x fun x => z 0‖ ≤ ‖x‖ * ‖z 0‖
e0 : (Finset.univ.prod fun i => (fun i => ‖z i‖) i) = ‖z 0‖ * Finset.univ.prod fun i => ‖z i.succ‖
e1 : ‖z 0‖ = (fun i => ‖z i‖) 0
e2 : (fun i => ‖z i.succ‖) = Fin.tail fun i => ‖z i‖
⊢ ‖x‖ * ‖z 0‖ * (‖xs‖ * Finset.univ.prod fun i => ‖z i.succ‖) =
    ‖x‖ * ‖xs‖ * (‖z 0‖ * Finset.univ.prod fun i => ‖z i.succ‖)
Tactic:
ring
State after:
no goals

State before:
n : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup A
inst✝² : NormedSpace 𝕜 A
inst✝¹ : NormedAddCommGroup B
inst✝ : NormedSpace 𝕜 B
x : ContinuousMultilinearMap 𝕜 (fun x => A) 𝕜
xs : ContinuousMultilinearMap 𝕜 (fun x => A) B
z : Fin (n + 1) → A
xsb : ‖xs fun i => z i.succ‖ ≤ ‖xs‖ * Finset.univ.prod fun i => ‖z i.succ‖
xb : ‖x fun x => z 0‖ ≤ ‖x‖ * ‖z 0‖
e0 : (Finset.univ.prod fun i => (fun i => ‖z i‖) i) = ‖z 0‖ * Finset.univ.prod fun i => ‖z i.succ‖
e1 : ‖z 0‖ = (fun i => ‖z i‖) 0
e2 : (fun i => ‖z i.succ‖) = Fin.tail fun i => ‖z i‖
⊢ ‖x‖ * ‖xs‖ * (‖z 0‖ * Finset.univ.prod fun i => ‖z i.succ‖) = ‖x‖ * ‖xs‖ * Finset.univ.prod fun i => ‖z i‖
Tactic:
rw [←e0]
State after:
no goals