Theorem: SchwartzMap.integral_vectorFourierIntegrand_pderivCLM_single_ofOrthonormalBasis (ForML/SchwartzFourier.lean)

State before:
E' : Type ?u.1423541
ι : 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✝²² : DecidableEq ι
inst✝²¹ : Fintype ι
inst✝²⁰ : NontriviallyNormedField 𝕜
inst✝¹⁹ : (i : ι) → NormedAddCommGroup (M i)
inst✝¹⁸ : (i : ι) → NormedSpace ℝ (M i)
inst✝¹⁷ : NormedAddCommGroup D
inst✝¹⁶ : NormedSpace ℝ D
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : InnerProductSpace ℝ E
inst✝¹³ : NormedAddCommGroup E'
inst✝¹² : InnerProductSpace ℝ E'
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℂ F
inst✝⁹ : NormedSpace 𝕜 F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
inst✝⁶ : MeasurableSpace E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : BorelSpace E
inst✝³ : MeasurableSpace E'
inst✝² : FiniteDimensional ℝ E'
inst✝¹ : BorelSpace E'
inst✝ : CompleteSpace F
v : OrthonormalBasis ι ℝ E
i : ι
f : 𝓢(E, F)
ξ : E
⊢ 𝓕ᵥ (⇑((pderivCLM ℝ ((LinearIsometryEquiv.symm v.repr) (Pi.single i 1))) f)) ξ =
    (2 * ↑π * I * ↑(v.repr ξ i)) • 𝓕ᵥ (⇑f) ξ
Tactic:
rw [RealVectorFourier.fourierIntegral_eq_fourierIntegral_euclidean_ofOrthonormalBasis v]
State after:
E' : Type ?u.1423541
ι : 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✝²² : DecidableEq ι
inst✝²¹ : Fintype ι
inst✝²⁰ : NontriviallyNormedField 𝕜
inst✝¹⁹ : (i : ι) → NormedAddCommGroup (M i)
inst✝¹⁸ : (i : ι) → NormedSpace ℝ (M i)
inst✝¹⁷ : NormedAddCommGroup D
inst✝¹⁶ : NormedSpace ℝ D
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : InnerProductSpace ℝ E
inst✝¹³ : NormedAddCommGroup E'
inst✝¹² : InnerProductSpace ℝ E'
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℂ F
inst✝⁹ : NormedSpace 𝕜 F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
inst✝⁶ : MeasurableSpace E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : BorelSpace E
inst✝³ : MeasurableSpace E'
inst✝² : FiniteDimensional ℝ E'
inst✝¹ : BorelSpace E'
inst✝ : CompleteSpace F
v : OrthonormalBasis ι ℝ E
i : ι
f : 𝓢(E, F)
ξ : E
⊢ 𝓕ᵥ (⇑((pderivCLM ℝ ((LinearIsometryEquiv.symm v.repr) (Pi.single i 1))) f) ∘ ⇑(LinearIsometryEquiv.symm v.repr))
      (v.repr ξ) =
    (2 * ↑π * I * ↑(v.repr ξ i)) • 𝓕ᵥ (⇑f) ξ

State before:
E' : Type ?u.1423541
ι : 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✝²² : DecidableEq ι
inst✝²¹ : Fintype ι
inst✝²⁰ : NontriviallyNormedField 𝕜
inst✝¹⁹ : (i : ι) → NormedAddCommGroup (M i)
inst✝¹⁸ : (i : ι) → NormedSpace ℝ (M i)
inst✝¹⁷ : NormedAddCommGroup D
inst✝¹⁶ : NormedSpace ℝ D
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : InnerProductSpace ℝ E
inst✝¹³ : NormedAddCommGroup E'
inst✝¹² : InnerProductSpace ℝ E'
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℂ F
inst✝⁹ : NormedSpace 𝕜 F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
inst✝⁶ : MeasurableSpace E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : BorelSpace E
inst✝³ : MeasurableSpace E'
inst✝² : FiniteDimensional ℝ E'
inst✝¹ : BorelSpace E'
inst✝ : CompleteSpace F
v : OrthonormalBasis ι ℝ E
i : ι
f : 𝓢(E, F)
ξ : E
⊢ 𝓕ᵥ (⇑((pderivCLM ℝ ((LinearIsometryEquiv.symm v.repr) (Pi.single i 1))) f) ∘ ⇑(LinearIsometryEquiv.symm v.repr))
      (v.repr ξ) =
    (2 * ↑π * I * ↑(v.repr ξ i)) • 𝓕ᵥ (⇑f) ξ
