Theorem: SchwartzMap.norm_innerSL_smul_le (ForML/IntegralAgainst.lean)

State before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
φ : 𝓢(E, F)
x : E
⊢ ‖(innerSL_smul φ) x‖ ≤ ‖x‖ * ‖φ x‖
Tactic:
rw [ContinuousLinearMap.opNorm_le_iff (mul_nonneg (norm_nonneg x) (norm_nonneg (φ x)))]
State after:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
φ : 𝓢(E, F)
x : E
⊢ ∀ (x_1 : E), ‖((innerSL_smul φ) x) x_1‖ ≤ ‖x‖ * ‖φ x‖ * ‖x_1‖

State before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
φ : 𝓢(E, F)
x : E
⊢ ∀ (x_1 : E), ‖((innerSL_smul φ) x) x_1‖ ≤ ‖x‖ * ‖φ x‖ * ‖x_1‖
Tactic:
intro m
State after:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
φ : 𝓢(E, F)
x m : E
⊢ ‖((innerSL_smul φ) x) m‖ ≤ ‖x‖ * ‖φ x‖ * ‖m‖

State before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
φ : 𝓢(E, F)
x m : E
⊢ ‖((innerSL_smul φ) x) m‖ ≤ ‖x‖ * ‖φ x‖ * ‖m‖
Tactic:
rw [SchwartzMap.innerSL_smul_apply, norm_smul]
State after:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
φ : 𝓢(E, F)
x m : E
⊢ ‖⟪x, m⟫_ℝ‖ * ‖φ x‖ ≤ ‖x‖ * ‖φ x‖ * ‖m‖

State before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
φ : 𝓢(E, F)
x m : E
⊢ ‖⟪x, m⟫_ℝ‖ * ‖φ x‖ ≤ ‖x‖ * ‖φ x‖ * ‖m‖
Tactic:
rw [← mul_rotate]
State after:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
φ : 𝓢(E, F)
x m : E
⊢ ‖⟪x, m⟫_ℝ‖ * ‖φ x‖ ≤ ‖m‖ * ‖x‖ * ‖φ x‖

State before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
φ : 𝓢(E, F)
x m : E
⊢ ‖⟪x, m⟫_ℝ‖ * ‖φ x‖ ≤ ‖m‖ * ‖x‖ * ‖φ x‖
Tactic:
refine mul_le_mul_of_nonneg_right ?_ (norm_nonneg (φ x))
State after:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
φ : 𝓢(E, F)
x m : E
⊢ ‖⟪x, m⟫_ℝ‖ ≤ ‖m‖ * ‖x‖

State before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
φ : 𝓢(E, F)
x m : E
⊢ ‖⟪x, m⟫_ℝ‖ ≤ ‖m‖ * ‖x‖
Tactic:
rw [mul_comm]
State after:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
φ : 𝓢(E, F)
x m : E
⊢ ‖⟪x, m⟫_ℝ‖ ≤ ‖x‖ * ‖m‖

State before:
𝕜 : Type u_1
𝕜' : Type u_2
D : Type u_3
E : Type u_4
F : Type u_5
G : Type u_6
inst✝² : NormedAddCommGroup E
hE : InnerProductSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
φ : 𝓢(E, F)
x m : E
⊢ ‖⟪x, m⟫_ℝ‖ ≤ ‖x‖ * ‖m‖
Tactic:
exact norm_inner_le_norm x m
State after:
no goals