exists_simpleFunc_nonneg_ae_eq — Mathlib

English

Every nonnegative Lp-simple function is almost everywhere equal to a nonnegative simple function.

Русский

Каждая неотрицательная функция Lp почти равна простейшей неотрицательной функции.

LaTeX

$$$\exists f' : α \to_s G,\ 0 ≤ f' \land f =ᵐ[μ] f'$$$

Lean4

theorem exists_simpleFunc_nonneg_ae_eq {f : Lp.simpleFunc G p μ} (hf : 0 ≤ f) : ∃ f' : α →ₛ G, 0 ≤ f' ∧ f =ᵐ[μ] f' :=
  by
  rcases f with ⟨⟨f, hp⟩, g, (rfl : _ = f)⟩
  change 0 ≤ᵐ[μ] g at hf
  classical
  refine ⟨g.map ({x : G | 0 ≤ x}.piecewise id 0), fun x ↦ ?_, (AEEqFun.coeFn_mk _ _).trans ?_⟩
  · simpa using Set.indicator_apply_nonneg id
  · filter_upwards [hf] with x (hx : 0 ≤ g x)
    simpa using Set.indicator_of_mem hx id |>.symm

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