integrable_iff — Mathlib

English

Two functions are integrable with respect to μ and ν, respectively, if and only if they are identDistrib.

Русский

Две функции интегрируемы по μ и ν тогда и только тогда, когда они идентично распределены.

LaTeX

$$$\text{IdentDistrib } f g μ ν \to (\text{Integrable } f μ \iff \text{Integrable } g ν)$$$

Lean4

theorem integrable_iff [NormedAddCommGroup γ] [BorelSpace γ] (h : IdentDistrib f g μ ν) :
    Integrable f μ ↔ Integrable g ν :=
  ⟨fun hf => h.integrable_snd hf, fun hg => h.symm.integrable_snd hg⟩

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