English
If f tends to a limit l at +∞, then μ_f(Ici x) = ∞ for all x.
Русский
Если f стремится к пределу l при +∞, то μ_f(Ici x) = ∞ для любого x.
LaTeX
$$μ_f(Ici x) = ∞$$
Lean4
theorem measure_Ici {l : ℝ} (hf : Tendsto f atTop (𝓝 l)) (x : ℝ) : f.measure (Ici x) = ofReal (l - leftLim f x) :=
by
refine tendsto_nhds_unique (tendsto_measure_Ico_atTop _ _) ?_
simp_rw [measure_Ico]
refine ENNReal.tendsto_ofReal (Tendsto.sub_const ?_ _)
have h_le1 : ∀ x, f (x - 1) ≤ leftLim f x := fun x => Monotone.le_leftLim f.mono (sub_one_lt x)
have h_le2 : ∀ x, leftLim f x ≤ f x := fun x => Monotone.leftLim_le f.mono le_rfl
refine tendsto_of_tendsto_of_tendsto_of_le_of_le (hf.comp ?_) hf h_le1 h_le2
rw [tendsto_atTop_atTop]
exact fun y => ⟨y + 1, fun z hyz => by rwa [le_sub_iff_add_le]⟩
