tendsto_zero_of_hasDerivAt_of_integrableOn_Iic

English

If f and f' are suitably integrable on (−∞, a], then the integral tends to ∫ f' as the left end tends to −∞.

Русский

Если f и f' интегрируемы на (−∞, a], то интеграл стремится к пределу по левой границе.

LaTeX

$$$\\text{tendsto} \\ i \\ mapsto ∫ x\\in Iic(a), f'(x) dx = ∫ x\\in Iic(a), f'(x) dx$.$$

Lean4

/-- If a function and its derivative are integrable on `(-∞, a]`, then the function tends to zero
at `-∞`. -/
theorem tendsto_zero_of_hasDerivAt_of_integrableOn_Iic (hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x)
    (f'int : IntegrableOn f' (Iic a)) (fint : IntegrableOn f (Iic a)) : Tendsto f atBot (𝓝 0) :=
  by
  let F : E →L[ℝ] Completion E := Completion.toComplL
  have Fderiv : ∀ x ∈ Iic a, HasDerivAt (F ∘ f) (F (f' x)) x := fun x hx ↦ F.hasFDerivAt.comp_hasDerivAt _ (hderiv x hx)
  have Fint : IntegrableOn (F ∘ f) (Iic a) := by apply F.integrable_comp fint
  have F'int : IntegrableOn (F ∘ f') (Iic a) := by apply F.integrable_comp f'int
  have A : Tendsto (F ∘ f) atBot (𝓝 (limUnder atBot (F ∘ f))) := by
    apply tendsto_limUnder_of_hasDerivAt_of_integrableOn_Iic Fderiv F'int
  have B : limUnder atBot (F ∘ f) = F 0 :=
    by
    have : IntegrableAtFilter (F ∘ f) atBot := by exact ⟨Iic a, Iic_mem_atBot _, Fint⟩
    apply IntegrableAtFilter.eq_zero_of_tendsto this ?_ A
    intro s hs
    rcases mem_atBot_sets.1 hs with ⟨b, hb⟩
    apply le_antisymm (le_top)
    rw [← volume_Iic (a := b)]
    exact measure_mono hb
  rwa [B, ← IsEmbedding.tendsto_nhds_iff] at A
  exact (Completion.isUniformEmbedding_coe E).isEmbedding

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