internlm/Lean-Github huggingface dataset:
Theorem: SchwartzMap.snorm_nnreal_one_add_norm_rpow_smul_lt_top
Proof state before:
case this.hx
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)
p : NNReal
hp : 0 < p
r : ℝ
hr : ↑(FiniteDimensional.finrank ℝ E) + 1 = r
C : ℝ
hC_nonneg : 0 ≤ C
x : E
hC : ‖f x‖ ^ ↑p ≤ C * (1 + ‖x‖) ^ (-(n * ↑p) + -r)
⊢ 0 ≤ 1 + ‖x‖
Tactic:
simp
Proof state after:
no goals
Theorem: SchwartzMap.snorm_nnreal_one_add_norm_rpow_smul_lt_top
Proof state before:
case intro.intro
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)
p : NNReal
hp : 0 < p
r : ℝ
hr : ↑(FiniteDimensional.finrank ℝ E) + 1 = r
C : ℝ
hC_nonneg : 0 ≤ C
hC : ∀ (x : E), ‖f x‖ ^ ↑p ≤ C * (1 + ‖x‖) ^ (-(n * ↑p) + -r)
this : ∫⁻ (x : E), ↑‖(1 + ‖x‖) ^ n • f x‖₊ ^ ↑p ≤ ∫⁻ (x : E), ENNReal.ofReal (C * (1 + ‖x‖) ^ (-r))
⊢ ∫⁻ (a : E), ↑‖(1 + ‖a‖) ^ n • f a‖₊ ^ ↑p < ⊤
Tactic:
refine lt_of_le_of_lt this ?_
Proof state after:
case intro.intro
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)
p : NNReal
hp : 0 < p
r : ℝ
hr : ↑(FiniteDimensional.finrank ℝ E) + 1 = r
C : ℝ
hC_nonneg : 0 ≤ C
hC : ∀ (x : E), ‖f x‖ ^ ↑p ≤ C * (1 + ‖x‖) ^ (-(n * ↑p) + -r)
this : ∫⁻ (x : E), ↑‖(1 + ‖x‖) ^ n • f x‖₊ ^ ↑p ≤ ∫⁻ (x : E), ENNReal.ofReal (C * (1 + ‖x‖) ^ (-r))
⊢ ∫⁻ (x : E), ENNReal.ofReal (C * (1 + ‖x‖) ^ (-r)) < ⊤
Theorem: SchwartzMap.snorm_nnreal_one_add_norm_rpow_smul_lt_top
Proof state before:
case intro.intro
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)
p : NNReal
hp : 0 < p
r : ℝ
hr : ↑(FiniteDimensional.finrank ℝ E) + 1 = r
C : ℝ
hC_nonneg : 0 ≤ C
hC : ∀ (x : E), ‖f x‖ ^ ↑p ≤ C * (1 + ‖x‖) ^ (-(n * ↑p) + -r)
this : ∫⁻ (x : E), ↑‖(1 + ‖x‖) ^ n • f x‖₊ ^ ↑p ≤ ∫⁻ (x : E), ENNReal.ofReal (C * (1 + ‖x‖) ^ (-r))
⊢ ∫⁻ (x : E), ENNReal.ofReal (C * (1 + ‖x‖) ^ (-r)) < ⊤
Tactic:
simp_rw [ENNReal.ofReal_mul hC_nonneg]
Proof state after:
case intro.intro
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)
p : NNReal
hp : 0 < p
r : ℝ
hr : ↑(FiniteDimensional.finrank ℝ E) + 1 = r
C : ℝ
hC_nonneg : 0 ≤ C
hC : ∀ (x : E), ‖f x‖ ^ ↑p ≤ C * (1 + ‖x‖) ^ (-(n * ↑p) + -r)
this : ∫⁻ (x : E), ↑‖(1 + ‖x‖) ^ n • f x‖₊ ^ ↑p ≤ ∫⁻ (x : E), ENNReal.ofReal (C * (1 + ‖x‖) ^ (-r))
⊢ ∫⁻ (x : E), ENNReal.ofReal C * ENNReal.ofReal ((1 + ‖x‖) ^ (-r)) < ⊤
Theorem: SchwartzMap.snorm_nnreal_one_add_norm_rpow_smul_lt_top
Proof state before:
case intro.intro
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)
p : NNReal
hp : 0 < p
r : ℝ
hr : ↑(FiniteDimensional.finrank ℝ E) + 1 = r
C : ℝ
hC_nonneg : 0 ≤ C
hC : ∀ (x : E), ‖f x‖ ^ ↑p ≤ C * (1 + ‖x‖) ^ (-(n * ↑p) + -r)
this : ∫⁻ (x : E), ↑‖(1 + ‖x‖) ^ n • f x‖₊ ^ ↑p ≤ ∫⁻ (x : E), ENNReal.ofReal (C * (1 + ‖x‖) ^ (-r))
⊢ ∫⁻ (x : E), ENNReal.ofReal C * ENNReal.ofReal ((1 + ‖x‖) ^ (-r)) < ⊤
Tactic:
rw [lintegral_const_mul]
Proof state after:
case intro.intro
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)
p : NNReal
hp : 0 < p
r : ℝ
hr : ↑(FiniteDimensional.finrank ℝ E) + 1 = r
C : ℝ
hC_nonneg : 0 ≤ C
hC : ∀ (x : E), ‖f x‖ ^ ↑p ≤ C * (1 + ‖x‖) ^ (-(n * ↑p) + -r)
this : ∫⁻ (x : E), ↑‖(1 + ‖x‖) ^ n • f x‖₊ ^ ↑p ≤ ∫⁻ (x : E), ENNReal.ofReal (C * (1 + ‖x‖) ^ (-r))
⊢ ENNReal.ofReal C * ∫⁻ (a : E), ENNReal.ofReal ((1 + ‖a‖) ^ (-r)) < ⊤

