English
If f is eventually differentiable near c on a punctured neighborhood and ||f(x)|| → ∞ as x → c, with f' = O(g) near c, then g is not interval integrable on any interval containing c.
Русский
Если f задана около c на punctured окне и ||f(x)|| → ∞ при x → c, при этом f' = O(g) около c, то g не интегрируема на любом интервале, содержащем c.
LaTeX
$$$\\neg \\text{IntervalIntegrable}(g, \\text{volume}, a, b)$ under punctured neighborhood conditions$$
Lean4
/-- If `f` is eventually differentiable along a nontrivial filter `l : Filter ℝ` that is generated
by convex sets, the norm of `f` tends to infinity along `l`, and `f' = O(g)` along `l`, where `f'`
is the derivative of `f`, then `g` is not integrable on any interval `a..b` such that
`[a, b] ∈ l`. -/
theorem not_intervalIntegrable_of_tendsto_norm_atTop_of_deriv_isBigO_filter {f : ℝ → E} {g : ℝ → F} {a b : ℝ}
(l : Filter ℝ) [NeBot l] [TendstoIxxClass Icc l l] (hl : [[a, b]] ∈ l) (hd : ∀ᶠ x in l, DifferentiableAt ℝ f x)
(hf : Tendsto (fun x => ‖f x‖) l atTop) (hfg : deriv f =O[l] g) : ¬IntervalIntegrable g volume a b :=
by
rw [intervalIntegrable_iff']
exact not_integrableOn_of_tendsto_norm_atTop_of_deriv_isBigO_filter _ hl hd hf hfg
