Prove2Me

`BookProof.ChapterSolovayTailDimension.substrateInterval_measure` (n : ℕ) : unitMeasure (substrateInterval n) = ENNReal.ofReal (1 / ((n : ℝ) + 1) - 1 / ((n : ℝ) + 2))

Proved
BookProof.ChapterSolovayTailDimension.substrateInterval_measure

by leonardopedro · Oct 25, 2026 · Mathlib 0df444a (Lean v4.33.1)

theoremstimepiece

Prove the following Lean 4 theorem from ChapterSolovayTailDimension.

BookProof.ChapterSolovayTailDimension.substrateInterval_measure (n : ℕ) : unitMeasure (substrateInterval n) = ENNReal.ofReal (1 / ((n : ℝ) + 1) - 1 / ((n : ℝ) + 2))

Formalization note: Lean 4 identifier BookProof.ChapterSolovayTailDimension.substrateInterval_measure.

Preamble
-- Generated from ChapterSolovayTailDimension.lean — theorem BookProof.ChapterSolovayTailDimension.substrateInterval_measure
import Mathlib
import Definitions.Def_ChapterSolovayTailDimension
import Definitions.Def_PhysMeasureBasis
open PhysMeasureBasis
open BookProof.ChapterSolovayTailDimension


noncomputable section

open MeasureTheory Set PhysMehler PhysMeasureBasis
open scoped ENNReal
Formal statement
theorem BookProof.ChapterSolovayTailDimension.substrateInterval_measure (n : ℕ) :
    unitMeasure (substrateInterval n)
      = ENNReal.ofReal (1 / ((n : ℝ) + 1) - 1 / ((n : ℝ) + 2)) := by sorry

View graph