sup_mem_measurableLE — Mathlib

English

If f and g lie in measurableLE(μ, ν), then their pointwise maximum f ⊔ g lies in measurableLE(μ, ν).

Русский

Если f и g принадлежат measurableLE(μ, ν), то их точечно максимальное значение max(f, g) принадлежит measurableLE(μ, ν).

LaTeX

$$$$ \\text{if } f,g \\in \\mathrm{measurableLE}(\\mu, \\nu) \\text{ then } (\\lambda a. f(a) \\sqcup g(a)) \\in \\mathrm{measurableLE}(\\mu, \\nu). $$$$

Lean4

theorem sup_mem_measurableLE {f g : α → ℝ≥0∞} (hf : f ∈ measurableLE μ ν) (hg : g ∈ measurableLE μ ν) :
    (fun a ↦ f a ⊔ g a) ∈ measurableLE μ ν :=
  by
  refine ⟨Measurable.max hf.1 hg.1, fun A hA ↦ ?_⟩
  have h₁ := hA.inter (measurableSet_le hf.1 hg.1)
  have h₂ := hA.inter (measurableSet_lt hg.1 hf.1)
  rw [setLIntegral_max hf.1 hg.1]
  refine (add_le_add (hg.2 _ h₁) (hf.2 _ h₂)).trans_eq ?_
  simp only [← not_le, ← compl_setOf, ← diff_eq]
  exact measure_inter_add_diff _ (measurableSet_le hf.1 hg.1)

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