eapprox_comp — Mathlib

English

For measurable f,g, eapprox of the composition equals the composition of eapprox: eapprox (f ∘ g) n = (eapprox f n) ∘ g.

Русский

Для измеримых f и g выполняется eapprox (f ∘ g) n = (eapprox f n) ∘ g.

LaTeX

$$$ eapprox\ (f \circ g)\ n = (eapprox\ f\ n) \circ g $$$

Lean4

theorem eapprox_comp [MeasurableSpace γ] {f : γ → ℝ≥0∞} {g : α → γ} {n : ℕ} (hf : Measurable f) (hg : Measurable g) :
    (eapprox (f ∘ g) n : α → ℝ≥0∞) = (eapprox f n : γ →ₛ ℝ≥0∞) ∘ g :=
  funext fun a => approx_comp a hf hg

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