measure_Ioi_of_tendsto_atTop_atTop

English

If f tends to atBot at −∞, then μ_f(Iic x) = ∞ for all x.

Русский

Если f стремится к −∞ при −∞, то μ_f(Iic x) = ∞ для любого x.

LaTeX

$$μ_f(Iic(x)) = ∞$$

Lean4

theorem measure_Ioi_of_tendsto_atTop_atTop (hf : Tendsto f atTop atTop) (x : ℝ) : f.measure (Ioi x) = ∞ :=
  by
  refine ENNReal.eq_top_of_forall_nnreal_le fun r ↦ ?_
  obtain ⟨N, hN⟩ := eventually_atTop.mp (tendsto_atTop.mp hf (r + f x))
  exact
    (f.measure_Ioc x (max x N) ▸
          ENNReal.coe_nnreal_eq r ▸
            (ENNReal.ofReal_le_ofReal <| le_tsub_of_add_le_right <| hN _ (le_max_right x N))).trans
      (measure_mono Ioc_subset_Ioi_self)

Похожие утверждения