English
For antitone f, the lintegral of u over f''s equals the lintegral over s of (-f') times u∘f, interpreting det via one-dimensional derivative.
Русский
Для антиинвариантной f линеграль над образами равен линегралу по исходному множеству от (-f')·u∘f.
LaTeX
$$$$ \\int_{f''s} u(x) dx = \\int_s (-f'(x)) \\cdot u(f(x)) dx $$$$
Lean4
theorem lintegral_image_eq_lintegral_deriv_mul_of_monotoneOn (hs : MeasurableSet s)
(hf' : ∀ x ∈ s, HasDerivWithinAt f (f' x) s x) (hf : MonotoneOn f s) (u : ℝ → ℝ≥0∞) :
∫⁻ x in f '' s, u x = ∫⁻ x in s, ENNReal.ofReal (f' x) * u (f x) :=
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 : ∫⁻ x in s, ENNReal.ofReal (f' x) * u (f x) = ∫⁻ x in c, ENNReal.ofReal (f' x) * u (f x) :=
by
have : ∫⁻ x in a, ENNReal.ofReal (f' x) * u (f x) = 0 := setLIntegral_measure_zero a _ (a_count.measure_zero volume)
rw [← h_union, lintegral_union (hb.union hc) h_disj, this, zero_add]
have : ∫⁻ x in b, ENNReal.ofReal (f' x) * u (f x) = 0 := setLIntegral_eq_zero hb (fun x hx ↦ by simp [deriv_b x hx])
rw [lintegral_union hc h_disj', this, zero_add]
have J : ∫⁻ x in f '' s, u x = ∫⁻ x in f '' c, u x :=
by
apply setLIntegral_congr
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
have : ∫⁻ x in c, ENNReal.ofReal (f' x) * u (f x) = ∫⁻ x in c, ENNReal.ofReal (|(F' x).det|) * u (f x) :=
by
apply setLIntegral_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 lintegral_image_eq_lintegral_abs_det_fderiv_mul _ hc hf' inj_c _
