Theorem: RealVectorFourier.fourierIntegral_eq_fourierIntegral_euclidean_ofOrthonormalBasis (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
v : OrthonormalBasis ι ℝ E
f : E → F
ξ : E
⊢ 𝓕ᵥ f ξ = 𝓕ᵥ (f ∘ ⇑(LinearIsometryEquiv.symm v.repr)) (v.repr ξ)
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
v : OrthonormalBasis ι ℝ E
f : E → F
ξ : E
⊢ ∫ (v : E), ↑(Real.fourierChar (Multiplicative.ofAdd (-((innerₛₗ ℝ) v) ξ))) • f v =
    𝓕ᵥ (f ∘ ⇑(LinearIsometryEquiv.symm v.repr)) (v.repr ξ)

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
v : OrthonormalBasis ι ℝ E
f : E → F
ξ : E
⊢ ∫ (v : E), ↑(Real.fourierChar (Multiplicative.ofAdd (-((innerₛₗ ℝ) v) ξ))) • f v =
    𝓕ᵥ (f ∘ ⇑(LinearIsometryEquiv.symm v.repr)) (v.repr ξ)
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
v : OrthonormalBasis ι ℝ E
f : E → F
ξ : E
⊢ ∫ (v : E), ↑(Real.fourierChar (Multiplicative.ofAdd (-((innerₛₗ ℝ) v) ξ))) • f v =
    ∫ (v_1 : EuclideanSpace ℝ ι),
      ↑(Real.fourierChar (Multiplicative.ofAdd (-((innerₛₗ ℝ) v_1) (v.repr ξ)))) •
        (f ∘ ⇑(LinearIsometryEquiv.symm v.repr)) v_1

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
v : OrthonormalBasis ι ℝ E
f : E → F
ξ : E
⊢ ∫ (v : E), ↑(Real.fourierChar (Multiplicative.ofAdd (-((innerₛₗ ℝ) v) ξ))) • f v =
    ∫ (v_1 : EuclideanSpace ℝ ι),
      ↑(Real.fourierChar (Multiplicative.ofAdd (-((innerₛₗ ℝ) v_1) (v.repr ξ)))) •
        (f ∘ ⇑(LinearIsometryEquiv.symm v.repr)) v_1
Tactic:
rw [← MeasurePreserving.integral_comp' (v.measurePreserving_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
v : OrthonormalBasis ι ℝ E
f : E → F
ξ : E
⊢ ∫ (v : E), ↑(Real.fourierChar (Multiplicative.ofAdd (-((innerₛₗ ℝ) v) ξ))) • f v =
    ∫ (x : E),
      ↑(Real.fourierChar (Multiplicative.ofAdd (-((innerₛₗ ℝ) ((OrthonormalBasis.measurableEquiv v) x)) (v.repr ξ)))) •
        (f ∘ ⇑(LinearIsometryEquiv.symm v.repr)) ((OrthonormalBasis.measurableEquiv v) x)

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
v : OrthonormalBasis ι ℝ E
f : E → F
ξ : E
⊢ ∫ (v : E), ↑(Real.fourierChar (Multiplicative.ofAdd (-((innerₛₗ ℝ) v) ξ))) • f v =
    ∫ (x : E),
      ↑(Real.fourierChar (Multiplicative.ofAdd (-((innerₛₗ ℝ) ((OrthonormalBasis.measurableEquiv v) x)) (v.repr ξ)))) •
        (f ∘ ⇑(LinearIsometryEquiv.symm v.repr)) ((OrthonormalBasis.measurableEquiv v) x)
Tactic:
conv =>
  rhs; arg 2; intro x
  change Real.fourierChar[-innerₛₗ ℝ (v.repr x) (v.repr ξ)] • f (v.repr.symm (v.repr x))
  simp
State after:
no goals