Source indexedtheorem · leanprover/lean4:v4.32.0

MeasureTheory.map_coe_addCircle_volume_eq

Carleson.ToMathlib.MeasureTheory.Integral.Periodic · Carleson/ToMathlib/MeasureTheory/Integral/Periodic.lean:101 to 115

Mathematical statement

Exact Lean statement

theorem map_coe_addCircle_volume_eq :
    Measure.map (fun (x : ℝ) ↦ (x : AddCircle T)) volume =
      (⊤ : ℝ≥0∞) • (volume : Measure (AddCircle T))

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem map_coe_addCircle_volume_eq :    Measure.map (fun (x : ℝ) ↦ (x : AddCircle T)) volume =      (⊤ : ℝ≥0∞) • (volume : Measure (AddCircle T)) := by  have : (volume : Measure ℝ) =      Measure.sum (fun (n : ℤ) ↦ volume.restrict (Ioc (n • T) ((n + 1) • T))) := by    rw [← restrict_iUnion (Set.pairwise_disjoint_Ioc_zsmul T) (fun n ↦ measurableSet_Ioc),      iUnion_Ioc_zsmul hT.out, restrict_univ]  rw [this, Measure.map_sum (by fun_prop)]  have A (n : ℤ) : Measure.map (fun (x : ℝ) ↦ (x : AddCircle T))      (volume.restrict (Ioc (n • T) ((n + 1) • T)) ) = volume := by    simp only [zsmul_eq_mul, Int.cast_add, Int.cast_one, add_mul, one_mul]    exact (AddCircle.measurePreserving_mk T (n * T)).map_eq  simp only [A]  ext s hs  simp [hs]