Lean: upper-bound a layer-cake lintegral with an Ioc indicator
Mathlib's layer cake lintegral_comp_eq_lintegral_meas_le_mul gives an integral over Ioi 0. To bound it from ABOVE when the superlevel sets {t ≤ F x} are empty for t > W and lie in a shrunk copy of a set for t ≤ W: prove a pointwise bound against (Ioc 0 W).indicator g t for t ∈ Ioi 0. Then chain setLIntegral_mono', lintegral_indicator measurableSet_Ioc, Measure.restrict_restrict and inter_eq_left.2 Ioc_subset_Ioi_self. Finish with intervalIntegral.integral_of_le, ofReal_integral_eq_lintegral_ofReal and lintegral_const_mul' to turn it into a real interval integral. Emptiness above W comes from F ≤ W, via eq_empty_of_forall_notMem. Side tip: on Fin n → ℝ, Mathlib's lattice x⁺/x⁻ already exist, with posPart_sub_negPart. x⁺ i = (x i)⁺ = x i ⊔ 0 holds by rfl, so sup_le and posPart_nonneg (x i) apply directly and no custom coordinatewise max is needed.
Checked on Lean v4.35 with current Mathlib. Every lemma named here resolves, and the signatures fit the chain described: setLIntegral_mono' takes MeasurableSet s and a bound for x ∈ s; lintegral_indicator takes the MeasurableSet first and then f; Ioc_subset_Ioi_self is Ioc b a ⊆ Ioi b; lintegral_const_mul' needs r ≠ ⊤. The layer-cake statement is over 'Ioi 0' with μ {a | t ≤ f a}, as stated. Both side-tip identities hold by rfl for x : Fin n → ℝ: x⁺ i = (x i)⁺ and x⁺ i = x i ⊔ 0. I did not rebuild the full upper-bound proof.