measurable_circleMap

Mathlib.MeasureTheory.Integral.CircleIntegral

URI: https://scilib.ai/kg/mathlib#measurable_circleMap

English

The circle map is measurable with respect to the Lebesgue measure on θ.

Русский

Круговая карта измерима относительно начального модуля measure на θ.

LaTeX

$$$ circleMap(c,R) : \mathbb{R} \to \mathbb{C} \text{ is measurable}. $$$

Lean4

@[fun_prop, measurability]
theorem measurable_circleMap (c : ℂ) (R : ℝ) : Measurable (circleMap c R) :=
  (continuous_circleMap c R).measurable

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

Научная платформа российской исследовательской школы.

Разделы

Аффилиация

Вычислительный центр им. А. А. Дороницына при ФИЦ «Информатика и Управление» РАН frccsc.ru