Tactic:
rw [RealVectorFourier.fourierIntegral_eq_fourierIntegral_euclidean_ofOrthonormalBasis v]
State after:
E' : Type ?u.1423541
ι : 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✝²² : DecidableEq ι
inst✝²¹ : Fintype ι
inst✝²⁰ : NontriviallyNormedField 𝕜
inst✝¹⁹ : (i : ι) → NormedAddCommGroup (M i)
inst✝¹⁸ : (i : ι) → NormedSpace ℝ (M i)
inst✝¹⁷ : NormedAddCommGroup D
inst✝¹⁶ : NormedSpace ℝ D
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : InnerProductSpace ℝ E
inst✝¹³ : NormedAddCommGroup E'
inst✝¹² : InnerProductSpace ℝ E'
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℂ F
inst✝⁹ : NormedSpace 𝕜 F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
inst✝⁶ : MeasurableSpace E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : BorelSpace E
inst✝³ : MeasurableSpace E'
inst✝² : FiniteDimensional ℝ E'
inst✝¹ : BorelSpace E'
inst✝ : CompleteSpace F
v : OrthonormalBasis ι ℝ E
i : ι
f : 𝓢(E, F)
ξ : E
⊢ 𝓕ᵥ (⇑((pderivCLM ℝ ((LinearIsometryEquiv.symm v.repr) (Pi.single i 1))) f) ∘ ⇑(LinearIsometryEquiv.symm v.repr))
      (v.repr ξ) =
    (2 * ↑π * I * ↑(v.repr ξ i)) • 𝓕ᵥ (⇑f ∘ ⇑(LinearIsometryEquiv.symm v.repr)) (v.repr ξ)

State before:
E' : Type ?u.1423541
ι : 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✝²² : DecidableEq ι
inst✝²¹ : Fintype ι
inst✝²⁰ : NontriviallyNormedField 𝕜
inst✝¹⁹ : (i : ι) → NormedAddCommGroup (M i)
inst✝¹⁸ : (i : ι) → NormedSpace ℝ (M i)
inst✝¹⁷ : NormedAddCommGroup D
inst✝¹⁶ : NormedSpace ℝ D
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : InnerProductSpace ℝ E
inst✝¹³ : NormedAddCommGroup E'
inst✝¹² : InnerProductSpace ℝ E'
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℂ F
inst✝⁹ : NormedSpace 𝕜 F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
inst✝⁶ : MeasurableSpace E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : BorelSpace E
inst✝³ : MeasurableSpace E'
inst✝² : FiniteDimensional ℝ E'
inst✝¹ : BorelSpace E'
inst✝ : CompleteSpace F
v : OrthonormalBasis ι ℝ E
i : ι
f : 𝓢(E, F)
ξ : E
⊢ 𝓕ᵥ (⇑((pderivCLM ℝ ((LinearIsometryEquiv.symm v.repr) (Pi.single i 1))) f) ∘ ⇑(LinearIsometryEquiv.symm v.repr))
      (v.repr ξ) =
    (2 * ↑π * I * ↑(v.repr ξ i)) • 𝓕ᵥ (⇑f ∘ ⇑(LinearIsometryEquiv.symm v.repr)) (v.repr ξ)
Tactic:
have := integral_vectorFourierIntegrand_pderivCLM_single_euclidean (i := i)
  (f := compEquiv v.repr.symm f) (ξ := v.repr ξ)
