English
A variant of the fundamental theorem on (-∞, a] with differentiability on (−∞, a] and continuity at a⁻.
Русский
Variant FTC на (−∞, a] с производной и непрерывностью на a−.
LaTeX
$$$\\int_{Iic(a)} f' = f(a) - m$ under hypotheses.$$
Lean4
/-- If the derivative of a function defined on the real line is integrable close to `-∞`, then
the function has a limit at `-∞`. -/
theorem tendsto_limUnder_of_hasDerivAt_of_integrableOn_Iic [CompleteSpace E]
(hderiv : ∀ x ∈ Iic a, HasDerivAt f (f' x) x) (f'int : IntegrableOn f' (Iic a)) :
Tendsto f atBot (𝓝 (limUnder atBot f)) :=
by
suffices ∃ a, Tendsto f atBot (𝓝 a) from tendsto_nhds_limUnder this
let g := f ∘ (fun x ↦ -x)
have hdg : ∀ x ∈ Ioi (-a), HasDerivAt g (-f' (-x)) x :=
by
intro x hx
have : -x ∈ Iic a := by simp only [mem_Iic, mem_Ioi, neg_le] at *; exact hx.le
simpa using HasDerivAt.scomp x (hderiv (-x) this) (hasDerivAt_neg' x)
have L : Tendsto g atTop (𝓝 (limUnder atTop g)) :=
by
apply tendsto_limUnder_of_hasDerivAt_of_integrableOn_Ioi hdg
exact
((MeasurePreserving.integrableOn_comp_preimage (Measure.measurePreserving_neg _)
(Homeomorph.neg ℝ).measurableEmbedding).2
f'int.neg).mono_set
(by simp)
refine ⟨limUnder atTop g, ?_⟩
have : Tendsto (fun x ↦ g (-x)) atBot (𝓝 (limUnder atTop g)) := L.comp tendsto_neg_atBot_atTop
simpa [g] using this
