integrable_snd — Mathlib

English

Integrability is preserved under identDistrib: if f is integrable with respect to μ, then g is integrable with respect to ν.

Русский

Интегрируемость сохраняется при identDistrib: если f интегрируемо по μ, то g интегрируемо по ν.

LaTeX

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

Lean4

theorem integrable_snd [NormedAddCommGroup γ] [BorelSpace γ] (h : IdentDistrib f g μ ν) (hf : Integrable f μ) :
    Integrable g ν := by
  rw [← memLp_one_iff_integrable] at hf ⊢
  exact h.memLp_snd hf

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