English
The polar-coordinate change of variables preserves integration for vector-valued f: the integral over the polar target of p_1 times f(polarCoord.symm(p)) equals the integral of f.
Русский
Замена переменных по полярным координатам сохраняет интеграл для векторно-значимых функций: интеграл по полярной целевой области от p_1 умноженного на f(polarCoord.symm(p)) равен интегралу f.
LaTeX
$$$\int_{p\in(\mathrm{Set.univ.pi}(\mathrm{polarCoord.target}))} p_1 \cdot f(\mathrm{polarCoord.symm}(p)) \, dp = \int_p f(p) \, dp.$$$
Lean4
/-- The function `x ^ (a / (b * x + c))` tends to `1` at `+∞`, for any real numbers `a`, `b`, and
`c` such that `b` is nonzero. -/
theorem tendsto_rpow_div_mul_add (a b c : ℝ) (hb : 0 ≠ b) : Tendsto (fun x => x ^ (a / (b * x + c))) atTop (𝓝 1) :=
by
refine
Tendsto.congr' ?_
((tendsto_exp_nhds_zero_nhds_one.comp
(by
simpa only [mul_zero, pow_one] using
(tendsto_const_nhds (x := a)).mul (tendsto_div_pow_mul_exp_add_atTop b c 1 hb))).comp
tendsto_log_atTop)
apply eventuallyEq_of_mem (Ioi_mem_atTop (0 : ℝ))
intro x hx
simp only [Set.mem_Ioi, Function.comp_apply] at hx ⊢
rw [exp_log hx, ← exp_log (rpow_pos_of_pos hx (a / (b * x + c))), log_rpow hx (a / (b * x + c))]
field_simp
