integral_deriv_comp_mul_deriv' — Mathlib

English

If f is differentiable with derivative f' and g is continuous, then ∫ (g ∘ f) f' equals ∫ g with substitution.

Русский

Если f дифференцируема, a g непрерывна, то интеграл по переменной равен интегралу по образу через подстановку.

LaTeX

$$$\\displaystyle \\int_a^b (g \\circ f)(x) f'(x) \\,dx = \\int_{f(a)}^{f(b)} g(u) \\,du$$$

Lean4

theorem integral_deriv_comp_mul_deriv' {f f' g g' : ℝ → ℝ} (hf : ContinuousOn f [[a, b]])
    (hff' : ∀ x ∈ Ioo (min a b) (max a b), HasDerivWithinAt f (f' x) (Ioi x) x) (hf' : ContinuousOn f' [[a, b]])
    (hg : ContinuousOn g [[f a, f b]])
    (hgg' : ∀ x ∈ Ioo (min (f a) (f b)) (max (f a) (f b)), HasDerivWithinAt g (g' x) (Ioi x) x)
    (hg' : ContinuousOn g' (f '' [[a, b]])) : (∫ x in a..b, (g' ∘ f) x * f' x) = (g ∘ f) b - (g ∘ f) a := by
  simpa [mul_comm] using integral_deriv_comp_smul_deriv' hf hff' hf' hg hgg' hg'

Похожие утверждения