case intro.intro.hf
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)
p : NNReal
hp : 0 < p
r : ℝ
hr : ↑(FiniteDimensional.finrank ℝ E) + 1 = r
C : ℝ
hC_nonneg : 0 ≤ C
hC : ∀ (x : E), ‖f x‖ ^ ↑p ≤ C * (1 + ‖x‖) ^ (-(n * ↑p) + -r)
this : ∫⁻ (x : E), ↑‖(1 + ‖x‖) ^ n • f x‖₊ ^ ↑p ≤ ∫⁻ (x : E), ENNReal.ofReal (C * (1 + ‖x‖) ^ (-r))
⊢ Measurable fun x => ENNReal.ofReal ((1 + ‖x‖) ^ (-r))
Theorem: SchwartzMap.snorm_nnreal_one_add_norm_rpow_smul_lt_top
Proof state before:
case intro.intro
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)
p : NNReal
hp : 0 < p
r : ℝ
hr : ↑(FiniteDimensional.finrank ℝ E) + 1 = r
C : ℝ
hC_nonneg : 0 ≤ C
hC : ∀ (x : E), ‖f x‖ ^ ↑p ≤ C * (1 + ‖x‖) ^ (-(n * ↑p) + -r)
this : ∫⁻ (x : E), ↑‖(1 + ‖x‖) ^ n • f x‖₊ ^ ↑p ≤ ∫⁻ (x : E), ENNReal.ofReal (C * (1 + ‖x‖) ^ (-r))
⊢ ENNReal.ofReal C * ∫⁻ (a : E), ENNReal.ofReal ((1 + ‖a‖) ^ (-r)) < ⊤

case intro.intro.hf
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)
p : NNReal
hp : 0 < p
r : ℝ
hr : ↑(FiniteDimensional.finrank ℝ E) + 1 = r
C : ℝ
hC_nonneg : 0 ≤ C
hC : ∀ (x : E), ‖f x‖ ^ ↑p ≤ C * (1 + ‖x‖) ^ (-(n * ↑p) + -r)
this : ∫⁻ (x : E), ↑‖(1 + ‖x‖) ^ n • f x‖₊ ^ ↑p ≤ ∫⁻ (x : E), ENNReal.ofReal (C * (1 + ‖x‖) ^ (-r))
⊢ Measurable fun x => ENNReal.ofReal ((1 + ‖x‖) ^ (-r))
Tactic:
swap
Proof state after:
case intro.intro.hf
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)
p : NNReal
hp : 0 < p
r : ℝ
hr : ↑(FiniteDimensional.finrank ℝ E) + 1 = r
C : ℝ
hC_nonneg : 0 ≤ C
hC : ∀ (x : E), ‖f x‖ ^ ↑p ≤ C * (1 + ‖x‖) ^ (-(n * ↑p) + -r)
this : ∫⁻ (x : E), ↑‖(1 + ‖x‖) ^ n • f x‖₊ ^ ↑p ≤ ∫⁻ (x : E), ENNReal.ofReal (C * (1 + ‖x‖) ^ (-r))
⊢ Measurable fun x => ENNReal.ofReal ((1 + ‖x‖) ^ (-r))

