English
Under temperate growth, the integral of |x|^k |f(x)| is bounded by a combination of the tail integral of (1+|x|)^{-μ.integrablePower} and the bounds on |f| and |x|^(k+μ.integrablePower).
Русский
При темперированном росте интеграл |x|^k |f(x)| ограничен сочетанием хвоста интеграла (1+|x|)^{-μ.integrablePower} и ограничениями на |f| и |x|^(k+μ.integrablePower).
LaTeX
$$$∫ |x|^k |f(x)| dμ ≤ 2^{μ.integrablePower} ( ∫ (1+|x|)^{-(μ.integrablePower)} dμ) (C_1 + C_2)$.$$
Lean4
/-- 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.
theorem 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‖) μ :=
by
apply ((integrable_pow_neg_integrablePower μ).const_mul (2 ^ μ.integrablePower * (C₁ + C₂))).mono'
· exact AEStronglyMeasurable.mul (aestronglyMeasurable_id.norm.pow _) h''f.norm
· filter_upwards with v
simp only [norm_mul, norm_pow, norm_norm]
apply pow_mul_le_of_le_of_pow_mul_le (norm_nonneg _) (norm_nonneg _) (hf v) (h'f v)