State after:
E' : Type ?u.1423541
ι : 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✝²² : DecidableEq ι
inst✝²¹ : Fintype ι
inst✝²⁰ : NontriviallyNormedField 𝕜
inst✝¹⁹ : (i : ι) → NormedAddCommGroup (M i)
inst✝¹⁸ : (i : ι) → NormedSpace ℝ (M i)
inst✝¹⁷ : NormedAddCommGroup D
inst✝¹⁶ : NormedSpace ℝ D
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : InnerProductSpace ℝ E
inst✝¹³ : NormedAddCommGroup E'
inst✝¹² : InnerProductSpace ℝ E'
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℂ F
inst✝⁹ : NormedSpace 𝕜 F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
inst✝⁶ : MeasurableSpace E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : BorelSpace E
inst✝³ : MeasurableSpace E'
inst✝² : FiniteDimensional ℝ E'
inst✝¹ : BorelSpace E'
inst✝ : CompleteSpace F
v : OrthonormalBasis ι ℝ E
i : ι
f : 𝓢(E, F)
ξ : E
this :
  𝓕ᵥ
      (⇑((pderivCLM ℝ (EuclideanSpace.single i 1))
          ((compEquiv (ContinuousLinearEquiv.mk (LinearIsometryEquiv.symm v.repr).toLinearEquiv)) f)))
      (v.repr ξ) =
    (2 * ↑π * I * ↑(v.repr ξ i)) •
      𝓕ᵥ (⇑((compEquiv (ContinuousLinearEquiv.mk (LinearIsometryEquiv.symm v.repr).toLinearEquiv)) f)) (v.repr ξ)
⊢ 𝓕ᵥ (⇑((pderivCLM ℝ ((LinearIsometryEquiv.symm v.repr) (Pi.single i 1))) f) ∘ ⇑(LinearIsometryEquiv.symm v.repr))
      (v.repr ξ) =
    (2 * ↑π * I * ↑(v.repr ξ i)) • 𝓕ᵥ (⇑f ∘ ⇑(LinearIsometryEquiv.symm v.repr)) (v.repr ξ)

State before:
E' : Type ?u.1423541
ι : 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✝²² : DecidableEq ι
inst✝²¹ : Fintype ι
inst✝²⁰ : NontriviallyNormedField 𝕜
inst✝¹⁹ : (i : ι) → NormedAddCommGroup (M i)
inst✝¹⁸ : (i : ι) → NormedSpace ℝ (M i)
inst✝¹⁷ : NormedAddCommGroup D
inst✝¹⁶ : NormedSpace ℝ D
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : InnerProductSpace ℝ E
inst✝¹³ : NormedAddCommGroup E'
inst✝¹² : InnerProductSpace ℝ E'
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℂ F
inst✝⁹ : NormedSpace 𝕜 F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
inst✝⁶ : MeasurableSpace E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : BorelSpace E
inst✝³ : MeasurableSpace E'
inst✝² : FiniteDimensional ℝ E'
inst✝¹ : BorelSpace E'
inst✝ : CompleteSpace F
v : OrthonormalBasis ι ℝ E
i : ι
f : 𝓢(E, F)
ξ : E
this :
  𝓕ᵥ
      (⇑((pderivCLM ℝ (EuclideanSpace.single i 1))
          ((compEquiv (ContinuousLinearEquiv.mk (LinearIsometryEquiv.symm v.repr).toLinearEquiv)) f)))
      (v.repr ξ) =
    (2 * ↑π * I * ↑(v.repr ξ i)) •
      𝓕ᵥ (⇑((compEquiv (ContinuousLinearEquiv.mk (LinearIsometryEquiv.symm v.repr).toLinearEquiv)) f)) (v.repr ξ)
⊢ 𝓕ᵥ (⇑((pderivCLM ℝ ((LinearIsometryEquiv.symm v.repr) (Pi.single i 1))) f) ∘ ⇑(LinearIsometryEquiv.symm v.repr))
      (v.repr ξ) =
    (2 * ↑π * I * ↑(v.repr ξ i)) • 𝓕ᵥ (⇑f ∘ ⇑(LinearIsometryEquiv.symm v.repr)) (v.repr ξ)
Tactic:
conv at this =>
  lhs; arg 4; intro x
  simp
  conv => arg 1; arg 2; intro y; simp
  change fderiv ℝ (f ∘ ⇑v.repr.toContinuousLinearEquiv.symm) x (EuclideanSpace.single i 1)
  rw [ContinuousLinearEquiv.comp_right_fderiv]
  simp
