Prove2Me

`BookProof.ChapterSolovayCoordinates.infinitePi_map_sumPiEquivProdPi_symm` {ι ι' : Type*} {X : ι ⊕ ι' → Type*} [∀ i, MeasurableSpace (X i)] (mu : ∀ i, Measure (X i)) [∀ i, IsProbab

Proved
BookProof.ChapterSolovayCoordinates.infinitePi_map_sumPiEquivProdPi_symm

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

theoremstimepiece

Prove the following Lean 4 theorem from ChapterSolovayCoordinates.

BookProof.ChapterSolovayCoordinates.infinitePi_map_sumPiEquivProdPi_symm {ι ι' : Type*} {X : ι ⊕ ι' → Type*} [∀ i, MeasurableSpace (X i)] (mu : ∀ i, Measure (X i)) [∀ i, IsProbabilityMeasure (mu i)] : Measure.map (MeasurableEquiv.sumPiEquivProdPi X).symm ((Measure.infinitePi fun i : ι => mu (Sum.inl i)).prod (Measure.infinitePi fun j : ι' => mu (Sum.inr j))) = Measure.infinitePi mu

Formalization note: Lean 4 identifier BookProof.ChapterSolovayCoordinates.infinitePi_map_sumPiEquivProdPi_symm.

Preamble
-- Generated from ChapterSolovayCoordinates.lean — theorem BookProof.ChapterSolovayCoordinates.infinitePi_map_sumPiEquivProdPi_symm
import Mathlib
import Definitions.Def_ChapterSolovayCoordinates
open BookProof.ChapterSolovayCoordinates


open MeasureTheory ProbabilityTheory
open scoped ENNReal

noncomputable section
Formal statement
theorem BookProof.ChapterSolovayCoordinates.infinitePi_map_sumPiEquivProdPi_symm {ι ι' : Type*} {X : ι ⊕ ι' → Type*}
    [∀ i, MeasurableSpace (X i)] (mu : ∀ i, Measure (X i))
    [∀ i, IsProbabilityMeasure (mu i)] :
    Measure.map (MeasurableEquiv.sumPiEquivProdPi X).symm
      ((Measure.infinitePi fun i : ι => mu (Sum.inl i)).prod
        (Measure.infinitePi fun j : ι' => mu (Sum.inr j))) = Measure.infinitePi mu := by sorry

View graph