English
A final polar-coordinate integration identity holds for functions from ι → ℂ to a normed space E, equating the transformed integral over the product with the original integral.
Русский
Финальная идентичность интегрирования по полярным координатам: преобразованный интеграл над произведением остаётся равным исходному интегралу.
LaTeX
$$$\int_{p \in (\mathrm{Set.univ.pi}\; (\mathrm{polarCoord.target}))} \left( \prod_i (p_i)_1 \right) \cdot f(\mathrm{polarCoord.symm}(p_i)) \, dp = \int_p f(p) \, dp.$$$
Lean4
/-- The function `exp(x) / x ^ s` tends to `+∞` at `+∞`, for any real number `s`. -/
theorem tendsto_exp_div_rpow_atTop (s : ℝ) : Tendsto (fun x : ℝ => exp x / x ^ s) atTop atTop :=
by
obtain ⟨n, hn⟩ := archimedean_iff_nat_lt.1 Real.instArchimedean s
refine tendsto_atTop_mono' _ ?_ (tendsto_exp_div_pow_atTop n)
filter_upwards [eventually_gt_atTop (0 : ℝ), eventually_ge_atTop (1 : ℝ)] with x hx₀ hx₁
gcongr
simpa using rpow_le_rpow_of_exponent_le hx₁ hn.le
