internlm/Lean-Github huggingface dataset:
Theorem: SchwartzMap.norm_le_sup_Iic_seminorm_mul_one_add_norm_pow_neg
Proof state before:
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
Tactic:
. refine 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
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
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
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
Tactic:
simpa
Proof state after:
no goals
Theorem: SchwartzMap.norm_le_sup_Iic_seminorm_mul_one_add_norm_pow_neg
Proof state before:
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
Tactic:
refine pow_one_add_norm_mul_norm_le_two_pow_sup_Iic_seminorm k f x
Proof state after:
no goals
Theorem: SchwartzMap.integral_norm_le_const_mul_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
r : ℕ
hr : FiniteDimensional.finrank ℝ E < r
f : 𝓢(E, F)
⊢ ∫ (x : E), ‖f x‖ ≤ (2 ^ r * ∫ (x : E), (1 + ‖x‖) ^ (-↑r)) * sup_Iic_seminorm 𝕜 r 0 f
Tactic:
have h_int : Integrable (fun (x : E) => (1 + ‖x‖) ^ (-r : ℝ))
Proof state after:
case h_int
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
r : ℕ
hr : FiniteDimensional.finrank ℝ E < r
f : 𝓢(E, F)
⊢ Integrable fun x => (1 + ‖x‖) ^ (-↑r)

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
r : ℕ
hr : FiniteDimensional.finrank ℝ E < r
f : 𝓢(E, F)
h_int : Integrable fun x => (1 + ‖x‖) ^ (-↑r)
⊢ ∫ (x : E), ‖f x‖ ≤ (2 ^ r * ∫ (x : E), (1 + ‖x‖) ^ (-↑r)) * sup_Iic_seminorm 𝕜 r 0 f
Theorem: SchwartzMap.integral_norm_le_const_mul_sup_Iic_seminorm
Proof state before:
case h_int
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
r : ℕ
hr : FiniteDimensional.finrank ℝ E < r
f : 𝓢(E, F)
⊢ Integrable fun x => (1 + ‖x‖) ^ (-↑r)

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
r : ℕ
hr : FiniteDimensional.finrank ℝ E < r
f : 𝓢(E, F)
h_int : Integrable fun x => (1 + ‖x‖) ^ (-↑r)
⊢ ∫ (x : E), ‖f x‖ ≤ (2 ^ r * ∫ (x : E), (1 + ‖x‖) ^ (-↑r)) * sup_Iic_seminorm 𝕜 r 0 f
Tactic:
. refine integrable_one_add_norm ?_
  norm_cast
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
r : ℕ
hr : FiniteDimensional.finrank ℝ E < r
f : 𝓢(E, F)
h_int : Integrable fun x => (1 + ‖x‖) ^ (-↑r)
⊢ ∫ (x : E), ‖f x‖ ≤ (2 ^ r * ∫ (x : E), (1 + ‖x‖) ^ (-↑r)) * sup_Iic_seminorm 𝕜 r 0 f
Theorem: SchwartzMap.integral_norm_le_const_mul_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
r : ℕ
hr : FiniteDimensional.finrank ℝ E < r
f : 𝓢(E, F)
h_int : Integrable fun x => (1 + ‖x‖) ^ (-↑r)
⊢ ∫ (x : E), ‖f x‖ ≤ (2 ^ r * ∫ (x : E), (1 + ‖x‖) ^ (-↑r)) * sup_Iic_seminorm 𝕜 r 0 f
Tactic:
conv => rhs; rw [mul_assoc]; rhs; rw [mul_comm]
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
r : ℕ
hr : FiniteDimensional.finrank ℝ E < r
f : 𝓢(E, F)
h_int : Integrable fun x => (1 + ‖x‖) ^ (-↑r)
⊢ ∫ (x : E), ‖f x‖ ≤ 2 ^ r * (sup_Iic_seminorm 𝕜 r 0 f * ∫ (x : E), (1 + ‖x‖) ^ (-↑r))
Theorem: SchwartzMap.integral_norm_le_const_mul_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
r : ℕ
hr : FiniteDimensional.finrank ℝ E < r
f : 𝓢(E, F)
h_int : Integrable fun x => (1 + ‖x‖) ^ (-↑r)
⊢ ∫ (x : E), ‖f x‖ ≤ 2 ^ r * (sup_Iic_seminorm 𝕜 r 0 f * ∫ (x : E), (1 + ‖x‖) ^ (-↑r))
Tactic:
rw [← mul_assoc]
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
r : ℕ
hr : FiniteDimensional.finrank ℝ E < r
f : 𝓢(E, F)
h_int : Integrable fun x => (1 + ‖x‖) ^ (-↑r)
⊢ ∫ (x : E), ‖f x‖ ≤ 2 ^ r * sup_Iic_seminorm 𝕜 r 0 f * ∫ (x : E), (1 + ‖x‖) ^ (-↑r)
Theorem: SchwartzMap.integral_norm_le_const_mul_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
r : ℕ
hr : FiniteDimensional.finrank ℝ E < r
f : 𝓢(E, F)
h_int : Integrable fun x => (1 + ‖x‖) ^ (-↑r)
⊢ ∫ (x : E), ‖f x‖ ≤ 2 ^ r * sup_Iic_seminorm 𝕜 r 0 f * ∫ (x : E), (1 + ‖x‖) ^ (-↑r)
Tactic:
rw [← integral_mul_left]
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
r : ℕ
hr : FiniteDimensional.finrank ℝ E < r
f : 𝓢(E, F)
h_int : Integrable fun x => (1 + ‖x‖) ^ (-↑r)
⊢ ∫ (x : E), ‖f x‖ ≤ ∫ (a : E), 2 ^ r * sup_Iic_seminorm 𝕜 r 0 f * (1 + ‖a‖) ^ (-↑r)
Theorem: SchwartzMap.integral_norm_le_const_mul_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
r : ℕ
hr : FiniteDimensional.finrank ℝ E < r
f : 𝓢(E, F)
h_int : Integrable fun x => (1 + ‖x‖) ^ (-↑r)
⊢ ∫ (x : E), ‖f x‖ ≤ ∫ (a : E), 2 ^ r * sup_Iic_seminorm 𝕜 r 0 f * (1 + ‖a‖) ^ (-↑r)
Tactic:
refine integral_mono f.integrable.norm (h_int.const_mul _) ?_
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
r : ℕ
hr : FiniteDimensional.finrank ℝ E < r
f : 𝓢(E, F)
h_int : Integrable fun x => (1 + ‖x‖) ^ (-↑r)
⊢ (fun x => ‖f x‖) ≤ fun a => 2 ^ r * sup_Iic_seminorm 𝕜 r 0 f * (1 + ‖a‖) ^ (-↑r)
Theorem: SchwartzMap.integral_norm_le_const_mul_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
r : ℕ
hr : FiniteDimensional.finrank ℝ E < r
f : 𝓢(E, F)
h_int : Integrable fun x => (1 + ‖x‖) ^ (-↑r)
⊢ (fun x => ‖f x‖) ≤ fun a => 2 ^ r * sup_Iic_seminorm 𝕜 r 0 f * (1 + ‖a‖) ^ (-↑r)
Tactic:
intro 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
r : ℕ
hr : FiniteDimensional.finrank ℝ E < r
f : 𝓢(E, F)
h_int : Integrable fun x => (1 + ‖x‖) ^ (-↑r)
x : E
⊢ (fun x => ‖f x‖) x ≤ (fun a => 2 ^ r * sup_Iic_seminorm 𝕜 r 0 f * (1 + ‖a‖) ^ (-↑r)) x
Theorem: SchwartzMap.integral_norm_le_const_mul_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
r : ℕ
hr : FiniteDimensional.finrank ℝ E < r
f : 𝓢(E, F)
h_int : Integrable fun x => (1 + ‖x‖) ^ (-↑r)
x : E
⊢ (fun x => ‖f x‖) x ≤ (fun a => 2 ^ r * sup_Iic_seminorm 𝕜 r 0 f * (1 + ‖a‖) ^ (-↑r)) x
Tactic:
simp
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
r : ℕ
hr : FiniteDimensional.finrank ℝ E < r
f : 𝓢(E, F)
h_int : Integrable fun x => (1 + ‖x‖) ^ (-↑r)
x : E
⊢ ‖f x‖ ≤ 2 ^ r * sup_Iic_seminorm 𝕜 r 0 f * (1 + ‖x‖) ^ (-↑r)
Theorem: SchwartzMap.integral_norm_le_const_mul_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
r : ℕ
hr : FiniteDimensional.finrank ℝ E < r
f : 𝓢(E, F)
h_int : Integrable fun x => (1 + ‖x‖) ^ (-↑r)
x : E
⊢ ‖f x‖ ≤ 2 ^ r * sup_Iic_seminorm 𝕜 r 0 f * (1 + ‖x‖) ^ (-↑r)
Tactic:
exact norm_le_sup_Iic_seminorm_mul_one_add_norm_pow_neg r f x
Proof state after:
no goals
Theorem: SchwartzMap.integral_norm_le_const_mul_sup_Iic_seminorm
Proof state before:
case h_int
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
r : ℕ
hr : FiniteDimensional.finrank ℝ E < r
f : 𝓢(E, F)
⊢ Integrable fun x => (1 + ‖x‖) ^ (-↑r)
Tactic:
refine integrable_one_add_norm ?_
Proof state after:
case h_int
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
r : ℕ
hr : FiniteDimensional.finrank ℝ E < r
f : 𝓢(E, F)
⊢ ↑(FiniteDimensional.finrank ℝ E) < ↑r
Theorem: SchwartzMap.integral_norm_le_const_mul_sup_Iic_seminorm
Proof state before:
case h_int
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
r : ℕ
hr : FiniteDimensional.finrank ℝ E < r
f : 𝓢(E, F)
⊢ ↑(FiniteDimensional.finrank ℝ E) < ↑r
Tactic:
norm_cast
Proof state after:
no goals
Theorem: SchwartzMap.toL1_add
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
φ θ : 𝓢(E, F)
⊢ toL1 (φ + θ) = toL1 φ + toL1 θ
Tactic:
rfl
Proof state after:
no goals
Theorem: SchwartzMap.toL1_smul
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
c : 𝕜
φ : 𝓢(E, F)
⊢ toL1 (c • φ) = c • toL1 φ
Tactic:
rfl
Proof state after:
no goals
Theorem: SchwartzMap.integralCLM'_apply
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
𝕜' : Type u_4
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : CompleteSpace F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
⊢ (integralCLM' 𝕜) f = ∫ (x : E), f x
Tactic:
rw [MeasureTheory.integral_eq _ f.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
𝕜 : Type u_3
𝕜' : Type u_4
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : CompleteSpace F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
⊢ (integralCLM' 𝕜) f = L1.integral (Integrable.toL1 (fun x => f x) (_ : Integrable fun x => f x))
Theorem: SchwartzMap.integralCLM'_apply
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
𝕜' : Type u_4
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : CompleteSpace F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
⊢ (integralCLM' 𝕜) f = L1.integral (Integrable.toL1 (fun x => f x) (_ : Integrable fun x => f x))
Tactic:
rw [integralCLM', L1.integral_def]
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
𝕜' : Type u_4
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : CompleteSpace F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
⊢ (ContinuousLinearMap.comp (L1.integralCLM' 𝕜) (toL1_CLM' 𝕜)) f =
    L1.integralCLM (Integrable.toL1 (fun x => f x) (_ : Integrable fun x => f x))
Theorem: SchwartzMap.integralCLM'_apply
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
𝕜' : Type u_4
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : CompleteSpace F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
⊢ (ContinuousLinearMap.comp (L1.integralCLM' 𝕜) (toL1_CLM' 𝕜)) f =
    L1.integralCLM (Integrable.toL1 (fun x => f x) (_ : Integrable fun x => f x))
Tactic:
rfl
Proof state after:
no goals
Theorem: SchwartzMap.integralCLM_apply
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
𝕜' : Type u_4
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : CompleteSpace F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
⊢ integralCLM f = ∫ (x : E), f x
Tactic:
rw [integralCLM]
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
𝕜' : Type u_4
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : CompleteSpace F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
⊢ (integralCLM' ℝ) f = ∫ (x : E), f x
Theorem: SchwartzMap.integralCLM_apply
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
𝕜' : Type u_4
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : CompleteSpace F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
⊢ (integralCLM' ℝ) f = ∫ (x : E), f x
Tactic:
exact integralCLM'_apply
Proof state after:
no goals
Theorem: SchwartzMap.integralCLM_neg_apply
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
𝕜' : Type u_4
inst✝³ : NontriviallyNormedField 𝕜
inst✝² : CompleteSpace F
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
⊢ integralCLM (-f) = -integralCLM f
Tactic:
rw [ContinuousLinearMap.map_neg]
Proof state after:
no goals
Theorem: SchwartzMap.integralCLM_smul_apply
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
𝕜' : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜✝
inst✝⁵ : CompleteSpace F
inst✝⁴ : NormedSpace 𝕜✝ F
inst✝³ : SMulCommClass ℝ 𝕜✝ F
𝕜 : Type u_5
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
c : 𝕜
f : 𝓢(E, F)
⊢ integralCLM (c • f) = c • integralCLM f
Tactic:
simp [integralCLM_apply, integral_smul]
Proof state after:
no goals
Theorem: SchwartzMap.Distribution.one_apply
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
𝕜' : Type u_4
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : SMulCommClass ℝ 𝕜 F
inst✝⁴ : NormedField 𝕜'
inst✝³ : NormedSpace ℝ 𝕜'
inst✝² : NormedSpace 𝕜' F
inst✝¹ : SMulCommClass ℝ 𝕜' F
inst✝ : IsScalarTower ℝ 𝕜' F
φ : 𝓢(E, F)
⊢ 1 φ = ∫ (x : E), φ x
Tactic:
change (One.one : 𝓢(E, F) →L[ℝ] F) φ = _
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
𝕜' : Type u_4
inst✝⁸ : NontriviallyNormedField 𝕜
inst✝⁷ : CompleteSpace F
inst✝⁶ : NormedSpace 𝕜 F
inst✝⁵ : SMulCommClass ℝ 𝕜 F
inst✝⁴ : NormedField 𝕜'
inst✝³ : NormedSpace ℝ 𝕜'
inst✝² : NormedSpace 𝕜' F
inst✝¹ : SMulCommClass ℝ 𝕜' F
inst✝ : IsScalarTower ℝ 𝕜' F
φ : 𝓢(E, F)
⊢ One.one φ = ∫ (x : E), φ x