English
If a and b are distinct and c is in their uIcc, and f is differentiable near c except possibly at c, with ||f(x)|| → ∞ as x → c within the punctured neighborhood, and f′ = O(g) along nhds within that neighborhood, then g is not interval integrable on a..b.
Русский
Если a ≠ b и c ∈ их uIcc, и f дифференцируема рядом с c, кроме самой точки c, с ||f(x)|| → ∞ при x → c внутри удаленного вокруг, и f′ = O(g) вдоль nhds внутри этого окрестности, то g не интегрируем на a..b.
LaTeX
$$$\\neg \\text{IntervalIntegrable}(g, \\text{volume}, a, b)$ under within-diff singleton conditions$$
Lean4
/-- If `f` grows in the punctured neighborhood of `c : ℝ` at least as fast as `1 / (x - c)`,
then it is not interval integrable on any nontrivial interval `a..b`, `c ∈ [a, b]`. -/
theorem not_intervalIntegrable_of_sub_inv_isBigO_punctured {f : ℝ → F} {a b c : ℝ}
(hf : (fun x => (x - c)⁻¹) =O[𝓝[≠] c] f) (hne : a ≠ b) (hc : c ∈ [[a, b]]) : ¬IntervalIntegrable f volume a b :=
by
have A : ∀ᶠ x in 𝓝[≠] c, HasDerivAt (fun x => Real.log (x - c)) (x - c)⁻¹ x :=
by
filter_upwards [self_mem_nhdsWithin] with x hx
simpa using ((hasDerivAt_id x).sub_const c).log (sub_ne_zero.2 hx)
have B : Tendsto (fun x => ‖Real.log (x - c)‖) (𝓝[≠] c) atTop :=
by
refine tendsto_abs_atBot_atTop.comp (Real.tendsto_log_nhdsNE_zero.comp ?_)
rw [← sub_self c]
exact ((hasDerivAt_id c).sub_const c).tendsto_nhdsNE one_ne_zero
exact
not_intervalIntegrable_of_tendsto_norm_atTop_of_deriv_isBigO_punctured (A.mono fun x hx => hx.differentiableAt) B
(hf.congr' (A.mono fun x hx => hx.deriv.symm) EventuallyEq.rfl) hne hc
