English
If f is real-valued, then μ.withDensity f is sigma-finite when μ is sigma-finite on a space.
Русский
Если f реально-valued, то μ.withDensity f — сигма-скончена при условии сигма-сконченности μ.
LaTeX
$$withDensity_ofReal$$
Lean4
/-- If `μ` is a σ-finite measure, then so is `μ.withDensity fun x ↦ f x`
for any `ℝ≥0`-valued function `f`. -/
protected instance withDensity [SigmaFinite μ] (f : α → ℝ≥0) : SigmaFinite (μ.withDensity (fun x ↦ f x)) :=
by
refine ⟨⟨⟨fun n ↦ spanningSets μ n ∩ f ⁻¹' (Iic n), fun _ ↦ trivial, fun n ↦ ?_, ?_⟩⟩⟩
· rw [withDensity_apply']
apply setLIntegral_lt_top_of_bddAbove
· exact ((measure_mono inter_subset_left).trans_lt (measure_spanningSets_lt_top μ n)).ne
· exact ⟨n, forall_mem_image.2 fun x hx ↦ hx.2⟩
· rw [iUnion_eq_univ_iff]
refine fun x ↦ ⟨max (spanningSetsIndex μ x) ⌈f x⌉₊, ?_, ?_⟩
· exact mem_spanningSets_of_index_le _ _ (le_max_left ..)
· simp [Nat.le_ceil]
