English
If f and x^(k+l) f bound by constants hold, then x^k f is bounded by a combination of these constants times (1+x)^(-l).
Русский
Если существуют границы на f и x^(k+l) f, то x^k f ограничено линейной комбинацией этих констант и (1+x)^(-l).
LaTeX
$$$\\ldots$$$
Lean4
/-- Pointwise inequality to control `x ^ k * f` in terms of `1 / (1 + x) ^ l` if one controls both
`f` (with a bound `C₁`) and `x ^ (k + l) * f` (with a bound `C₂`). This will be used to check
integrability of `x ^ k * f x` when `f` is a Schwartz function, and to control explicitly its
integral in terms of suitable seminorms of `f`. -/
theorem pow_mul_le_of_le_of_pow_mul_le {C₁ C₂ : ℝ} {k l : ℕ} {x f : ℝ} (hx : 0 ≤ x) (hf : 0 ≤ f) (h₁ : f ≤ C₁)
(h₂ : x ^ (k + l) * f ≤ C₂) : x ^ k * f ≤ 2 ^ l * (C₁ + C₂) * (1 + x) ^ (-(l : ℝ)) :=
by
have : 0 ≤ C₂ := le_trans (by positivity) h₂
have : 2 ^ l * (C₁ + C₂) * (1 + x) ^ (-(l : ℝ)) = ((1 + x) / 2) ^ (-(l : ℝ)) * (C₁ + C₂) :=
by
rw [Real.div_rpow (by linarith) zero_le_two]
simp [div_eq_inv_mul, ← Real.rpow_neg_one, ← Real.rpow_mul]
ring
rw [this]
rcases le_total x 1 with h'x | h'x
· gcongr
· apply (pow_le_one₀ hx h'x).trans
apply Real.one_le_rpow_of_pos_of_le_one_of_nonpos
· linarith
· linarith
· simp
· linarith
·
calc
x ^ k * f = x ^ (-(l : ℝ)) * (x ^ (k + l) * f) :=
by
rw [← Real.rpow_natCast, ← Real.rpow_natCast, ← mul_assoc, ← Real.rpow_add (by linarith)]
simp
_ ≤ ((1 + x) / 2) ^ (-(l : ℝ)) * (C₁ + C₂) :=
by
apply mul_le_mul _ _ (by positivity) (by positivity)
· exact Real.rpow_le_rpow_of_nonpos (by linarith) (by linarith) (by simp)
· exact h₂.trans (by linarith)
