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

State before:
n✝ : ℕ
𝕜✝ : Type
inst✝⁴ : NontriviallyNormedField 𝕜✝
R A B E : Type
inst✝³ : Semiring R
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
n k : ℕ
x : E
⊢ ‖termCmmap 𝕜 n k x‖ ≤ ‖x‖
Tactic:
induction' n with n nh
State after:
case zero
n : ℕ
𝕜✝ : Type
inst✝⁴ : NontriviallyNormedField 𝕜✝
R A B E : Type
inst✝³ : Semiring R
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
k : ℕ
x : E
⊢ ‖termCmmap 𝕜 0 k x‖ ≤ ‖x‖

case succ
n✝ : ℕ
𝕜✝ : Type
inst✝⁴ : NontriviallyNormedField 𝕜✝
R A B E : Type
inst✝³ : Semiring R
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
k : ℕ
x : E
n : ℕ
nh : ‖termCmmap 𝕜 n k x‖ ≤ ‖x‖
⊢ ‖termCmmap 𝕜 (n + 1) k x‖ ≤ ‖x‖

State before:
case zero
n : ℕ
𝕜✝ : Type
inst✝⁴ : NontriviallyNormedField 𝕜✝
R A B E : Type
inst✝³ : Semiring R
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
k : ℕ
x : E
⊢ ‖termCmmap 𝕜 0 k x‖ ≤ ‖x‖
Tactic:
simp only [termCmmap, le_refl, ContinuousMultilinearMap.norm_constOfIsEmpty]
State after:
no goals

State before:
case succ
n✝ : ℕ
𝕜✝ : Type
inst✝⁴ : NontriviallyNormedField 𝕜✝
R A B E : Type
inst✝³ : Semiring R
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
k : ℕ
x : E
n : ℕ
nh : ‖termCmmap 𝕜 n k x‖ ≤ ‖x‖
⊢ ‖termCmmap 𝕜 (n + 1) k x‖ ≤ ‖x‖
Tactic:
rw [termCmmap]
State after:
case succ
n✝ : ℕ
𝕜✝ : Type
inst✝⁴ : NontriviallyNormedField 𝕜✝
R A B E : Type
inst✝³ : Semiring R
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
k : ℕ
x : E
n : ℕ
nh : ‖termCmmap 𝕜 n k x‖ ≤ ‖x‖
⊢ ‖(fun k x => smulCmmap 𝕜 (𝕜 × 𝕜) E (if n < k then fstCmmap 𝕜 𝕜 𝕜 else sndCmmap 𝕜 𝕜 𝕜) (termCmmap 𝕜 n k x)) k x‖ ≤ ‖x‖

State before:
case succ
n✝ : ℕ
𝕜✝ : Type
inst✝⁴ : NontriviallyNormedField 𝕜✝
R A B E : Type
inst✝³ : Semiring R
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
k : ℕ
x : E
n : ℕ
nh : ‖termCmmap 𝕜 n k x‖ ≤ ‖x‖
⊢ ‖(fun k x => smulCmmap 𝕜 (𝕜 × 𝕜) E (if n < k then fstCmmap 𝕜 𝕜 𝕜 else sndCmmap 𝕜 𝕜 𝕜) (termCmmap 𝕜 n k x)) k x‖ ≤ ‖x‖
Tactic:
simp only
State after:
case succ
n✝ : ℕ
𝕜✝ : Type
inst✝⁴ : NontriviallyNormedField 𝕜✝
R A B E : Type
inst✝³ : Semiring R
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
k : ℕ
x : E
n : ℕ
nh : ‖termCmmap 𝕜 n k x‖ ≤ ‖x‖
⊢ ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (if n < k then fstCmmap 𝕜 𝕜 𝕜 else sndCmmap 𝕜 𝕜 𝕜) (termCmmap 𝕜 n k x)‖ ≤ ‖x‖

