awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
ι : Type u_2
b : ι → ℝ
⊢ Eq (α := (a : { x : ι → ℝ // ∀ (i : ι), x i ∈ Ioc (b i) (b i + 1) }) → UnitAddTorus ι)
    (⇑(measurableEquivPiIoc b).symm : (a : { x : ι → ℝ // ∀ (i : ι), x i ∈ Ioc (b i) (b i + 1) }) → UnitAddTorus ι)
    fun (x : { x : ι → ℝ // ∀ (i : ι), x i ∈ Ioc (b i) (b i + 1) }) (i : ι) ↦
    (↑((↑x : ι → ℝ) i) : ℝ ⧸ AddSubgroup.zmultiples 1)

Tactic:
rfl

Premises used: Pi.map, rfl
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
ι : Type u_2
b : ι → ℝ
y : { x : ι → ℝ // ∀ (i : ι), x i ∈ Ioc (b i) (b i + 1) }
⊢ Eq (α := UnitAddTorus ι)
    (((measurableEquivPiIoc b).symm : (a : { x : ι → ℝ // ∀ (i : ι), x i ∈ Ioc (b i) (b i + 1) }) → UnitAddTorus ι) y :
      UnitAddTorus ι)
    fun (i : ι) ↦
    ((↑((↑y : ι → ℝ) i) : HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples 1)) :
      HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples 1))

Tactic:
rfl

Premises used: Pi.map, rfl
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
a : d → ℝ
⊢ MeasurePreserving (α := UnitAddTorus d) (β := { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) })
    (⇑(measurableEquivPiIoc a) : (a_1 : UnitAddTorus d) → { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) }) volume
    (Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume)

Tactic:
(⟨(measurableEquivPiIoc a).symm.measurable, symm ?_⟩ :
    MeasurePreserving (measurableEquivPiIoc a).symm _ _).symm

Premises used: MeasureTheory.MeasurePreserving.symm, MeasureTheory.MeasurePreserving.mk, MeasurableEquiv.symm, UnitAddTorus.measurableEquivPiIoc, MeasurableEquiv.measurable, symm
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
a : d → ℝ
refine :
  Eq (α := Measure (UnitAddTorus d)) (volume : Measure (UnitAddTorus d))
    (Measure.map (α := { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) })
      (⇑(measurableEquivPiIoc a).symm : (a : { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) }) → UnitAddTorus d)
      (Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume))
⊢ MeasurePreserving (α := UnitAddTorus d) (β := { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) })
    (⇑(measurableEquivPiIoc a) : (a_1 : UnitAddTorus d) → { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) }) volume
    (Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume)

Tactic:
refine (⟨(measurableEquivPiIoc a).symm.measurable, symm ?_⟩ :
    MeasurePreserving (measurableEquivPiIoc a).symm _ _).symm

Premises used: MeasureTheory.MeasurePreserving.symm, MeasureTheory.MeasurePreserving.mk, MeasurableEquiv.symm, UnitAddTorus.measurableEquivPiIoc, MeasurableEquiv.measurable, symm
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
a : d → ℝ
⊢ Eq.{u_1 + 1} (α := Measure ((a : d) → HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples 1)))
    (Measure.map (fun (x : d → ℝ) (i : d) ↦ (↑(x i) : ℝ ⧸ AddSubgroup.zmultiples 1))
      (Measure.map (α := { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) })
        (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1)))
        (Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume)))
    (Measure.map (α := { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) })
      ((fun (x : d → ℝ) (i : d) ↦ (↑(x i) : ℝ ⧸ AddSubgroup.zmultiples 1)) ∘
        Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1)))
      (Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume))

Tactic:
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)})
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
a : d → ℝ
this :
  Eq.{u_1 + 1} (α := Measure ((a : d) → HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples 1)))
    (Measure.map (fun (x : d → ℝ) (i : d) ↦ (↑(x i) : ℝ ⧸ AddSubgroup.zmultiples 1))
      (Measure.map (α := { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) })
        (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1)))
        (Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume)))
    (Measure.map
      (fun (x : { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) }) (i : d) ↦
        (↑((↑x : d → ℝ) i) : ℝ ⧸ AddSubgroup.zmultiples 1))
      (Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume))
simp_rw :
  Eq.{u_1 + 1} (α := Measure (UnitAddTorus d)) (volume : Measure (UnitAddTorus d))
    (Measure.map (fun (x : d → ℝ) (i : d) ↦ (↑(x i) : ℝ ⧸ AddSubgroup.zmultiples 1))
      (Measure.map (α := { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) })
        (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1)))
        (Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume)))
