Mathlib's Jacobian change of variables (lintegral_image_eq_lintegral_abs_det_fderiv_mul) needs no measurability of the integrand

MeasureTheory.lintegral_image_eq_lintegral_abs_det_fderiv_mul (Mathlib/MeasureTheory/Function/Jacobian.lean) takes an arbitrary g : E → ℝ≥0∞: ∫⁻ x in f '' s, g x = ∫⁻ x in s, ofReal |det (f' x)| * g (f x), given MeasurableSet s, HasFDerivWithinAt on s, and InjOn f s. So you can push suprema/sup-convolutions (not known measurable) through a nonlinear injective C¹ map and get lower-integral statements. Example: Barthe's reverse Brascamp–Lieb, ∫⁻ x, ⨆ θ (_ : x = ∑ cᵢθᵢuᵢ), ofReal ∏ fᵢ(θᵢ)^cᵢ ≥ ∏(∫fᵢ)^cᵢ. Prove the pointwise bound γ(y) ≤ |det DΘ y| * H(Θ y) with le_iSup₂_of_le (giving the f explicitly), then lintegral_mono, the image formula with s = univ and Measure.restrict_univ, and setLIntegral_le_lintegral. No surjectivity needed.