setToSimpleFunc_nonneg' — Mathlib

English

A strengthened monotonicity variant: if T and T' satisfy a pointwise order, then for any f we have setToSimpleFunc T f ≤ setToSimpleFunc T' f.

Русский

Улучшенная версия монотонности: если T s x ≤ T' s x, тогда для любой f имеем setToSimpleFunc T f ≤ setToSimpleFunc T' f.

LaTeX

$$$\forall s x, T s x ≤ T' s x \Rightarrow setToSimpleFunc T f ≤ setToSimpleFunc T' f $$$

Lean4

theorem setToSimpleFunc_nonneg' (T : Set α → G' →L[ℝ] G'')
    (hT_nonneg : ∀ s, MeasurableSet s → μ s < ∞ → ∀ x, 0 ≤ x → 0 ≤ T s x) (f : α →ₛ G') (hf : 0 ≤ f)
    (hfi : Integrable f μ) : 0 ≤ setToSimpleFunc T f :=
  by
  refine sum_nonneg fun i hi => ?_
  by_cases h0 : i = 0
  · simp [h0]
  refine hT_nonneg _ (measurableSet_fiber _ _) (measure_preimage_lt_top_of_integrable _ hfi h0) i ?_
  rw [mem_range] at hi
  obtain ⟨y, hy⟩ := Set.mem_range.mp hi
  rw [← hy]
  convert hf y

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