integral_comp_smul_deriv_Ioi — Mathlib

English

Let f: ℝ → ℝ and g: ℝ → E with a differentiability and integrability framework on the half-line Ioi a. Then, under suitable hypotheses, the change of variables formula holds for the integral of f' times (g ∘ f) over Ioi a, equaling the integral of g over Ioi (f(a)).

Русский

Пусть f: ℝ → ℝ и g: ℝ → E удовлетворяют условиям дифференцируемости на Ioi a; тогда формула замены переменной для интеграла вида f'(x)(g(f(x))) по x > a равна интегралу g по u > f(a).

LaTeX

$$$$ \int_{x \in Ioi a} f'(x) \cdot (g \circ f)(x) \, dx = \int_{u \in Ioi (f(a))} g(u) \, du. $$$$

Lean4

/-- Change-of-variables formula for `Ioi` integrals of vector-valued functions, proved by taking
limits from the result for finite intervals. -/
theorem integral_comp_smul_deriv_Ioi {f f' : ℝ → ℝ} {g : ℝ → E} {a : ℝ} (hf : ContinuousOn f <| Ici a)
    (hft : Tendsto f atTop atTop) (hff' : ∀ x ∈ Ioi a, HasDerivWithinAt f (f' x) (Ioi x) x)
    (hg_cont : ContinuousOn g <| f '' Ioi a) (hg1 : IntegrableOn g <| f '' Ici a)
    (hg2 : IntegrableOn (fun x => f' x • (g ∘ f) x) (Ici a)) :
    (∫ x in Ioi a, f' x • (g ∘ f) x) = ∫ u in Ioi (f a), g u :=
  by
  have eq : ∀ b : ℝ, a < b → (∫ x in a..b, f' x • (g ∘ f) x) = ∫ u in f a..f b, g u := fun b hb ↦
    by
    have i1 : Ioo (min a b) (max a b) ⊆ Ioi a := by
      rw [min_eq_left hb.le]
      exact Ioo_subset_Ioi_self
    have i2 : [[a, b]] ⊆ Ici a := by rw [uIcc_of_le hb.le]; exact Icc_subset_Ici_self
    refine
        intervalIntegral.integral_comp_smul_deriv''' (hf.mono i2) (fun x hx => hff' x <| mem_of_mem_of_subset hx i1)
          (hg_cont.mono <| image_mono ?_) (hg1.mono_set <| image_mono ?_) (hg2.mono_set i2) <;>
      assumption
  rw [integrableOn_Ici_iff_integrableOn_Ioi] at hg2
  have t2 := intervalIntegral_tendsto_integral_Ioi _ hg2 tendsto_id
  have : Ioi (f a) ⊆ f '' Ici a :=
    Ioi_subset_Ici_self.trans <|
      IsPreconnected.intermediate_value_Ici isPreconnected_Ici left_mem_Ici (le_principal_iff.mpr <| Ici_mem_atTop _) hf
        hft
  have t1 := (intervalIntegral_tendsto_integral_Ioi _ (hg1.mono_set this) tendsto_id).comp hft
  exact tendsto_nhds_unique (Tendsto.congr' (eventuallyEq_of_mem (Ioi_mem_atTop a) eq) t2) t1

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