English
If a function and its derivative are integrable near infinity, then f(∞) = 0 under the appropriate continuous extension to the completion space.
Русский
Если функция и её производная интегрируемы в окрестности бесконечности, то в подходящем рамках непрерывного продолжения в ХП функция стремится к нулю на бесконечности.
LaTeX
$$$\\text{Tendsto}\\ f\\ atTop\\ (\\mathcal{N}\\ 0).$$$
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_Ioi (hderiv : ∀ x ∈ Ioi a, HasDerivAt f (f' x) x)
(f'int : IntegrableOn f' (Ioi a)) (fint : IntegrableOn f (Ioi a)) : Tendsto f atTop (𝓝 0) :=
by
let F : E →L[ℝ] Completion E := Completion.toComplL
have Fderiv : ∀ x ∈ Ioi a, HasDerivAt (F ∘ f) (F (f' x)) x := fun x hx ↦ F.hasFDerivAt.comp_hasDerivAt _ (hderiv x hx)
have Fint : IntegrableOn (F ∘ f) (Ioi a) := by apply F.integrable_comp fint
have F'int : IntegrableOn (F ∘ f') (Ioi a) := by apply F.integrable_comp f'int
have A : Tendsto (F ∘ f) atTop (𝓝 (limUnder atTop (F ∘ f))) := by
apply tendsto_limUnder_of_hasDerivAt_of_integrableOn_Ioi Fderiv F'int
have B : limUnder atTop (F ∘ f) = F 0 :=
by
have : IntegrableAtFilter (F ∘ f) atTop := by exact ⟨Ioi a, Ioi_mem_atTop _, Fint⟩
apply IntegrableAtFilter.eq_zero_of_tendsto this ?_ A
intro s hs
rcases mem_atTop_sets.1 hs with ⟨b, hb⟩
rw [← top_le_iff, ← volume_Ici (a := b)]
exact measure_mono hb
rwa [B, ← IsEmbedding.tendsto_nhds_iff] at A
exact (Completion.isUniformEmbedding_coe E).isEmbedding
