awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
f : UnitAddTorus d → ℝ≥0∞
a : d → ℝ
⊢ ∫⁻ (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

Tactic:
rfl
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : UnitAddTorus d → E
a : d → ℝ
⊢ Eq.{u_3 + 1} (α := E)
    (@integral _ _ _ _ (MeasurableSpace.pi (X := fun (a : d) ↦ UnitAddCircle))
      (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))
      fun (y : UnitAddTorus d) ↦ f y)
    (@integral _ _ _ _ (Subtype.instMeasurableSpace (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)
      fun (x : { 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)
          x))

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

Premises used: MeasurableEquiv.symm, MeasureTheory.integral_map_equiv, UnitAddTorus.measurableEquivPiIoc
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : UnitAddTorus d → E
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₁ :
  Eq.{u_3 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (Measure.restrict volume {x : d → ℝ | ∀ (i : d), x i ∈ Ioc (a i) (a i + 1)}) fun (x : d → ℝ) ↦
      f fun (i : d) ↦ (↑(x i) : ℝ ⧸ AddSubgroup.zmultiples 1))
    (@integral _ _ _ _ (Subtype.instMeasurableSpace (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)
      fun (x : { 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)
          x))
⊢ Eq.{u_3 + 1} (α := E) (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : UnitAddTorus d) ↦ f x)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (Measure.restrict volume {x : d → ℝ | ∀ (i : d), x i ∈ Ioc (a i) (a i + 1)}) fun (x : d → ℝ) ↦
      f fun (i : d) ↦ (↑(x i) : ℝ ⧸ AddSubgroup.zmultiples 1))

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

Premises used: MeasurableEquiv.symm, MeasureTheory.integral_map_equiv, UnitAddTorus.measurableEquivPiIoc
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : UnitAddTorus d → E
a : d → ℝ
e_5 :
  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
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : UnitAddTorus d → E
a : d → ℝ
e_5 :
  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
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : UnitAddTorus d → E
a : d → ℝ
h :
  Eq.{u_3 + 1} (α := E)
    (@integral _ _ _ _
      (Subtype.instMeasurableSpace (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 (d → ℝ)))
      fun (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))
    (@integral _ _ _ _ (Subtype.instMeasurableSpace (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)
      fun (x : { 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)
          x))
⊢ Eq.{u_3 + 1} (α := E)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (Measure.restrict volume {x : d → ℝ | ∀ (i : d), x i ∈ Ioc (a i) (a i + 1)}) fun (x : d → ℝ) ↦
      f fun (i : d) ↦ (↑(x i) : ℝ ⧸ AddSubgroup.zmultiples 1))
    (@integral _ _ _ _ (Subtype.instMeasurableSpace (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)
      fun (x : { 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)
          x))

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

Premises used: MeasureTheory.integral_subtype_comap, measurableSet_Ioc, MeasurableSet.univ_pi'
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
E : Type u_3
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℝ E
f : UnitAddTorus d → E
a : d → ℝ
⊢ Eq.{u_3 + 1} (α := E)
    (@integral _ _ _ _
      (Subtype.instMeasurableSpace (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 (d → ℝ)))
      fun (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))
    (@integral _ _ _ _ (Subtype.instMeasurableSpace (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)
      fun (x : { 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)
          x))

Tactic:
rfl
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
p : ℝ≥0∞
inst_1 : Fact (1 ≤ p)
n : d → ℤ
⊢ (↑(↑(mFourierLp p n) : UnitAddTorus d →ₘ[volume] ℂ) :
      UnitAddTorus d → ℂ) =ᶠ[ae (F := Measure (UnitAddTorus d)) volume]
    (⇑(mFourier n) : (a : UnitAddTorus d) → ℂ)

Tactic:
ContinuousMap.coeFn_toLp volume (mFourier n)

Premises used: MeasureTheory.MeasureSpace.volume, UnitAddTorus.mFourier, ContinuousMap.coeFn_toLp
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
p : ℝ≥0∞
inst_1 : Fact (1 ≤ p)
hp : p ≠ ∞
⊢ Eq.{u_1 + 1} (α := Submodule ℂ ↥(Lp ℂ p volume)) (topologicalClosure (span ℂ (range (mFourierLp p)))) ⊤

Tactic:
simpa only [map_span, ContinuousLinearMap.coe_coe, ← range_comp, Function.comp_def] using
    (ContinuousMap.toLp_denseRange ℂ volume ℂ hp).topologicalClosure_map_submodule
      span_mFourier_closure_eq_top

Premises used: Set.range_comp, ContinuousMap.toLp_denseRange, DenseRange.topologicalClosure_map_submodule, ContinuousLinearMap.coe_coe, Function.comp_def, MeasureTheory.MeasureSpace.volume, UnitAddTorus.span_mFourier_closure_eq_top, Submodule.map_span, Complex
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
rw : ∀ (i j : d → ℤ), inner ℂ (E := ↥(Lp ℂ 2 volume)) (mFourierLp 2 i) (mFourierLp 2 j) = if i = j then 1 else 0
⊢ Orthonormal.{0, u_1, u_1} ℂ (E := ↥(Lp ℂ 2 volume)) (mFourierLp 2)

Tactic:
rw [orthonormal_iff_ite]

Premises used: orthonormal_iff_ite
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
m n : d → ℤ
simp :
  Eq (α := ℂ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : UnitAddTorus d) ↦
      (mFourier (n + -m) : (a : UnitAddTorus d) → ℂ) x)
    (if m = n then 1 else 0)
⊢ inner ℂ (E := ↥(Lp ℂ 2 volume)) (mFourierLp 2 m) (mFourierLp 2 n) = if m = n then 1 else 0

Tactic:
simp only [ContinuousMap.inner_toLp, ← mFourier_neg, ← mFourier_add]

Premises used: UnitAddTorus.mFourier_add, UnitAddTorus.mFourier_neg, MeasureTheory.ContinuousMap.inner_toLp
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
m n : d → ℤ
pos :
  ∀ (h : m = n),
    Eq (α := ℂ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : UnitAddTorus d) ↦
        (mFourier (n + -m) : (a : UnitAddTorus d) → ℂ) x)
      1