State before:
case succ
n✝ : ℕ
𝕜✝ : Type
inst✝⁴ : NontriviallyNormedField 𝕜✝
R A B E : Type
inst✝³ : Semiring R
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
k : ℕ
x : E
n : ℕ
nh : ‖termCmmap 𝕜 n k x‖ ≤ ‖x‖
⊢ ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (if n < k then fstCmmap 𝕜 𝕜 𝕜 else sndCmmap 𝕜 𝕜 𝕜) (termCmmap 𝕜 n k x)‖ ≤ ‖x‖
Tactic:
generalize ht : termCmmap 𝕜 n k x = t
State after:
case succ
n✝ : ℕ
𝕜✝ : Type
inst✝⁴ : NontriviallyNormedField 𝕜✝
R A B E : Type
inst✝³ : Semiring R
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
k : ℕ
x : E
n : ℕ
nh : ‖termCmmap 𝕜 n k x‖ ≤ ‖x‖
t : ContinuousMultilinearMap 𝕜 (fun x => 𝕜 × 𝕜) E
ht : termCmmap 𝕜 n k x = t
⊢ ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (if n < k then fstCmmap 𝕜 𝕜 𝕜 else sndCmmap 𝕜 𝕜 𝕜) t‖ ≤ ‖x‖

State before:
case succ
n✝ : ℕ
𝕜✝ : Type
inst✝⁴ : NontriviallyNormedField 𝕜✝
R A B E : Type
inst✝³ : Semiring R
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
k : ℕ
x : E
n : ℕ
nh : ‖termCmmap 𝕜 n k x‖ ≤ ‖x‖
t : ContinuousMultilinearMap 𝕜 (fun x => 𝕜 × 𝕜) E
ht : termCmmap 𝕜 n k x = t
⊢ ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (if n < k then fstCmmap 𝕜 𝕜 𝕜 else sndCmmap 𝕜 𝕜 𝕜) t‖ ≤ ‖x‖
Tactic:
rw [ht] at nh
State after:
case succ
n✝ : ℕ
𝕜✝ : Type
inst✝⁴ : NontriviallyNormedField 𝕜✝
R A B E : Type
inst✝³ : Semiring R
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
k : ℕ
x : E
n : ℕ
t : ContinuousMultilinearMap 𝕜 (fun x => 𝕜 × 𝕜) E
nh : ‖t‖ ≤ ‖x‖
ht : termCmmap 𝕜 n k x = t
⊢ ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (if n < k then fstCmmap 𝕜 𝕜 𝕜 else sndCmmap 𝕜 𝕜 𝕜) t‖ ≤ ‖x‖

State before:
case succ
n✝ : ℕ
𝕜✝ : Type
inst✝⁴ : NontriviallyNormedField 𝕜✝
R A B E : Type
inst✝³ : Semiring R
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
k : ℕ
x : E
n : ℕ
t : ContinuousMultilinearMap 𝕜 (fun x => 𝕜 × 𝕜) E
nh : ‖t‖ ≤ ‖x‖
ht : termCmmap 𝕜 n k x = t
⊢ ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (if n < k then fstCmmap 𝕜 𝕜 𝕜 else sndCmmap 𝕜 𝕜 𝕜) t‖ ≤ ‖x‖
Tactic:
have tn := smulCmmap_norm (if n < k then fstCmmap 𝕜 𝕜 𝕜 else sndCmmap 𝕜 𝕜 𝕜) t
State after:
case succ
n✝ : ℕ
𝕜✝ : Type
inst✝⁴ : NontriviallyNormedField 𝕜✝
R A B E : Type
inst✝³ : Semiring R
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
k : ℕ
x : E
n : ℕ
t : ContinuousMultilinearMap 𝕜 (fun x => 𝕜 × 𝕜) E
nh : ‖t‖ ≤ ‖x‖
ht : termCmmap 𝕜 n k x = t
tn :
  ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (if n < k then fstCmmap 𝕜 𝕜 𝕜 else sndCmmap 𝕜 𝕜 𝕜) t‖ ≤
    ‖if n < k then fstCmmap 𝕜 𝕜 𝕜 else sndCmmap 𝕜 𝕜 𝕜‖ * ‖t‖
⊢ ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (if n < k then fstCmmap 𝕜 𝕜 𝕜 else sndCmmap 𝕜 𝕜 𝕜) t‖ ≤ ‖x‖

State before:
case succ
n✝ : ℕ
𝕜✝ : Type
inst✝⁴ : NontriviallyNormedField 𝕜✝
R A B E : Type
inst✝³ : Semiring R
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
k : ℕ
x : E
n : ℕ
t : ContinuousMultilinearMap 𝕜 (fun x => 𝕜 × 𝕜) E
nh : ‖t‖ ≤ ‖x‖
ht : termCmmap 𝕜 n k x = t
tn :
  ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (if n < k then fstCmmap 𝕜 𝕜 𝕜 else sndCmmap 𝕜 𝕜 𝕜) t‖ ≤
    ‖if n < k then fstCmmap 𝕜 𝕜 𝕜 else sndCmmap 𝕜 𝕜 𝕜‖ * ‖t‖
