internlm/Lean-Github huggingface dataset:
Theorem: SchwartzMap.integrable_norm_pow_mul_norm
Proof state before:
case refine_2
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
n : ℕ
f : 𝓢(E, F)
⊢ snorm (fun a => ‖a‖ ^ n * ‖f a‖) 1 volume ≤ snorm (fun x => (1 + ‖x‖) ^ ↑n • f x) (↑1) volume
Tactic:
refine snorm_mono ?_
Proof state after:
case refine_2
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
n : ℕ
f : 𝓢(E, F)
⊢ ∀ (x : E), ‖‖x‖ ^ n * ‖f x‖‖ ≤ ‖(1 + ‖x‖) ^ ↑n • f x‖
Theorem: SchwartzMap.integrable_norm_pow_mul_norm
Proof state before:
case refine_2
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
n : ℕ
f : 𝓢(E, F)
⊢ ∀ (x : E), ‖‖x‖ ^ n * ‖f x‖‖ ≤ ‖(1 + ‖x‖) ^ ↑n • f x‖
Tactic:
intro x
Proof state after:
case refine_2
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
n : ℕ
f : 𝓢(E, F)
x : E
⊢ ‖‖x‖ ^ n * ‖f x‖‖ ≤ ‖(1 + ‖x‖) ^ ↑n • f x‖
Theorem: SchwartzMap.integrable_norm_pow_mul_norm
Proof state before:
case refine_2
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
n : ℕ
f : 𝓢(E, F)
x : E
⊢ ‖‖x‖ ^ n * ‖f x‖‖ ≤ ‖(1 + ‖x‖) ^ ↑n • f x‖
Tactic:
simp [norm_smul]
Proof state after:
case refine_2
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
n : ℕ
f : 𝓢(E, F)
x : E
⊢ ‖x‖ ^ n * ‖f x‖ ≤ |1 + ‖x‖| ^ n * ‖f x‖
Theorem: SchwartzMap.integrable_norm_pow_mul_norm
Proof state before:
case refine_2
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
n : ℕ
f : 𝓢(E, F)
x : E
⊢ ‖x‖ ^ n * ‖f x‖ ≤ |1 + ‖x‖| ^ n * ‖f x‖
Tactic:
refine mul_le_mul_of_nonneg_right ?_ (norm_nonneg (f x))
Proof state after:
case refine_2
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
n : ℕ
f : 𝓢(E, F)
x : E
⊢ ‖x‖ ^ n ≤ |1 + ‖x‖| ^ n
Theorem: SchwartzMap.integrable_norm_pow_mul_norm
Proof state before:
case refine_2
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
n : ℕ
f : 𝓢(E, F)
x : E
⊢ ‖x‖ ^ n ≤ |1 + ‖x‖| ^ n
Tactic:
rw [abs_of_nonneg (by simp)]
Proof state after:
case refine_2
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
n : ℕ
f : 𝓢(E, F)
x : E
⊢ ‖x‖ ^ n ≤ (1 + ‖x‖) ^ n
Theorem: SchwartzMap.integrable_norm_pow_mul_norm
Proof state before:
case refine_2
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
n : ℕ
f : 𝓢(E, F)
x : E
⊢ ‖x‖ ^ n ≤ (1 + ‖x‖) ^ n
Tactic:
refine pow_le_pow_left ?_ ?_ _ <;> simp
Proof state after:
no goals
Theorem: SchwartzMap.integrable_norm_pow_mul_norm
Proof 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
n : ℕ
f : 𝓢(E, F)
x : E
⊢ 0 ≤ 1 + ‖x‖
Tactic:
simp
Proof state after:
no goals
Theorem: SchwartzMap.snorm_nnreal_lt_top
Proof 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
f : 𝓢(E, F)
p : NNReal
hp : 0 < p
⊢ snorm (⇑f) (↑p) volume < ⊤
Tactic:
simpa using snorm_nnreal_one_add_norm_rpow_smul_lt_top 0 f hp
Proof state after:
no goals
Theorem: SchwartzMap.snorm_lt_top
Proof 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
f : 𝓢(E, F)
p : ENNReal
⊢ snorm (⇑f) p volume < ⊤
Tactic:
cases p with
| none => exact snorm_top_lt_top f
| some p =>
  simp
  cases eq_or_lt_of_le (zero_le p) with
  | inl hp => simp [← hp]
  | inr hp => exact snorm_nnreal_lt_top f hp
