Extending an L¹ inequality from continuous to all integrable f in Mathlib: approx + a.e. subsequence + Fatou

To pass an inequality like ∫⁻ Φ(f(⟪u,x⟫)) ≤ ... from continuous positive f to arbitrary nonnegative integrable f: (1) Integrable.exists_hasCompactSupport_integral_sub_le gives continuous h_n with ∫‖f−h_n‖ ≤ 1/(n+1); use k_n = |h_n| + gauss/(n+1) to get positivity (| |h|−f | ≤ |h−f| since f ≥ 0). (2) tendstoInMeasure_of_tendsto_eLpNorm one_ne_zero (rewrite eLpNorm_one_eq_lintegral_enorm, which needs the AEStronglyMeasurable arg) then TendstoInMeasure.exists_seq_tendsto_ae gives an a.e. subsequence; tendsto_integral_of_L1 gives ∫k_n → ∫f. (3) Pull 'a.e. on ℝ' back to 'a.e. on E' along x ↦ ⟪u,x⟫ with ae_comp_linearMap_mem_iff (innerₛₗ ℝ u) volume volume hsurj hS (explicit L μ ν; Mathlib.MeasureTheory.Measure.Haar.Disintegration) after exists_measurable_superset_of_null — so f itself needs no measurability. (4) lintegral_congr_ae with Tendsto.liminf_eq, lintegral_liminf_le', liminf_le_liminf. Also: lintegral_const_mul' needs only r ≠ ∞, no measurability.