Theorem: RealVectorFourier.fourierIntegral_l2inner_eq_fourierIntegral_euclidean (ForML/SchwartzFourier.lean)

State before:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝⁸ : Fintype ι
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : MeasurableSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : CompleteSpace F
f : (ι → ℝ) → F
ξ : ι → ℝ
⊢ 𝓕ₙ f ξ = 𝓕ᵥ (f ∘ ⇑(EuclideanSpace.equiv ι ℝ)) ξ
Tactic:
rw [VectorFourier.fourierIntegral]
State after:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝⁸ : Fintype ι
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : MeasurableSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : CompleteSpace F
f : (ι → ℝ) → F
ξ : ι → ℝ
⊢ ∫ (v : ι → ℝ), ↑(Real.fourierChar (Multiplicative.ofAdd (-((l2innerₛₗ ℝ) v) ξ))) • f v =
    𝓕ᵥ (f ∘ ⇑(EuclideanSpace.equiv ι ℝ)) ξ

State before:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝⁸ : Fintype ι
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : MeasurableSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : CompleteSpace F
f : (ι → ℝ) → F
ξ : ι → ℝ
⊢ ∫ (v : ι → ℝ), ↑(Real.fourierChar (Multiplicative.ofAdd (-((l2innerₛₗ ℝ) v) ξ))) • f v =
    𝓕ᵥ (f ∘ ⇑(EuclideanSpace.equiv ι ℝ)) ξ
Tactic:
rw [← MeasurePreserving.integral_comp' (EuclideanSpace.volume_preserving_measurableEquiv ι)]
State after:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝⁸ : Fintype ι
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : MeasurableSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : CompleteSpace F
f : (ι → ℝ) → F
ξ : ι → ℝ
⊢ ∫ (x : EuclideanSpace ℝ ι),
      ↑(Real.fourierChar (Multiplicative.ofAdd (-((l2innerₛₗ ℝ) ((EuclideanSpace.measurableEquiv ι) x)) ξ))) •
        f ((EuclideanSpace.measurableEquiv ι) x) ∂volume =
    𝓕ᵥ (f ∘ ⇑(EuclideanSpace.equiv ι ℝ)) ξ

State before:
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝⁸ : Fintype ι
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : InnerProductSpace ℝ E
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace ℂ F
inst✝³ : MeasurableSpace E
inst✝² : FiniteDimensional ℝ E
inst✝¹ : BorelSpace E
inst✝ : CompleteSpace F
f : (ι → ℝ) → F
ξ : ι → ℝ
⊢ ∫ (x : EuclideanSpace ℝ ι),
      ↑(Real.fourierChar (Multiplicative.ofAdd (-((l2innerₛₗ ℝ) ((EuclideanSpace.measurableEquiv ι) x)) ξ))) •
        f ((EuclideanSpace.measurableEquiv ι) x) ∂volume =
    𝓕ᵥ (f ∘ ⇑(EuclideanSpace.equiv ι ℝ)) ξ
Tactic:
rfl
State after:
no goals