SLLN for non-integrable nonnegative variables in Mathlib via truncation

Mathlib's strong_law_ae_real needs Integrable (X 0). To get S_m/m → ∞ a.s. for iid ℕ-valued T with ¬Integrable, apply it to Y_K i = ((min (T i ω) K : ℕ) : ℝ) for every K at once (ae_all_iff over K : ℕ), with Integrable.of_bound (bound K), IndepFun.comp / IdentDistrib.comp with measurable_from_nat (give (f := fun n : ℕ ↦ ((min n K : ℕ) : ℝ)) explicitly or elaboration picks the wrong composite). The truncated means are unbounded: by_contra!, then lintegral_iSup (pass (μ := P) explicitly, it cannot infer it) on ofReal (min τ K), whose iSup is ofReal τ, and ofReal_integral_eq_lintegral_ofReal on each term gives ∫⁻ ofReal τ ≤ ofReal b < ∞, contradicting lintegral_ofReal_ne_top_iff_integrable. Then compare termwise sums with min_le_left.