English
If a ≠ b and c ∈ [a,b], and f is differentiable near c within [a,b]\{c}, with ||f(x)|| → ∞ as x → c inside [a,b]\{c}, and f' = O(g) along nhds within the punctured singleton, then g is not interval integrable on a..b.
Русский
Если a ≠ b и c ∈ [a,b], и функция f дифференцируема в окрестности c внутри [a,b]\{c}, ||f(x)|| → ∞ при x → c внутри [a,b]\{c}, и f' = O(g) вдоль nhds внутри удаленной точки, то g не интегрируема на a..b.
LaTeX
$$$\\neg \\text{IntervalIntegrable}(g, \\text{volume}, a, b)$ under within-diff singleton hypotheses$$
Lean4
/-- If `a ≠ b`, `c ∈ [a, b]`, `f` is differentiable in the neighborhood of `c` within
`[a, b] \ {c}`, `‖f x‖ → ∞` as `x → c` within `[a, b] \ {c}`, and `f' = O(g)` along
`𝓝[[a, b] \ {c}] c`, where `f'` is the derivative of `f`, then `g` is not interval integrable on
`a..b`. -/
theorem not_intervalIntegrable_of_tendsto_norm_atTop_of_deriv_isBigO_within_diff_singleton {f : ℝ → E} {g : ℝ → F}
{a b c : ℝ} (hne : a ≠ b) (hc : c ∈ [[a, b]]) (h_deriv : ∀ᶠ x in 𝓝[[[a, b]] \ { c }] c, DifferentiableAt ℝ f x)
(h_infty : Tendsto (fun x => ‖f x‖) (𝓝[[[a, b]] \ { c }] c) atTop) (hg : deriv f =O[𝓝[[[a, b]] \ { c }] c] g) :
¬IntervalIntegrable g volume a b :=
by
obtain ⟨l, hl, hl', hle, hmem⟩ : ∃ l : Filter ℝ, TendstoIxxClass Icc l l ∧ l.NeBot ∧ l ≤ 𝓝 c ∧ [[a, b]] \ { c } ∈ l :=
by
rcases (min_lt_max.2 hne).gt_or_lt c with hlt | hlt
· refine ⟨𝓝[<] c, inferInstance, inferInstance, inf_le_left, ?_⟩
rw [← Iic_diff_right]
exact diff_mem_nhdsWithin_diff (Icc_mem_nhdsLE_of_mem ⟨hlt, hc.2⟩) _
· refine ⟨𝓝[>] c, inferInstance, inferInstance, inf_le_left, ?_⟩
rw [← Ici_diff_left]
exact diff_mem_nhdsWithin_diff (Icc_mem_nhdsGE_of_mem ⟨hc.1, hlt⟩) _
have : l ≤ 𝓝[[[a, b]] \ { c }] c := le_inf hle (le_principal_iff.2 hmem)
exact
not_intervalIntegrable_of_tendsto_norm_atTop_of_deriv_isBigO_filter l (mem_of_superset hmem diff_subset)
(h_deriv.filter_mono this) (h_infty.mono_left this) (hg.mono this)
