Theorem: RealVectorFourier.fourierIntegral_euclidean_eq_fourierIntegral_l2inner (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 : EuclideanSpace ℝ ι → F
ξ : EuclideanSpace ℝ ι
⊢ 𝓕ᵥ f ξ = 𝓕ₙ f ξ
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 : EuclideanSpace ℝ ι → F
ξ : EuclideanSpace ℝ ι
⊢ ∫ (v : EuclideanSpace ℝ ι), ↑(Real.fourierChar (Multiplicative.ofAdd (-((innerₛₗ ℝ) v) ξ))) • f v = 𝓕ₙ f ξ

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 : EuclideanSpace ℝ ι → F
ξ : EuclideanSpace ℝ ι
⊢ ∫ (v : EuclideanSpace ℝ ι), ↑(Real.fourierChar (Multiplicative.ofAdd (-((innerₛₗ ℝ) v) ξ))) • f v = 𝓕ₙ f ξ
Tactic:
rw [← MeasurePreserving.integral_comp' (EuclideanSpace.volume_preserving_measurableEquiv ι).symm]
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 : EuclideanSpace ℝ ι → F
ξ : EuclideanSpace ℝ ι
⊢ ∫ (x : ι → ℝ),
      ↑(Real.fourierChar (Multiplicative.ofAdd (-((innerₛₗ ℝ) ((EuclideanSpace.measurableEquiv ι).symm x)) ξ))) •
        f ((EuclideanSpace.measurableEquiv ι).symm x) ∂volume =
    𝓕ₙ f ξ

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 : EuclideanSpace ℝ ι → F
ξ : EuclideanSpace ℝ ι
⊢ ∫ (x : ι → ℝ),
      ↑(Real.fourierChar (Multiplicative.ofAdd (-((innerₛₗ ℝ) ((EuclideanSpace.measurableEquiv ι).symm x)) ξ))) •
        f ((EuclideanSpace.measurableEquiv ι).symm x) ∂volume =
    𝓕ₙ f ξ
Tactic:
rfl
State after:
no goals