Proof state after:
no goals
Theorem: SchwartzMap.snorm_lt_top
Proof state before:
case none
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
f : 𝓢(E, F)
⊢ snorm (⇑f) none volume < ⊤
Tactic:
exact snorm_top_lt_top f
Proof state after:
no goals
Theorem: SchwartzMap.snorm_lt_top
Proof state before:
case some
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
f : 𝓢(E, F)
p : NNReal
⊢ snorm (⇑f) (some p) volume < ⊤
Tactic:
simp
Proof state after:
case some
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
f : 𝓢(E, F)
p : NNReal
⊢ snorm (⇑f) (↑p) volume < ⊤
Theorem: SchwartzMap.snorm_lt_top
Proof state before:
case some
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
f : 𝓢(E, F)
p : NNReal
⊢ snorm (⇑f) (↑p) volume < ⊤
Tactic:
cases eq_or_lt_of_le (zero_le p) with
| inl hp => simp [← hp]
| inr hp => exact snorm_nnreal_lt_top f hp
Proof state after:
no goals
Theorem: SchwartzMap.snorm_lt_top
Proof state before:
case some.inl
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
f : 𝓢(E, F)
p : NNReal
hp : 0 = p
⊢ snorm (⇑f) (↑p) volume < ⊤
Tactic:
simp [← hp]
Proof state after:
no goals
Theorem: SchwartzMap.snorm_lt_top
Proof state before:
case some.inr
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
f : 𝓢(E, F)
p : NNReal
hp : 0 < p
⊢ snorm (⇑f) (↑p) volume < ⊤
Tactic:
exact snorm_nnreal_lt_top f hp
Proof state after:
no goals
Theorem: SchwartzMap.coeFn_toL1
Proof 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
f : 𝓢(E, F)
⊢ ↑↑(toL1 f) =ᵐ[volume] ⇑f
Tactic:
simp [toL1, coeFn_toLp]
Proof state after:
no goals
Theorem: SchwartzMap.norm_toL1_eq_integral
Proof 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
f : 𝓢(E, F)
⊢ ‖toL1 f‖ = ∫ (x : E), ‖f x‖
Tactic:
simp [toL1, toLp, addHomLp]
Proof 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
f : 𝓢(E, F)
⊢ ENNReal.toReal (snorm (⇑f) 1 volume) = ∫ (x : E), ‖f x‖
Theorem: SchwartzMap.norm_toL1_eq_integral
Proof 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
f : 𝓢(E, F)
⊢ ENNReal.toReal (snorm (⇑f) 1 volume) = ∫ (x : E), ‖f x‖
Tactic:
rw [snorm_one_eq_lintegral_nnnorm]
Proof 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
f : 𝓢(E, F)
⊢ ENNReal.toReal (∫⁻ (x : E), ↑‖f x‖₊) = ∫ (x : E), ‖f x‖
Theorem: SchwartzMap.norm_toL1_eq_integral
Proof 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
f : 𝓢(E, F)
⊢ ENNReal.toReal (∫⁻ (x : E), ↑‖f x‖₊) = ∫ (x : E), ‖f x‖
Tactic:
rw [integral_norm_eq_lintegral_nnnorm f.continuous.aestronglyMeasurable]
Proof state after:
no goals
Theorem: SchwartzMap.integrable
Proof 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
f : 𝓢(E, F)
⊢ Integrable fun x => f x
Tactic:
rw [← memℒp_one_iff_integrable]
Proof 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
f : 𝓢(E, F)
⊢ Memℒp (fun x => f x) 1
Theorem: SchwartzMap.integrable
Proof 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
f : 𝓢(E, F)
⊢ Memℒp (fun x => f x) 1
Tactic:
exact memℒp f 1
Proof state after:
no goals
Theorem: SchwartzMap.bound
Proof 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
f : 𝓢(E, F)
⊢ ∀ (x : E), ‖f x‖ ≤ ‖toBoundedContinuousFunction f‖
Tactic:
exact BoundedContinuousFunction.norm_coe_le_norm (toBoundedContinuousFunction f)
Proof state after:
no goals
Theorem: SchwartzMap.pow_one_add_norm_mul_norm_le_two_pow_sup_Iic_seminorm
Proof 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
Proof 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
Theorem: SchwartzMap.pow_one_add_norm_mul_norm_le_two_pow_sup_Iic_seminorm
Proof 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
Proof 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
Theorem: SchwartzMap.pow_one_add_norm_mul_norm_le_two_pow_sup_Iic_seminorm
Proof 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
Proof 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
Theorem: SchwartzMap.pow_one_add_norm_mul_norm_le_two_pow_sup_Iic_seminorm
Proof 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
Proof state after:
no goals
Theorem: SchwartzMap.pow_norm_mul_norm_le_two_pow_sup_Iic_seminorm
Proof 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)
Proof 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‖
Theorem: SchwartzMap.pow_norm_mul_norm_le_two_pow_sup_Iic_seminorm
Proof 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 _)
Proof 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
Theorem: SchwartzMap.pow_norm_mul_norm_le_two_pow_sup_Iic_seminorm
Proof 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
Proof state after:
no goals
Theorem: SchwartzMap.norm_le_sup_Iic_seminorm_mul_one_add_norm_pow_neg
Proof 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
⊢ ‖f x‖ ≤ 2 ^ k * sup_Iic_seminorm 𝕜 k 0 f * (1 + ‖x‖) ^ (-↑k)
Tactic:
simp [Real.rpow_neg]
Proof 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
⊢ ‖f x‖ ≤ 2 ^ k * sup_Iic_seminorm 𝕜 k 0 f * ((1 + ‖x‖) ^ k)⁻¹
Theorem: SchwartzMap.norm_le_sup_Iic_seminorm_mul_one_add_norm_pow_neg
Proof 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
⊢ ‖f x‖ ≤ 2 ^ k * sup_Iic_seminorm 𝕜 k 0 f * ((1 + ‖x‖) ^ k)⁻¹
Tactic:
rw [mul_comm, inv_mul_eq_div]
Proof 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
⊢ ‖f x‖ ≤ 2 ^ k * sup_Iic_seminorm 𝕜 k 0 f / (1 + ‖x‖) ^ k
Theorem: SchwartzMap.norm_le_sup_Iic_seminorm_mul_one_add_norm_pow_neg
Proof 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
⊢ ‖f x‖ ≤ 2 ^ k * sup_Iic_seminorm 𝕜 k 0 f / (1 + ‖x‖) ^ k
Tactic:
simp [le_div_iff']
Proof 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
⊢ (1 + ‖x‖) ^ k * ‖f x‖ ≤ 2 ^ k * sup_Iic_seminorm 𝕜 k 0 f
Theorem: SchwartzMap.norm_le_sup_Iic_seminorm_mul_one_add_norm_pow_neg
Proof 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 : (1 + ‖x‖) ^ k * ‖f x‖ ≤ ↑2 ^ k * sup_Iic_seminorm 𝕜 k 0 f
Proof state after:
case this
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

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 * sup_Iic_seminorm 𝕜 k 0 f
⊢ (1 + ‖x‖) ^ k * ‖f x‖ ≤ 2 ^ k * sup_Iic_seminorm 𝕜 k 0 f