English
For antitone f, the integral identity holds with the derivative sign reversed in the integrand: ∫ g over image equals ∫ (-f') • g∘f over the domain.
Русский
Для антиинвариантной f интеграционная формула сохраняется с противоположным знаком внутри интеграла: образ равен интегралу от (-f')·g∘f по исходному множеству.
LaTeX
$$$$ \\int_{f''s} g(x) dx = \\int_s (-f'(x)) \\cdot g(f(x)) dx $$$$
Lean4
/-- Change of variable formula for differentiable functions: if a real function `f` is
monotone and differentiable on a measurable set `s`, then the Bochner integral of a function
`g : ℝ → F` on `f '' s` coincides with the integral of `(f' x) • g ∘ f` on `s` . -/
theorem integral_image_eq_integral_deriv_smul_of_monotoneOn (hs : MeasurableSet s)
(hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x) (hf : MonotoneOn f s) (g : ℝ → F) :
∫ x in f '' s, g x = ∫ x in s, f' x • g (f x) :=
by
by_cases H : IntegrableOn g (f '' s); swap
· rw [integral_undef H, integral_undef]
simpa [integrableOn_image_iff_integrableOn_deriv_smul_of_monotoneOn hs hf' hf] using H
have H' : IntegrableOn (fun x ↦ (f' x) • g (f x)) s :=
(integrableOn_image_iff_integrableOn_deriv_smul_of_monotoneOn hs hf' hf g).1 H
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 a_s : a ⊆ s := by rw [← h_union]; exact subset_union_left
have bc_s : b ∪ c ⊆ s := by rw [← h_union]; exact subset_union_right
have b_s : b ⊆ s := by rw [← h_union]; exact subset_union_left.trans subset_union_right
have c_s : c ⊆ s := by rw [← h_union]; exact subset_union_right.trans subset_union_right
have I : ∫ x in s, f' x • g (f x) = ∫ x in c, f' x • g (f x) :=
by
have : ∫ x in a, f' x • g (f x) = 0 := setIntegral_measure_zero _ (a_count.measure_zero volume)
rw [← h_union, setIntegral_union h_disj (hb.union hc) (H'.mono_set a_s) (H'.mono_set bc_s), this, zero_add]
have : ∫ x in b, f' x • g (f x) = 0 := setIntegral_eq_zero_of_forall_eq_zero (fun x hx ↦ by simp [deriv_b x hx])
rw [setIntegral_union h_disj' hc (H'.mono_set b_s) (H'.mono_set c_s), this, zero_add]
have J : ∫ x in f '' s, g x = ∫ x in f '' c, g x :=
by
apply setIntegral_congr_set
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]
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
have : ∫ x in c, f' x • g (f x) = ∫ x in c, |(F' x).det| • g (f x) :=
by
apply setIntegral_congr_fun hc (fun x hx ↦ ?_)
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)]
rw [this]
exact
integral_image_eq_integral_abs_det_fderiv_smul _ hc hF' inj_c
_
/- Change of variable formula for differentiable functions: if a real function `f` is
antitone and differentiable on a measurable set `s`, then the Lebesgue integral of a function
`u : ℝ → ℝ≥0∞` on `f '' s` coincides with the integral of `(-f' x) * u ∘ f` on `s`.
Note that the measurability of `f '' s` is given by `MeasurableSet.image_of_antitoneOn`. -/
