English
For vector-valued functions with u, v differentiable on [a,b] and derivatives u', v' with appropriate integrability, the IBP identity holds: ∫_a^b (u x) · v'(x) + u'(x) · v(x) dx = u(b) · v(b) − u(a) · v(a).
Русский
Для векторных функций, где u и v дифференцируемы на [a,b] с производными u', v' и интегрируемостью, выполняется тождество IBP: ∫_a^b (u(x) · v'(x) + u'(x) · v(x)) dx = u(b) · v(b) − u(a) · v(a).
LaTeX
$$$\\displaystyle \\int_a^b (u(x) \\cdot v'(x) + u'(x) \\cdot v(x)) \\,dx = u(b) \\cdot v(b) - u(a) \\cdot v(a)$$$
Lean4
/-- Change of variables, general form. If `f` is continuous on `[a, b]` and has
right-derivative `f'` in `(a, b)`, `g` is continuous on `f '' (a, b)` and integrable on
`f '' [a, b]`, and `f' x • (g ∘ f) x` is integrable on `[a, b]`,
then we can substitute `u = f x` to get `∫ x in a..b, f' x • (g ∘ f) x = ∫ u in f a..f b, g u`.
If the function `f` is monotone or antitone, see also
`integral_image_eq_integral_deriv_smul_of_monotoneOn` dropping all assumptions on `g`. -/
theorem integral_comp_smul_deriv''' (hf : ContinuousOn f [[a, b]])
(hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x)
(hg_cont : ContinuousOn g (f '' Ioo (min a b) (max a b))) (hg1 : IntegrableOn g (f '' [[a, b]]))
(hg2 : IntegrableOn (fun x ↦ f' x • (g ∘ f) x) [[a, b]]) : (∫ x in a..b, f' x • (g ∘ f) x) = ∫ u in f a..f b, g u :=
by
by_cases hE : CompleteSpace E; swap
· simp [intervalIntegral, integral, hE]
rw [hf.image_uIcc, ← intervalIntegrable_iff'] at hg1
have h_cont : ContinuousOn (fun u ↦ ∫ t in f a..f u, g t) [[a, b]] :=
by
refine (continuousOn_primitive_interval' hg1 ?_).comp hf ?_
· rw [← hf.image_uIcc]; exact mem_image_of_mem f left_mem_uIcc
· rw [← hf.image_uIcc]; exact mapsTo_image _ _
have h_der :
∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt (fun u ↦ ∫ t in f a..f u, g t) (f' x • (g ∘ f) x) (Ioi x) x :=
by
intro x hx
obtain ⟨c, hc⟩ := nonempty_Ioo.mpr hx.1
obtain ⟨d, hd⟩ := nonempty_Ioo.mpr hx.2
have cdsub : [[c, d]] ⊆ Ioo (min a b) (max a b) :=
by
rw [uIcc_of_le (hc.2.trans hd.1).le]
exact Icc_subset_Ioo hc.1 hd.2
replace hg_cont := hg_cont.mono (image_mono cdsub)
let J := [[sInf (f '' [[c, d]]), sSup (f '' [[c, d]])]]
have hJ : f '' [[c, d]] = J := (hf.mono (cdsub.trans Ioo_subset_Icc_self)).image_uIcc
rw [hJ] at hg_cont
have h2x : f x ∈ J := by rw [← hJ]; exact mem_image_of_mem _ (mem_uIcc_of_le hc.2.le hd.1.le)
have h2g : IntervalIntegrable g volume (f a) (f x) :=
by
refine hg1.mono_set ?_
rw [← hf.image_uIcc]
exact hf.surjOn_uIcc left_mem_uIcc (Ioo_subset_Icc_self hx)
have h3g : StronglyMeasurableAtFilter g (𝓝[J] f x) :=
hg_cont.stronglyMeasurableAtFilter_nhdsWithin measurableSet_Icc (f x)
haveI : Fact (f x ∈ J) := ⟨h2x⟩
have : HasDerivWithinAt (fun u ↦ ∫ x in f a..u, g x) (g (f x)) J (f x) :=
intervalIntegral.integral_hasDerivWithinAt_right h2g h3g (hg_cont (f x) h2x)
refine (this.scomp x ((hff' x hx).Ioo_of_Ioi hd.1) ?_).Ioi_of_Ioo hd.1
rw [← hJ]
refine (mapsTo_image _ _).mono ?_ Subset.rfl
exact Ioo_subset_Icc_self.trans ((Icc_subset_Icc_left hc.2.le).trans Icc_subset_uIcc)
rw [← intervalIntegrable_iff'] at hg2
simp_rw [integral_eq_sub_of_hasDeriv_right h_cont h_der hg2, integral_same, sub_zero]
