English
When transporting via a measurable equivalence, the density formula remains the same under the image; the pushforward equals the target measure on the image.
Русский
При переносе по измеримой эквивалентности плотность сохраняется, образная мера равна целевой мере на образе.
LaTeX
$$$$ \\mathrm{withDensity}(g) \\mapsto \\mathrm{map}(f)(\\mathrm{withDensity}(g)) = \\mu|_{f''s} $$$$
Lean4
/-- Integrability in the change of variable formula for differentiable functions: if a real
function `f` is monotone and differentiable on a measurable set `s`, then a function
`g : ℝ → F` is integrable on `f '' s` if and only if `f' x • g ∘ f` is integrable on `s` . -/
theorem integrableOn_image_iff_integrableOn_deriv_smul_of_monotoneOn (hs : MeasurableSet s)
(hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x) (hf : MonotoneOn f s) (g : ℝ → F) :
IntegrableOn g (f '' s) ↔ IntegrableOn (fun x ↦ (f' x) • g (f x)) s :=
by
rcases exists_decomposition_of_monotoneOn_hasDerivWithinAt hs hf hf' with
⟨a, b, c, h_union, ha, hb, hc, h_disj, h_disj', a_count, fb_count, deriv_b, deriv_c, inj_c⟩
have I : IntegrableOn (fun x => (f' x) • g (f x)) s ↔ IntegrableOn (fun x => (f' x) • g (f x)) c :=
by
have A : IntegrableOn (fun x ↦ f' x • g (f x)) a := IntegrableOn.of_measure_zero (a_count.measure_zero volume)
have B : IntegrableOn (fun x ↦ f' x • g (f x)) b :=
by
have : IntegrableOn (fun x ↦ (0 : F)) b := by simp
exact this.congr_fun (fun x hx ↦ by simp [deriv_b x hx]) hb
simp only [← h_union, integrableOn_union, A, B, true_and]
have J : IntegrableOn g (f '' s) ↔ IntegrableOn g (f '' c) :=
by
apply integrableOn_congr_set_ae
rw [← h_union, image_union, image_union]
have A : (f '' a ∪ (f '' b ∪ f '' c) : Set ℝ) =ᵐ[volume] (f '' b ∪ f '' c : Set ℝ) :=
by
refine union_ae_eq_right_of_ae_eq_empty (ae_eq_empty.mpr ?_)
exact (a_count.image _).measure_zero _
have B : (f '' b ∪ f '' c : Set ℝ) =ᵐ[volume] f '' c :=
union_ae_eq_right_of_ae_eq_empty (ae_eq_empty.mpr (fb_count.measure_zero _))
exact A.trans B
rw [I, J]
have c_s : c ⊆ s := by rw [← h_union]; exact subset_union_right.trans subset_union_right
let F' : ℝ → (ℝ →L[ℝ] ℝ) := fun x ↦ ContinuousLinearMap.smulRight (1 : ℝ →L[ℝ] ℝ) (f' x)
have hF' (x : ℝ) (hx : x ∈ c) : HasFDerivWithinAt f (F' x) c x := (hf' x (c_s hx)).hasFDerivWithinAt.mono c_s
rw [integrableOn_image_iff_integrableOn_abs_det_fderiv_smul _ hc hF' inj_c]
apply integrableOn_congr_fun (fun x hx ↦ ?_) hc
simp only [LinearMap.det_ring, ContinuousLinearMap.coe_coe, ContinuousLinearMap.smulRight_apply,
ContinuousLinearMap.one_apply, smul_eq_mul, one_mul, F']
rw [abs_of_nonneg (deriv_c x hx)]
