internlm/Lean-Github huggingface dataset:
Theorem: smul_cmmap_cont
Proof state before:
n : ℕ
𝕜 : Type
inst✝⁶ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid A
inst✝³ : Module 𝕜 A
inst✝² : TopologicalSpace A
inst✝¹ : NormedAddCommGroup B
inst✝ : NormedSpace 𝕜 B
x : ContinuousMultilinearMap 𝕜 (fun x => A) 𝕜
xs : ContinuousMultilinearMap 𝕜 (fun x => A) B
⊢ Continuous (smulCmmapFn x xs)
Tactic:
apply Continuous.smul
Proof state after:
case hf
n : ℕ
𝕜 : Type
inst✝⁶ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid A
inst✝³ : Module 𝕜 A
inst✝² : TopologicalSpace A
inst✝¹ : NormedAddCommGroup B
inst✝ : NormedSpace 𝕜 B
x : ContinuousMultilinearMap 𝕜 (fun x => A) 𝕜
xs : ContinuousMultilinearMap 𝕜 (fun x => A) B
⊢ Continuous fun x_1 => x.toFun fun x => x_1 0

case hg
n : ℕ
𝕜 : Type
inst✝⁶ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid A
inst✝³ : Module 𝕜 A
inst✝² : TopologicalSpace A
inst✝¹ : NormedAddCommGroup B
inst✝ : NormedSpace 𝕜 B
x : ContinuousMultilinearMap 𝕜 (fun x => A) 𝕜
xs : ContinuousMultilinearMap 𝕜 (fun x => A) B
⊢ Continuous fun x => xs.toFun fun i => x i.succ
Theorem: smul_cmmap_cont
Proof state before:
case hf
n : ℕ
𝕜 : Type
inst✝⁶ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid A
inst✝³ : Module 𝕜 A
inst✝² : TopologicalSpace A
inst✝¹ : NormedAddCommGroup B
inst✝ : NormedSpace 𝕜 B
x : ContinuousMultilinearMap 𝕜 (fun x => A) 𝕜
xs : ContinuousMultilinearMap 𝕜 (fun x => A) B
⊢ Continuous fun x_1 => x.toFun fun x => x_1 0

case hg
n : ℕ
𝕜 : Type
inst✝⁶ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid A
inst✝³ : Module 𝕜 A
inst✝² : TopologicalSpace A
inst✝¹ : NormedAddCommGroup B
inst✝ : NormedSpace 𝕜 B
x : ContinuousMultilinearMap 𝕜 (fun x => A) 𝕜
xs : ContinuousMultilinearMap 𝕜 (fun x => A) B
⊢ Continuous fun x => xs.toFun fun i => x i.succ
Tactic:
repeat continuity
Proof state after:
no goals
Theorem: smul_cmmap_cont
Proof state before:
case hg
n : ℕ
𝕜 : Type
inst✝⁶ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid A
inst✝³ : Module 𝕜 A
inst✝² : TopologicalSpace A
inst✝¹ : NormedAddCommGroup B
inst✝ : NormedSpace 𝕜 B
x : ContinuousMultilinearMap 𝕜 (fun x => A) 𝕜
xs : ContinuousMultilinearMap 𝕜 (fun x => A) B
⊢ Continuous fun x => xs.toFun fun i => x i.succ
Tactic:
continuity
Proof state after:
no goals
Theorem: smulCmmap_apply
Proof state before:
n : ℕ
𝕜 : Type
inst✝⁶ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid A
inst✝³ : Module 𝕜 A
inst✝² : TopologicalSpace 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 fun x => z 0) • xs fun i => z i.succ
Tactic:
rw [smulCmmap, ←ContinuousMultilinearMap.toFun_eq_coe]
Proof state after:
n : ℕ
𝕜 : Type
inst✝⁶ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid A
inst✝³ : Module 𝕜 A
inst✝² : TopologicalSpace A
inst✝¹ : NormedAddCommGroup B
inst✝ : NormedSpace 𝕜 B
x : ContinuousMultilinearMap 𝕜 (fun x => A) 𝕜
xs : ContinuousMultilinearMap 𝕜 (fun x => A) B
z : Fin (n + 1) → A
⊢ { toFun := smulCmmapFn x xs, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }.toFun z =
    (x fun x => z 0) • xs fun i => z i.succ
Theorem: smulCmmap_apply
Proof state before:
n : ℕ
𝕜 : Type
inst✝⁶ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid A
inst✝³ : Module 𝕜 A
inst✝² : TopologicalSpace A
inst✝¹ : NormedAddCommGroup B
inst✝ : NormedSpace 𝕜 B
x : ContinuousMultilinearMap 𝕜 (fun x => A) 𝕜
xs : ContinuousMultilinearMap 𝕜 (fun x => A) B
z : Fin (n + 1) → A
⊢ { toFun := smulCmmapFn x xs, map_add' := ⋯, map_smul' := ⋯, cont := ⋯ }.toFun z =
    (x fun x => z 0) • xs fun i => z i.succ
Tactic:
simp only
Proof state after:
n : ℕ
𝕜 : Type
inst✝⁶ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid A
inst✝³ : Module 𝕜 A
inst✝² : TopologicalSpace A
inst✝¹ : NormedAddCommGroup B
inst✝ : NormedSpace 𝕜 B
x : ContinuousMultilinearMap 𝕜 (fun x => A) 𝕜
xs : ContinuousMultilinearMap 𝕜 (fun x => A) B
z : Fin (n + 1) → A
⊢ smulCmmapFn x xs z = (x fun x => z 0) • xs fun i => z i.succ
Theorem: smulCmmap_apply
Proof state before:
n : ℕ
𝕜 : Type
inst✝⁶ : NontriviallyNormedField 𝕜
R A B E : Type
inst✝⁵ : Semiring R
inst✝⁴ : AddCommMonoid A
inst✝³ : Module 𝕜 A
inst✝² : TopologicalSpace A
inst✝¹ : NormedAddCommGroup B
inst✝ : NormedSpace 𝕜 B
x : ContinuousMultilinearMap 𝕜 (fun x => A) 𝕜
xs : ContinuousMultilinearMap 𝕜 (fun x => A) B
z : Fin (n + 1) → A
⊢ smulCmmapFn x xs z = (x fun x => z 0) • xs fun i => z i.succ
Tactic:
rfl
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
⊢ ‖smulCmmap 𝕜 A B x xs‖ ≤ ‖x‖ * ‖xs‖
Tactic:
apply ContinuousMultilinearMap.opNorm_le_bound
Proof 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‖
Theorem: smulCmmap_norm
Proof 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
Proof 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‖
Theorem: smulCmmap_norm
Proof 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
Proof 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‖
Theorem: smulCmmap_norm
Proof 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]
Proof 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‖
Theorem: smulCmmap_norm
Proof 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
Proof 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‖
Theorem: smulCmmap_norm
Proof 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
Proof 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‖
Theorem: smulCmmap_norm
Proof 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
Proof 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‖
Theorem: smulCmmap_norm
Proof 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‖
Proof 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‖
Theorem: smulCmmap_norm
Proof 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
Proof 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‖
Theorem: smulCmmap_norm
Proof 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
Proof 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‖
Theorem: smulCmmap_norm
Proof 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
Proof 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‖
Theorem: smulCmmap_norm
Proof 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
Proof 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‖
Theorem: smulCmmap_norm
Proof 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
Proof 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‖
Theorem: smulCmmap_norm
Proof 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]
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 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]
Proof 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‖)