English
Let f: ℂ → E, c ∈ ℂ, and R ∈ ℝ. If E is a NormedSpace over ℂ, then CircleIntegrable f c R is equivalent to the interval integrability of the function θ ↦ deriv(circleMap c R) θ • f(circleMap c R θ) on the interval [0, 2π] with respect to Lebesgue measure.
Русский
Пусть f: ℂ → E, c ∈ ℂ и R ∈ ℝ. Тогда CircleIntegrable f c R эквивалентно интегрируемости по интервалу функции θ ↦ deriv(circleMap c R) θ • f(circleMap c R θ) на отрезке [0, 2π] по мере Лебега.
LaTeX
$$$CircleIntegrable(f,c,R) \\iff IntervalIntegrable\\bigl(\\lambda\\theta. deriv(circleMap\\;c\\;R)\\;\\theta \\cdot f(circleMap\\;c\\;R\\;\\theta)\\bigr)\\;volume\\;0\\;2\\pi$$$
Lean4
theorem circleIntegrable_iff [NormedSpace ℂ E] {f : ℂ → E} {c : ℂ} (R : ℝ) :
CircleIntegrable f c R ↔
IntervalIntegrable (fun θ : ℝ => deriv (circleMap c R) θ • f (circleMap c R θ)) volume 0 (2 * π) :=
by
by_cases h₀ : R = 0
· simp +unfoldPartialApp [h₀, const]
refine ⟨fun h => h.out, fun h => ?_⟩
simp only [CircleIntegrable, intervalIntegrable_iff, deriv_circleMap] at h ⊢
refine (h.norm.const_mul |R|⁻¹).mono' ?_ ?_
· have H : ∀ {θ}, circleMap 0 R θ * I ≠ 0 := fun {θ} => by simp [h₀, I_ne_zero]
simpa only [inv_smul_smul₀ H] using
((continuous_circleMap 0 R).aestronglyMeasurable.mul_const I).aemeasurable.inv.aestronglyMeasurable.smul
h.aestronglyMeasurable
· simp [norm_smul, h₀]
