English
Auxiliary result: if a function f is eventually differentiable along a nontrivial convex filter l, and ||f|| → ∞ along l while f′ = O(g) along l, then g is not integrable on any set k ∈ l.
Русский
Вспомогательный пример: если f растет до бесконечности вдоль неконечной выпуклой фильтрации l и производная f′ = O(g) вдоль l, то g не интегрируема на любом множестве k ∈ l.
LaTeX
$$$\\forall f,g,l,\\ (\\text{convex}, \\text{nontrivial})\\ (f' = O_l(g)) \\land (\\|f\\| \\to \\infty \\text{ along } l) \\Rightarrow \\neg \\operatorname{IntegrableOn}(g, k)\\text{ for any } k\\in l$$$
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 set `k` belonging to `l`.
Auxiliary version assuming that `E` is complete. -/
theorem not_integrableOn_of_tendsto_norm_atTop_of_deriv_isBigO_filter_aux [CompleteSpace E] {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
intro hgi
obtain ⟨C, hC₀, s, hsl, hsub, hfd, hg⟩ :
∃ (C : ℝ) (_ : 0 ≤ C),
∃ s ∈ l,
(∀ x ∈ s, ∀ y ∈ s, [[x, y]] ⊆ k) ∧
(∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ [[x, y]], DifferentiableAt ℝ f z) ∧
∀ x ∈ s, ∀ y ∈ s, ∀ z ∈ [[x, y]], ‖deriv f z‖ ≤ C * ‖g z‖ :=
by
rcases hfg.exists_nonneg with ⟨C, C₀, hC⟩
have h : ∀ᶠ x : ℝ × ℝ in l ×ˢ l, ∀ y ∈ [[x.1, x.2]], (DifferentiableAt ℝ f y ∧ ‖deriv f y‖ ≤ C * ‖g y‖) ∧ y ∈ k :=
(tendsto_fst.uIcc tendsto_snd).eventually ((hd.and hC.bound).and hl).smallSets
rcases mem_prod_self_iff.1 h with ⟨s, hsl, hs⟩
simp only [prod_subset_iff, mem_setOf_eq] at hs
exact
⟨C, C₀, s, hsl, fun x hx y hy z hz => (hs x hx y hy z hz).2, fun x hx y hy z hz => (hs x hx y hy z hz).1.1,
fun x hx y hy z hz => (hs x hx y hy z hz).1.2⟩
replace hgi : IntegrableOn (fun x ↦ C * ‖g x‖) k := by exact hgi.norm.smul C
obtain ⟨c, hc, d, hd, hlt⟩ : ∃ c ∈ s, ∃ d ∈ s, (‖f c‖ + ∫ y in k, C * ‖g y‖) < ‖f d‖ :=
by
rcases Filter.nonempty_of_mem hsl with ⟨c, hc⟩
have : ∀ᶠ x in l, (‖f c‖ + ∫ y in k, C * ‖g y‖) < ‖f x‖ := hf.eventually (eventually_gt_atTop _)
exact ⟨c, hc, (this.and hsl).exists.imp fun d hd => ⟨hd.2, hd.1⟩⟩
specialize hsub c hc d hd; specialize hfd c hc d hd
replace hg : ∀ x ∈ Ι c d, ‖deriv f x‖ ≤ C * ‖g x‖ := fun z hz => hg c hc d hd z ⟨hz.1.le, hz.2⟩
have hg_ae : ∀ᵐ x ∂volume.restrict (Ι c d), ‖deriv f x‖ ≤ C * ‖g x‖ := (ae_restrict_mem measurableSet_uIoc).mono hg
have hsub' : Ι c d ⊆ k := Subset.trans Ioc_subset_Icc_self hsub
have hfi : IntervalIntegrable (deriv f) volume c d :=
by
rw [intervalIntegrable_iff]
have : IntegrableOn (fun x ↦ C * ‖g x‖) (Ι c d) := IntegrableOn.mono hgi hsub' le_rfl
exact Integrable.mono' this (aestronglyMeasurable_deriv _ _) hg_ae
refine hlt.not_ge (sub_le_iff_le_add'.1 ?_)
calc
‖f d‖ - ‖f c‖ ≤ ‖f d - f c‖ := norm_sub_norm_le _ _
_ = ‖∫ x in c..d, deriv f x‖ := (congr_arg _ (integral_deriv_eq_sub hfd hfi).symm)
_ = ‖∫ x in Ι c d, deriv f x‖ := (norm_integral_eq_norm_integral_uIoc _)
_ ≤ ∫ x in Ι c d, ‖deriv f x‖ := (norm_integral_le_integral_norm _)
_ ≤ ∫ x in Ι c d, C * ‖g x‖ := (setIntegral_mono_on hfi.norm.def' (hgi.mono_set hsub') measurableSet_uIoc hg)
_ ≤ ∫ x in k, C * ‖g x‖ := by
apply setIntegral_mono_set hgi (ae_of_all _ fun x => mul_nonneg hC₀ (norm_nonneg _)) hsub'.eventuallyLE
