-- Mathlib/Analysis/Distribution/SchwartzSpace.lean
theorem _root_.MeasureTheory.Measure.HasTemperateGrowth.exists_eLpNorm_lt_top (p : ℝ≥0∞)
    {μ : Measure D} (hμ : μ.HasTemperateGrowth) :
    ∃ k : ℕ, eLpNorm (fun x ↦ (1 + ‖x‖) ^ (-k : ℝ)) p μ < ⊤

Proof state:
case coe.inr.intro
D : Type u_3
inst✝¹ : NormedAddCommGroup D
inst✝ : MeasurableSpace D
μ : Measure D
hμ : μ.HasTemperateGrowth
p : ℝ≥0
hp : ↑p ≠ 0
h_one_add : ∀ (x : D), 0 < 1 + ‖x‖
hp_pos : 0 < ↑p
l : ℕ
hl : Integrable (fun x => (1 + ‖x‖) ^ (-↑l)) μ
k : ℕ := ⌈↑l / ↑p⌉₊
hlk : ↑l ≤ ↑k * ↑p
⊢ ∃ k, eLpNorm (fun x => (1 + ‖x‖) ^ (-↑k)) (↑p) μ < ⊤

Tactic:
use k

Result:
case h
D : Type u_3
inst✝¹ : NormedAddCommGroup D
inst✝ : MeasurableSpace D
μ : Measure D
hμ : μ.HasTemperateGrowth
p : ℝ≥0
hp : ↑p ≠ 0
h_one_add : ∀ (x : D), 0 < 1 + ‖x‖
hp_pos : 0 < ↑p
l : ℕ
hl : Integrable (fun x => (1 + ‖x‖) ^ (-↑l)) μ
k : ℕ := ⌈↑l / ↑p⌉₊
hlk : ↑l ≤ ↑k * ↑p
⊢ eLpNorm (fun x => (1 + ‖x‖) ^ (-↑k)) (↑p) μ < ⊤

Proof state:
D : Type u_3
inst✝¹ : NormedAddCommGroup D
inst✝ : MeasurableSpace D
μ : Measure D
hμ : μ.HasTemperateGrowth
p : ℝ≥0
hp : ↑p = 0
⊢ eLpNorm (fun x => (1 + ‖x‖) ^ (-↑0)) (↑p) μ < ⊤

Tactic:
simp [hp]

Result:
no goals

Proof state:
D : Type u_3
inst✝¹ : NormedAddCommGroup D
inst✝ : MeasurableSpace D
μ : Measure D
hμ : μ.HasTemperateGrowth
p : ℝ≥0
hp : ↑p ≠ 0
h_one_add : ∀ (x : D), 0 < 1 + ‖x‖
hp_pos : 0 < ↑p
l : ℕ
hl : Integrable (fun x => (1 + ‖x‖) ^ (-↑l)) μ
k : ℕ := ⌈↑l / ↑p⌉₊
hlk : ↑l ≤ ↑k * ↑p
this : ∫⁻ (a : D), ‖(1 + ‖a‖) ^ (-(↑k * ↑p))‖ₑ ∂μ < ⊤
x : D
⊢ ‖(1 + ‖x‖) ^ (-(↑k * ↑p))‖ₑ = ‖(1 + ‖x‖) ^ (-↑k)‖ₑ ^ ↑p

Tactic:
rw [← neg_mul, Real.rpow_mul (h_one_add x).le]

Result:
D : Type u_3
inst✝¹ : NormedAddCommGroup D
inst✝ : MeasurableSpace D
μ : Measure D
hμ : μ.HasTemperateGrowth
p : ℝ≥0
hp : ↑p ≠ 0
h_one_add : ∀ (x : D), 0 < 1 + ‖x‖
hp_pos : 0 < ↑p
l : ℕ
hl : Integrable (fun x => (1 + ‖x‖) ^ (-↑l)) μ
k : ℕ := ⌈↑l / ↑p⌉₊
hlk : ↑l ≤ ↑k * ↑p
this : ∫⁻ (a : D), ‖(1 + ‖a‖) ^ (-(↑k * ↑p))‖ₑ ∂μ < ⊤
x : D
⊢ ‖((1 + ‖x‖) ^ (-↑k)) ^ ↑p‖ₑ = ‖(1 + ‖x‖) ^ (-↑k)‖ₑ ^ ↑p

Proof state:
D : Type u_3
inst✝¹ : NormedAddCommGroup D
inst✝ : MeasurableSpace D
μ : Measure D
hμ : μ.HasTemperateGrowth
p : ℝ≥0
hp : ↑p ≠ 0
h_one_add : ∀ (x : D), 0 < 1 + ‖x‖
hp_pos : 0 < ↑p
l : ℕ
hl : Integrable (fun x => (1 + ‖x‖) ^ (-↑l)) μ
k : ℕ := ⌈↑l / ↑p⌉₊
⊢ ↑l ≤ ↑k * ↑p