State after:
E' : Type ?u.1423541
ι : 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✝²² : DecidableEq ι
inst✝²¹ : Fintype ι
inst✝²⁰ : NontriviallyNormedField 𝕜
inst✝¹⁹ : (i : ι) → NormedAddCommGroup (M i)
inst✝¹⁸ : (i : ι) → NormedSpace ℝ (M i)
inst✝¹⁷ : NormedAddCommGroup D
inst✝¹⁶ : NormedSpace ℝ D
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : InnerProductSpace ℝ E
inst✝¹³ : NormedAddCommGroup E'
inst✝¹² : InnerProductSpace ℝ E'
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℂ F
inst✝⁹ : NormedSpace 𝕜 F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
inst✝⁶ : MeasurableSpace E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : BorelSpace E
inst✝³ : MeasurableSpace E'
inst✝² : FiniteDimensional ℝ E'
inst✝¹ : BorelSpace E'
inst✝ : CompleteSpace F
v : OrthonormalBasis ι ℝ E
i : ι
f : 𝓢(E, F)
ξ : E
this :
  𝓕ᵥ
      (fun x =>
        (fderiv ℝ (⇑f) ((ContinuousLinearEquiv.symm (LinearIsometryEquiv.toContinuousLinearEquiv v.repr)) x))
          ((ContinuousLinearEquiv.symm (LinearIsometryEquiv.toContinuousLinearEquiv v.repr))
            (EuclideanSpace.single i 1)))
      (v.repr ξ) =
    (2 * ↑π * I * ↑(v.repr ξ i)) •
      𝓕ᵥ (⇑((compEquiv (ContinuousLinearEquiv.mk (LinearIsometryEquiv.symm v.repr).toLinearEquiv)) f)) (v.repr ξ)
⊢ 𝓕ᵥ (⇑((pderivCLM ℝ ((LinearIsometryEquiv.symm v.repr) (Pi.single i 1))) f) ∘ ⇑(LinearIsometryEquiv.symm v.repr))
      (v.repr ξ) =
    (2 * ↑π * I * ↑(v.repr ξ i)) • 𝓕ᵥ (⇑f ∘ ⇑(LinearIsometryEquiv.symm v.repr)) (v.repr ξ)

State before:
E' : Type ?u.1423541
ι : 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✝²² : DecidableEq ι
inst✝²¹ : Fintype ι
inst✝²⁰ : NontriviallyNormedField 𝕜
inst✝¹⁹ : (i : ι) → NormedAddCommGroup (M i)
inst✝¹⁸ : (i : ι) → NormedSpace ℝ (M i)
inst✝¹⁷ : NormedAddCommGroup D
inst✝¹⁶ : NormedSpace ℝ D
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : InnerProductSpace ℝ E
inst✝¹³ : NormedAddCommGroup E'
inst✝¹² : InnerProductSpace ℝ E'
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℂ F
inst✝⁹ : NormedSpace 𝕜 F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
inst✝⁶ : MeasurableSpace E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : BorelSpace E
inst✝³ : MeasurableSpace E'
inst✝² : FiniteDimensional ℝ E'
inst✝¹ : BorelSpace E'
inst✝ : CompleteSpace F
v : OrthonormalBasis ι ℝ E
i : ι
f : 𝓢(E, F)
ξ : E
this :
  𝓕ᵥ
      (fun x =>
        (fderiv ℝ (⇑f) ((ContinuousLinearEquiv.symm (LinearIsometryEquiv.toContinuousLinearEquiv v.repr)) x))
          ((ContinuousLinearEquiv.symm (LinearIsometryEquiv.toContinuousLinearEquiv v.repr))
            (EuclideanSpace.single i 1)))
      (v.repr ξ) =
    (2 * ↑π * I * ↑(v.repr ξ i)) •
      𝓕ᵥ (⇑((compEquiv (ContinuousLinearEquiv.mk (LinearIsometryEquiv.symm v.repr).toLinearEquiv)) f)) (v.repr ξ)
⊢ 𝓕ᵥ (⇑((pderivCLM ℝ ((LinearIsometryEquiv.symm v.repr) (Pi.single i 1))) f) ∘ ⇑(LinearIsometryEquiv.symm v.repr))
      (v.repr ξ) =
    (2 * ↑π * I * ↑(v.repr ξ i)) • 𝓕ᵥ (⇑f ∘ ⇑(LinearIsometryEquiv.symm v.repr)) (v.repr ξ)
Tactic:
exact this
State after:
no goals