⊢ Eq (α := Measure (UnitAddTorus d)) (volume : Measure (UnitAddTorus d))
    (Measure.map (α := { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) })
      (⇑(measurableEquivPiIoc a).symm : (a : { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) }) → UnitAddTorus d)
      (Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume))

Tactic:
simp_rw [coe_symm_measurableEquivPiIoc, ← this]

Premises used: UnitAddTorus.coe_symm_measurableEquivPiIoc
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
a : d → ℝ
this :
  Eq.{u_1 + 1} (α := Measure ((a : d) → HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples 1)))
    (Measure.map (fun (x : d → ℝ) (i : d) ↦ (↑(x i) : ℝ ⧸ AddSubgroup.zmultiples 1))
      (Measure.map (α := { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) })
        (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1)))
        (Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume)))
    (Measure.map
      (fun (x : { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) }) (i : d) ↦
        (↑((↑x : d → ℝ) i) : ℝ ⧸ AddSubgroup.zmultiples 1))
      (Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume))
⊢ Eq.{u_1 + 1} (α := Measure ((i : d) → HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples 1)))
    (Measure.pi (α := fun (i : d) ↦ HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples 1))
      fun (i : d) ↦ volume)
    (Measure.map (fun (a : (i : d) → ℝ) (i : d) ↦ (↑(a i) : ℝ ⧸ AddSubgroup.zmultiples 1))
      (Measure.pi (α := fun (i : d) ↦ ℝ) fun (i : d) ↦ Measure.restrict volume (Ioc (a i) (a i + 1))))

Tactic:
(measurePreserving_pi _ _ (fun i => AddCircle.measurePreserving_mk 1 (a i))).map_eq.symm

Premises used: MeasureTheory.measurePreserving_pi, MeasureTheory.MeasurePreserving.map_eq, AddCircle.measurePreserving_mk, OfNat.ofNat, Eq.symm
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
a : d → ℝ
this :
  Eq.{u_1 + 1} (α := Measure ((a : d) → HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples 1)))
    (Measure.map (fun (x : d → ℝ) (i : d) ↦ (↑(x i) : ℝ ⧸ AddSubgroup.zmultiples 1))
      (Measure.map (α := { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) })
        (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1)))
        (Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume)))
    (Measure.map
      (fun (x : { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) }) (i : d) ↦
        (↑((↑x : d → ℝ) i) : ℝ ⧸ AddSubgroup.zmultiples 1))
      (Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume))
h :
  Eq.{u_1 + 1} (α := Measure (UnitAddTorus d)) (volume : Measure (UnitAddTorus d))
    (Measure.pi (α := fun (i : d) ↦ HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples 1))
      fun (i : d) ↦ volume)
h₁ :
  Eq.{u_1 + 1} (α := Measure (d → ℝ))
    (Measure.map (α := { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) })
      (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1)))
      (Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume))
    (Measure.pi (α := fun (i : d) ↦ ℝ) fun (i : d) ↦ Measure.restrict volume (Ioc (a i) (a i + 1)))
⊢ Eq.{u_1 + 1} (α := Measure (UnitAddTorus d)) (volume : Measure (UnitAddTorus d))
    (Measure.map (fun (x : d → ℝ) (i : d) ↦ (↑(x i) : ℝ ⧸ AddSubgroup.zmultiples 1))
      (Measure.map (α := { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) })
        (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1)))
        (Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume)))

Tactic:
convert! (measurePreserving_pi _ _ (fun i => AddCircle.measurePreserving_mk 1 (a i))).map_eq.symm

Premises used: MeasureTheory.measurePreserving_pi, MeasureTheory.MeasurePreserving.map_eq, AddCircle.measurePreserving_mk, OfNat.ofNat, Eq.symm
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
a : d → ℝ
this :
  Eq.{u_1 + 1} (α := Measure ((a : d) → HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples 1)))
    (Measure.map (fun (x : d → ℝ) (i : d) ↦ (↑(x i) : ℝ ⧸ AddSubgroup.zmultiples 1))
      (Measure.map (α := { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) })
        (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1)))
        (Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume)))
    (Measure.map
      (fun (x : { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) }) (i : d) ↦
        (↑((↑x : d → ℝ) i) : ℝ ⧸ AddSubgroup.zmultiples 1))
      (Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume))
⊢ Eq.{u_1 + 1} (α := Measure (UnitAddTorus d)) (volume : Measure (UnitAddTorus d))
    (Measure.pi (α := fun (i : d) ↦ HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples 1))
      fun (i : d) ↦ volume)

Tactic:
simp [volume, AddCircle.haarAddCircle]

