internlm/Lean-Github huggingface dataset:
Theorem: smulCmmap_norm
Proof 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
Proof state after:
no goals
Theorem: smulCmmap_norm
Proof 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
Proof state after:
no goals
Theorem: smulCmmap_norm
Proof 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]
Proof state after:
no goals
Theorem: termCmmap_apply
Proof state before:
n✝ : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SMulCommClass 𝕜 𝕜 E
inst✝ : IsScalarTower 𝕜 𝕜 E
n k : ℕ
a b : 𝕜
x : E
⊢ ((termCmmap 𝕜 n k x) fun x => (a, b)) = a ^ min k n • b ^ (n - k) • x
Tactic:
induction' n with n h
Proof state after:
case zero
n : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SMulCommClass 𝕜 𝕜 E
inst✝ : IsScalarTower 𝕜 𝕜 E
k : ℕ
a b : 𝕜
x : E
⊢ ((termCmmap 𝕜 0 k x) fun x => (a, b)) = a ^ min k 0 • b ^ (0 - k) • x

case succ
n✝ : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SMulCommClass 𝕜 𝕜 E
inst✝ : IsScalarTower 𝕜 𝕜 E
k : ℕ
a b : 𝕜
x : E
n : ℕ
h : ((termCmmap 𝕜 n k x) fun x => (a, b)) = a ^ min k n • b ^ (n - k) • x
⊢ ((termCmmap 𝕜 (n + 1) k x) fun x => (a, b)) = a ^ min k (n + 1) • b ^ (n + 1 - k) • x
Theorem: termCmmap_apply
Proof state before:
case zero
n : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SMulCommClass 𝕜 𝕜 E
inst✝ : IsScalarTower 𝕜 𝕜 E
k : ℕ
a b : 𝕜
x : E
⊢ ((termCmmap 𝕜 0 k x) fun x => (a, b)) = a ^ min k 0 • b ^ (0 - k) • x
Tactic:
simp only [termCmmap, ContinuousMultilinearMap.constOfIsEmpty_apply, min_zero, pow_zero,
  zero_tsub, one_smul, Nat.zero_eq]
Proof state after:
no goals
Theorem: termCmmap_apply
Proof state before:
case succ
n✝ : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SMulCommClass 𝕜 𝕜 E
inst✝ : IsScalarTower 𝕜 𝕜 E
k : ℕ
a b : 𝕜
x : E
n : ℕ
h : ((termCmmap 𝕜 n k x) fun x => (a, b)) = a ^ min k n • b ^ (n - k) • x
⊢ ((termCmmap 𝕜 (n + 1) k x) fun x => (a, b)) = a ^ min k (n + 1) • b ^ (n + 1 - k) • x
Tactic:
rw [termCmmap, smulCmmap_apply, h]
Proof state after:
case succ
n✝ : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SMulCommClass 𝕜 𝕜 E
inst✝ : IsScalarTower 𝕜 𝕜 E
k : ℕ
a b : 𝕜
x : E
n : ℕ
h : ((termCmmap 𝕜 n k x) fun x => (a, b)) = a ^ min k n • b ^ (n - k) • x
⊢ ((if n < k then fstCmmap 𝕜 𝕜 𝕜 else sndCmmap 𝕜 𝕜 𝕜) fun x => (a, b)) • a ^ min k n • b ^ (n - k) • x =
    a ^ min k (n + 1) • b ^ (n + 1 - k) • x
Theorem: termCmmap_apply
Proof state before:
case succ
n✝ : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SMulCommClass 𝕜 𝕜 E
inst✝ : IsScalarTower 𝕜 𝕜 E
k : ℕ
a b : 𝕜
x : E
n : ℕ
h : ((termCmmap 𝕜 n k x) fun x => (a, b)) = a ^ min k n • b ^ (n - k) • x
⊢ ((if n < k then fstCmmap 𝕜 𝕜 𝕜 else sndCmmap 𝕜 𝕜 𝕜) fun x => (a, b)) • a ^ min k n • b ^ (n - k) • x =
    a ^ min k (n + 1) • b ^ (n + 1 - k) • x
Tactic:
by_cases nk : n < k
Proof state after:
case pos
n✝ : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SMulCommClass 𝕜 𝕜 E
inst✝ : IsScalarTower 𝕜 𝕜 E
k : ℕ
a b : 𝕜
x : E
n : ℕ
h : ((termCmmap 𝕜 n k x) fun x => (a, b)) = a ^ min k n • b ^ (n - k) • x
nk : n < k
⊢ ((if n < k then fstCmmap 𝕜 𝕜 𝕜 else sndCmmap 𝕜 𝕜 𝕜) fun x => (a, b)) • a ^ min k n • b ^ (n - k) • x =
    a ^ min k (n + 1) • b ^ (n + 1 - k) • x