case intro.intro
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)
p : NNReal
hp : 0 < p
r : ℝ
hr : ↑(FiniteDimensional.finrank ℝ E) + 1 = r
C : ℝ
hC_nonneg : 0 ≤ C
hC : ∀ (x : E), ‖f x‖ ^ ↑p ≤ C * (1 + ‖x‖) ^ (-(n * ↑p) + -r)
this : ∫⁻ (x : E), ↑‖(1 + ‖x‖) ^ n • f x‖₊ ^ ↑p ≤ ∫⁻ (x : E), ENNReal.ofReal (C * (1 + ‖x‖) ^ (-r))
⊢ ENNReal.ofReal C * ∫⁻ (a : E), ENNReal.ofReal ((1 + ‖a‖) ^ (-r)) < ⊤
Theorem: SchwartzMap.snorm_nnreal_one_add_norm_rpow_smul_lt_top
Proof state before:
case intro.intro.hf
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)
p : NNReal
hp : 0 < p
r : ℝ
hr : ↑(FiniteDimensional.finrank ℝ E) + 1 = r
C : ℝ
hC_nonneg : 0 ≤ C
hC : ∀ (x : E), ‖f x‖ ^ ↑p ≤ C * (1 + ‖x‖) ^ (-(n * ↑p) + -r)
this : ∫⁻ (x : E), ↑‖(1 + ‖x‖) ^ n • f x‖₊ ^ ↑p ≤ ∫⁻ (x : E), ENNReal.ofReal (C * (1 + ‖x‖) ^ (-r))
⊢ Measurable fun x => ENNReal.ofReal ((1 + ‖x‖) ^ (-r))

case intro.intro
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)
p : NNReal
hp : 0 < p
r : ℝ
hr : ↑(FiniteDimensional.finrank ℝ E) + 1 = r
C : ℝ
hC_nonneg : 0 ≤ C
hC : ∀ (x : E), ‖f x‖ ^ ↑p ≤ C * (1 + ‖x‖) ^ (-(n * ↑p) + -r)
this : ∫⁻ (x : E), ↑‖(1 + ‖x‖) ^ n • f x‖₊ ^ ↑p ≤ ∫⁻ (x : E), ENNReal.ofReal (C * (1 + ‖x‖) ^ (-r))
⊢ ENNReal.ofReal C * ∫⁻ (a : E), ENNReal.ofReal ((1 + ‖a‖) ^ (-r)) < ⊤
Tactic:
. refine Measurable.ennreal_ofReal ?_
  exact Measurable.pow_const (Measurable.const_add measurable_norm _) _
