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

State before:
E' : Type ?u.310147
ι : 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
f : 𝓢(E, F)
ξ : E
⊢ (vectorFourierIntegrand ξ) f =
    (compEquiv
        (ContinuousLinearEquiv.trans (LinearIsometryEquiv.toContinuousLinearEquiv v.repr) (EuclideanSpace.equiv ι ℝ)))
      ((realVectorFourierIntegrand (v.repr ξ))
        ((compEquiv
            (ContinuousLinearEquiv.symm
              (ContinuousLinearEquiv.trans (LinearIsometryEquiv.toContinuousLinearEquiv v.repr)
                (EuclideanSpace.equiv ι ℝ))))
          f))
Tactic:
ext x
State after:
case h
E' : Type ?u.310147
ι : 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
f : 𝓢(E, F)
ξ x : E
⊢ ((vectorFourierIntegrand ξ) f) x =
    ((compEquiv
          (ContinuousLinearEquiv.trans (LinearIsometryEquiv.toContinuousLinearEquiv v.repr) (EuclideanSpace.equiv ι ℝ)))
        ((realVectorFourierIntegrand (v.repr ξ))
          ((compEquiv
              (ContinuousLinearEquiv.symm
                (ContinuousLinearEquiv.trans (LinearIsometryEquiv.toContinuousLinearEquiv v.repr)
                  (EuclideanSpace.equiv ι ℝ))))
            f)))
      x

State before:
case h
E' : Type ?u.310147
ι : 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
f : 𝓢(E, F)
ξ x : E
⊢ ((vectorFourierIntegrand ξ) f) x =
    ((compEquiv
          (ContinuousLinearEquiv.trans (LinearIsometryEquiv.toContinuousLinearEquiv v.repr) (EuclideanSpace.equiv ι ℝ)))
        ((realVectorFourierIntegrand (v.repr ξ))
          ((compEquiv
              (ContinuousLinearEquiv.symm
                (ContinuousLinearEquiv.trans (LinearIsometryEquiv.toContinuousLinearEquiv v.repr)
                  (EuclideanSpace.equiv ι ℝ))))
            f)))
      x
Tactic:
simp
State after:
case h
E' : Type ?u.310147
ι : 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
f : 𝓢(E, F)
ξ x : E
⊢ ((vectorFourierIntegrand ξ) f) x =
    ((realVectorFourierIntegrand (v.repr ξ))
        ((compEquiv
            (ContinuousLinearEquiv.symm
              (ContinuousLinearEquiv.trans (LinearIsometryEquiv.toContinuousLinearEquiv v.repr)
                (EuclideanSpace.equiv ι ℝ))))
          f))
      ((WithLp.equiv 2 (ι → ℝ)) (v.repr x))

State before:
case h
E' : Type ?u.310147
ι : 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
f : 𝓢(E, F)
ξ x : E
⊢ ((vectorFourierIntegrand ξ) f) x =
    ((realVectorFourierIntegrand (v.repr ξ))
        ((compEquiv
            (ContinuousLinearEquiv.symm
              (ContinuousLinearEquiv.trans (LinearIsometryEquiv.toContinuousLinearEquiv v.repr)
                (EuclideanSpace.equiv ι ℝ))))
          f))
      ((WithLp.equiv 2 (ι → ℝ)) (v.repr x))
Tactic:
rw [vectorFourierIntegrand_apply_realVectorFourierIntegrand_ofOrthonormalBasis v]
State after:
case h
E' : Type ?u.310147
ι : 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
f : 𝓢(E, F)
ξ x : E
⊢ ((realVectorFourierIntegrand (v.repr ξ))
        ((compEquiv
            (ContinuousLinearEquiv.symm
              (ContinuousLinearEquiv.trans (LinearIsometryEquiv.toContinuousLinearEquiv v.repr)
                (EuclideanSpace.equiv ι ℝ))))
          f))
      (v.repr x) =
    ((realVectorFourierIntegrand (v.repr ξ))
        ((compEquiv
            (ContinuousLinearEquiv.symm
              (ContinuousLinearEquiv.trans (LinearIsometryEquiv.toContinuousLinearEquiv v.repr)
                (EuclideanSpace.equiv ι ℝ))))
          f))
      ((WithLp.equiv 2 (ι → ℝ)) (v.repr x))

State before:
case h
E' : Type ?u.310147
ι : 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
f : 𝓢(E, F)
ξ x : E
⊢ ((realVectorFourierIntegrand (v.repr ξ))
        ((compEquiv
            (ContinuousLinearEquiv.symm
              (ContinuousLinearEquiv.trans (LinearIsometryEquiv.toContinuousLinearEquiv v.repr)
                (EuclideanSpace.equiv ι ℝ))))
          f))
      (v.repr x) =
    ((realVectorFourierIntegrand (v.repr ξ))
        ((compEquiv
            (ContinuousLinearEquiv.symm
              (ContinuousLinearEquiv.trans (LinearIsometryEquiv.toContinuousLinearEquiv v.repr)
                (EuclideanSpace.equiv ι ℝ))))
          f))
      ((WithLp.equiv 2 (ι → ℝ)) (v.repr x))
Tactic:
rfl
State after:
no goals