case neg
n✝ : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SMulCommClass 𝕜 𝕜 E
inst✝ : IsScalarTower 𝕜 𝕜 E
k : ℕ
a b : 𝕜
x : E
n : ℕ
h : ((termCmmap 𝕜 n k x) fun x => (a, b)) = a ^ min k n • b ^ (n - k) • x
nk : ¬n < k
⊢ ((if n < k then fstCmmap 𝕜 𝕜 𝕜 else sndCmmap 𝕜 𝕜 𝕜) fun x => (a, b)) • a ^ min k n • b ^ (n - k) • x =
    a ^ min k (n + 1) • b ^ (n + 1 - k) • x
Theorem: termCmmap_apply
Proof state before:
case pos
n✝ : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SMulCommClass 𝕜 𝕜 E
inst✝ : IsScalarTower 𝕜 𝕜 E
k : ℕ
a b : 𝕜
x : E
n : ℕ
h : ((termCmmap 𝕜 n k x) fun x => (a, b)) = a ^ min k n • b ^ (n - k) • x
nk : n < k
⊢ ((if n < k then fstCmmap 𝕜 𝕜 𝕜 else sndCmmap 𝕜 𝕜 𝕜) fun x => (a, b)) • a ^ min k n • b ^ (n - k) • x =
    a ^ min k (n + 1) • b ^ (n + 1 - k) • x
Tactic:
simp [nk]
Proof state after:
case pos
n✝ : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SMulCommClass 𝕜 𝕜 E
inst✝ : IsScalarTower 𝕜 𝕜 E
k : ℕ
a b : 𝕜
x : E
n : ℕ
h : ((termCmmap 𝕜 n k x) fun x => (a, b)) = a ^ min k n • b ^ (n - k) • x
nk : n < k
⊢ ((fstCmmap 𝕜 𝕜 𝕜) fun x => (a, b)) • a ^ min k n • b ^ (n - k) • x = a ^ min k (n + 1) • b ^ (n + 1 - k) • x
Theorem: termCmmap_apply
Proof state before:
case pos
n✝ : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SMulCommClass 𝕜 𝕜 E
inst✝ : IsScalarTower 𝕜 𝕜 E
k : ℕ
a b : 𝕜
x : E
n : ℕ
h : ((termCmmap 𝕜 n k x) fun x => (a, b)) = a ^ min k n • b ^ (n - k) • x
nk : n < k
⊢ ((fstCmmap 𝕜 𝕜 𝕜) fun x => (a, b)) • a ^ min k n • b ^ (n - k) • x = a ^ min k (n + 1) • b ^ (n + 1 - k) • x
Tactic:
rw [fstCmmap_apply]
Proof state after:
case pos
n✝ : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SMulCommClass 𝕜 𝕜 E
inst✝ : IsScalarTower 𝕜 𝕜 E
k : ℕ
a b : 𝕜
x : E
n : ℕ
h : ((termCmmap 𝕜 n k x) fun x => (a, b)) = a ^ min k n • b ^ (n - k) • x
nk : n < k
⊢ a • a ^ min k n • b ^ (n - k) • x = a ^ min k (n + 1) • b ^ (n + 1 - k) • x
Theorem: termCmmap_apply
Proof state before:
case pos
n✝ : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SMulCommClass 𝕜 𝕜 E
inst✝ : IsScalarTower 𝕜 𝕜 E
k : ℕ
a b : 𝕜
x : E
n : ℕ
h : ((termCmmap 𝕜 n k x) fun x => (a, b)) = a ^ min k n • b ^ (n - k) • x
nk : n < k
⊢ a • a ^ min k n • b ^ (n - k) • x = a ^ min k (n + 1) • b ^ (n + 1 - k) • x
Tactic:
have nsk : n.succ ≤ k := Nat.succ_le_iff.mpr nk
Proof state after:
case pos
n✝ : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SMulCommClass 𝕜 𝕜 E
inst✝ : IsScalarTower 𝕜 𝕜 E
k : ℕ
a b : 𝕜
x : E
n : ℕ
h : ((termCmmap 𝕜 n k x) fun x => (a, b)) = a ^ min k n • b ^ (n - k) • x
nk : n < k
nsk : n.succ ≤ k
⊢ a • a ^ min k n • b ^ (n - k) • x = a ^ min k (n + 1) • b ^ (n + 1 - k) • x
Theorem: termCmmap_apply
Proof state before:
case pos
n✝ : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SMulCommClass 𝕜 𝕜 E
inst✝ : IsScalarTower 𝕜 𝕜 E
k : ℕ
a b : 𝕜
x : E
n : ℕ
h : ((termCmmap 𝕜 n k x) fun x => (a, b)) = a ^ min k n • b ^ (n - k) • x
nk : n < k
nsk : n.succ ≤ k
⊢ a • a ^ min k n • b ^ (n - k) • x = a ^ min k (n + 1) • b ^ (n + 1 - k) • x
Tactic:
rw [min_eq_right nk.le, min_eq_right nsk, Nat.sub_eq_zero_of_le nk.le,
  Nat.sub_eq_zero_of_le nsk]
