circleIntegrable_def — Mathlib

English

A function f is CircleIntegrable with center c and radius R if f(circleMap(c,R,·)) is integrable on [0,2π].

Русский

Функция f считается CircleIntegrable с центром c и радиусом R тогда и только тогда, когда f(circleMap(c,R,·)) интегрируема на [0,2π].

LaTeX

$$$CircleIntegrable(f,c,R) \iff \ IntervalIntegrable\left(\lambda\theta. f(circleMap(c,R,\theta))\right)\;\text{volume}\;0\;(2\pi).$$$

Lean4

theorem circleIntegrable_def (f : ℂ → E) (c : ℂ) (R : ℝ) :
    CircleIntegrable f c R ↔ IntervalIntegrable (fun θ : ℝ ↦ f (circleMap c R θ)) volume 0 (2 * π) :=
  Iff.rfl

Похожие утверждения