memLp_iff — Mathlib

English

If f,g are identDistrib, membership in Lp for f implies membership in Lp for g with the same p.

Русский

Если f и g идентично распределены, членство в Lp для f влечет членство в Lp для g с тем же p.

LaTeX

$$$\text{MemLp } f p μ \to\text{MemLp } g p ν$$$

Lean4

theorem memLp_iff [NormedAddCommGroup γ] [BorelSpace γ] {p : ℝ≥0∞} (h : IdentDistrib f g μ ν) :
    MemLp f p μ ↔ MemLp g p ν :=
  ⟨fun hf => h.memLp_snd hf, fun hg => h.symm.memLp_snd hg⟩

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