Proof state after:
case pos
n✝ : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SMulCommClass 𝕜 𝕜 E
inst✝ : IsScalarTower 𝕜 𝕜 E
k : ℕ
a b : 𝕜
x : E
n : ℕ
h : ((termCmmap 𝕜 n k x) fun x => (a, b)) = a ^ min k n • b ^ (n - k) • x
nk : n < k
nsk : n.succ ≤ k
⊢ a • a ^ n • b ^ 0 • x = a ^ n.succ • b ^ 0 • x
Theorem: termCmmap_apply
Proof state before:
case pos
n✝ : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SMulCommClass 𝕜 𝕜 E
inst✝ : IsScalarTower 𝕜 𝕜 E
k : ℕ
a b : 𝕜
x : E
n : ℕ
h : ((termCmmap 𝕜 n k x) fun x => (a, b)) = a ^ min k n • b ^ (n - k) • x
nk : n < k
nsk : n.succ ≤ k
⊢ a • a ^ n • b ^ 0 • x = a ^ n.succ • b ^ 0 • x
Tactic:
simp only [pow_zero, one_smul, ← smul_assoc, smul_eq_mul, Nat.succ_eq_add_one, pow_succ']
Proof state after:
no goals
Theorem: termCmmap_apply
Proof state before:
case neg
n✝ : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SMulCommClass 𝕜 𝕜 E
inst✝ : IsScalarTower 𝕜 𝕜 E
k : ℕ
a b : 𝕜
x : E
n : ℕ
h : ((termCmmap 𝕜 n k x) fun x => (a, b)) = a ^ min k n • b ^ (n - k) • x
nk : ¬n < k
⊢ ((if n < k then fstCmmap 𝕜 𝕜 𝕜 else sndCmmap 𝕜 𝕜 𝕜) fun x => (a, b)) • a ^ min k n • b ^ (n - k) • x =
    a ^ min k (n + 1) • b ^ (n + 1 - k) • x
Tactic:
simp [nk]
Proof state after:
case neg
n✝ : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SMulCommClass 𝕜 𝕜 E
inst✝ : IsScalarTower 𝕜 𝕜 E
k : ℕ
a b : 𝕜
x : E
n : ℕ
h : ((termCmmap 𝕜 n k x) fun x => (a, b)) = a ^ min k n • b ^ (n - k) • x
nk : ¬n < k
⊢ ((sndCmmap 𝕜 𝕜 𝕜) fun x => (a, b)) • a ^ min k n • b ^ (n - k) • x = a ^ min k (n + 1) • b ^ (n + 1 - k) • x
Theorem: termCmmap_apply
Proof state before:
case neg
n✝ : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SMulCommClass 𝕜 𝕜 E
inst✝ : IsScalarTower 𝕜 𝕜 E
k : ℕ
a b : 𝕜
x : E
n : ℕ
h : ((termCmmap 𝕜 n k x) fun x => (a, b)) = a ^ min k n • b ^ (n - k) • x
nk : ¬n < k
⊢ ((sndCmmap 𝕜 𝕜 𝕜) fun x => (a, b)) • a ^ min k n • b ^ (n - k) • x = a ^ min k (n + 1) • b ^ (n + 1 - k) • x
Tactic:
simp at nk
Proof state after:
case neg
n✝ : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SMulCommClass 𝕜 𝕜 E
inst✝ : IsScalarTower 𝕜 𝕜 E
k : ℕ
a b : 𝕜
x : E
n : ℕ
h : ((termCmmap 𝕜 n k x) fun x => (a, b)) = a ^ min k n • b ^ (n - k) • x
nk : k ≤ n
⊢ ((sndCmmap 𝕜 𝕜 𝕜) fun x => (a, b)) • a ^ min k n • b ^ (n - k) • x = a ^ min k (n + 1) • b ^ (n + 1 - k) • x
Theorem: termCmmap_apply
Proof state before:
case neg
n✝ : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SMulCommClass 𝕜 𝕜 E
inst✝ : IsScalarTower 𝕜 𝕜 E
k : ℕ
a b : 𝕜
x : E
n : ℕ
h : ((termCmmap 𝕜 n k x) fun x => (a, b)) = a ^ min k n • b ^ (n - k) • x
nk : k ≤ n
⊢ ((sndCmmap 𝕜 𝕜 𝕜) fun x => (a, b)) • a ^ min k n • b ^ (n - k) • x = a ^ min k (n + 1) • b ^ (n + 1 - k) • x
Tactic:
rw [sndCmmap_apply]
Proof state after:
case neg
n✝ : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SMulCommClass 𝕜 𝕜 E
inst✝ : IsScalarTower 𝕜 𝕜 E
k : ℕ
a b : 𝕜
x : E
n : ℕ
h : ((termCmmap 𝕜 n k x) fun x => (a, b)) = a ^ min k n • b ^ (n - k) • x
nk : k ≤ n
⊢ b • a ^ min k n • b ^ (n - k) • x = a ^ min k (n + 1) • b ^ (n + 1 - k) • x
Theorem: termCmmap_apply
Proof state before:
case neg
n✝ : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SMulCommClass 𝕜 𝕜 E
inst✝ : IsScalarTower 𝕜 𝕜 E
k : ℕ
a b : 𝕜
x : E
n : ℕ
h : ((termCmmap 𝕜 n k x) fun x => (a, b)) = a ^ min k n • b ^ (n - k) • x
nk : k ≤ n
⊢ b • a ^ min k n • b ^ (n - k) • x = a ^ min k (n + 1) • b ^ (n + 1 - k) • x
Tactic:
have nsk : k ≤ n.succ := Nat.le_succ_of_le nk
Proof state after:
case neg
n✝ : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SMulCommClass 𝕜 𝕜 E
inst✝ : IsScalarTower 𝕜 𝕜 E
k : ℕ
a b : 𝕜
x : E
n : ℕ
h : ((termCmmap 𝕜 n k x) fun x => (a, b)) = a ^ min k n • b ^ (n - k) • x
nk : k ≤ n
nsk : k ≤ n.succ
⊢ b • a ^ min k n • b ^ (n - k) • x = a ^ min k (n + 1) • b ^ (n + 1 - k) • x
Theorem: termCmmap_apply
Proof state before:
case neg
n✝ : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SMulCommClass 𝕜 𝕜 E
inst✝ : IsScalarTower 𝕜 𝕜 E
k : ℕ
a b : 𝕜
x : E
n : ℕ
h : ((termCmmap 𝕜 n k x) fun x => (a, b)) = a ^ min k n • b ^ (n - k) • x
nk : k ≤ n
nsk : k ≤ n.succ
⊢ b • a ^ min k n • b ^ (n - k) • x = a ^ min k (n + 1) • b ^ (n + 1 - k) • x
Tactic:
rw [min_eq_left nk, min_eq_left nsk]
Proof state after:
case neg
n✝ : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SMulCommClass 𝕜 𝕜 E
inst✝ : IsScalarTower 𝕜 𝕜 E
k : ℕ
a b : 𝕜
x : E
n : ℕ
h : ((termCmmap 𝕜 n k x) fun x => (a, b)) = a ^ min k n • b ^ (n - k) • x
nk : k ≤ n
nsk : k ≤ n.succ
⊢ b • a ^ k • b ^ (n - k) • x = a ^ k • b ^ (n + 1 - k) • x
Theorem: termCmmap_apply
Proof state before:
case neg
n✝ : ℕ
𝕜 : Type
inst✝⁵ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁴ : Semiring R
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : SMulCommClass 𝕜 𝕜 E
inst✝ : IsScalarTower 𝕜 𝕜 E
k : ℕ
a b : 𝕜
x : E
n : ℕ
h : ((termCmmap 𝕜 n k x) fun x => (a, b)) = a ^ min k n • b ^ (n - k) • x
nk : k ≤ n
nsk : k ≤ n.succ
⊢ b • a ^ k • b ^ (n - k) • x = a ^ k • b ^ (n + 1 - k) • x
Tactic:
rw [smul_comm b _, ← smul_assoc b _ _, smul_eq_mul, ← pow_succ', ← Nat.sub_add_comm nk]
Proof state after:
no goals
Theorem: termCmmap_norm
Proof 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
Proof 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‖
Theorem: termCmmap_norm
Proof 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]
Proof state after:
no goals
Theorem: termCmmap_norm
Proof 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]
Proof 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‖
Theorem: termCmmap_norm
Proof 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
Proof 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‖
Theorem: termCmmap_norm
Proof 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
Proof 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‖
Theorem: termCmmap_norm
Proof 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
Proof 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‖
Theorem: termCmmap_norm
Proof 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
Proof 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‖
Theorem: termCmmap_norm
Proof 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
Proof 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‖
Theorem: termCmmap_norm
Proof 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 ⊢
Proof 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‖