⊢ ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (if n < k then fstCmmap 𝕜 𝕜 𝕜 else sndCmmap 𝕜 𝕜 𝕜) t‖ ≤ ‖x‖
Tactic:
by_cases nk : n < k
State after:
case pos
n✝ : ℕ
𝕜✝ : Type
inst✝⁴ : NontriviallyNormedField 𝕜✝
R A B E : Type
inst✝³ : Semiring R
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
k : ℕ
x : E
n : ℕ
t : ContinuousMultilinearMap 𝕜 (fun x => 𝕜 × 𝕜) E
nh : ‖t‖ ≤ ‖x‖
ht : termCmmap 𝕜 n k x = t
tn :
  ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (if n < k then fstCmmap 𝕜 𝕜 𝕜 else sndCmmap 𝕜 𝕜 𝕜) t‖ ≤
    ‖if n < k then fstCmmap 𝕜 𝕜 𝕜 else sndCmmap 𝕜 𝕜 𝕜‖ * ‖t‖
nk : n < k
⊢ ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (if n < k then fstCmmap 𝕜 𝕜 𝕜 else sndCmmap 𝕜 𝕜 𝕜) t‖ ≤ ‖x‖

case neg
n✝ : ℕ
𝕜✝ : Type
inst✝⁴ : NontriviallyNormedField 𝕜✝
R A B E : Type
inst✝³ : Semiring R
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
k : ℕ
x : E
n : ℕ
t : ContinuousMultilinearMap 𝕜 (fun x => 𝕜 × 𝕜) E
nh : ‖t‖ ≤ ‖x‖
ht : termCmmap 𝕜 n k x = t
tn :
  ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (if n < k then fstCmmap 𝕜 𝕜 𝕜 else sndCmmap 𝕜 𝕜 𝕜) t‖ ≤
    ‖if n < k then fstCmmap 𝕜 𝕜 𝕜 else sndCmmap 𝕜 𝕜 𝕜‖ * ‖t‖
nk : ¬n < k
⊢ ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (if n < k then fstCmmap 𝕜 𝕜 𝕜 else sndCmmap 𝕜 𝕜 𝕜) t‖ ≤ ‖x‖

State before:
case pos
n✝ : ℕ
𝕜✝ : Type
inst✝⁴ : NontriviallyNormedField 𝕜✝
R A B E : Type
inst✝³ : Semiring R
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
k : ℕ
x : E
n : ℕ
t : ContinuousMultilinearMap 𝕜 (fun x => 𝕜 × 𝕜) E
nh : ‖t‖ ≤ ‖x‖
ht : termCmmap 𝕜 n k x = t
tn :
  ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (if n < k then fstCmmap 𝕜 𝕜 𝕜 else sndCmmap 𝕜 𝕜 𝕜) t‖ ≤
    ‖if n < k then fstCmmap 𝕜 𝕜 𝕜 else sndCmmap 𝕜 𝕜 𝕜‖ * ‖t‖
nk : n < k
⊢ ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (if n < k then fstCmmap 𝕜 𝕜 𝕜 else sndCmmap 𝕜 𝕜 𝕜) t‖ ≤ ‖x‖
Tactic:
simp [nk] at tn ⊢
State after:
case pos
n✝ : ℕ
𝕜✝ : Type
inst✝⁴ : NontriviallyNormedField 𝕜✝
R A B E : Type
inst✝³ : Semiring R
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
k : ℕ
x : E
n : ℕ
t : ContinuousMultilinearMap 𝕜 (fun x => 𝕜 × 𝕜) E
nh : ‖t‖ ≤ ‖x‖
ht : termCmmap 𝕜 n k x = t
nk : n < k
tn : ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (fstCmmap 𝕜 𝕜 𝕜) t‖ ≤ ‖fstCmmap 𝕜 𝕜 𝕜‖ * ‖t‖
⊢ ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (fstCmmap 𝕜 𝕜 𝕜) t‖ ≤ ‖x‖

