Theorem: SchwartzMap.integral_norm_le_const_mul_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
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 : ℝ))
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

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
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

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]
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))

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]
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)

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]
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)

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 _) ?_
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)

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
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

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
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)

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
State after:
no goals

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 ?_
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

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
State after:
no goals