theorem lintegral_antitone_mul_le {f g k : NNReal → ENNReal} (hf : AEMeasurable f MeasureTheory.volume) (hg : AEMeasurable g MeasureTheory.volume) (h : ∀ {t : NNReal}, ∫⁻ (s : NNReal) in Set.Iio t, f s ≤ ∫⁻ (s : NNReal) in Set.Iio t, g s) (hk : Antitone k) : ∫⁻ (s : NNReal), k s * f s ≤ ∫⁻ (s : NNReal), k s * g s