-- Mathlib/Analysis/Distribution/SchwartzSpace.lean
/-- Given a function such that `f` and `x ^ (k + l) * f` are bounded for a suitable `l`, then
`x ^ k * f` is integrable. The bounds are not relevant for the integrability conclusion, but they
are relevant for bounding the integral in `integral_pow_mul_le_of_le_of_pow_mul_le`. We formulate
the two lemmas with the same set of assumptions for ease of applications. -/
-- We redeclare `E` here to avoid the `NormedSpace ℝ E` typeclass available throughout this file.
lemma integrable_of_le_of_pow_mul_le
    {E : Type*} [NormedAddCommGroup E]
    {μ : Measure D} [μ.HasTemperateGrowth] {f : D → E} {C₁ C₂ : ℝ} {k : ℕ}
    (hf : ∀ x, ‖f x‖ ≤ C₁) (h'f : ∀ x, ‖x‖ ^ (k + μ.integrablePower) * ‖f x‖ ≤ C₂)
    (h''f : AEStronglyMeasurable f μ) :
    Integrable (fun x ↦ ‖x‖ ^ k * ‖f x‖) μ

Proof state:
case hf
D : Type u_3
inst✝⁵ : NormedAddCommGroup D
inst✝⁴ : MeasurableSpace D
inst✝³ : BorelSpace D
inst✝² : SecondCountableTopology D
E : Type u_8
inst✝¹ : NormedAddCommGroup E
μ : Measure D
inst✝ : μ.HasTemperateGrowth
f : D → E
C₁ C₂ : ℝ
k : ℕ
hf : ∀ (x : D), ‖f x‖ ≤ C₁
h'f : ∀ (x : D), ‖x‖ ^ (k + μ.integrablePower) * ‖f x‖ ≤ C₂
h''f : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable (fun x => ‖x‖ ^ k * ‖f x‖) μ

Tactic:
exact AEStronglyMeasurable.mul (aestronglyMeasurable_id.norm.pow _) h''f.norm

Result:
no goals

Proof state:
case h.h
D : Type u_3
inst✝⁵ : NormedAddCommGroup D
inst✝⁴ : MeasurableSpace D
inst✝³ : BorelSpace D
inst✝² : SecondCountableTopology D
E : Type u_8
inst✝¹ : NormedAddCommGroup E
μ : Measure D
inst✝ : μ.HasTemperateGrowth
f : D → E
C₁ C₂ : ℝ
k : ℕ
hf : ∀ (x : D), ‖f x‖ ≤ C₁
h'f : ∀ (x : D), ‖x‖ ^ (k + μ.integrablePower) * ‖f x‖ ≤ C₂
h''f : AEStronglyMeasurable f μ
v : D
⊢ ‖v‖ ^ k * ‖f v‖ ≤ 2 ^ μ.integrablePower * (C₁ + C₂) * (1 + ‖v‖) ^ (-↑μ.integrablePower)

Tactic:
apply pow_mul_le_of_le_of_pow_mul_le (norm_nonneg _) (norm_nonneg _) (hf v) (h'f v)

Result:
no goals

Proof state:
D : Type u_3
inst✝⁵ : NormedAddCommGroup D
inst✝⁴ : MeasurableSpace D
inst✝³ : BorelSpace D
inst✝² : SecondCountableTopology D
E : Type u_8
inst✝¹ : NormedAddCommGroup E
μ : Measure D
inst✝ : μ.HasTemperateGrowth
f : D → E
C₁ C₂ : ℝ
k : ℕ
hf : ∀ (x : D), ‖f x‖ ≤ C₁
h'f : ∀ (x : D), ‖x‖ ^ (k + μ.integrablePower) * ‖f x‖ ≤ C₂
h''f : AEStronglyMeasurable f μ
⊢ Integrable (fun x => ‖x‖ ^ k * ‖f x‖) μ

Tactic:
apply ((integrable_pow_neg_integrablePower μ).const_mul (2 ^ μ.integrablePower * (C₁ + C₂))).mono'

Result:
case hf
D : Type u_3
inst✝⁵ : NormedAddCommGroup D
inst✝⁴ : MeasurableSpace D
inst✝³ : BorelSpace D
inst✝² : SecondCountableTopology D
E : Type u_8
inst✝¹ : NormedAddCommGroup E
μ : Measure D
inst✝ : μ.HasTemperateGrowth
f : D → E
C₁ C₂ : ℝ
k : ℕ
hf : ∀ (x : D), ‖f x‖ ≤ C₁
h'f : ∀ (x : D), ‖x‖ ^ (k + μ.integrablePower) * ‖f x‖ ≤ C₂
h''f : AEStronglyMeasurable f μ
⊢ AEStronglyMeasurable (fun x => ‖x‖ ^ k * ‖f x‖) μ

case h
D : Type u_3
inst✝⁵ : NormedAddCommGroup D
inst✝⁴ : MeasurableSpace D
inst✝³ : BorelSpace D
inst✝² : SecondCountableTopology D
E : Type u_8
inst✝¹ : NormedAddCommGroup E
μ : Measure D
inst✝ : μ.HasTemperateGrowth
f : D → E
C₁ C₂ : ℝ
k : ℕ
hf : ∀ (x : D), ‖f x‖ ≤ C₁
h'f : ∀ (x : D), ‖x‖ ^ (k + μ.integrablePower) * ‖f x‖ ≤ C₂
h''f : AEStronglyMeasurable f μ
⊢ ∀ᵐ (a : D) ∂μ, ‖‖a‖ ^ k * ‖f a‖‖ ≤ 2 ^ μ.integrablePower * (C₁ + C₂) * (1 + ‖a‖) ^ (-↑μ.integrablePower)

Proof state:
case h
D : Type u_3
inst✝⁵ : NormedAddCommGroup D
inst✝⁴ : MeasurableSpace D
inst✝³ : BorelSpace D
inst✝² : SecondCountableTopology D
E : Type u_8
inst✝¹ : NormedAddCommGroup E
μ : Measure D
inst✝ : μ.HasTemperateGrowth
f : D → E
C₁ C₂ : ℝ
k : ℕ
hf : ∀ (x : D), ‖f x‖ ≤ C₁
h'f : ∀ (x : D), ‖x‖ ^ (k + μ.integrablePower) * ‖f x‖ ≤ C₂
h''f : AEStronglyMeasurable f μ
⊢ ∀ᵐ (a : D) ∂μ, ‖‖a‖ ^ k * ‖f a‖‖ ≤ 2 ^ μ.integrablePower * (C₁ + C₂) * (1 + ‖a‖) ^ (-↑μ.integrablePower)

Tactic:
filter_upwards with v

Result:
case h.h
D : Type u_3
inst✝⁵ : NormedAddCommGroup D
inst✝⁴ : MeasurableSpace D
inst✝³ : BorelSpace D
inst✝² : SecondCountableTopology D
E : Type u_8
inst✝¹ : NormedAddCommGroup E
μ : Measure D
inst✝ : μ.HasTemperateGrowth
f : D → E
C₁ C₂ : ℝ
k : ℕ
hf : ∀ (x : D), ‖f x‖ ≤ C₁
h'f : ∀ (x : D), ‖x‖ ^ (k + μ.integrablePower) * ‖f x‖ ≤ C₂
h''f : AEStronglyMeasurable f μ
v : D
⊢ ‖‖v‖ ^ k * ‖f v‖‖ ≤ 2 ^ μ.integrablePower * (C₁ + C₂) * (1 + ‖v‖) ^ (-↑μ.integrablePower)

Proof state:
case h.h
D : Type u_3
inst✝⁵ : NormedAddCommGroup D
inst✝⁴ : MeasurableSpace D
inst✝³ : BorelSpace D
inst✝² : SecondCountableTopology D
E : Type u_8
inst✝¹ : NormedAddCommGroup E
μ : Measure D
inst✝ : μ.HasTemperateGrowth
f : D → E
C₁ C₂ : ℝ
k : ℕ
hf : ∀ (x : D), ‖f x‖ ≤ C₁
h'f : ∀ (x : D), ‖x‖ ^ (k + μ.integrablePower) * ‖f x‖ ≤ C₂
h''f : AEStronglyMeasurable f μ
v : D
⊢ ‖‖v‖ ^ k * ‖f v‖‖ ≤ 2 ^ μ.integrablePower * (C₁ + C₂) * (1 + ‖v‖) ^ (-↑μ.integrablePower)

Tactic:
simp only [norm_mul, norm_pow, norm_norm]

Result:
case h.h
D : Type u_3
inst✝⁵ : NormedAddCommGroup D
inst✝⁴ : MeasurableSpace D
inst✝³ : BorelSpace D
inst✝² : SecondCountableTopology D
E : Type u_8
inst✝¹ : NormedAddCommGroup E
μ : Measure D
inst✝ : μ.HasTemperateGrowth
f : D → E
C₁ C₂ : ℝ
k : ℕ
hf : ∀ (x : D), ‖f x‖ ≤ C₁
h'f : ∀ (x : D), ‖x‖ ^ (k + μ.integrablePower) * ‖f x‖ ≤ C₂
h''f : AEStronglyMeasurable f μ
v : D
⊢ ‖v‖ ^ k * ‖f v‖ ≤ 2 ^ μ.integrablePower * (C₁ + C₂) * (1 + ‖v‖) ^ (-↑μ.integrablePower)