neg :
  ∀ (h : ¬m = n),
    Eq (α := ℂ)
      (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : UnitAddTorus d) ↦
        (mFourier (n + -m) : (a : UnitAddTorus d) → ℂ) x)
      0
⊢ Eq (α := ℂ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : UnitAddTorus d) ↦
      (mFourier (n + -m) : (a : UnitAddTorus d) → ℂ) x)
    (if m = n then 1 else 0)

Tactic:
split_ifs with h
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
m n : d → ℤ
h : m = n
⊢ Eq (α := ℂ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : UnitAddTorus d) ↦
      (mFourier (n + -m) : (a : UnitAddTorus d) → ℂ) x)
    1

Tactic:
simpa only [h, add_neg_cancel, mFourier_zero, probReal_univ, one_smul] using
      integral_const (α := UnitAddTorus d) (μ := volume) (1 : ℂ)

Premises used: add_neg_cancel, UnitAddTorus.mFourier_zero, one_smul, MeasureTheory.integral_const, MeasureTheory.probReal_univ, OfNat.ofNat
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
m n : d → ℤ
h : ¬m = n
neg :
  Eq (α := ℂ)
    (∏ i : d,
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : UnitAddCircle) ↦
        (fourier ((n + -m) i) : (a : AddCircle 1) → ℂ) x)
    0
⊢ Eq (α := ℂ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : UnitAddTorus d) ↦
      (mFourier (n + -m) : (a : UnitAddTorus d) → ℂ) x)
    0

Tactic:
rw [mFourier, ContinuousMap.coe_mk, MeasureTheory.integral_fintype_prod_volume_eq_prod]

