Theorem: SchwartzMap.snorm_nnreal_one_add_norm_rpow_smul_lt_top (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
n : ℝ
f : 𝓢(E, F)
p : NNReal
hp : 0 < p
⊢ snorm (fun x => (1 + ‖x‖) ^ n • f x) (↑p) volume < ⊤
Tactic:
simp [snorm, hp.ne', snorm']
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
n : ℝ
f : 𝓢(E, F)
p : NNReal
hp : 0 < p
⊢ (∫⁻ (a : E), ↑‖(1 + ‖a‖) ^ n • f a‖₊ ^ ↑p) ^ (↑p)⁻¹ < ⊤

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
⊢ (∫⁻ (a : E), ↑‖(1 + ‖a‖) ^ n • f a‖₊ ^ ↑p) ^ (↑p)⁻¹ < ⊤
Tactic:
refine ENNReal_rpow_lt_top (inv_pos_of_pos hp) ?_
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
n : ℝ
f : 𝓢(E, F)
p : NNReal
hp : 0 < p
⊢ ∫⁻ (a : E), ↑‖(1 + ‖a‖) ^ n • f a‖₊ ^ ↑p < ⊤

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
⊢ ∫⁻ (a : E), ↑‖(1 + ‖a‖) ^ n • f a‖₊ ^ ↑p < ⊤
Tactic:
generalize hr : (FiniteDimensional.finrank ℝ E + 1 : ℝ) = r
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
n : ℝ
f : 𝓢(E, F)
p : NNReal
hp : 0 < p
r : ℝ
hr : ↑(FiniteDimensional.finrank ℝ E) + 1 = r
⊢ ∫⁻ (a : E), ↑‖(1 + ‖a‖) ^ n • f a‖₊ ^ ↑p < ⊤

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
⊢ ∫⁻ (a : E), ↑‖(1 + ‖a‖) ^ n • f a‖₊ ^ ↑p < ⊤
Tactic:
rcases pow_norm_le_pow_one_add_norm f hp (r + n * p) with ⟨C, ⟨hC_nonneg, hC⟩⟩
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‖ ^ (fun a => ↑a) p ≤ C * (1 + ‖x‖) ^ (-(r + n * ↑p))
⊢ ∫⁻ (a : E), ↑‖(1 + ‖a‖) ^ n • f a‖₊ ^ ↑p < ⊤

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‖ ^ (fun a => ↑a) p ≤ C * (1 + ‖x‖) ^ (-(r + n * ↑p))
⊢ ∫⁻ (a : E), ↑‖(1 + ‖a‖) ^ n • f a‖₊ ^ ↑p < ⊤
Tactic:
simp at hC
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)
⊢ ∫⁻ (a : E), ↑‖(1 + ‖a‖) ^ n • f a‖₊ ^ ↑p < ⊤

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)
⊢ ∫⁻ (a : E), ↑‖(1 + ‖a‖) ^ n • f a‖₊ ^ ↑p < ⊤
Tactic:
suffices : ∫⁻ (x : E), (‖(1 + ‖x‖) ^ n • f x‖₊ : ENNReal) ^ (p : ℝ) ≤ ∫⁻ (x : E), ENNReal.ofReal (C * (1 + ‖x‖) ^ (-r))
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), ↑‖(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))

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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