-- Mathlib/Analysis/Distribution/SchwartzSpace.lean
/-- Given a function such that `f` and `x ^ (k + l) * f` are bounded for a suitable `l`, then
one can bound explicitly the integral of `x ^ k * f`. -/
-- We redeclare `E` here to avoid the `NormedSpace ℝ E` typeclass available throughout this file.
lemma integral_pow_mul_le_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₂) :
    ∫ x, ‖x‖ ^ k * ‖f x‖ ∂μ ≤ 2 ^ μ.integrablePower *
      (∫ x, (1 + ‖x‖) ^ (- (μ.integrablePower : ℝ)) ∂μ) * (C₁ + C₂)

Proof state:
case hgi
D : Type u_3
inst✝³ : NormedAddCommGroup D
inst✝² : MeasurableSpace 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₂
⊢ Integrable (fun a => 2 ^ μ.integrablePower * (1 + ‖a‖) ^ (-↑μ.integrablePower) * (C₁ + C₂)) μ

Tactic:
exact ((integrable_pow_neg_integrablePower μ).const_mul _).mul_const _

Result:
no goals

Proof state:
D : Type u_3
inst✝³ : NormedAddCommGroup D
inst✝² : MeasurableSpace 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₂
⊢ ∫ (x : D), ‖x‖ ^ k * ‖f x‖ ∂μ ≤ (2 ^ μ.integrablePower * ∫ (x : D), (1 + ‖x‖) ^ (-↑μ.integrablePower) ∂μ) * (C₁ + C₂)

Tactic:
rw [← integral_mul_left, ← integral_mul_right]

Result:
D : Type u_3
inst✝³ : NormedAddCommGroup D
inst✝² : MeasurableSpace 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₂
⊢ ∫ (x : D), ‖x‖ ^ k * ‖f x‖ ∂μ ≤ ∫ (a : D), 2 ^ μ.integrablePower * (1 + ‖a‖) ^ (-↑μ.integrablePower) * (C₁ + C₂) ∂μ

Proof state:
case h.h
D : Type u_3
inst✝³ : NormedAddCommGroup D
inst✝² : MeasurableSpace 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₂
v : D
⊢ ‖v‖ ^ k * ‖f v‖ ≤ 2 ^ μ.integrablePower * (1 + ‖v‖) ^ (-↑μ.integrablePower) * (C₁ + C₂)

Tactic:
exact (pow_mul_le_of_le_of_pow_mul_le (norm_nonneg _) (norm_nonneg _) (hf v) (h'f v)).trans
  (le_of_eq (by ring))

Result:
no goals

Proof state:
D : Type u_3
inst✝³ : NormedAddCommGroup D
inst✝² : MeasurableSpace 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₂
v : D
⊢ 0 v ≤ ‖v‖ ^ k * ‖f v‖

Tactic:
positivity

Result:
no goals

Proof state:
case hf
D : Type u_3
inst✝³ : NormedAddCommGroup D
inst✝² : MeasurableSpace 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₂
⊢ 0 ≤ᶠ[ae μ] fun a => ‖a‖ ^ k * ‖f a‖

Tactic:
filter_upwards with v using by positivity

Result:
no goals

Proof state:
D : Type u_3
inst✝³ : NormedAddCommGroup D
inst✝² : MeasurableSpace 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₂
v : D
⊢ 2 ^ μ.integrablePower * (C₁ + C₂) * (1 + ‖v‖) ^ (-↑μ.integrablePower) =
    2 ^ μ.integrablePower * (1 + ‖v‖) ^ (-↑μ.integrablePower) * (C₁ + C₂)

Tactic:
ring

Result:
no goals

Proof state:
case h
D : Type u_3
inst✝³ : NormedAddCommGroup D
inst✝² : MeasurableSpace 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₂
⊢ (fun a => ‖a‖ ^ k * ‖f a‖) ≤ᶠ[ae μ] fun a => 2 ^ μ.integrablePower * (1 + ‖a‖) ^ (-↑μ.integrablePower) * (C₁ + C₂)

Tactic:
filter_upwards with v

Result:
case h.h
D : Type u_3
inst✝³ : NormedAddCommGroup D
inst✝² : MeasurableSpace 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₂
v : D
⊢ ‖v‖ ^ k * ‖f v‖ ≤ 2 ^ μ.integrablePower * (1 + ‖v‖) ^ (-↑μ.integrablePower) * (C₁ + C₂)

Proof state:
D : Type u_3
inst✝³ : NormedAddCommGroup D
inst✝² : MeasurableSpace 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₂
⊢ ∫ (x : D), ‖x‖ ^ k * ‖f x‖ ∂μ ≤ ∫ (a : D), 2 ^ μ.integrablePower * (1 + ‖a‖) ^ (-↑μ.integrablePower) * (C₁ + C₂) ∂μ

Tactic:
apply integral_mono_of_nonneg

Result:
case hf
D : Type u_3
inst✝³ : NormedAddCommGroup D
inst✝² : MeasurableSpace 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₂
⊢ 0 ≤ᶠ[ae μ] fun a => ‖a‖ ^ k * ‖f a‖

case hgi
D : Type u_3
inst✝³ : NormedAddCommGroup D
inst✝² : MeasurableSpace 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₂
⊢ Integrable (fun a => 2 ^ μ.integrablePower * (1 + ‖a‖) ^ (-↑μ.integrablePower) * (C₁ + C₂)) μ

case h
D : Type u_3
inst✝³ : NormedAddCommGroup D
inst✝² : MeasurableSpace 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₂
⊢ (fun a => ‖a‖ ^ k * ‖f a‖) ≤ᶠ[ae μ] fun a => 2 ^ μ.integrablePower * (1 + ‖a‖) ^ (-↑μ.integrablePower) * (C₁ + C₂)