English
If f is differentiable in a punctured neighborhood of c, with ||f(x)|| → ∞ as x → c, and f' = O(g) along 𝓝[≠] c, then g is not interval integrable on any nontrivial interval a..b with c ∈ [a,b].
Русский
Если f дифференцируема в окружности pункты вокруг c, и ||f(x)|| → ∞ при x → c, и f' = O(g) вдоль 𝓝[≠] c, то g не интегрируем по любому не тривиальному интервалу a..b, где c ∈ [a,b].
LaTeX
$$$\\neg \\text{IntervalIntegrable}(g, \\text{volume}, a, b)$$$
Lean4
/-- If `f` is differentiable in a punctured neighborhood of `c`, `‖f x‖ → ∞` as `x → c` (more
formally, along the filter `𝓝[≠] c`), and `f' = O(g)` along `𝓝[≠] c`, where `f'` is the derivative
of `f`, then `g` is not interval integrable on any nontrivial interval `a..b` such that
`c ∈ [a, b]`. -/
theorem not_intervalIntegrable_of_tendsto_norm_atTop_of_deriv_isBigO_punctured {f : ℝ → E} {g : ℝ → F} {a b c : ℝ}
(h_deriv : ∀ᶠ x in 𝓝[≠] c, DifferentiableAt ℝ f x) (h_infty : Tendsto (fun x => ‖f x‖) (𝓝[≠] c) atTop)
(hg : deriv f =O[𝓝[≠] c] g) (hne : a ≠ b) (hc : c ∈ [[a, b]]) : ¬IntervalIntegrable g volume a b :=
have : 𝓝[[[a, b]] \ { c }] c ≤ 𝓝[≠] c := nhdsWithin_mono _ inter_subset_right
not_intervalIntegrable_of_tendsto_norm_atTop_of_deriv_isBigO_within_diff_singleton hne hc (h_deriv.filter_mono this)
(h_infty.mono_left this) (hg.mono this)
