volume_eq_stieltjes_id — Mathlib

English

The volume on the real line coincides with the Stieltjes measure coming from the identity function: volume = StieltjesFunction.id.measure.

Русский

Объем на вещественной прямой совпадает с Stieltjes-мерой, порождаемой тождественной функцией: volume = StieltjesFunction.id.measure.

LaTeX

$$$\text{volume} = \mathrm{StieltjesFunction.id.measure}$$$

Lean4

/-- The volume on the real line (as a particular case of the volume on a finite-dimensional
inner product space) coincides with the Stieltjes measure coming from the identity function. -/
theorem volume_eq_stieltjes_id : (volume : Measure ℝ) = StieltjesFunction.id.measure :=
  by
  haveI : IsAddLeftInvariant StieltjesFunction.id.measure :=
    ⟨fun a =>
      Eq.symm <|
        Real.measure_ext_Ioo_rat fun p q => by
          simp only [Measure.map_apply (measurable_const_add a) measurableSet_Ioo, sub_sub_sub_cancel_right,
            StieltjesFunction.measure_Ioo, StieltjesFunction.id_leftLim, StieltjesFunction.id_apply, id,
            preimage_const_add_Ioo]⟩
  have A : StieltjesFunction.id.measure (stdOrthonormalBasis ℝ ℝ).toBasis.parallelepiped = 1 :=
    by
    change StieltjesFunction.id.measure (parallelepiped (stdOrthonormalBasis ℝ ℝ)) = 1
    rcases parallelepiped_orthonormalBasis_one_dim (stdOrthonormalBasis ℝ ℝ) with (H | H) <;>
      simp only [H, StieltjesFunction.measure_Icc, StieltjesFunction.id_apply, id, tsub_zero,
        StieltjesFunction.id_leftLim, sub_neg_eq_add, zero_add, ENNReal.ofReal_one]
  conv_rhs =>
    rw [addHaarMeasure_unique StieltjesFunction.id.measure (stdOrthonormalBasis ℝ ℝ).toBasis.parallelepiped, A]
  simp only [volume, Module.Basis.addHaar, one_smul]

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