memLp_snd — Mathlib

English

If f and g are identically distributed, then ae-properties transferred from f apply to g.

Русский

Если f и g идентично распределены, то свойства, относящиеся к f, переходят к g

LaTeX

$$$h.ae_snd (pmeas) (hp)$$$

Lean4

theorem memLp_snd [NormedAddCommGroup γ] [BorelSpace γ] {p : ℝ≥0∞} (h : IdentDistrib f g μ ν) (hf : MemLp f p μ) :
    MemLp g p ν := by
  refine ⟨h.aestronglyMeasurable_snd hf.aestronglyMeasurable, ?_⟩
  rw [← h.eLpNorm_eq]
  exact hf.2

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