snd_sum

Mathlib.MeasureTheory.Measure.Prod

URI: https://scilib.ai/kg/mathlib#MeasureTheory.Measure.snd_sum

English

The second marginal commutes with a (countable) sum of measures: snd( sum μ_i ) = sum snd( μ_i ).

Русский

Вторая маргинальная мера commuting с суммой мер: snd( ∑ μ_i ) = ∑ snd( μ_i ).

LaTeX

$$snd( sum μ ) = sum ( snd ∘ μ )$$

Lean4

theorem snd_sum {ι : Type*} (μ : ι → Measure (α × β)) : (sum μ).snd = sum (fun n ↦ (μ n).snd) :=
  map_sum measurable_snd.aemeasurable

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

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

Разделы

Аффилиация

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