Theorem: SchwartzMap.pow_one_add_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
⊢ (1 + ‖x‖) ^ k * ‖f x‖ ≤ 2 ^ k * sup_Iic_seminorm 𝕜 k 0 f
Tactic:
have := @one_add_le_sup_seminorm_apply 𝕜 E F _ _ _ _ _ _ _ (k, 0) k 0
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
this :
  k ≤ (k, 0).1 →
    0 ≤ (k, 0).2 →
      ∀ (f : 𝓢(E, F)) (x : E),
        (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ 0 (⇑f) x‖ ≤
          2 ^ (k, 0).1 * (Finset.sup (Finset.Iic (k, 0)) fun m => SchwartzMap.seminorm 𝕜 m.1 m.2) f
⊢ (1 + ‖x‖) ^ k * ‖f x‖ ≤ 2 ^ k * sup_Iic_seminorm 𝕜 k 0 f

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
this :
  k ≤ (k, 0).1 →
    0 ≤ (k, 0).2 →
      ∀ (f : 𝓢(E, F)) (x : E),
        (1 + ‖x‖) ^ k * ‖iteratedFDeriv ℝ 0 (⇑f) x‖ ≤
          2 ^ (k, 0).1 * (Finset.sup (Finset.Iic (k, 0)) fun m => SchwartzMap.seminorm 𝕜 m.1 m.2) f
⊢ (1 + ‖x‖) ^ k * ‖f x‖ ≤ 2 ^ k * sup_Iic_seminorm 𝕜 k 0 f
Tactic:
simp at this
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
this :
  ∀ (f : 𝓢(E, F)) (x : E),
    (1 + ‖x‖) ^ k * ‖f x‖ ≤ 2 ^ k * (Finset.sup (Finset.Iic (k, 0)) fun m => SchwartzMap.seminorm 𝕜 m.1 m.2) f
⊢ (1 + ‖x‖) ^ k * ‖f x‖ ≤ 2 ^ k * sup_Iic_seminorm 𝕜 k 0 f

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
this :
  ∀ (f : 𝓢(E, F)) (x : E),
    (1 + ‖x‖) ^ k * ‖f x‖ ≤ 2 ^ k * (Finset.sup (Finset.Iic (k, 0)) fun m => SchwartzMap.seminorm 𝕜 m.1 m.2) f
⊢ (1 + ‖x‖) ^ k * ‖f x‖ ≤ 2 ^ k * sup_Iic_seminorm 𝕜 k 0 f
Tactic:
specialize this 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
this : (1 + ‖x‖) ^ k * ‖f x‖ ≤ 2 ^ k * (Finset.sup (Finset.Iic (k, 0)) fun m => SchwartzMap.seminorm 𝕜 m.1 m.2) f
⊢ (1 + ‖x‖) ^ k * ‖f x‖ ≤ 2 ^ k * sup_Iic_seminorm 𝕜 k 0 f

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
this : (1 + ‖x‖) ^ k * ‖f x‖ ≤ 2 ^ k * (Finset.sup (Finset.Iic (k, 0)) fun m => SchwartzMap.seminorm 𝕜 m.1 m.2) f
⊢ (1 + ‖x‖) ^ k * ‖f x‖ ≤ 2 ^ k * sup_Iic_seminorm 𝕜 k 0 f
Tactic:
simpa
State after:
no goals