internlm/Lean-Github huggingface dataset:
Theorem: SchwartzMap.integrable_one_add_norm_rpow_smul
Proof state before:
case refine_1
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)
⊢ AEStronglyMeasurable (fun x => (1 + ‖x‖) ^ n • f x) volume
Tactic:
refine AEStronglyMeasurable.smul ?_ f.continuous.aestronglyMeasurable
Proof state after:
case refine_1
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)
⊢ AEStronglyMeasurable (fun x => (1 + ‖x‖) ^ n) volume
Theorem: SchwartzMap.integrable_one_add_norm_rpow_smul
Proof state before:
case refine_1
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)
⊢ AEStronglyMeasurable (fun x => (1 + ‖x‖) ^ n) volume
Tactic:
refine (AEMeasurable.pow_const ?_ n).aestronglyMeasurable
Proof state after:
case refine_1
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)
⊢ AEMeasurable fun x => 1 + ‖x‖
Theorem: SchwartzMap.integrable_one_add_norm_rpow_smul
Proof state before:
case refine_1
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)
⊢ AEMeasurable fun x => 1 + ‖x‖
Tactic:
exact (continuous_const.add continuous_norm).aemeasurable
Proof state after:
no goals
Theorem: SchwartzMap.integrable_one_add_norm_rpow_smul
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)
⊢ HasFiniteIntegral fun x => (1 + ‖x‖) ^ n • f x
Tactic:
rw [HasFiniteIntegral]
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)
⊢ ∫⁻ (a : E), ↑‖(1 + ‖a‖) ^ n • f a‖₊ < ⊤
Theorem: SchwartzMap.integrable_one_add_norm_rpow_smul
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)
⊢ ∫⁻ (a : E), ↑‖(1 + ‖a‖) ^ n • f a‖₊ < ⊤
Tactic:
rw [← snorm_one_eq_lintegral_nnnorm]
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)
⊢ snorm (fun a => (1 + ‖a‖) ^ n • f a) 1 volume < ⊤
Theorem: SchwartzMap.integrable_one_add_norm_rpow_smul
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 => (1 + ‖a‖) ^ n • f a) 1 volume < ⊤
Tactic:
exact snorm_nnreal_one_add_norm_rpow_smul_lt_top n f zero_lt_one
Proof state after:
no goals
Theorem: SchwartzMap.integrable_norm_pow_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
n : ℕ
f : 𝓢(E, F)
⊢ Integrable fun x => ‖x‖ ^ n • f x
Tactic:
refine And.intro ?_ ?_
Proof state after:
case refine_1
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)
⊢ AEStronglyMeasurable (fun x => ‖x‖ ^ n • f x) volume

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)
⊢ HasFiniteIntegral fun x => ‖x‖ ^ n • f x
Theorem: SchwartzMap.integrable_norm_pow_smul
Proof state before:
case refine_1
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)
⊢ AEStronglyMeasurable (fun x => ‖x‖ ^ n • f x) volume

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)
⊢ HasFiniteIntegral fun x => ‖x‖ ^ n • f x
Tactic:
. refine AEStronglyMeasurable.smul ?_ f.continuous.aestronglyMeasurable
  refine (AEMeasurable.pow_const ?_ n).aestronglyMeasurable
  exact measurable_norm.aemeasurable
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)
⊢ HasFiniteIntegral fun x => ‖x‖ ^ n • f x
Theorem: SchwartzMap.integrable_norm_pow_smul
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)
⊢ HasFiniteIntegral fun x => ‖x‖ ^ n • f x
Tactic:
. rw [HasFiniteIntegral]
  rw [← snorm_one_eq_lintegral_nnnorm]
  refine lt_of_le_of_lt ?_ (snorm_nnreal_one_add_norm_rpow_smul_lt_top n f zero_lt_one)
  refine snorm_mono ?_
  intro x
  simp [norm_smul]
  refine mul_le_mul_of_nonneg_right ?_ (norm_nonneg (f x))
  rw [abs_of_nonneg (by simp)]
  refine pow_le_pow_left ?_ ?_ _ <;> simp
