exists_isFiniteMeasure_absolutelyContinuous

English

The definition sfiniteSeq μ is the (noncomputable) sequence of finite measures whose sum equals μ.

Русский

Определение sfiniteSeq μ — это последовательность конечных мер, сумма которых равна μ.

LaTeX

$$sfiniteSeq μ$$

Lean4

/-- For an s-finite measure `μ`, there exists a finite measure `ν`
such that each of `μ` and `ν` is absolutely continuous with respect to the other.
-/
theorem exists_isFiniteMeasure_absolutelyContinuous [SFinite μ] : ∃ ν : Measure α, IsFiniteMeasure ν ∧ μ ≪ ν ∧ ν ≪ μ :=
  by
  rcases ENNReal.exists_pos_tsum_mul_lt_of_countable top_ne_zero (sfiniteSeq μ · univ) fun _ ↦ measure_ne_top _ _ with
    ⟨c, hc₀, hc⟩
  have {s : Set α} : sum (fun n ↦ c n • sfiniteSeq μ n) s = 0 ↔ μ s = 0 :=
    by
    conv_rhs => rw [← sum_sfiniteSeq μ, sum_apply_of_countable]
    simp [(hc₀ _).ne']
  refine ⟨.sum fun n ↦ c n • sfiniteSeq μ n, ⟨?_⟩, fun _ ↦ this.1, fun _ ↦ this.2⟩
  simpa [mul_comm] using hc

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