Premises used: UnitAddTorus.mFourier, ContinuousMap.coe_mk, MeasureTheory.integral_fintype_prod_volume_eq_prod
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
m n : d → ℤ
h : ¬m = n
neg :
  ∀ (i : d) (hi : m i ≠ n i),
    Eq (α := ℂ)
      (∏ i : d,
        @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : UnitAddCircle) ↦
          (fourier ((n + -m) i) : (a : AddCircle 1) → ℂ) x)
      0
⊢ Eq (α := ℂ)
    (∏ i : d,
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : UnitAddCircle) ↦
        (fourier ((n + -m) i) : (a : AddCircle 1) → ℂ) x)
    0

Tactic:
obtain ⟨i, hi⟩ := Function.ne_iff.mp h

Premises used: Function.ne_iff, Iff.mp
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
m n : d → ℤ
h : ¬m = n
i : d
hi : m i ≠ n i
neg :
  Eq (α := ℂ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : UnitAddCircle) ↦
      (fourier ((n + -m) i) : (a : AddCircle 1) → ℂ) x)
    0
⊢ Eq (α := ℂ)
    (∏ i : d,
      @integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : UnitAddCircle) ↦
        (fourier ((n + -m) i) : (a : AddCircle 1) → ℂ) x)
    0

Tactic:
apply Finset.prod_eq_zero (Finset.mem_univ i)

Premises used: Finset.mem_univ, Finset.prod_eq_zero
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
m n : d → ℤ
h : ¬m = n
i : d
hi : m i ≠ n i
⊢ Eq (α := ℂ)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (x : UnitAddCircle) ↦
      (fourier ((n + -m) i) : (a : AddCircle 1) → ℂ) x)
    0

Tactic:
simpa only [eq_false_intro hi, if_false, ContinuousMap.inner_toLp, ← fourier_neg,
    ← fourier_add] using (orthonormal_iff_ite.mp <| orthonormal_fourier) (m i) (n i)

Premises used: orthonormal_fourier, if_false, fourier_neg, Iff.mp, orthonormal_iff_ite, fourier_add, MeasureTheory.ContinuousMap.inner_toLp, eq_false_intro
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
E : Type u_2
inst_1 : NormedAddCommGroup E
inst_2 : NormedSpace ℂ E
f : UnitAddTorus d → E
n : d → ℤ
a : d → ℝ
⊢ mFourierCoeff f n =
    @integral _ _ _ _ MeasureSpace.toMeasurableSpace
      (Measure.restrict volume {x : d → ℝ | ∀ (i : d), x i ∈ Ioc (a i) (a i + 1)}) fun (x : d → ℝ) ↦
      HSMul.hSMul (α := ℂ)
        ((mFourier (-n) : (a : UnitAddTorus d) → ℂ) fun (i : d) ↦ (↑(x i) : ℝ ⧸ AddSubgroup.zmultiples 1) : ℂ)
        (f fun (i : d) ↦ (↑(x i) : ℝ ⧸ AddSubgroup.zmultiples 1))

Tactic:
integral_preimage (fun x => (mFourier (-n)) x • f x) a

Premises used: UnitAddTorus.integral_preimage, UnitAddTorus.mFourierCoeff, UnitAddTorus.mFourier, HSMul.hSMul, DFunLike.coe, Neg.neg
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
⊢ Ne (α := ℝ≥0∞) 2 ∞

Tactic:
simp
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
⊢ Eq.{u_1 + 1} (α := (a : d → ℤ) → ↥(Lp ℂ 2 volume)) (⇑mFourierBasis : (a : d → ℤ) → ↥(Lp ℂ 2 volume)) (mFourierLp 2)

Tactic:
HilbertBasis.coe_mk _ _

Premises used: HilbertBasis.coe_mk, Set.Mem, setOf
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
f : ↥(Lp ℂ 2 volume)
i : d → ℤ
trans :
  Eq (α := (fun (x : d → ℤ) ↦ ℂ) i)
    ((↑((HilbertBasis.repr mFourierBasis : (a : ↥(Lp ℂ 2 volume)) → ↥(lp (fun (x : d → ℤ) ↦ ℂ) 2)) f) :
        (i : d → ℤ) → (fun (x : d → ℤ) ↦ ℂ) i)
      i)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (t : UnitAddTorus d) ↦
      HMul.hMul (α := ℂ)
        ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(↑(mFourierLp 2 i) : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) t) :
          ℂ)
        ((↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) t))