Proof state after:
no goals
Theorem: SchwartzMap.integrable_norm_pow_smul
Proof state before:
case refine_1
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)
⊢ AEStronglyMeasurable (fun x => ‖x‖ ^ n • f x) volume
Tactic:
refine AEStronglyMeasurable.smul ?_ f.continuous.aestronglyMeasurable
Proof state after:
case refine_1
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)
⊢ AEStronglyMeasurable (fun x => ‖x‖ ^ n) volume
Theorem: SchwartzMap.integrable_norm_pow_smul
Proof state before:
case refine_1
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)
⊢ AEStronglyMeasurable (fun x => ‖x‖ ^ n) volume
Tactic:
refine (AEMeasurable.pow_const ?_ n).aestronglyMeasurable
Proof state after:
case refine_1
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)
⊢ AEMeasurable fun x => ‖x‖
Theorem: SchwartzMap.integrable_norm_pow_smul
Proof state before:
case refine_1
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)
⊢ AEMeasurable fun x => ‖x‖
Tactic:
exact measurable_norm.aemeasurable
Proof state after:
no goals
Theorem: SchwartzMap.integrable_norm_pow_smul
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)
⊢ HasFiniteIntegral fun x => ‖x‖ ^ n • f x
Tactic:
rw [HasFiniteIntegral]
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)
⊢ ∫⁻ (a : E), ↑‖‖a‖ ^ n • f a‖₊ < ⊤
Theorem: SchwartzMap.integrable_norm_pow_smul
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)
⊢ ∫⁻ (a : E), ↑‖‖a‖ ^ n • f a‖₊ < ⊤
Tactic:
rw [← snorm_one_eq_lintegral_nnnorm]
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)
⊢ snorm (fun a => ‖a‖ ^ n • f a) 1 volume < ⊤
Theorem: SchwartzMap.integrable_norm_pow_smul
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 < ⊤
Tactic:
refine lt_of_le_of_lt ?_ (snorm_nnreal_one_add_norm_rpow_smul_lt_top n f zero_lt_one)
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)
⊢ snorm (fun a => ‖a‖ ^ n • f a) 1 volume ≤ snorm (fun x => (1 + ‖x‖) ^ ↑n • f x) (↑1) volume
Theorem: SchwartzMap.integrable_norm_pow_smul
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_smul
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_smul
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_smul
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_smul
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_smul
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_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
n : ℕ
f : 𝓢(E, F)
x : E
⊢ 0 ≤ 1 + ‖x‖
Tactic:
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)
⊢ Integrable fun x => ‖x‖ ^ n * ‖f x‖
Tactic:
refine And.intro ?_ ?_
Proof state after:
case refine_1
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)
⊢ AEStronglyMeasurable (fun x => ‖x‖ ^ n * ‖f x‖) volume

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)
⊢ HasFiniteIntegral fun x => ‖x‖ ^ n * ‖f x‖
Theorem: SchwartzMap.integrable_norm_pow_mul_norm
Proof state before:
case refine_1
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)
⊢ AEStronglyMeasurable (fun x => ‖x‖ ^ n * ‖f x‖) volume

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)
⊢ HasFiniteIntegral fun x => ‖x‖ ^ n * ‖f x‖
Tactic:
. refine AEStronglyMeasurable.mul ?_ f.continuous.norm.aestronglyMeasurable
  refine (AEMeasurable.pow_const ?_ n).aestronglyMeasurable
  exact measurable_norm.aemeasurable
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)
⊢ HasFiniteIntegral fun x => ‖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)
⊢ HasFiniteIntegral fun x => ‖x‖ ^ n * ‖f x‖
Tactic:
. rw [HasFiniteIntegral]
  rw [← snorm_one_eq_lintegral_nnnorm]
  refine lt_of_le_of_lt ?_ (snorm_nnreal_one_add_norm_rpow_smul_lt_top n f zero_lt_one)
  refine snorm_mono ?_
  intro x
  simp [norm_smul]
  refine mul_le_mul_of_nonneg_right ?_ (norm_nonneg (f x))
  rw [abs_of_nonneg (by simp)]
  refine pow_le_pow_left ?_ ?_ _ <;> simp
Proof state after:
no goals
Theorem: SchwartzMap.integrable_norm_pow_mul_norm
Proof state before:
case refine_1
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)
⊢ AEStronglyMeasurable (fun x => ‖x‖ ^ n * ‖f x‖) volume
Tactic:
refine AEStronglyMeasurable.mul ?_ f.continuous.norm.aestronglyMeasurable
Proof state after:
case refine_1
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)
⊢ AEStronglyMeasurable (fun x => ‖x‖ ^ n) volume
Theorem: SchwartzMap.integrable_norm_pow_mul_norm
Proof state before:
case refine_1
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)
⊢ AEStronglyMeasurable (fun x => ‖x‖ ^ n) volume
Tactic:
refine (AEMeasurable.pow_const ?_ n).aestronglyMeasurable
Proof state after:
case refine_1
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)
⊢ AEMeasurable fun x => ‖x‖
Theorem: SchwartzMap.integrable_norm_pow_mul_norm
Proof state before:
case refine_1
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)
⊢ AEMeasurable fun x => ‖x‖
Tactic:
exact measurable_norm.aemeasurable
Proof state after:
no goals
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)
⊢ HasFiniteIntegral fun x => ‖x‖ ^ n * ‖f x‖
Tactic:
rw [HasFiniteIntegral]
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)
⊢ ∫⁻ (a : E), ↑‖‖a‖ ^ n * ‖f a‖‖₊ < ⊤
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)
⊢ ∫⁻ (a : E), ↑‖‖a‖ ^ n * ‖f a‖‖₊ < ⊤
Tactic:
rw [← snorm_one_eq_lintegral_nnnorm]
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)
⊢ snorm (fun a => ‖a‖ ^ n * ‖f a‖) 1 volume < ⊤
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 < ⊤
Tactic:
refine lt_of_le_of_lt ?_ (snorm_nnreal_one_add_norm_rpow_smul_lt_top n f zero_lt_one)
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)
⊢ snorm (fun a => ‖a‖ ^ n * ‖f a‖) 1 volume ≤ snorm (fun x => (1 + ‖x‖) ^ ↑n • f x) (↑1) volume