Tactic:
simpa [div_le_iff₀ hp_pos] using Nat.le_ceil (l / p : ℝ)

Result:
no goals

Proof state:
case h.hx
D : Type u_3
inst✝¹ : NormedAddCommGroup D
inst✝ : MeasurableSpace D
μ : Measure D
hμ : μ.HasTemperateGrowth
p : ℝ≥0
hp : ↑p ≠ 0
h_one_add : ∀ (x : D), 0 < 1 + ‖x‖
hp_pos : 0 < ↑p
l : ℕ
hl : Integrable (fun x => (1 + ‖x‖) ^ (-↑l)) μ
k : ℕ := ⌈↑l / ↑p⌉₊
hlk : ↑l ≤ ↑k * ↑p
x : D
⊢ 1 ≤ 1 + ‖x‖

Tactic:
simp

Result:
no goals

Proof state:
case coe.inl
D : Type u_3
inst✝¹ : NormedAddCommGroup D
inst✝ : MeasurableSpace D
μ : Measure D
hμ : μ.HasTemperateGrowth
p : ℝ≥0
hp : ↑p = 0
⊢ ∃ k, eLpNorm (fun x => (1 + ‖x‖) ^ (-↑k)) (↑p) μ < ⊤

Tactic:
exact ⟨0, by simp [hp]⟩

Result:
no goals

Proof state:
case coe.inr
D : Type u_3
inst✝¹ : NormedAddCommGroup D
inst✝ : MeasurableSpace D
μ : Measure D
hμ : μ.HasTemperateGrowth
p : ℝ≥0
hp : ↑p ≠ 0
h_one_add : ∀ (x : D), 0 < 1 + ‖x‖
⊢ ∃ k, eLpNorm (fun x => (1 + ‖x‖) ^ (-↑k)) (↑p) μ < ⊤

Tactic:
have hp_pos : 0 < (p : ℝ) := by simpa [zero_lt_iff] using hp

Result:
case coe.inr
D : Type u_3
inst✝¹ : NormedAddCommGroup D
inst✝ : MeasurableSpace D
μ : Measure D
hμ : μ.HasTemperateGrowth
p : ℝ≥0
hp : ↑p ≠ 0
h_one_add : ∀ (x : D), 0 < 1 + ‖x‖
hp_pos : 0 < ↑p
⊢ ∃ k, eLpNorm (fun x => (1 + ‖x‖) ^ (-↑k)) (↑p) μ < ⊤

Proof state:
D : Type u_3
inst✝¹ : NormedAddCommGroup D
inst✝ : MeasurableSpace D
μ : Measure D
hμ : μ.HasTemperateGrowth
p : ℝ≥0
hp : ↑p ≠ 0
h_one_add : ∀ (x : D), 0 < 1 + ‖x‖
⊢ 0 < ↑p

Tactic:
simpa [zero_lt_iff] using hp

Result:
no goals

Proof state:
D : Type u_3
inst✝¹ : NormedAddCommGroup D
inst✝ : MeasurableSpace D
μ : Measure D
hμ : μ.HasTemperateGrowth
p : ℝ≥0
hp : ↑p ≠ 0
h_one_add : ∀ (x : D), 0 < 1 + ‖x‖
hp_pos : 0 < ↑p
l : ℕ
hl : Integrable (fun x => (1 + ‖x‖) ^ (-↑l)) μ
k : ℕ := ⌈↑l / ↑p⌉₊
hlk : ↑l ≤ ↑k * ↑p
this : ∫⁻ (a : D), ‖(1 + ‖a‖) ^ (-(↑k * ↑p))‖ₑ ∂μ < ⊤
x : D
⊢ ‖((1 + ‖x‖) ^ (-↑k)) ^ ↑p‖ₑ = ‖(1 + ‖x‖) ^ (-↑k)‖ₑ ^ ↑p

Tactic:
exact Real.enorm_rpow_of_nonneg (Real.rpow_nonneg (h_one_add x).le _) NNReal.zero_le_coe

Result:
no goals

Proof state:
D : Type u_3
inst✝¹ : NormedAddCommGroup D
inst✝ : MeasurableSpace D
μ : Measure D
hμ : μ.HasTemperateGrowth
⊢ ∀ᵐ (x : D) ∂μ, ‖(1 + ‖x‖) ^ (-↑0)‖ ≤ 1

Tactic:
simp

Result:
no goals