trans₁ :
  (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (t : UnitAddTorus d) ↦
      HMul.hMul (α := ℂ)
        ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(↑(mFourierLp 2 i) : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) t) :
          ℂ)
        ((↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) t)) =
    mFourierCoeff (↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) i
⊢ (↑((HilbertBasis.repr mFourierBasis : (a : ↥(Lp ℂ 2 volume)) → ↥(lp (fun (x : d → ℤ) ↦ ℂ) 2)) f) :
        (i : d → ℤ) → (fun (x : d → ℤ) ↦ ℂ) i)
      i =
    mFourierCoeff (↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) i

Tactic:
trans ∫ t, conj (mFourierLp 2 i t) * f t
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
f : ↥(Lp ℂ 2 volume)
i : d → ℤ
rw :
  Eq (α := (fun (x : d → ℤ) ↦ ℂ) i)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (a : UnitAddTorus d) ↦
      inner ℂ ((↑(↑(mFourierLp 2 i) : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) a)
        ((↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) a))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (t : UnitAddTorus d) ↦
      HMul.hMul (α := ℂ)
        ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(↑(mFourierLp 2 i) : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) t) :
          ℂ)
        ((↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) t))
⊢ Eq (α := (fun (x : d → ℤ) ↦ ℂ) i)
    ((↑((HilbertBasis.repr mFourierBasis : (a : ↥(Lp ℂ 2 volume)) → ↥(lp (fun (x : d → ℤ) ↦ ℂ) 2)) f) :
        (i : d → ℤ) → (fun (x : d → ℤ) ↦ ℂ) i)
      i)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (t : UnitAddTorus d) ↦
      HMul.hMul (α := ℂ)
        ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(↑(mFourierLp 2 i) : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) t) :
          ℂ)
        ((↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) t))

Tactic:
rw [mFourierBasis.repr_apply_apply f i, MeasureTheory.L2.inner_def, coe_mFourierBasis]

Premises used: UnitAddTorus.coe_mFourierBasis, MeasureTheory.L2.inner_def, UnitAddTorus.mFourierBasis, HilbertBasis.repr_apply_apply
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
f : ↥(Lp ℂ 2 volume)
i : d → ℤ
⊢ Eq (α := (fun (x : d → ℤ) ↦ ℂ) i)
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (a : UnitAddTorus d) ↦
      inner ℂ ((↑(↑(mFourierLp 2 i) : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) a)
        ((↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) a))
    (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (t : UnitAddTorus d) ↦
      HMul.hMul (α := ℂ)
        ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(↑(mFourierLp 2 i) : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) t) :
          ℂ)
        ((↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) t))

Tactic:
simp only [RCLike.inner_apply, mul_comm]

Premises used: RCLike.inner_apply, mul_comm
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
f : ↥(Lp ℂ 2 volume)
i : d → ℤ
h :
  (ae (F := Measure (UnitAddTorus d)) volume).EventuallyEq (β := (fun (x : d → ℤ) ↦ ℂ) i)
    (fun (a : UnitAddTorus d) ↦
      HMul.hMul (α := ℂ)
        ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(↑(mFourierLp 2 i) : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) a) :
          ℂ)
        ((↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) a))
    fun (a : UnitAddTorus d) ↦
    HSMul.hSMul (α := ℂ) ((mFourier (-i) : (a : UnitAddTorus d) → ℂ) a : ℂ)
      ((↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) a)
⊢ (@integral _ _ _ _ MeasureSpace.toMeasurableSpace volume fun (t : UnitAddTorus d) ↦
      HMul.hMul (α := ℂ)
        ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(↑(mFourierLp 2 i) : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) t) :
          ℂ)
        ((↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) t)) =
    mFourierCoeff (↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) i

Tactic:
apply integral_congr_ae

