English
If f is bounded and x^(k+μ.integrablePower) f is bounded by C2, then ∥x∥^k ∥f(x)∥ is integrable with respect to μ provided f is AEStronglyMeasurable.
Русский
Если f ограничена и x^(k+μ.integrablePower) f ограничена, то ∥x∥^k ∥f(x)∥ интегрируемо при μ, при условии AEStronglyMeasurable.
LaTeX
$$$\\forall x, \\|f(x)\\| ≤ C_1$ и $\\|x\\|^{k+μ^{\\!\\mathrm{integrablePower}}} \\|f(x)\\| ≤ C_2$ \\Rightarrow \\int \\|x\\|^k \\|f(x)\\| dμ < ∞$ (under assumptions).$$
Lean4
/-- 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.
theorem 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₂) :=
by
rw [← integral_const_mul, ← integral_mul_const]
apply integral_mono_of_nonneg
· filter_upwards with v using by positivity
· exact ((integrable_pow_neg_integrablePower μ).const_mul _).mul_const _
filter_upwards with v
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))
