English
If T is nonnegative in the sense described, then for any nonnegative f, setToFun μ T hT f ≥ 0.
Русский
Если T удовлетворяет неотрицательности и f неотрицательна, то setToFun неотрицателен.
LaTeX
$$$\forall f\ge 0,\; \mathrm{setToFun}(\mu, T) h_T f \ge 0$$$
Lean4
theorem setToFun_nonneg {T : Set α → G' →L[ℝ] G''} {C : ℝ} (hT : DominatedFinMeasAdditive μ T C)
(hT_nonneg : ∀ s, MeasurableSet s → μ s < ∞ → ∀ x, 0 ≤ x → 0 ≤ T s x) {f : α → G'} (hf : 0 ≤ᵐ[μ] f) :
0 ≤ setToFun μ T hT f := by
by_cases hfi : Integrable f μ
· simp_rw [setToFun_eq _ hfi]
refine L1.setToL1_nonneg hT hT_nonneg ?_
rw [← Lp.coeFn_le]
have h0 := Lp.coeFn_zero G' 1 μ
have h := Integrable.coeFn_toL1 hfi
filter_upwards [h0, h, hf] with _ h0a ha hfa
rw [h0a, ha]
exact hfa
· simp_rw [setToFun_undef _ hfi, le_rfl]
