internlm/Lean-Github huggingface dataset:
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 < ⊤

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
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)
⊢ ∫⁻ (x : E), ↑‖(1 + ‖x‖) ^ n • f x‖₊ ^ ↑p ≤ ∫⁻ (x : E), ENNReal.ofReal (C * (1 + ‖x‖) ^ (-r))
Tactic:
. refine lt_of_le_of_lt this ?_
  simp_rw [ENNReal.ofReal_mul hC_nonneg]
  rw [lintegral_const_mul]
  swap
  . refine Measurable.ennreal_ofReal ?_
    exact Measurable.pow_const (Measurable.const_add measurable_norm _) _
  refine ENNReal.mul_lt_top (by simp) ?_
  rw [← lt_top_iff_ne_top]
  refine finite_integral_one_add_norm ?_
  simp [← hr]
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
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)
⊢ ∫⁻ (x : E), ↑‖(1 + ‖x‖) ^ n • f x‖₊ ^ ↑p ≤ ∫⁻ (x : E), ENNReal.ofReal (C * (1 + ‖x‖) ^ (-r))
Theorem: SchwartzMap.snorm_nnreal_one_add_norm_rpow_smul_lt_top
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
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)
⊢ ∫⁻ (x : E), ↑‖(1 + ‖x‖) ^ n • f x‖₊ ^ ↑p ≤ ∫⁻ (x : E), ENNReal.ofReal (C * (1 + ‖x‖) ^ (-r))
Tactic:
refine lintegral_mono ?_
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
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)
⊢ (fun x => ↑‖(1 + ‖x‖) ^ n • f x‖₊ ^ ↑p) ≤ fun x => ENNReal.ofReal (C * (1 + ‖x‖) ^ (-r))
Theorem: SchwartzMap.snorm_nnreal_one_add_norm_rpow_smul_lt_top
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
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)
⊢ (fun x => ↑‖(1 + ‖x‖) ^ n • f x‖₊ ^ ↑p) ≤ fun x => ENNReal.ofReal (C * (1 + ‖x‖) ^ (-r))
Tactic:
intro x
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
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)
x : E
⊢ (fun x => ↑‖(1 + ‖x‖) ^ n • f x‖₊ ^ ↑p) x ≤ (fun x => ENNReal.ofReal (C * (1 + ‖x‖) ^ (-r))) x
Theorem: SchwartzMap.snorm_nnreal_one_add_norm_rpow_smul_lt_top
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
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)
x : E
⊢ (fun x => ↑‖(1 + ‖x‖) ^ n • f x‖₊ ^ ↑p) x ≤ (fun x => ENNReal.ofReal (C * (1 + ‖x‖) ^ (-r))) x
Tactic:
specialize hC x
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
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)
⊢ (fun x => ↑‖(1 + ‖x‖) ^ n • f x‖₊ ^ ↑p) x ≤ (fun x => ENNReal.ofReal (C * (1 + ‖x‖) ^ (-r))) x
Theorem: SchwartzMap.snorm_nnreal_one_add_norm_rpow_smul_lt_top
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
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)
⊢ (fun x => ↑‖(1 + ‖x‖) ^ n • f x‖₊ ^ ↑p) x ≤ (fun x => ENNReal.ofReal (C * (1 + ‖x‖) ^ (-r))) x
Tactic:
simp
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
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)
⊢ ↑‖(1 + ‖x‖) ^ n • f x‖₊ ^ ↑p ≤ ENNReal.ofReal (C * (1 + ‖x‖) ^ (-r))
Theorem: SchwartzMap.snorm_nnreal_one_add_norm_rpow_smul_lt_top
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
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)
⊢ ↑‖(1 + ‖x‖) ^ n • f x‖₊ ^ ↑p ≤ ENNReal.ofReal (C * (1 + ‖x‖) ^ (-r))
Tactic:
rw [ENNReal.ofReal]
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
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)
⊢ ↑‖(1 + ‖x‖) ^ n • f x‖₊ ^ ↑p ≤ ↑(Real.toNNReal (C * (1 + ‖x‖) ^ (-r)))
Theorem: SchwartzMap.snorm_nnreal_one_add_norm_rpow_smul_lt_top
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
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)
⊢ ↑‖(1 + ‖x‖) ^ n • f x‖₊ ^ ↑p ≤ ↑(Real.toNNReal (C * (1 + ‖x‖) ^ (-r)))
Tactic:
rw [ENNReal.coe_rpow_of_nonneg _ p.coe_nonneg]
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
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)
⊢ ↑(‖(1 + ‖x‖) ^ n • f x‖₊ ^ ↑p) ≤ ↑(Real.toNNReal (C * (1 + ‖x‖) ^ (-r)))
Theorem: SchwartzMap.snorm_nnreal_one_add_norm_rpow_smul_lt_top
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
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)
⊢ ↑(‖(1 + ‖x‖) ^ n • f x‖₊ ^ ↑p) ≤ ↑(Real.toNNReal (C * (1 + ‖x‖) ^ (-r)))
Tactic:
norm_cast
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
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)
⊢ ‖(1 + ‖x‖) ^ n • f x‖₊ ^ ↑p ≤ Real.toNNReal (C * (1 + ‖x‖) ^ (-r))
Theorem: SchwartzMap.snorm_nnreal_one_add_norm_rpow_smul_lt_top
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
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)
⊢ ‖(1 + ‖x‖) ^ n • f x‖₊ ^ ↑p ≤ Real.toNNReal (C * (1 + ‖x‖) ^ (-r))
Tactic:
rw [← norm_toNNReal]
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
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)
⊢ Real.toNNReal ‖(1 + ‖x‖) ^ n • f x‖ ^ ↑p ≤ Real.toNNReal (C * (1 + ‖x‖) ^ (-r))
Theorem: SchwartzMap.snorm_nnreal_one_add_norm_rpow_smul_lt_top
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
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)
⊢ Real.toNNReal ‖(1 + ‖x‖) ^ n • f x‖ ^ ↑p ≤ Real.toNNReal (C * (1 + ‖x‖) ^ (-r))
Tactic:
simp [← Real.toNNReal_rpow_of_nonneg, norm_nonneg]
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
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)
⊢ Real.toNNReal (‖(1 + ‖x‖) ^ n • f x‖ ^ ↑p) ≤ Real.toNNReal (C * (1 + ‖x‖) ^ (-r))
Theorem: SchwartzMap.snorm_nnreal_one_add_norm_rpow_smul_lt_top
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
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)
⊢ Real.toNNReal (‖(1 + ‖x‖) ^ n • f x‖ ^ ↑p) ≤ Real.toNNReal (C * (1 + ‖x‖) ^ (-r))
Tactic:
refine Real.toNNReal_le_toNNReal ?_
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
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)
⊢ ‖(1 + ‖x‖) ^ n • f x‖ ^ ↑p ≤ C * (1 + ‖x‖) ^ (-r)
Theorem: SchwartzMap.snorm_nnreal_one_add_norm_rpow_smul_lt_top
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
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)
⊢ ‖(1 + ‖x‖) ^ n • f x‖ ^ ↑p ≤ C * (1 + ‖x‖) ^ (-r)
Tactic:
simp [norm_smul]
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
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)
⊢ (|(1 + ‖x‖) ^ n| * ‖f x‖) ^ ↑p ≤ C * (1 + ‖x‖) ^ (-r)
Theorem: SchwartzMap.snorm_nnreal_one_add_norm_rpow_smul_lt_top
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
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)
⊢ (|(1 + ‖x‖) ^ n| * ‖f x‖) ^ ↑p ≤ C * (1 + ‖x‖) ^ (-r)
Tactic:
rw [Real.mul_rpow (by simp) (by simp)]
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
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)
⊢ |(1 + ‖x‖) ^ n| ^ ↑p * ‖f x‖ ^ ↑p ≤ C * (1 + ‖x‖) ^ (-r)
Theorem: SchwartzMap.snorm_nnreal_one_add_norm_rpow_smul_lt_top
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
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)
⊢ |(1 + ‖x‖) ^ n| ^ ↑p * ‖f x‖ ^ ↑p ≤ C * (1 + ‖x‖) ^ (-r)
Tactic:
rw [abs_of_nonneg (by simp)]
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
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)
⊢ ((1 + ‖x‖) ^ n) ^ ↑p * ‖f x‖ ^ ↑p ≤ C * (1 + ‖x‖) ^ (-r)
Theorem: SchwartzMap.snorm_nnreal_one_add_norm_rpow_smul_lt_top
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
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)
⊢ ((1 + ‖x‖) ^ n) ^ ↑p * ‖f x‖ ^ ↑p ≤ C * (1 + ‖x‖) ^ (-r)
Tactic:
rw [← Real.rpow_mul (by simp)]
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
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)
⊢ (1 + ‖x‖) ^ (n * ↑p) * ‖f x‖ ^ ↑p ≤ C * (1 + ‖x‖) ^ (-r)
Theorem: SchwartzMap.snorm_nnreal_one_add_norm_rpow_smul_lt_top
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
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)
⊢ (1 + ‖x‖) ^ (n * ↑p) * ‖f x‖ ^ ↑p ≤ C * (1 + ‖x‖) ^ (-r)
Tactic:
rw [← le_div_iff' (by simp)]
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
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)
⊢ ‖f x‖ ^ ↑p ≤ C * (1 + ‖x‖) ^ (-r) / (1 + ‖x‖) ^ (n * ↑p)
Theorem: SchwartzMap.snorm_nnreal_one_add_norm_rpow_smul_lt_top
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
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)
⊢ ‖f x‖ ^ ↑p ≤ C * (1 + ‖x‖) ^ (-r) / (1 + ‖x‖) ^ (n * ↑p)
Tactic:
refine le_of_le_of_eq hC ?_
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
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)
⊢ C * (1 + ‖x‖) ^ (-(n * ↑p) + -r) = C * (1 + ‖x‖) ^ (-r) / (1 + ‖x‖) ^ (n * ↑p)
Theorem: SchwartzMap.snorm_nnreal_one_add_norm_rpow_smul_lt_top
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
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)
⊢ C * (1 + ‖x‖) ^ (-(n * ↑p) + -r) = C * (1 + ‖x‖) ^ (-r) / (1 + ‖x‖) ^ (n * ↑p)
Tactic:
rw [Real.rpow_add (by simp)]
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
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)
⊢ C * ((1 + ‖x‖) ^ (-(n * ↑p)) * (1 + ‖x‖) ^ (-r)) = C * (1 + ‖x‖) ^ (-r) / (1 + ‖x‖) ^ (n * ↑p)
Theorem: SchwartzMap.snorm_nnreal_one_add_norm_rpow_smul_lt_top
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
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)
⊢ C * ((1 + ‖x‖) ^ (-(n * ↑p)) * (1 + ‖x‖) ^ (-r)) = C * (1 + ‖x‖) ^ (-r) / (1 + ‖x‖) ^ (n * ↑p)
Tactic:
rw [mul_div_assoc, div_eq_inv_mul]
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
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)
⊢ C * ((1 + ‖x‖) ^ (-(n * ↑p)) * (1 + ‖x‖) ^ (-r)) = C * (((1 + ‖x‖) ^ (n * ↑p))⁻¹ * (1 + ‖x‖) ^ (-r))
Theorem: SchwartzMap.snorm_nnreal_one_add_norm_rpow_smul_lt_top
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
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)
⊢ C * ((1 + ‖x‖) ^ (-(n * ↑p)) * (1 + ‖x‖) ^ (-r)) = C * (((1 + ‖x‖) ^ (n * ↑p))⁻¹ * (1 + ‖x‖) ^ (-r))
Tactic:
rw [Real.rpow_neg]
Proof state after:
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‖