-- 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 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
x : D
⊢ ‖(1 + ‖x‖) ^ (-(↑k * ↑p))‖ ≤ (1 + ‖x‖) ^ (-↑l)

Tactic:
rw [Real.norm_of_nonneg (Real.rpow_nonneg (h_one_add x).le _)]

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
x : D
⊢ (1 + ‖x‖) ^ (-(↑k * ↑p)) ≤ (1 + ‖x‖) ^ (-↑l)

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 : HasFiniteIntegral (fun x => (1 + ‖x‖) ^ (-(↑k * ↑p))) μ
⊢ eLpNorm (fun x => (1 + ‖x‖) ^ (-↑k)) (↑p) μ < ⊤

Tactic:
rw [hasFiniteIntegral_iff_enorm] at this

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))‖ₑ ∂μ < ⊤
⊢ 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⌉₊
⊢ ∃ k, eLpNorm (fun x => (1 + ‖x‖) ^ (-↑k)) (↑p) μ < ⊤

Tactic:
have hlk : l ≤ k * (p : ℝ) := by simpa [div_le_iff₀ hp_pos] using Nat.le_ceil (l / p : ℝ)

Result:
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) μ < ⊤

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))‖ₑ ∂μ < ⊤
⊢ eLpNorm (fun x => (1 + ‖x‖) ^ (-↑k)) (↑p) μ < ⊤

Tactic:
rw [eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top hp ENNReal.coe_ne_top]

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))‖ₑ ∂μ < ⊤
⊢ ∫⁻ (a : D), ‖(1 + ‖a‖) ^ (-↑k)‖ₑ ^ (↑p).toReal ∂μ < ⊤

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

Tactic:
exact ⟨0, eLpNormEssSup_lt_top_of_ae_bound (C := 1) (by simp)⟩

Result:
no goals

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, eLpNorm (fun x => (1 + ‖x‖) ^ (-↑k)) (↑p) μ < ⊤

Tactic:
let k := ⌈(l / p : ℝ)⌉₊

Result:
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⌉₊
⊢ ∃ k, eLpNorm (fun x => (1 + ‖x‖) ^ (-↑k)) (↑p) μ < ⊤

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‖
hp_pos : 0 < ↑p
⊢ ∃ k, eLpNorm (fun x => (1 + ‖x‖) ^ (-↑k)) (↑p) μ < ⊤

Tactic:
rcases hμ.exists_integrable with ⟨l, hl⟩

Result:
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, eLpNorm (fun x => (1 + ‖x‖) ^ (-↑k)) (↑p) μ < ⊤

Proof state:
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
⊢ HasFiniteIntegral (fun x => (1 + ‖x‖) ^ (-(↑k * ↑p))) μ

Tactic:
refine hl.hasFiniteIntegral.mono' (ae_of_all μ fun x ↦ ?_)

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
x : D
⊢ ‖(1 + ‖x‖) ^ (-(↑k * ↑p))‖ ≤ (1 + ‖x‖) ^ (-↑l)

Proof state:
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
x : D
⊢ (1 + ‖x‖) ^ (-(↑k * ↑p)) ≤ (1 + ‖x‖) ^ (-↑l)

Tactic:
gcongr

Result:
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‖

Proof state:
case coe.inr
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:
have h_one_add (x : D) : 0 < 1 + ‖x‖ := lt_add_of_pos_of_le zero_lt_one (norm_nonneg x)

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‖
⊢ ∃ 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‖
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))‖ₑ ∂μ < ⊤
⊢ ∫⁻ (a : D), ‖(1 + ‖a‖) ^ (-↑k)‖ₑ ^ (↑p).toReal ∂μ < ⊤

Tactic:
simp only [ENNReal.coe_toReal]

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))‖ₑ ∂μ < ⊤
⊢ ∫⁻ (a : D), ‖(1 + ‖a‖) ^ (-↑k)‖ₑ ^ ↑p ∂μ < ⊤