Update AddCircleMulti.lean

Author: CoolRmal

Mathlib/Analysis/Fourier/AddCircleMulti.lean

@@ -153,6 +153,28 @@ def measurableEquivPiIco : UnitAddTorus d ≃ᵐ {x : d → ℝ | ∀ i, x i ∈
   (MeasurableEquiv.piCongrRight fun i => AddCircle.measurableEquivIco 1 (a i)).trans <|
   MeasurableEquiv.subtypePiEquivPi.symm
 
+theorem lintegral_preimage (f : UnitAddTorus d → ℝ≥0∞) (a : d → ℝ) :
+    ∫⁻ x : UnitAddTorus d, f x =
+    ∫⁻ (x : d → ℝ) in {x : d → ℝ | ∀ i, x i ∈ Ioc (a i) (a i + 1)}, f (fun i => x i) := by
+  have m : MeasurableSet {x : d → ℝ | ∀ i, x i ∈ Ioc (a i) (a i + 1)} :=
+    (MeasurableSet.univ_pi (fun i : d => measurableSet_Ioc (a := a i) (b := a i + 1))).congr
+    (by grind)
+  have hl : (measurableEquivPiIoc a).symm = fun (x : {x : d → ℝ | ∀ i, x i ∈ Ioc (a i) (a i + 1)})
+    (i : d) => (x.1 i : UnitAddCircle) := rfl
+  convert lintegral_map_equiv (μ := volume.comap Subtype.val) f (measurableEquivPiIoc a).symm
+  · have := Measure.map_map (μ := volume.comap Subtype.val) (measurable_pi_lambda
+      (fun (x : d → ℝ) => (fun i => x i : UnitAddTorus d))
+      (fun i => AddCircle.measurable_mk'.comp (measurable_pi_apply i)))
+      measurable_subtype_coe (α := {x : d → ℝ | ∀ i, x i ∈ Ioc (a i) (a i + 1)})
+    simp only [coe_setOf, mem_setOf_eq, Function.comp_def] at this
+    simp_rw [hl, coe_setOf, mem_setOf_eq, ← this]
+    convert (measurePreserving_pi _ _ (fun i => AddCircle.measurePreserving_mk 1 (a i))).map_eq.symm
+    · simp [volume, AddCircle.haarAddCircle]
+    · convert (map_comap_subtype_coe m volume)
+      convert (Measure.restrict_pi_pi (fun i => volume) (fun i => Ioc (a i) (a i + 1))).symm
+      grind
+  · simp only [← coe_eq_subtype, hl, lintegral_subtype_comap m (f := fun x => f (fun i => x i))]
+
 variable {E : Type*} [NormedAddCommGroup E] [NormedSpace ℝ E]
 
 theorem integral_preimage (f : UnitAddTorus d → E) (a : d → ℝ) :