English
If f is eventually differentiable along a nontrivial filter l and ||f|| → ∞ along l, with f' = O(g) along l, then g is not interval integrable on any interval a..b.
Русский
Если f конечна дифференцируема вдоль неабсолютно-тривиального фильтра l и ||f|| → ∞ вдоль l, причем f' = O(g) вдоль l, то g не интегрируема по интервалу a..b.
LaTeX
$$$\\neg \\text{IntervalIntegrable}(g, \\text{volume}, a, b)$ under the stated Big-O/differentiability hypotheses$$
Lean4
theorem not_integrableOn_of_tendsto_norm_atTop_of_deriv_isBigO_filter {f : ℝ → E} {g : ℝ → F} {k : Set ℝ} (l : Filter ℝ)
[NeBot l] [TendstoIxxClass Icc l l] (hl : k ∈ l) (hd : ∀ᶠ x in l, DifferentiableAt ℝ f x)
(hf : Tendsto (fun x => ‖f x‖) l atTop) (hfg : deriv f =O[l] g) : ¬IntegrableOn g k :=
by
let a : E →ₗᵢ[ℝ] UniformSpace.Completion E := UniformSpace.Completion.toComplₗᵢ
let f' := a ∘ f
have h'd : ∀ᶠ x in l, DifferentiableAt ℝ f' x := by
filter_upwards [hd] with x hx using a.toContinuousLinearMap.differentiableAt.comp x hx
have h'f : Tendsto (fun x => ‖f' x‖) l atTop := hf.congr (fun x ↦ by simp [f'])
have h'fg : deriv f' =O[l] g := by
apply IsBigO.trans _ hfg
rw [← isBigO_norm_norm]
suffices (fun x ↦ ‖deriv f' x‖) =ᶠ[l] (fun x ↦ ‖deriv f x‖) by exact this.isBigO
filter_upwards [hd] with x hx
have : deriv f' x = a (deriv f x) := by
rw [fderiv_comp_deriv x _ hx]
· have : fderiv ℝ a (f x) = a.toContinuousLinearMap := a.toContinuousLinearMap.fderiv
simp only [this]
rfl
· exact a.toContinuousLinearMap.differentiableAt
simp only [this]
simp
exact not_integrableOn_of_tendsto_norm_atTop_of_deriv_isBigO_filter_aux l hl h'd h'f h'fg