Premises used: MeasureTheory.MeasureSpace.volume, AddCircle.haarAddCircle
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
a : d → ℝ
this :
  Eq.{u_1 + 1} (α := Measure ((a : d) → HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples 1)))
    (Measure.map (fun (x : d → ℝ) (i : d) ↦ (↑(x i) : ℝ ⧸ AddSubgroup.zmultiples 1))
      (Measure.map (α := { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) })
        (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1)))
        (Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume)))
    (Measure.map
      (fun (x : { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) }) (i : d) ↦
        (↑((↑x : d → ℝ) i) : ℝ ⧸ AddSubgroup.zmultiples 1))
      (Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume))
⊢ Eq.{u_1 + 1} (α := Measure ((i : d) → ℝ))
    (Measure.map (α :=
        { x : (i : d) → ℝ //
          Membership.mem (γ := Set ((i : d) → ℝ)) {f : (i : d) → ℝ | ∀ (i : d), f i ∈ Ioc (a i) (a i + 1)} x })
        (Subtype.val (p := fun (x : (i : d) → ℝ) ↦
          Membership.mem (γ := Set ((i : d) → ℝ)) {f : (i : d) → ℝ | ∀ (i : d), f i ∈ Ioc (a i) (a i + 1)} x))
        (Measure.comap
          (Subtype.val (p := fun (x : (i : d) → ℝ) ↦
            Membership.mem (γ := Set ((i : d) → ℝ)) {f : (i : d) → ℝ | ∀ (i : d), f i ∈ Ioc (a i) (a i + 1)} x))
          (volume : Measure ((i : d) → ℝ))) :
      Measure ((i : d) → ℝ))
    (Measure.restrict volume {f : (i : d) → ℝ | ∀ (i : d), f i ∈ Ioc (a i) (a i + 1)} : Measure ((i : d) → ℝ))

Tactic:
(map_comap_subtype_coe (MeasurableSet.univ_pi' (fun i => measurableSet_Ioc (a := a i))) volume)

Premises used: MeasureTheory.MeasureSpace.volume, measurableSet_Ioc, map_comap_subtype_coe, MeasurableSet.univ_pi'
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
a : d → ℝ
this :
  Eq.{u_1 + 1} (α := Measure ((a : d) → HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples 1)))
    (Measure.map (fun (x : d → ℝ) (i : d) ↦ (↑(x i) : ℝ ⧸ AddSubgroup.zmultiples 1))
      (Measure.map (α := { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) })
        (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1)))
        (Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume)))
    (Measure.map
      (fun (x : { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) }) (i : d) ↦
        (↑((↑x : d → ℝ) i) : ℝ ⧸ AddSubgroup.zmultiples 1))
      (Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume))
h :
  Eq.{u_1 + 1} (α := Measure (d → ℝ))
    (Measure.pi (α := fun (i : d) ↦ ℝ) fun (i : d) ↦ Measure.restrict volume (Ioc (a i) (a i + 1)))
    (Measure.restrict volume {f : (i : d) → ℝ | ∀ (i : d), f i ∈ Ioc (a i) (a i + 1)})
⊢ Eq.{u_1 + 1} (α := Measure (d → ℝ))
    (Measure.map (α := { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) })
      (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1)))
      (Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume))
    (Measure.pi (α := fun (i : d) ↦ ℝ) fun (i : d) ↦ Measure.restrict volume (Ioc (a i) (a i + 1)))

Tactic:
convert!
    (map_comap_subtype_coe (MeasurableSet.univ_pi' (fun i => measurableSet_Ioc (a := a i))) volume)

Premises used: MeasureTheory.MeasureSpace.volume, measurableSet_Ioc, map_comap_subtype_coe, MeasurableSet.univ_pi'
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
a : d → ℝ
this :
  Eq.{u_1 + 1} (α := Measure ((a : d) → HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples 1)))
    (Measure.map (fun (x : d → ℝ) (i : d) ↦ (↑(x i) : ℝ ⧸ AddSubgroup.zmultiples 1))
      (Measure.map (α := { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) })
        (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1)))
        (Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume)))
    (Measure.map
      (fun (x : { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) }) (i : d) ↦
        (↑((↑x : d → ℝ) i) : ℝ ⧸ AddSubgroup.zmultiples 1))
      (Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume))
⊢ Eq.{u_1 + 1} (α := Measure ((i : d) → ℝ))
    (Measure.pi (α := fun (i : d) ↦ ℝ) fun (i : d) ↦ Measure.restrict volume (Ioc (a i) (a i + 1)))
    (Measure.restrict (Measure.pi (α := fun (i : d) ↦ ℝ) fun (i : d) ↦ volume)
      (Set.pi (α := fun (i : d) ↦ ℝ) univ fun (i : d) ↦ Ioc (a i) (a i + 1)))

Tactic:
(Measure.restrict_pi_pi (fun i => volume) (fun i => Ioc (a i) (a i + 1))).symm

Premises used: Set.Ioc, MeasureTheory.Measure.restrict_pi_pi, MeasureTheory.MeasureSpace.volume, HAdd.hAdd, OfNat.ofNat, Eq.symm
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
a : d → ℝ
this :
  Eq.{u_1 + 1} (α := Measure ((a : d) → HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples 1)))
    (Measure.map (fun (x : d → ℝ) (i : d) ↦ (↑(x i) : ℝ ⧸ AddSubgroup.zmultiples 1))
      (Measure.map (α := { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) })
        (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1)))
        (Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume)))
    (Measure.map
      (fun (x : { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) }) (i : d) ↦
        (↑((↑x : d → ℝ) i) : ℝ ⧸ AddSubgroup.zmultiples 1))
      (Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume))
h :
  Eq.{u_1 + 1} (α := Set ((i : d) → ℝ)) {f : (i : d) → ℝ | ∀ (i : d), f i ∈ Ioc (a i) (a i + 1)}
    (Set.pi (α := fun (i : d) ↦ ℝ) univ fun (i : d) ↦ Ioc (a i) (a i + 1))
⊢ Eq.{u_1 + 1} (α := Measure (d → ℝ))
    (Measure.pi (α := fun (i : d) ↦ ℝ) fun (i : d) ↦ Measure.restrict volume (Ioc (a i) (a i + 1)))
    (Measure.restrict volume {f : (i : d) → ℝ | ∀ (i : d), f i ∈ Ioc (a i) (a i + 1)})

Tactic:
convert! (Measure.restrict_pi_pi (fun i => volume) (fun i => Ioc (a i) (a i + 1))).symm

Premises used: Set.Ioc, MeasureTheory.Measure.restrict_pi_pi, MeasureTheory.MeasureSpace.volume, HAdd.hAdd, OfNat.ofNat, Eq.symm
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
a : d → ℝ
this :
  Eq.{u_1 + 1} (α := Measure ((a : d) → HasQuotient.Quotient ℝ (B := AddSubgroup ℝ) (AddSubgroup.zmultiples 1)))
    (Measure.map (fun (x : d → ℝ) (i : d) ↦ (↑(x i) : ℝ ⧸ AddSubgroup.zmultiples 1))
      (Measure.map (α := { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) })
        (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1)))
        (Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume)))
    (Measure.map
      (fun (x : { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) }) (i : d) ↦
        (↑((↑x : d → ℝ) i) : ℝ ⧸ AddSubgroup.zmultiples 1))
      (Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume))
⊢ Eq.{u_1 + 1} (α := Set ((i : d) → ℝ)) {f : (i : d) → ℝ | ∀ (i : d), f i ∈ Ioc (a i) (a i + 1)}
    (Set.pi (α := fun (i : d) ↦ ℝ) univ fun (i : d) ↦ Ioc (a i) (a i + 1))

Tactic:
grind
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
f : UnitAddTorus d → ℝ≥0∞
a : d → ℝ
⊢ ∫⁻ (a : UnitAddTorus d),
      f
        a ∂Measure.map (α := { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) })
        (⇑(measurableEquivPiIoc a).symm : (a : { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) }) → UnitAddTorus d)
        (Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume) =
    ∫⁻ (a_1 : { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) }),
      f
        (((measurableEquivPiIoc a).symm : (a : { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) }) → UnitAddTorus d)
          a_1) ∂Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume

Tactic:
lintegral_map_equiv (μ := volume.comap Subtype.val) f (measurableEquivPiIoc a).symm

Premises used: MeasurableEquiv.symm, UnitAddTorus.measurableEquivPiIoc, MeasureTheory.lintegral_map_equiv
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
f : UnitAddTorus d → ℝ≥0∞
a : d → ℝ
h :
  Eq.{u_1 + 1} (α := MeasurableSpace (UnitAddTorus d)) MeasureSpace.toMeasurableSpace
      (MeasurableSpace.pi (X := fun (a : d) ↦ UnitAddCircle)) →
    Eq (α := Measure (UnitAddTorus d)) volume
      (Measure.map (α := { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) })
        (⇑(measurableEquivPiIoc a).symm : (a : { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) }) → UnitAddTorus d)
        (Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume))
h₁ :
  (∫⁻ (x : d → ℝ) in {x : d → ℝ | ∀ (i : d), x i ∈ Ioc (a i) (a i + 1)},
      f fun (i : d) ↦ (↑(x i) : ℝ ⧸ AddSubgroup.zmultiples 1)) =
    ∫⁻ (a_1 : { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) }),
      f
        (((measurableEquivPiIoc a).symm : (a : { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) }) → UnitAddTorus d)
          a_1) ∂Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume
⊢ ∫⁻ (x : UnitAddTorus d), f x =
    ∫⁻ (x : d → ℝ) in {x : d → ℝ | ∀ (i : d), x i ∈ Ioc (a i) (a i + 1)},
      f fun (i : d) ↦ (↑(x i) : ℝ ⧸ AddSubgroup.zmultiples 1)

Tactic:
convert! lintegral_map_equiv (μ := volume.comap Subtype.val) f (measurableEquivPiIoc a).symm

Premises used: MeasurableEquiv.symm, UnitAddTorus.measurableEquivPiIoc, MeasureTheory.lintegral_map_equiv
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
f : UnitAddTorus d → ℝ≥0∞
a : d → ℝ
e_2 :
  Eq.{u_1 + 1} (α := MeasurableSpace (UnitAddTorus d)) MeasureSpace.toMeasurableSpace
    (MeasurableSpace.pi (X := fun (a : d) ↦ UnitAddCircle))
⊢ Eq (α := Measure (UnitAddTorus d)) volume
    (Measure.map (α := { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) })
      (⇑(measurableEquivPiIoc a).symm : (a : { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) }) → UnitAddTorus d)
      (Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume))

Tactic:
(measurePreserving_equivPiIoc a).symm.map_eq.symm

Premises used: MeasureTheory.MeasurePreserving.symm, UnitAddTorus.measurePreserving_equivPiIoc, MeasureTheory.MeasurePreserving.map_eq, Eq.symm
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
f : UnitAddTorus d → ℝ≥0∞
a : d → ℝ
e_2 :
  Eq.{u_1 + 1} (α := MeasurableSpace (UnitAddTorus d)) MeasureSpace.toMeasurableSpace
    (MeasurableSpace.pi (X := fun (a : d) ↦ UnitAddCircle))
⊢ Eq (α := Measure (UnitAddTorus d)) volume
    (Measure.map (α := { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) })
      (⇑(measurableEquivPiIoc a).symm : (a : { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) }) → UnitAddTorus d)
      (Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume))

Tactic:
exact (measurePreserving_equivPiIoc a).symm.map_eq.symm

Premises used: MeasureTheory.MeasurePreserving.symm, UnitAddTorus.measurePreserving_equivPiIoc, MeasureTheory.MeasurePreserving.map_eq, Eq.symm
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
f : UnitAddTorus d → ℝ≥0∞
a : d → ℝ
h :
  ∫⁻ (x : (↑{f : (i : d) → ℝ | ∀ (i : d), f i ∈ Ioc (a i) (a i + 1)} : Type u_1)),
      f fun (i : d) ↦
        (↑((↑x : (i : d) → ℝ) i) :
          ℝ ⧸
            AddSubgroup.zmultiples
              1) ∂Measure.comap
        (Subtype.val (p := fun (x : (i : d) → ℝ) ↦
          Membership.mem (γ := Set ((i : d) → ℝ)) {f : (i : d) → ℝ | ∀ (i : d), f i ∈ Ioc (a i) (a i + 1)} x))
        (volume : Measure (d → ℝ)) =
    ∫⁻ (a_1 : { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) }),
      f
        (((measurableEquivPiIoc a).symm : (a : { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) }) → UnitAddTorus d)
          a_1) ∂Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume
⊢ (∫⁻ (x : d → ℝ) in {x : d → ℝ | ∀ (i : d), x i ∈ Ioc (a i) (a i + 1)},
      f fun (i : d) ↦ (↑(x i) : ℝ ⧸ AddSubgroup.zmultiples 1)) =
    ∫⁻ (a_1 : { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) }),
      f
        (((measurableEquivPiIoc a).symm : (a : { x : d → ℝ // ∀ (i : d), x i ∈ Ioc (a i) (a i + 1) }) → UnitAddTorus d)
          a_1) ∂Measure.comap (Subtype.val (p := fun (x : d → ℝ) ↦ ∀ (i : d), x i ∈ Ioc (a i) (a i + 1))) volume

Tactic:
rw [← lintegral_subtype_comap (MeasurableSet.univ_pi' (fun i => measurableSet_Ioc))]

Premises used: MeasureTheory.lintegral_subtype_comap, measurableSet_Ioc, MeasurableSet.univ_pi'