An Abel-type lemma for nonincreasing weights #
If h : [0,1] → [0,1] is nonincreasing and all partial integrals ∫_{[0,u]} f are
nonnegative, then ∫ h f ≥ 0. This is the layer-cake/Fubini step in the proof of Lemma 5.1 (iii).
theorem
Papers.OrendayLaresRockel2026XiBeta.integral_lowerSet_nonneg
{S : Set ↑unitInterval}
(hS : IsLowerSet S)
{f : ↑unitInterval → ℝ}
(hpart : ∀ (u : ↑unitInterval), 0 ≤ ∫ (t : ↑unitInterval) in Set.Iic u, f t)
:
The integral of f over a lower set of [0,1] is nonnegative if all partial integrals are.
theorem
Papers.OrendayLaresRockel2026XiBeta.integral_antitone_mul_nonneg
{h f : ↑unitInterval → ℝ}
(hh : Antitone h)
(hb : ∀ (u : ↑unitInterval), h u ∈ Set.Icc 0 1)
(hfm : Measurable f)
(hfb : ∀ (u : ↑unitInterval), |f u| ≤ 1)
(hpart : ∀ (u : ↑unitInterval), 0 ≤ ∫ (t : ↑unitInterval) in Set.Iic u, f t)
: