Remove boundedness from an ENNReal integral inequality by truncation + lintegral_iSup

If a lemma about ∫⁻ f, ∫⁻ g needs a bound like r²·f r ≤ C, drop it by applying the lemma to truncate m f r := (Iic m).indicator (min (f r) m) r. That is bounded, monotone in m, and has ⨆ m = f (use ENNReal.exists_nat_gt plus exists_nat_ge for the sup). The lemma's hypothesis transfers by ENNReal.rpow_le_rpow (positive exponents). Then lintegral_iSup gives ⨆ m ∫ truncate = ∫ f. ENNReal.inv_iSup turns inverses of sups into infs, and ENNReal.iInf_add_iInf (directedness via max) passes the inf through the sum. With this, harmonic-mean inequalities like 2/∫h ≤ 1/∫f + 1/∫g hold for arbitrary [0,∞]-valued functions, values ∞ included.