integral_def

Mathlib.MeasureTheory.Integral.Bochner.L1

URI: https://scilib.ai/kg/mathlib#MeasureTheory.SimpleFunc.integral_def

English

The integral of a simple function with respect to μ equals its setToSimpleFunc weighted by μ.

Русский

Интеграл простой функции по мере μ равен его интегралу через weighted SMul.

LaTeX

$$$$\text{integral } μ f = f.setToSimpleFunc (weightedSMul μ).$$$$

Lean4

theorem integral_def {_ : MeasurableSpace α} (μ : Measure α) (f : α →ₛ F) :
    f.integral μ = f.setToSimpleFunc (weightedSMul μ) :=
  rfl

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

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

Разделы

Аффилиация

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