Change of variables in the plane for densities scaling by the Jacobian

A density f on a region s of ℝ × ℝ that is |det dφ| times g ∘ φ, for an injective differentiable change of coordinates φ, has the same integral over s as g over φ '' s. If instead f is the signed det dφ times g ∘ φ, then the lower Lebesgue integral of ‖f‖ₑ over s equals that of ‖g‖ₑ over φ '' s, without any orientation assumption. This packages Mathlib's change of variables formula (MeasureTheory.integral_image_eq_integral_abs_det_fderiv_smul) for Lebesgue measure on the plane, where densities of this kind arise as coefficients of two-forms.

Main results

• TauCeti.integral_image_eq_integral_of_eq_abs_det_smul: the Bochner integral of a density scaling by |det dφ|.
• TauCeti.lintegral_enorm_image_eq_lintegral_enorm_of_eq_det_smul: the lower Lebesgue integral of the size of a density scaling by det dφ.
• TauCeti.lintegral_ofReal_image_eq_lintegral_ofReal_of_eq_abs_det_mul: the lower Lebesgue integral of the positive part of a real density scaling by |det dφ|.

theorem TauCeti.integral_image_eq_integral_of_eq_abs_det_smul {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {φ : ℝ × ℝ → ℝ × ℝ} {s : Set (ℝ × ℝ)} {f g : ℝ × ℝ → F} (hs : MeasurableSet s) (hinj : Set.InjOn φ s) (hφ : ∀ w ∈ s, DifferentiableAt ℝ φ w) (hf : ∀ w ∈ s, f w = |(fderiv ℝ φ w).det| • g (φ w)) : ∫ (z : ℝ × ℝ) in φ '' s, g z = ∫ (w : ℝ × ℝ) in s, f w

Change of variables for a density. If a density f on a measurable set s is |det dφ| times g ∘ φ, for a change of coordinates φ that is injective and differentiable on s, then the integral of g over φ '' s is the integral of f over s.

theorem TauCeti.lintegral_enorm_image_eq_lintegral_enorm_of_eq_det_smul {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {φ : ℝ × ℝ → ℝ × ℝ} {s : Set (ℝ × ℝ)} {f g : ℝ × ℝ → F} (hs : MeasurableSet s) (hinj : Set.InjOn φ s) (hφ : ∀ w ∈ s, DifferentiableAt ℝ φ w) (hf : ∀ w ∈ s, f w = (fderiv ℝ φ w).det • g (φ w)) : ∫⁻ (z : ℝ × ℝ) in φ '' s, ‖g z‖ₑ = ∫⁻ (w : ℝ × ℝ) in s, ‖f w‖ₑ

Change of variables for the size of a density. If a density f on a measurable set s is det dφ times g ∘ φ, for a change of coordinates φ that is injective and differentiable on s, then the lower Lebesgue integral of ‖g‖ₑ over φ '' s is that of ‖f‖ₑ over s. No orientation, integrability or measurability hypothesis is needed.

theorem TauCeti.lintegral_ofReal_image_eq_lintegral_ofReal_of_eq_abs_det_mul {φ : ℝ × ℝ → ℝ × ℝ} {s : Set (ℝ × ℝ)} {f g : ℝ × ℝ → ℝ} (hs : MeasurableSet s) (hinj : Set.InjOn φ s) (hφ : ∀ w ∈ s, DifferentiableAt ℝ φ w) (hf : ∀ w ∈ s, f w = |(fderiv ℝ φ w).det| * g (φ w)) : ∫⁻ (z : ℝ × ℝ) in φ '' s, ENNReal.ofReal (g z) = ∫⁻ (w : ℝ × ℝ) in s, ENNReal.ofReal (f w)

Change of variables for the positive part of a density. If a real density f on a measurable set s is |det dφ| times g ∘ φ, for a change of coordinates φ that is injective and differentiable on s, then the lower Lebesgue integral of the positive part of g over φ '' s is that of f over s. No integrability or measurability hypothesis is needed.