toSignedMeasure_toMeasureOfZeroLE

English

Let μ be a finite measure. The signed measure associated to μ, when converted back to a measure via the zero-bound construction on the whole space, equals μ.

Русский

Пусть μ — конечная мера. Связанная с μ сигнальная мера, приведённая обратно к мере с помощью конструктора нулевого порога на весь пространство, совпадает с μ.

LaTeX

$$$\mu = \left( \mu^{\mathrm{toSignedMeasure}} \right)^{\mathrm{toMeasureOfZeroLE}}(\mathrm{univ}, \mathrm{univ}, 0 \le \mu^{\mathrm{toSignedMeasure}}) $$$

Lean4

theorem toSignedMeasure_toMeasureOfZeroLE :
    μ.toSignedMeasure.toMeasureOfZeroLE Set.univ MeasurableSet.univ
        ((le_restrict_univ_iff_le _ _).2 (zero_le_toSignedMeasure μ)) =
      μ :=
  by
  refine Measure.ext fun i hi => ?_
  lift μ i to ℝ≥0 using (measure_lt_top _ _).ne with m hm
  rw [SignedMeasure.toMeasureOfZeroLE_apply _ _ _ hi, ENNReal.coe_inj]
  congr
  simp [hi, ← hm, measureReal_def]

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