Premises used: MeasureTheory.integral_congr_ae
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
f : ↥(Lp ℂ 2 volume)
i : d → ℤ
h :
  ∀ (a : UnitAddTorus d)
    (ht :
      (↑(↑(mFourierLp 2 i) : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) a =
        (mFourier i : (a : UnitAddTorus d) → ℂ) a),
    HMul.hMul (α := ℂ)
        ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(↑(mFourierLp 2 i) : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) a) :
          ℂ)
        ((↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) a) =
      HSMul.hSMul (α := ℂ) ((mFourier (-i) : (a : UnitAddTorus d) → ℂ) a : ℂ)
        ((↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) a)
⊢ (ae (F := Measure (UnitAddTorus d)) volume).EventuallyEq (β := (fun (x : d → ℤ) ↦ ℂ) i)
    (fun (a : UnitAddTorus d) ↦
      HMul.hMul (α := ℂ)
        ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(↑(mFourierLp 2 i) : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) a) :
          ℂ)
        ((↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) a))
    fun (a : UnitAddTorus d) ↦
    HSMul.hSMul (α := ℂ) ((mFourier (-i) : (a : UnitAddTorus d) → ℂ) a : ℂ)
      ((↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) a)

Tactic:
filter_upwards [coeFn_mFourierLp 2 i] with _ ht

Premises used: UnitAddTorus.coeFn_mFourierLp, OfNat.ofNat
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
f : ↥(Lp ℂ 2 volume)
i : d → ℤ
a : UnitAddTorus d
ht :
  (↑(↑(mFourierLp 2 i) : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) a =
    (mFourier i : (a : UnitAddTorus d) → ℂ) a
h :
  HMul.hMul (α := ℂ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ((mFourier i : (a : UnitAddTorus d) → ℂ) a : ℂ) : ℂ)
      ((↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) a) =
    HSMul.hSMul (α := ℂ) ((mFourier (-i) : (a : UnitAddTorus d) → ℂ) a : ℂ)
      ((↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) a)
h₁ :
  HMul.hMul (α := ℂ) ((mFourier (-i) : (a : UnitAddTorus d) → ℂ) a : ℂ)
      ((↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) a) =
    HSMul.hSMul (α := ℂ) ((mFourier (-i) : (a : UnitAddTorus d) → ℂ) a : ℂ)
      ((↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) a)
h₂ h₃ :
  HMul.hMul (α := ℂ) ((mFourier (-i) : (a : UnitAddTorus d) → ℂ) a : ℂ)
      ((↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) a) =
    HMul.hMul (α := ℂ) ((mFourier (-i) : (a : UnitAddTorus d) → ℂ) a : ℂ)
      ((↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) a)
⊢ HMul.hMul (α := ℂ)
      ((starRingEnd ℂ : (a : ℂ) → ℂ) ((↑(↑(mFourierLp 2 i) : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) a) : ℂ)
      ((↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) a) =
    HSMul.hSMul (α := ℂ) ((mFourier (-i) : (a : UnitAddTorus d) → ℂ) a : ℂ)
      ((↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) a)

Tactic:
rw [ht, ← mFourier_neg, smul_eq_mul]

Premises used: UnitAddTorus.mFourier_neg, smul_eq_mul
-- Module: Mathlib.Analysis.Fourier.AddCircleMulti
Goal:
d : Type u_1
inst : Fintype d
f : ↥(Lp ℂ 2 volume)
⊢ HasSum
    (fun (i : d → ℤ) ↦
      HSMul.hSMul (β := ↥(Lp ℂ 2 volume)) (mFourierCoeff (↑(↑f : UnitAddTorus d →ₘ[volume] ℂ) : UnitAddTorus d → ℂ) i)
        (mFourierLp 2 i))
    f

Tactic:
simpa [← coe_mFourierBasis, mFourierBasis_repr] using mFourierBasis.hasSum_repr f

Premises used: UnitAddTorus.coe_mFourierBasis, HilbertBasis.hasSum_repr, UnitAddTorus.mFourierBasis, UnitAddTorus.mFourierBasis_repr