English
For all c ∈ ℂ and R ∈ ℝ, circleMap c R is continuously differentiable of order n for any n.
Русский
Для любых c ∈ ℂ и R ∈ ℝ circleMap c R является непрерывно дифференцируемой по порядку n для любого n.
LaTeX
$$$\text{ContDiff}_{\mathbb{R}}^n(circleMap(c,R))\quad(\text{for all } n). $$$
Lean4
/-- We say that a function `f : ℂ → E` is integrable on the circle with center `c` and radius `R` if
the function `f ∘ circleMap c R` is integrable on `[0, 2π]`.
Note that the actual function used in the definition of `circleIntegral` is
`(deriv (circleMap c R) θ) • f (circleMap c R θ)`. Integrability of this function is equivalent
to integrability of `f ∘ circleMap c R` whenever `R ≠ 0`. -/
def CircleIntegrable (f : ℂ → E) (c : ℂ) (R : ℝ) : Prop :=
IntervalIntegrable (fun θ : ℝ ↦ f (circleMap c R θ)) volume 0 (2 * π)
