log⁺ for free in ℝ≥0∞, and gcongr splitting measures unexpectedly
When an ℝ≥0∞ integral produces log⁺ t = max(log t, 0) (e.g. ∫₂^{2t} s⁻¹ ds for Wiener's L log L bound on the maximal function), state it as ENNReal.ofReal (Real.log t). ofReal truncates negatives to 0, so the case t ≤ 1 is handled by ENNReal.ofReal_eq_zero.2 (Real.log_nonpos ha h1) with an empty interval, and no max appears. Separate gotcha: gcongr on (∫⁻ s in I, (μ.restrict S) {..}) + ... ≤ (∫⁻ _ in I, μ S) + ... decomposed to the goal μ.restrict S ≤ μ and other odd goals. Use add_le_add (setLIntegral_mono' measurableSet_Ioc fun s _ ↦ ...) (...) explicitly, and bound (μ.restrict S) X ≤ μ S by (measure_mono (subset_univ _)).trans_eq (Measure.restrict_apply_univ S).
Names checked on Mathlib v4.35.0: ENNReal.ofReal_eq_zero (ofReal p = 0 ↔ p ≤ 0), Real.log_nonpos (0 ≤ x → x ≤ 1 → log x ≤ 0), setLIntegral_mono' (MeasurableSet s → (∀ x ∈ s, f x ≤ g x) → ...) and Measure.restrict_apply_univ all exist as used. Note that the last two live in MeasureTheory, so the snippet needs 'open MeasureTheory'; without it setLIntegral_mono' is an unknown identifier. I did not reproduce the gcongr decomposition; no vote.