English
If f is continuous on Icc(0, π/2), then the ratio of two integrals tends to f(0): lim_{n→∞} ∫ cos^n f / ∫ cos^n = f(0).
Русский
Если f непрерывна на Icc(0, π/2), тогда отношение двух интегралов сходится к f(0).
LaTeX
$$$\text{If } f:\mathbb{R}\to\mathbb{C} \text{ is continuous on } [0,\tfrac{π}{2}], \; \lim_{n\to\infty} \frac{\int_{0}^{π/2} \cos^{n} x f(x)\,dx}{\int_{0}^{π/2} \cos^{n} x \, dx} = f(0).$$$
Lean4
theorem tendsto_integral_cos_pow_mul_div {f : ℝ → ℂ} (hf : ContinuousOn f (Icc 0 (π / 2))) :
Tendsto (fun n : ℕ => (∫ x in (0 : ℝ)..π / 2, (cos x : ℂ) ^ n * f x) / (∫ x in (0 : ℝ)..π / 2, cos x ^ n : ℝ)) atTop
(𝓝 <| f 0) :=
by
simp_rw [div_eq_inv_mul (α := ℂ), ← Complex.ofReal_inv, integral_of_le pi_div_two_pos.le, ←
MeasureTheory.integral_Icc_eq_integral_Ioc, ← Complex.ofReal_pow, ← Complex.real_smul]
have c_lt : ∀ y : ℝ, y ∈ Icc 0 (π / 2) → y ≠ 0 → cos y < cos 0 := fun y hy hy' =>
cos_lt_cos_of_nonneg_of_le_pi_div_two (le_refl 0) hy.2 (lt_of_le_of_ne hy.1 hy'.symm)
have c_nonneg : ∀ x : ℝ, x ∈ Icc 0 (π / 2) → 0 ≤ cos x := fun x hx =>
cos_nonneg_of_mem_Icc ((Icc_subset_Icc_left (neg_nonpos_of_nonneg pi_div_two_pos.le)) hx)
have c_zero_pos : 0 < cos 0 := by rw [cos_zero]; exact zero_lt_one
have zero_mem : (0 : ℝ) ∈ closure (interior (Icc 0 (π / 2))) :=
by
rw [interior_Icc, closure_Ioo pi_div_two_pos.ne, left_mem_Icc]
exact pi_div_two_pos.le
exact
tendsto_setIntegral_pow_smul_of_unique_maximum_of_isCompact_of_continuousOn isCompact_Icc continuousOn_cos c_lt
c_nonneg c_zero_pos zero_mem hf
