Theorem: SchwartzMap.pow_norm_mul_norm_le_two_pow_sup_Iic_seminorm (ForML/SchwartzLp.lean)

State before:
E : Type u_1
F : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
mE : MeasureSpace E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : BorelSpace E
inst✝³ : Measure.IsAddHaarMeasure volume
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
k : ℕ
f : 𝓢(E, F)
x : E
⊢ ‖x‖ ^ k * ‖f x‖ ≤ 2 ^ k * sup_Iic_seminorm 𝕜 k 0 f
Tactic:
refine le_trans ?_ (pow_one_add_norm_mul_norm_le_two_pow_sup_Iic_seminorm k f x)
State after:
E : Type u_1
F : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
mE : MeasureSpace E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : BorelSpace E
inst✝³ : Measure.IsAddHaarMeasure volume
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
k : ℕ
f : 𝓢(E, F)
x : E
⊢ ‖x‖ ^ k * ‖f x‖ ≤ (1 + ‖x‖) ^ k * ‖f x‖

State before:
E : Type u_1
F : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
mE : MeasureSpace E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : BorelSpace E
inst✝³ : Measure.IsAddHaarMeasure volume
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
k : ℕ
f : 𝓢(E, F)
x : E
⊢ ‖x‖ ^ k * ‖f x‖ ≤ (1 + ‖x‖) ^ k * ‖f x‖
Tactic:
refine mul_le_mul_of_nonneg_right ?_ (norm_nonneg _)
State after:
E : Type u_1
F : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
mE : MeasureSpace E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : BorelSpace E
inst✝³ : Measure.IsAddHaarMeasure volume
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
k : ℕ
f : 𝓢(E, F)
x : E
⊢ ‖x‖ ^ k ≤ (1 + ‖x‖) ^ k

State before:
E : Type u_1
F : Type u_2
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedSpace ℝ E
inst✝⁷ : NormedAddCommGroup F
inst✝⁶ : NormedSpace ℝ F
mE : MeasureSpace E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : BorelSpace E
inst✝³ : Measure.IsAddHaarMeasure volume
𝕜 : Type u_3
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
k : ℕ
f : 𝓢(E, F)
x : E
⊢ ‖x‖ ^ k ≤ (1 + ‖x‖) ^ k
Tactic:
refine pow_le_pow_left ?_ ?_ k <;> simp
State after:
no goals