Proof state after:
case intro.intro
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)
p : NNReal
hp : 0 < p
r : ℝ
hr : ↑(FiniteDimensional.finrank ℝ E) + 1 = r
C : ℝ
hC_nonneg : 0 ≤ C
hC : ∀ (x : E), ‖f x‖ ^ ↑p ≤ C * (1 + ‖x‖) ^ (-(n * ↑p) + -r)
this : ∫⁻ (x : E), ↑‖(1 + ‖x‖) ^ n • f x‖₊ ^ ↑p ≤ ∫⁻ (x : E), ENNReal.ofReal (C * (1 + ‖x‖) ^ (-r))
⊢ ENNReal.ofReal C * ∫⁻ (a : E), ENNReal.ofReal ((1 + ‖a‖) ^ (-r)) < ⊤
Theorem: SchwartzMap.snorm_nnreal_one_add_norm_rpow_smul_lt_top
Proof state before:
case intro.intro
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)
p : NNReal
hp : 0 < p
r : ℝ
hr : ↑(FiniteDimensional.finrank ℝ E) + 1 = r
C : ℝ
hC_nonneg : 0 ≤ C
hC : ∀ (x : E), ‖f x‖ ^ ↑p ≤ C * (1 + ‖x‖) ^ (-(n * ↑p) + -r)
this : ∫⁻ (x : E), ↑‖(1 + ‖x‖) ^ n • f x‖₊ ^ ↑p ≤ ∫⁻ (x : E), ENNReal.ofReal (C * (1 + ‖x‖) ^ (-r))
⊢ ENNReal.ofReal C * ∫⁻ (a : E), ENNReal.ofReal ((1 + ‖a‖) ^ (-r)) < ⊤
Tactic:
refine ENNReal.mul_lt_top (by simp) ?_
Proof state after:
case intro.intro
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)
p : NNReal
hp : 0 < p
r : ℝ
hr : ↑(FiniteDimensional.finrank ℝ E) + 1 = r
C : ℝ
hC_nonneg : 0 ≤ C
hC : ∀ (x : E), ‖f x‖ ^ ↑p ≤ C * (1 + ‖x‖) ^ (-(n * ↑p) + -r)
this : ∫⁻ (x : E), ↑‖(1 + ‖x‖) ^ n • f x‖₊ ^ ↑p ≤ ∫⁻ (x : E), ENNReal.ofReal (C * (1 + ‖x‖) ^ (-r))
⊢ ∫⁻ (a : E), ENNReal.ofReal ((1 + ‖a‖) ^ (-r)) ≠ ⊤
Theorem: SchwartzMap.snorm_nnreal_one_add_norm_rpow_smul_lt_top
Proof state before:
case intro.intro
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)
p : NNReal
hp : 0 < p
r : ℝ
hr : ↑(FiniteDimensional.finrank ℝ E) + 1 = r
C : ℝ
hC_nonneg : 0 ≤ C
hC : ∀ (x : E), ‖f x‖ ^ ↑p ≤ C * (1 + ‖x‖) ^ (-(n * ↑p) + -r)
this : ∫⁻ (x : E), ↑‖(1 + ‖x‖) ^ n • f x‖₊ ^ ↑p ≤ ∫⁻ (x : E), ENNReal.ofReal (C * (1 + ‖x‖) ^ (-r))
⊢ ∫⁻ (a : E), ENNReal.ofReal ((1 + ‖a‖) ^ (-r)) ≠ ⊤
Tactic:
rw [← lt_top_iff_ne_top]
Proof state after:
case intro.intro
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)
p : NNReal
hp : 0 < p
r : ℝ
hr : ↑(FiniteDimensional.finrank ℝ E) + 1 = r
C : ℝ
hC_nonneg : 0 ≤ C
hC : ∀ (x : E), ‖f x‖ ^ ↑p ≤ C * (1 + ‖x‖) ^ (-(n * ↑p) + -r)
this : ∫⁻ (x : E), ↑‖(1 + ‖x‖) ^ n • f x‖₊ ^ ↑p ≤ ∫⁻ (x : E), ENNReal.ofReal (C * (1 + ‖x‖) ^ (-r))
⊢ ∫⁻ (a : E), ENNReal.ofReal ((1 + ‖a‖) ^ (-r)) < ⊤
Theorem: SchwartzMap.snorm_nnreal_one_add_norm_rpow_smul_lt_top
Proof state before:
case intro.intro
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)
p : NNReal
hp : 0 < p
r : ℝ
hr : ↑(FiniteDimensional.finrank ℝ E) + 1 = r
C : ℝ
hC_nonneg : 0 ≤ C
hC : ∀ (x : E), ‖f x‖ ^ ↑p ≤ C * (1 + ‖x‖) ^ (-(n * ↑p) + -r)
this : ∫⁻ (x : E), ↑‖(1 + ‖x‖) ^ n • f x‖₊ ^ ↑p ≤ ∫⁻ (x : E), ENNReal.ofReal (C * (1 + ‖x‖) ^ (-r))
⊢ ∫⁻ (a : E), ENNReal.ofReal ((1 + ‖a‖) ^ (-r)) < ⊤
Tactic:
refine finite_integral_one_add_norm ?_
Proof state after:
case intro.intro
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)
p : NNReal
hp : 0 < p
r : ℝ
hr : ↑(FiniteDimensional.finrank ℝ E) + 1 = r
C : ℝ
hC_nonneg : 0 ≤ C
hC : ∀ (x : E), ‖f x‖ ^ ↑p ≤ C * (1 + ‖x‖) ^ (-(n * ↑p) + -r)
this : ∫⁻ (x : E), ↑‖(1 + ‖x‖) ^ n • f x‖₊ ^ ↑p ≤ ∫⁻ (x : E), ENNReal.ofReal (C * (1 + ‖x‖) ^ (-r))
⊢ ↑(FiniteDimensional.finrank ℝ E) < r
Theorem: SchwartzMap.snorm_nnreal_one_add_norm_rpow_smul_lt_top
Proof state before:
case intro.intro
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)
p : NNReal
hp : 0 < p
r : ℝ
hr : ↑(FiniteDimensional.finrank ℝ E) + 1 = r
C : ℝ
hC_nonneg : 0 ≤ C
hC : ∀ (x : E), ‖f x‖ ^ ↑p ≤ C * (1 + ‖x‖) ^ (-(n * ↑p) + -r)
this : ∫⁻ (x : E), ↑‖(1 + ‖x‖) ^ n • f x‖₊ ^ ↑p ≤ ∫⁻ (x : E), ENNReal.ofReal (C * (1 + ‖x‖) ^ (-r))
⊢ ↑(FiniteDimensional.finrank ℝ E) < r
Tactic:
simp [← hr]
Proof state after:
no goals
Theorem: SchwartzMap.snorm_nnreal_one_add_norm_rpow_smul_lt_top
Proof state before:
case intro.intro.hf
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)
p : NNReal
hp : 0 < p
r : ℝ
hr : ↑(FiniteDimensional.finrank ℝ E) + 1 = r
C : ℝ
hC_nonneg : 0 ≤ C
hC : ∀ (x : E), ‖f x‖ ^ ↑p ≤ C * (1 + ‖x‖) ^ (-(n * ↑p) + -r)
this : ∫⁻ (x : E), ↑‖(1 + ‖x‖) ^ n • f x‖₊ ^ ↑p ≤ ∫⁻ (x : E), ENNReal.ofReal (C * (1 + ‖x‖) ^ (-r))
⊢ Measurable fun x => ENNReal.ofReal ((1 + ‖x‖) ^ (-r))
Tactic:
refine Measurable.ennreal_ofReal ?_
Proof state after:
case intro.intro.hf
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)
p : NNReal
hp : 0 < p
r : ℝ
hr : ↑(FiniteDimensional.finrank ℝ E) + 1 = r
C : ℝ
hC_nonneg : 0 ≤ C
hC : ∀ (x : E), ‖f x‖ ^ ↑p ≤ C * (1 + ‖x‖) ^ (-(n * ↑p) + -r)
this : ∫⁻ (x : E), ↑‖(1 + ‖x‖) ^ n • f x‖₊ ^ ↑p ≤ ∫⁻ (x : E), ENNReal.ofReal (C * (1 + ‖x‖) ^ (-r))
⊢ Measurable fun x => (1 + ‖x‖) ^ (-r)
Theorem: SchwartzMap.snorm_nnreal_one_add_norm_rpow_smul_lt_top
Proof state before:
case intro.intro.hf
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)
p : NNReal
hp : 0 < p
r : ℝ
hr : ↑(FiniteDimensional.finrank ℝ E) + 1 = r
C : ℝ
hC_nonneg : 0 ≤ C
hC : ∀ (x : E), ‖f x‖ ^ ↑p ≤ C * (1 + ‖x‖) ^ (-(n * ↑p) + -r)
this : ∫⁻ (x : E), ↑‖(1 + ‖x‖) ^ n • f x‖₊ ^ ↑p ≤ ∫⁻ (x : E), ENNReal.ofReal (C * (1 + ‖x‖) ^ (-r))
⊢ Measurable fun x => (1 + ‖x‖) ^ (-r)
Tactic:
exact Measurable.pow_const (Measurable.const_add measurable_norm _) _
Proof state after:
no goals
Theorem: SchwartzMap.snorm_nnreal_one_add_norm_rpow_smul_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
n : ℝ
f : 𝓢(E, F)
p : NNReal
hp : 0 < p
r : ℝ
hr : ↑(FiniteDimensional.finrank ℝ E) + 1 = r
C : ℝ
hC_nonneg : 0 ≤ C
hC : ∀ (x : E), ‖f x‖ ^ ↑p ≤ C * (1 + ‖x‖) ^ (-(n * ↑p) + -r)
this : ∫⁻ (x : E), ↑‖(1 + ‖x‖) ^ n • f x‖₊ ^ ↑p ≤ ∫⁻ (x : E), ENNReal.ofReal (C * (1 + ‖x‖) ^ (-r))
⊢ ENNReal.ofReal C ≠ ⊤
Tactic:
simp
Proof state after:
no goals
Theorem: SchwartzMap.snorm_nnreal_one_add_norm_rpow_smul_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
n : ℝ
f : 𝓢(E, F)
p : NNReal
hp : 0 < p
r : ℝ
hr : ↑(FiniteDimensional.finrank ℝ E) + 1 = r
C : ℝ
hC_nonneg : 0 ≤ C
x : E
hC : ‖f x‖ ^ ↑p ≤ C * (1 + ‖x‖) ^ (-(n * ↑p) + -r)
⊢ 0 ≤ |(1 + ‖x‖) ^ n|
Tactic:
simp
Proof state after:
no goals
Theorem: SchwartzMap.snorm_nnreal_one_add_norm_rpow_smul_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
n : ℝ
f : 𝓢(E, F)
p : NNReal
hp : 0 < p
r : ℝ
hr : ↑(FiniteDimensional.finrank ℝ E) + 1 = r
C : ℝ
hC_nonneg : 0 ≤ C
x : E
hC : ‖f x‖ ^ ↑p ≤ C * (1 + ‖x‖) ^ (-(n * ↑p) + -r)
⊢ 0 ≤ ‖f x‖
Tactic:
simp
Proof state after:
no goals
Theorem: SchwartzMap.snorm_nnreal_one_add_norm_rpow_smul_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
n : ℝ
f : 𝓢(E, F)
p : NNReal
hp : 0 < p
r : ℝ
hr : ↑(FiniteDimensional.finrank ℝ E) + 1 = r
C : ℝ
hC_nonneg : 0 ≤ C
x : E
hC : ‖f x‖ ^ ↑p ≤ C * (1 + ‖x‖) ^ (-(n * ↑p) + -r)
⊢ 0 ≤ (1 + ‖x‖) ^ n
Tactic:
simp
Proof state after:
no goals
Theorem: SchwartzMap.snorm_nnreal_one_add_norm_rpow_smul_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
n : ℝ
f : 𝓢(E, F)
p : NNReal
hp : 0 < p
r : ℝ
hr : ↑(FiniteDimensional.finrank ℝ E) + 1 = r
C : ℝ
hC_nonneg : 0 ≤ C
x : E
hC : ‖f x‖ ^ ↑p ≤ C * (1 + ‖x‖) ^ (-(n * ↑p) + -r)
⊢ 0 ≤ 1 + ‖x‖
Tactic:
simp
Proof state after:
no goals
Theorem: SchwartzMap.snorm_nnreal_one_add_norm_rpow_smul_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
n : ℝ
f : 𝓢(E, F)
p : NNReal
hp : 0 < p
r : ℝ
hr : ↑(FiniteDimensional.finrank ℝ E) + 1 = r
C : ℝ
hC_nonneg : 0 ≤ C
x : E
hC : ‖f x‖ ^ ↑p ≤ C * (1 + ‖x‖) ^ (-(n * ↑p) + -r)
⊢ 0 < (1 + ‖x‖) ^ (n * ↑p)
Tactic:
simp
Proof state after:
no goals
Theorem: SchwartzMap.snorm_nnreal_one_add_norm_rpow_smul_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
n : ℝ
f : 𝓢(E, F)
p : NNReal
hp : 0 < p
r : ℝ
hr : ↑(FiniteDimensional.finrank ℝ E) + 1 = r
C : ℝ
hC_nonneg : 0 ≤ C
x : E
hC : ‖f x‖ ^ ↑p ≤ C * (1 + ‖x‖) ^ (-(n * ↑p) + -r)
⊢ 0 < 1 + ‖x‖
Tactic:
simp
Proof state after:
no goals
Theorem: SchwartzMap.integrable_one_add_norm_rpow_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 => (1 + ‖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 => (1 + ‖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 => (1 + ‖x‖) ^ n • f 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)
⊢ AEStronglyMeasurable (fun x => (1 + ‖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 => (1 + ‖x‖) ^ n • f x
Tactic:
. refine AEStronglyMeasurable.smul ?_ f.continuous.aestronglyMeasurable
  refine (AEMeasurable.pow_const ?_ n).aestronglyMeasurable
  exact (continuous_const.add continuous_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 => (1 + ‖x‖) ^ n • f x
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]
  rw [← snorm_one_eq_lintegral_nnnorm]
  exact snorm_nnreal_one_add_norm_rpow_smul_lt_top n f zero_lt_one
Proof state after:
no goals