State before:
case pos
n✝ : ℕ
𝕜✝ : Type
inst✝⁴ : NontriviallyNormedField 𝕜✝
R A B E : Type
inst✝³ : Semiring R
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
k : ℕ
x : E
n : ℕ
t : ContinuousMultilinearMap 𝕜 (fun x => 𝕜 × 𝕜) E
nh : ‖t‖ ≤ ‖x‖
ht : termCmmap 𝕜 n k x = t
nk : n < k
tn : ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (fstCmmap 𝕜 𝕜 𝕜) t‖ ≤ ‖fstCmmap 𝕜 𝕜 𝕜‖ * ‖t‖
⊢ ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (fstCmmap 𝕜 𝕜 𝕜) t‖ ≤ ‖x‖
Tactic:
rw [fstCmmap_norm] at tn
State after:
case pos
n✝ : ℕ
𝕜✝ : Type
inst✝⁴ : NontriviallyNormedField 𝕜✝
R A B E : Type
inst✝³ : Semiring R
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
k : ℕ
x : E
n : ℕ
t : ContinuousMultilinearMap 𝕜 (fun x => 𝕜 × 𝕜) E
nh : ‖t‖ ≤ ‖x‖
ht : termCmmap 𝕜 n k x = t
nk : n < k
tn : ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (fstCmmap 𝕜 𝕜 𝕜) t‖ ≤ 1 * ‖t‖
⊢ ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (fstCmmap 𝕜 𝕜 𝕜) t‖ ≤ ‖x‖

State before:
case pos
n✝ : ℕ
𝕜✝ : Type
inst✝⁴ : NontriviallyNormedField 𝕜✝
R A B E : Type
inst✝³ : Semiring R
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
k : ℕ
x : E
n : ℕ
t : ContinuousMultilinearMap 𝕜 (fun x => 𝕜 × 𝕜) E
nh : ‖t‖ ≤ ‖x‖
ht : termCmmap 𝕜 n k x = t
nk : n < k
tn : ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (fstCmmap 𝕜 𝕜 𝕜) t‖ ≤ 1 * ‖t‖
⊢ ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (fstCmmap 𝕜 𝕜 𝕜) t‖ ≤ ‖x‖
Tactic:
simp at tn
State after:
case pos
n✝ : ℕ
𝕜✝ : Type
inst✝⁴ : NontriviallyNormedField 𝕜✝
R A B E : Type
inst✝³ : Semiring R
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
k : ℕ
x : E
n : ℕ
t : ContinuousMultilinearMap 𝕜 (fun x => 𝕜 × 𝕜) E
nh : ‖t‖ ≤ ‖x‖
ht : termCmmap 𝕜 n k x = t
nk : n < k
tn : ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (fstCmmap 𝕜 𝕜 𝕜) t‖ ≤ ‖t‖
⊢ ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (fstCmmap 𝕜 𝕜 𝕜) t‖ ≤ ‖x‖

State before:
case pos
n✝ : ℕ
𝕜✝ : Type
inst✝⁴ : NontriviallyNormedField 𝕜✝
R A B E : Type
inst✝³ : Semiring R
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
k : ℕ
x : E
n : ℕ
t : ContinuousMultilinearMap 𝕜 (fun x => 𝕜 × 𝕜) E
nh : ‖t‖ ≤ ‖x‖
ht : termCmmap 𝕜 n k x = t
nk : n < k
tn : ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (fstCmmap 𝕜 𝕜 𝕜) t‖ ≤ ‖t‖
⊢ ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (fstCmmap 𝕜 𝕜 𝕜) t‖ ≤ ‖x‖
Tactic:
exact _root_.trans tn nh
State after:
no goals

State before:
case neg
n✝ : ℕ
𝕜✝ : Type
inst✝⁴ : NontriviallyNormedField 𝕜✝
R A B E : Type
inst✝³ : Semiring R
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
k : ℕ
x : E
n : ℕ
t : ContinuousMultilinearMap 𝕜 (fun x => 𝕜 × 𝕜) E
nh : ‖t‖ ≤ ‖x‖
ht : termCmmap 𝕜 n k x = t
tn :
  ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (if n < k then fstCmmap 𝕜 𝕜 𝕜 else sndCmmap 𝕜 𝕜 𝕜) t‖ ≤
    ‖if n < k then fstCmmap 𝕜 𝕜 𝕜 else sndCmmap 𝕜 𝕜 𝕜‖ * ‖t‖
