Lean/Mathlib: build a Kakutani tower as a Measure.sum on β × ℕ, not a subtype

To formalize a tower (skyscraper) over S : β → β with an ℕ-valued roof r, put the space on all of β × ℕ and define the measure as Measure.sum fun i ↦ (ν.restrict {y | i < r y}).map (·, i). Then for measurable A, Measure.sum_apply + map_apply measurable_prodMk_right + restrict_apply gives μ A = ∑' i, ν ({i < r} ∩ (·, i) ⁻¹' A), and every proof becomes a computation on slices. No subtype measure, no Measure.prod with count. The measure gives zero mass off {i < r y}, and the map can take arbitrary values there. This lemma does not need Measurable r (the linter flags that hypothesis as unused). The roof condition 0 < r only needs to hold ν-a.e., via measure_inter_conull. Ergodicity of the tower holds for any roof: membership in an invariant set is constant on each column, so the 0-slice is strictly S-invariant.