English
Let f: α → E be integrable along a filter l with respect to μ, and suppose μ(s) = ∞ for every s ∈ l. If f tends to a along l, then the limit must be 0; in particular a = 0.
Русский
Пусть f: α → E интегрируема вдоль фильтра l по мере μ, и для каждого множества s ∈ l мера μ(s) бесконечна. Если f стремится к пределу a вдоль l, то предел обязательно равен нулю; то есть a = 0.
LaTeX
$$$\\left( \\text{IntegrableAtFilter } f\\ l\\ μ \\right) \\wedge \\left( \\forall s \\in l,\\ μ s = \\infty \\right) \\wedge \\left( Tendsto\\ f\\ l\\ (\\mathcal{N} a) \\right) \\Rightarrow a = 0$$$
Lean4
/-- If a function converges along a filter to a limit `a`, is integrable along this filter, and
all elements of the filter have infinite measure, then the limit has to vanish. -/
theorem eq_zero_of_tendsto {f : α → E} (h : IntegrableAtFilter f l μ) (h' : ∀ s ∈ l, μ s = ∞) {a : E}
(hf : Tendsto f l (𝓝 a)) : a = 0 := by
by_contra H
obtain ⟨ε, εpos, hε⟩ : ∃ (ε : ℝ), 0 < ε ∧ ε < ‖a‖ := exists_between (norm_pos_iff.mpr H)
rcases h with ⟨u, ul, hu⟩
let v := u ∩ {b | ε < ‖f b‖}
have hv : IntegrableOn f v μ := hu.mono_set inter_subset_left
have vl : v ∈ l := inter_mem ul ((tendsto_order.1 hf.norm).1 _ hε)
have : μ.restrict v v < ∞ :=
lt_of_le_of_lt (measure_mono inter_subset_right) (Integrable.measure_gt_lt_top hv.norm εpos)
have : μ v ≠ ∞ := ne_of_lt (by simpa only [Measure.restrict_apply_self])
exact this (h' v vl)