nk : ¬n < k
⊢ ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (if n < k then fstCmmap 𝕜 𝕜 𝕜 else sndCmmap 𝕜 𝕜 𝕜) t‖ ≤ ‖x‖
Tactic:
simp [nk] at tn ⊢
State after:
case neg
n✝ : ℕ
𝕜✝ : Type
inst✝⁴ : NontriviallyNormedField 𝕜✝
R A B E : Type
inst✝³ : Semiring R
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
k : ℕ
x : E
n : ℕ
t : ContinuousMultilinearMap 𝕜 (fun x => 𝕜 × 𝕜) E
nh : ‖t‖ ≤ ‖x‖
ht : termCmmap 𝕜 n k x = t
nk : ¬n < k
tn : ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (sndCmmap 𝕜 𝕜 𝕜) t‖ ≤ ‖sndCmmap 𝕜 𝕜 𝕜‖ * ‖t‖
⊢ ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (sndCmmap 𝕜 𝕜 𝕜) t‖ ≤ ‖x‖

State before:
case neg
n✝ : ℕ
𝕜✝ : Type
inst✝⁴ : NontriviallyNormedField 𝕜✝
R A B E : Type
inst✝³ : Semiring R
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
k : ℕ
x : E
n : ℕ
t : ContinuousMultilinearMap 𝕜 (fun x => 𝕜 × 𝕜) E
nh : ‖t‖ ≤ ‖x‖
ht : termCmmap 𝕜 n k x = t
nk : ¬n < k
tn : ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (sndCmmap 𝕜 𝕜 𝕜) t‖ ≤ ‖sndCmmap 𝕜 𝕜 𝕜‖ * ‖t‖
⊢ ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (sndCmmap 𝕜 𝕜 𝕜) t‖ ≤ ‖x‖
Tactic:
rw [sndCmmap_norm] at tn
State after:
case neg
n✝ : ℕ
𝕜✝ : Type
inst✝⁴ : NontriviallyNormedField 𝕜✝
R A B E : Type
inst✝³ : Semiring R
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
k : ℕ
x : E
n : ℕ
t : ContinuousMultilinearMap 𝕜 (fun x => 𝕜 × 𝕜) E
nh : ‖t‖ ≤ ‖x‖
ht : termCmmap 𝕜 n k x = t
nk : ¬n < k
tn : ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (sndCmmap 𝕜 𝕜 𝕜) t‖ ≤ 1 * ‖t‖
⊢ ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (sndCmmap 𝕜 𝕜 𝕜) t‖ ≤ ‖x‖

State before:
case neg
n✝ : ℕ
𝕜✝ : Type
inst✝⁴ : NontriviallyNormedField 𝕜✝
R A B E : Type
inst✝³ : Semiring R
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
k : ℕ
x : E
n : ℕ
t : ContinuousMultilinearMap 𝕜 (fun x => 𝕜 × 𝕜) E
nh : ‖t‖ ≤ ‖x‖
ht : termCmmap 𝕜 n k x = t
nk : ¬n < k
tn : ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (sndCmmap 𝕜 𝕜 𝕜) t‖ ≤ 1 * ‖t‖
⊢ ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (sndCmmap 𝕜 𝕜 𝕜) t‖ ≤ ‖x‖
Tactic:
simp at tn
State after:
case neg
n✝ : ℕ
𝕜✝ : Type
inst✝⁴ : NontriviallyNormedField 𝕜✝
R A B E : Type
inst✝³ : Semiring R
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
k : ℕ
x : E
n : ℕ
t : ContinuousMultilinearMap 𝕜 (fun x => 𝕜 × 𝕜) E
nh : ‖t‖ ≤ ‖x‖
ht : termCmmap 𝕜 n k x = t
nk : ¬n < k
tn : ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (sndCmmap 𝕜 𝕜 𝕜) t‖ ≤ ‖t‖
⊢ ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (sndCmmap 𝕜 𝕜 𝕜) t‖ ≤ ‖x‖

State before:
case neg
n✝ : ℕ
𝕜✝ : Type
inst✝⁴ : NontriviallyNormedField 𝕜✝
R A B E : Type
inst✝³ : Semiring R
𝕜 : Type
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
k : ℕ
x : E
n : ℕ
t : ContinuousMultilinearMap 𝕜 (fun x => 𝕜 × 𝕜) E
nh : ‖t‖ ≤ ‖x‖
ht : termCmmap 𝕜 n k x = t
nk : ¬n < k
tn : ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (sndCmmap 𝕜 𝕜 𝕜) t‖ ≤ ‖t‖
⊢ ‖smulCmmap 𝕜 (𝕜 × 𝕜) E (sndCmmap 𝕜 𝕜 𝕜) t‖ ≤ ‖x‖
Tactic:
exact _root_.trans tn nh
State after:
no goals