withDensity_coe — Mathlib

English

If f is continuous and nonnegative, then the measure μ with density f is locally finite.

Русский

Если f непрерывна и неотрицательна, тогда мера μ с плотностью f локально конечна.

LaTeX

$$$ \text{If } f \in C(\alpha,[0,\infty)),\; \mu^{f} \text{ is locally finite}$$$

Lean4

theorem withDensity_coe {f : α → ℝ≥0} (hf : Continuous f) : IsLocallyFiniteMeasure (μ.withDensity fun x ↦ f x) :=
  by
  refine ⟨fun x ↦ ?_⟩
  rcases
    (μ.finiteAt_nhds x).exists_mem_basis
      ((nhds_basis_opens' x).restrict_subset ((hf.tendsto x).eventually_le_const (lt_add_one _))) with
    ⟨U, ⟨⟨hUx, hUo⟩, hUf⟩, hμU⟩
  refine ⟨U, hUx, ?_⟩
  rw [withDensity_apply _ hUo.measurableSet]
  exact setLIntegral_lt_top_of_bddAbove hμU.ne ⟨f x + 1, forall_mem_image.2 hUf⟩

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