English
If f is nonnegative in L1 and hT is dominated with a nonnegativity condition, then setToL1 hT f is nonnegative.
Русский
Если f ≥ 0 почти всюду и выполняется неотрицательное условие для hT, то setToL1 hT f ≥ 0.
LaTeX
$$$0 \leq setToL1\, h_T\, f,$$$
Lean4
theorem setToL1_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 ≤ setToL1 hT f :=
by
suffices ∀ f : { g : α →₁[μ] G' // 0 ≤ g }, 0 ≤ setToL1 hT f from this (⟨f, hf⟩ : { g : α →₁[μ] G' // 0 ≤ g })
refine fun g =>
@isClosed_property { g : α →₁ₛ[μ] G' // 0 ≤ g } { g : α →₁[μ] G' // 0 ≤ g } _ _ (fun g => 0 ≤ setToL1 hT g)
(denseRange_coeSimpleFuncNonnegToLpNonneg 1 μ G' one_ne_top) ?_ ?_ g
· exact isClosed_le continuous_zero ((setToL1 hT).continuous.comp continuous_induced_dom)
· intro g
have : (coeSimpleFuncNonnegToLpNonneg 1 μ G' g : α →₁[μ] G') = (g : α →₁ₛ[μ] G') := rfl
rw [this, setToL1_eq_setToL1SCLM]
exact setToL1S_nonneg (fun s => hT.eq_zero_of_measure_zero) hT.1 hT_nonneg g.2
