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

State before:
E' : Type ?u.1044983
ι : 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
f : 𝓢(E, F)
⊢ HasFTaylorSeriesUpTo ⊤ (fun ξ => ∫ (x : E), ((vectorFourierIntegrand ξ) f) x) fun ξ n =>
    (-(2 * ↑π * I)) ^ n •
      ∫ (x : E),
        ContinuousMultilinearMap.compContinuousLinearMap
          (ContinuousMultilinearMap.mkPiRing ℝ (Fin n) (((vectorFourierIntegrand ξ) f) x)) fun x_1 => (innerSL ℝ) x
Tactic:
rw [hasFTaylorSeriesUpTo_top_iff]
State after:
E' : Type ?u.1044983
ι : 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
f : 𝓢(E, F)
⊢ ∀ (n : ℕ),
    HasFTaylorSeriesUpTo (↑n) (fun ξ => ∫ (x : E), ((vectorFourierIntegrand ξ) f) x) fun ξ n =>
      (-(2 * ↑π * I)) ^ n •
        ∫ (x : E),
          ContinuousMultilinearMap.compContinuousLinearMap
            (ContinuousMultilinearMap.mkPiRing ℝ (Fin n) (((vectorFourierIntegrand ξ) f) x)) fun x_1 => (innerSL ℝ) x

State before:
E' : Type ?u.1044983
ι : 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
f : 𝓢(E, F)
⊢ ∀ (n : ℕ),
    HasFTaylorSeriesUpTo (↑n) (fun ξ => ∫ (x : E), ((vectorFourierIntegrand ξ) f) x) fun ξ n =>
      (-(2 * ↑π * I)) ^ n •
        ∫ (x : E),
          ContinuousMultilinearMap.compContinuousLinearMap
            (ContinuousMultilinearMap.mkPiRing ℝ (Fin n) (((vectorFourierIntegrand ξ) f) x)) fun x_1 => (innerSL ℝ) x
Tactic:
intro n
State after:
E' : Type ?u.1044983
ι : 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
f : 𝓢(E, F)
n : ℕ
⊢ HasFTaylorSeriesUpTo (↑n) (fun ξ => ∫ (x : E), ((vectorFourierIntegrand ξ) f) x) fun ξ n =>
    (-(2 * ↑π * I)) ^ n •
      ∫ (x : E),
        ContinuousMultilinearMap.compContinuousLinearMap
          (ContinuousMultilinearMap.mkPiRing ℝ (Fin n) (((vectorFourierIntegrand ξ) f) x)) fun x_1 => (innerSL ℝ) x

State before:
case zero
E' : Type ?u.1044983
ι : 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
f : 𝓢(E, F)
⊢ HasFTaylorSeriesUpTo (↑Nat.zero) (fun ξ => ∫ (x : E), ((vectorFourierIntegrand ξ) f) x) fun ξ n =>
    (-(2 * ↑π * I)) ^ n •
      ∫ (x : E),
        ContinuousMultilinearMap.compContinuousLinearMap
          (ContinuousMultilinearMap.mkPiRing ℝ (Fin n) (((vectorFourierIntegrand ξ) f) x)) fun x_1 => (innerSL ℝ) x
Tactic:
rw [ENat.coe_zero, hasFTaylorSeriesUpTo_zero_iff]
State after:
case zero
E' : Type ?u.1044983
ι : 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
f : 𝓢(E, F)
⊢ (Continuous fun ξ => ∫ (x : E), ((vectorFourierIntegrand ξ) f) x) ∧
    ∀ (x : E),
      ContinuousMultilinearMap.uncurry0
          ((-(2 * ↑π * I)) ^ 0 •
            ∫ (x_1 : E),
              ContinuousMultilinearMap.compContinuousLinearMap
                (ContinuousMultilinearMap.mkPiRing ℝ (Fin 0) (((vectorFourierIntegrand x) f) x_1)) fun x =>
                (innerSL ℝ) x_1) =
        ∫ (x_1 : E), ((vectorFourierIntegrand x) f) x_1

State before:
case zero
E' : Type ?u.1044983
ι : 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
f : 𝓢(E, F)
⊢ (Continuous fun ξ => ∫ (x : E), ((vectorFourierIntegrand ξ) f) x) ∧
    ∀ (x : E),
      ContinuousMultilinearMap.uncurry0
          ((-(2 * ↑π * I)) ^ 0 •
            ∫ (x_1 : E),
              ContinuousMultilinearMap.compContinuousLinearMap
                (ContinuousMultilinearMap.mkPiRing ℝ (Fin 0) (((vectorFourierIntegrand x) f) x_1)) fun x =>
                (innerSL ℝ) x_1) =
        ∫ (x_1 : E), ((vectorFourierIntegrand x) f) x_1
Tactic:
refine And.intro ?_ ?_
State after:
case zero.refine_1
E' : Type ?u.1044983
ι : 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
f : 𝓢(E, F)
⊢ Continuous fun ξ => ∫ (x : E), ((vectorFourierIntegrand ξ) f) x

case zero.refine_2
E' : Type ?u.1044983
ι : 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
f : 𝓢(E, F)
⊢ ∀ (x : E),
    ContinuousMultilinearMap.uncurry0
        ((-(2 * ↑π * I)) ^ 0 •
          ∫ (x_1 : E),
            ContinuousMultilinearMap.compContinuousLinearMap
              (ContinuousMultilinearMap.mkPiRing ℝ (Fin 0) (((vectorFourierIntegrand x) f) x_1)) fun x =>
              (innerSL ℝ) x_1) =
      ∫ (x_1 : E), ((vectorFourierIntegrand x) f) x_1

State before:
case zero.refine_1
E' : Type ?u.1044983
ι : 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
f : 𝓢(E, F)
⊢ Continuous fun ξ => ∫ (x : E), ((vectorFourierIntegrand ξ) f) x
Tactic:
exact continuous_integral_vectorFourierIntegrand
State after:
no goals

State before:
case zero.refine_2
E' : Type ?u.1044983
ι : 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
f : 𝓢(E, F)
⊢ ∀ (x : E),
    ContinuousMultilinearMap.uncurry0
        ((-(2 * ↑π * I)) ^ 0 •
          ∫ (x_1 : E),
            ContinuousMultilinearMap.compContinuousLinearMap
              (ContinuousMultilinearMap.mkPiRing ℝ (Fin 0) (((vectorFourierIntegrand x) f) x_1)) fun x =>
              (innerSL ℝ) x_1) =
      ∫ (x_1 : E), ((vectorFourierIntegrand x) f) x_1
Tactic:
intro ξ
State after:
case zero.refine_2
E' : Type ?u.1044983
ι : 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
f : 𝓢(E, F)
ξ : E
⊢ ContinuousMultilinearMap.uncurry0
      ((-(2 * ↑π * I)) ^ 0 •
        ∫ (x : E),
          ContinuousMultilinearMap.compContinuousLinearMap
            (ContinuousMultilinearMap.mkPiRing ℝ (Fin 0) (((vectorFourierIntegrand ξ) f) x)) fun x_1 => (innerSL ℝ) x) =
    ∫ (x : E), ((vectorFourierIntegrand ξ) f) x

State before:
case zero.refine_2
E' : Type ?u.1044983
ι : 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
f : 𝓢(E, F)
ξ : E
⊢ ContinuousMultilinearMap.uncurry0
      ((-(2 * ↑π * I)) ^ 0 •
        ∫ (x : E),
          ContinuousMultilinearMap.compContinuousLinearMap
            (ContinuousMultilinearMap.mkPiRing ℝ (Fin 0) (((vectorFourierIntegrand ξ) f) x)) fun x_1 => (innerSL ℝ) x) =
    ∫ (x : E), ((vectorFourierIntegrand ξ) f) x
Tactic:
simp
State after:
case zero.refine_2
E' : Type ?u.1044983
ι : 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
f : 𝓢(E, F)
ξ : E
⊢ (∫ (x : E),
        ContinuousMultilinearMap.compContinuousLinearMap
          (ContinuousMultilinearMap.mkPiRing ℝ (Fin 0) (((vectorFourierIntegrand ξ) f) x)) fun x_1 => (innerSL ℝ) x)
      0 =
    ∫ (x : E), ((vectorFourierIntegrand ξ) f) x

State before:
case zero.refine_2
E' : Type ?u.1044983
ι : 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
f : 𝓢(E, F)
ξ : E
⊢ (∫ (x : E),
        ContinuousMultilinearMap.compContinuousLinearMap
          (ContinuousMultilinearMap.mkPiRing ℝ (Fin 0) (((vectorFourierIntegrand ξ) f) x)) fun x_1 => (innerSL ℝ) x)
      0 =
    ∫ (x : E), ((vectorFourierIntegrand ξ) f) x
Tactic:
sorry
State after:
no goals

State before:
case succ
E' : Type ?u.1044983
ι : 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
f : 𝓢(E, F)
n : ℕ
IH :
  HasFTaylorSeriesUpTo (↑n) (fun ξ => ∫ (x : E), ((vectorFourierIntegrand ξ) f) x) fun ξ n =>
    (-(2 * ↑π * I)) ^ n •
      ∫ (x : E),
        ContinuousMultilinearMap.compContinuousLinearMap
          (ContinuousMultilinearMap.mkPiRing ℝ (Fin n) (((vectorFourierIntegrand ξ) f) x)) fun x_1 => (innerSL ℝ) x
⊢ HasFTaylorSeriesUpTo (↑(Nat.succ n)) (fun ξ => ∫ (x : E), ((vectorFourierIntegrand ξ) f) x) fun ξ n =>
    (-(2 * ↑π * I)) ^ n •
      ∫ (x : E),
        ContinuousMultilinearMap.compContinuousLinearMap
          (ContinuousMultilinearMap.mkPiRing ℝ (Fin n) (((vectorFourierIntegrand ξ) f) x)) fun x_1 => (innerSL ℝ) x
Tactic:
rw [← hasFTaylorSeriesUpToOn_univ_iff, Nat.cast_succ]
State after:
case succ
E' : Type ?u.1044983
ι : 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
f : 𝓢(E, F)
n : ℕ
IH :
  HasFTaylorSeriesUpTo (↑n) (fun ξ => ∫ (x : E), ((vectorFourierIntegrand ξ) f) x) fun ξ n =>
    (-(2 * ↑π * I)) ^ n •
      ∫ (x : E),
        ContinuousMultilinearMap.compContinuousLinearMap
          (ContinuousMultilinearMap.mkPiRing ℝ (Fin n) (((vectorFourierIntegrand ξ) f) x)) fun x_1 => (innerSL ℝ) x
⊢ HasFTaylorSeriesUpToOn (↑n + 1) (fun ξ => ∫ (x : E), ((vectorFourierIntegrand ξ) f) x)
    (fun ξ n =>
      (-(2 * ↑π * I)) ^ n •
        ∫ (x : E),
          ContinuousMultilinearMap.compContinuousLinearMap
            (ContinuousMultilinearMap.mkPiRing ℝ (Fin n) (((vectorFourierIntegrand ξ) f) x)) fun x_1 => (innerSL ℝ) x)
    Set.univ

State before:
case succ
E' : Type ?u.1044983
ι : 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
f : 𝓢(E, F)
n : ℕ
IH :
  HasFTaylorSeriesUpTo (↑n) (fun ξ => ∫ (x : E), ((vectorFourierIntegrand ξ) f) x) fun ξ n =>
    (-(2 * ↑π * I)) ^ n •
      ∫ (x : E),
        ContinuousMultilinearMap.compContinuousLinearMap
          (ContinuousMultilinearMap.mkPiRing ℝ (Fin n) (((vectorFourierIntegrand ξ) f) x)) fun x_1 => (innerSL ℝ) x
⊢ HasFTaylorSeriesUpToOn (↑n + 1) (fun ξ => ∫ (x : E), ((vectorFourierIntegrand ξ) f) x)
    (fun ξ n =>
      (-(2 * ↑π * I)) ^ n •
        ∫ (x : E),
          ContinuousMultilinearMap.compContinuousLinearMap
            (ContinuousMultilinearMap.mkPiRing ℝ (Fin n) (((vectorFourierIntegrand ξ) f) x)) fun x_1 => (innerSL ℝ) x)
    Set.univ
Tactic:
rw [hasFTaylorSeriesUpToOn_succ_iff_left]
State after:
case succ
E' : Type ?u.1044983
ι : 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
f : 𝓢(E, F)
n : ℕ
IH :
  HasFTaylorSeriesUpTo (↑n) (fun ξ => ∫ (x : E), ((vectorFourierIntegrand ξ) f) x) fun ξ n =>
    (-(2 * ↑π * I)) ^ n •
      ∫ (x : E),
        ContinuousMultilinearMap.compContinuousLinearMap
          (ContinuousMultilinearMap.mkPiRing ℝ (Fin n) (((vectorFourierIntegrand ξ) f) x)) fun x_1 => (innerSL ℝ) x
⊢ HasFTaylorSeriesUpToOn (↑n) (fun ξ => ∫ (x : E), ((vectorFourierIntegrand ξ) f) x)
      (fun ξ n =>
        (-(2 * ↑π * I)) ^ n •
          ∫ (x : E),
            ContinuousMultilinearMap.compContinuousLinearMap
              (ContinuousMultilinearMap.mkPiRing ℝ (Fin n) (((vectorFourierIntegrand ξ) f) x)) fun x_1 => (innerSL ℝ) x)
      Set.univ ∧
    (∀ x ∈ Set.univ,
        HasFDerivWithinAt
          (fun y =>
            (-(2 * ↑π * I)) ^ n •
              ∫ (x : E),
                ContinuousMultilinearMap.compContinuousLinearMap
                  (ContinuousMultilinearMap.mkPiRing ℝ (Fin n) (((vectorFourierIntegrand y) f) x)) fun x_1 =>
                  (innerSL ℝ) x)
          (ContinuousMultilinearMap.curryLeft
            ((-(2 * ↑π * I)) ^ Nat.succ n •
              ∫ (x_1 : E),
                ContinuousMultilinearMap.compContinuousLinearMap
                  (ContinuousMultilinearMap.mkPiRing ℝ (Fin (Nat.succ n)) (((vectorFourierIntegrand x) f) x_1)) fun x =>
                  (innerSL ℝ) x_1))
          Set.univ x) ∧
      ContinuousOn
        (fun x =>
          (-(2 * ↑π * I)) ^ (n + 1) •
            ∫ (x_1 : E),
              ContinuousMultilinearMap.compContinuousLinearMap
                (ContinuousMultilinearMap.mkPiRing ℝ (Fin (n + 1)) (((vectorFourierIntegrand x) f) x_1)) fun x =>
                (innerSL ℝ) x_1)
        Set.univ

State before:
case succ
E' : Type ?u.1044983
ι : 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
f : 𝓢(E, F)
n : ℕ
IH :
  HasFTaylorSeriesUpTo (↑n) (fun ξ => ∫ (x : E), ((vectorFourierIntegrand ξ) f) x) fun ξ n =>
    (-(2 * ↑π * I)) ^ n •
      ∫ (x : E),
        ContinuousMultilinearMap.compContinuousLinearMap
          (ContinuousMultilinearMap.mkPiRing ℝ (Fin n) (((vectorFourierIntegrand ξ) f) x)) fun x_1 => (innerSL ℝ) x
⊢ HasFTaylorSeriesUpToOn (↑n) (fun ξ => ∫ (x : E), ((vectorFourierIntegrand ξ) f) x)
      (fun ξ n =>
        (-(2 * ↑π * I)) ^ n •
          ∫ (x : E),
            ContinuousMultilinearMap.compContinuousLinearMap
              (ContinuousMultilinearMap.mkPiRing ℝ (Fin n) (((vectorFourierIntegrand ξ) f) x)) fun x_1 => (innerSL ℝ) x)
      Set.univ ∧
    (∀ x ∈ Set.univ,
        HasFDerivWithinAt
          (fun y =>
            (-(2 * ↑π * I)) ^ n •
              ∫ (x : E),
                ContinuousMultilinearMap.compContinuousLinearMap
                  (ContinuousMultilinearMap.mkPiRing ℝ (Fin n) (((vectorFourierIntegrand y) f) x)) fun x_1 =>
                  (innerSL ℝ) x)
          (ContinuousMultilinearMap.curryLeft
            ((-(2 * ↑π * I)) ^ Nat.succ n •
              ∫ (x_1 : E),
                ContinuousMultilinearMap.compContinuousLinearMap
                  (ContinuousMultilinearMap.mkPiRing ℝ (Fin (Nat.succ n)) (((vectorFourierIntegrand x) f) x_1)) fun x =>
                  (innerSL ℝ) x_1))
          Set.univ x) ∧
      ContinuousOn
        (fun x =>
          (-(2 * ↑π * I)) ^ (n + 1) •
            ∫ (x_1 : E),
              ContinuousMultilinearMap.compContinuousLinearMap
                (ContinuousMultilinearMap.mkPiRing ℝ (Fin (n + 1)) (((vectorFourierIntegrand x) f) x_1)) fun x =>
                (innerSL ℝ) x_1)
        Set.univ
Tactic:
refine And.intro ?_ ?_
State after:
case succ.refine_1
E' : Type ?u.1044983
ι : 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
f : 𝓢(E, F)
n : ℕ
IH :
  HasFTaylorSeriesUpTo (↑n) (fun ξ => ∫ (x : E), ((vectorFourierIntegrand ξ) f) x) fun ξ n =>
    (-(2 * ↑π * I)) ^ n •
      ∫ (x : E),
        ContinuousMultilinearMap.compContinuousLinearMap
          (ContinuousMultilinearMap.mkPiRing ℝ (Fin n) (((vectorFourierIntegrand ξ) f) x)) fun x_1 => (innerSL ℝ) x
⊢ HasFTaylorSeriesUpToOn (↑n) (fun ξ => ∫ (x : E), ((vectorFourierIntegrand ξ) f) x)
    (fun ξ n =>
      (-(2 * ↑π * I)) ^ n •
        ∫ (x : E),
          ContinuousMultilinearMap.compContinuousLinearMap
            (ContinuousMultilinearMap.mkPiRing ℝ (Fin n) (((vectorFourierIntegrand ξ) f) x)) fun x_1 => (innerSL ℝ) x)
    Set.univ

case succ.refine_2
E' : Type ?u.1044983
ι : 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
f : 𝓢(E, F)
n : ℕ
IH :
  HasFTaylorSeriesUpTo (↑n) (fun ξ => ∫ (x : E), ((vectorFourierIntegrand ξ) f) x) fun ξ n =>
    (-(2 * ↑π * I)) ^ n •
      ∫ (x : E),
        ContinuousMultilinearMap.compContinuousLinearMap
          (ContinuousMultilinearMap.mkPiRing ℝ (Fin n) (((vectorFourierIntegrand ξ) f) x)) fun x_1 => (innerSL ℝ) x
⊢ (∀ x ∈ Set.univ,
      HasFDerivWithinAt
        (fun y =>
          (-(2 * ↑π * I)) ^ n •
            ∫ (x : E),
              ContinuousMultilinearMap.compContinuousLinearMap
                (ContinuousMultilinearMap.mkPiRing ℝ (Fin n) (((vectorFourierIntegrand y) f) x)) fun x_1 =>
                (innerSL ℝ) x)
        (ContinuousMultilinearMap.curryLeft
          ((-(2 * ↑π * I)) ^ Nat.succ n •
            ∫ (x_1 : E),
              ContinuousMultilinearMap.compContinuousLinearMap
                (ContinuousMultilinearMap.mkPiRing ℝ (Fin (Nat.succ n)) (((vectorFourierIntegrand x) f) x_1)) fun x =>
                (innerSL ℝ) x_1))
        Set.univ x) ∧
    ContinuousOn
      (fun x =>
        (-(2 * ↑π * I)) ^ (n + 1) •
          ∫ (x_1 : E),
            ContinuousMultilinearMap.compContinuousLinearMap
              (ContinuousMultilinearMap.mkPiRing ℝ (Fin (n + 1)) (((vectorFourierIntegrand x) f) x_1)) fun x =>
              (innerSL ℝ) x_1)
      Set.univ

State before:
case succ.refine_1
E' : Type ?u.1044983
ι : 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
f : 𝓢(E, F)
n : ℕ
IH :
  HasFTaylorSeriesUpTo (↑n) (fun ξ => ∫ (x : E), ((vectorFourierIntegrand ξ) f) x) fun ξ n =>
    (-(2 * ↑π * I)) ^ n •
      ∫ (x : E),
        ContinuousMultilinearMap.compContinuousLinearMap
          (ContinuousMultilinearMap.mkPiRing ℝ (Fin n) (((vectorFourierIntegrand ξ) f) x)) fun x_1 => (innerSL ℝ) x
⊢ HasFTaylorSeriesUpToOn (↑n) (fun ξ => ∫ (x : E), ((vectorFourierIntegrand ξ) f) x)
    (fun ξ n =>
      (-(2 * ↑π * I)) ^ n •
        ∫ (x : E),
          ContinuousMultilinearMap.compContinuousLinearMap
            (ContinuousMultilinearMap.mkPiRing ℝ (Fin n) (((vectorFourierIntegrand ξ) f) x)) fun x_1 => (innerSL ℝ) x)
    Set.univ
Tactic:
rw [hasFTaylorSeriesUpToOn_univ_iff]
State after:
case succ.refine_1
E' : Type ?u.1044983
ι : 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
f : 𝓢(E, F)
n : ℕ
IH :
  HasFTaylorSeriesUpTo (↑n) (fun ξ => ∫ (x : E), ((vectorFourierIntegrand ξ) f) x) fun ξ n =>
    (-(2 * ↑π * I)) ^ n •
      ∫ (x : E),
        ContinuousMultilinearMap.compContinuousLinearMap
          (ContinuousMultilinearMap.mkPiRing ℝ (Fin n) (((vectorFourierIntegrand ξ) f) x)) fun x_1 => (innerSL ℝ) x
⊢ HasFTaylorSeriesUpTo (↑n) (fun ξ => ∫ (x : E), ((vectorFourierIntegrand ξ) f) x) fun ξ n =>
    (-(2 * ↑π * I)) ^ n •
      ∫ (x : E),
        ContinuousMultilinearMap.compContinuousLinearMap
          (ContinuousMultilinearMap.mkPiRing ℝ (Fin n) (((vectorFourierIntegrand ξ) f) x)) fun x_1 => (innerSL ℝ) x

State before:
case succ.refine_1
E' : Type ?u.1044983
ι : 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
f : 𝓢(E, F)
n : ℕ
IH :
  HasFTaylorSeriesUpTo (↑n) (fun ξ => ∫ (x : E), ((vectorFourierIntegrand ξ) f) x) fun ξ n =>
    (-(2 * ↑π * I)) ^ n •
      ∫ (x : E),
        ContinuousMultilinearMap.compContinuousLinearMap
          (ContinuousMultilinearMap.mkPiRing ℝ (Fin n) (((vectorFourierIntegrand ξ) f) x)) fun x_1 => (innerSL ℝ) x
⊢ HasFTaylorSeriesUpTo (↑n) (fun ξ => ∫ (x : E), ((vectorFourierIntegrand ξ) f) x) fun ξ n =>
    (-(2 * ↑π * I)) ^ n •
      ∫ (x : E),
        ContinuousMultilinearMap.compContinuousLinearMap
          (ContinuousMultilinearMap.mkPiRing ℝ (Fin n) (((vectorFourierIntegrand ξ) f) x)) fun x_1 => (innerSL ℝ) x
Tactic:
exact IH
State after:
no goals

State before:
case succ.refine_2
E' : Type ?u.1044983
ι : 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
f : 𝓢(E, F)
n : ℕ
IH :
  HasFTaylorSeriesUpTo (↑n) (fun ξ => ∫ (x : E), ((vectorFourierIntegrand ξ) f) x) fun ξ n =>
    (-(2 * ↑π * I)) ^ n •
      ∫ (x : E),
        ContinuousMultilinearMap.compContinuousLinearMap
          (ContinuousMultilinearMap.mkPiRing ℝ (Fin n) (((vectorFourierIntegrand ξ) f) x)) fun x_1 => (innerSL ℝ) x
⊢ (∀ x ∈ Set.univ,
      HasFDerivWithinAt
        (fun y =>
          (-(2 * ↑π * I)) ^ n •
            ∫ (x : E),
              ContinuousMultilinearMap.compContinuousLinearMap
                (ContinuousMultilinearMap.mkPiRing ℝ (Fin n) (((vectorFourierIntegrand y) f) x)) fun x_1 =>
                (innerSL ℝ) x)
        (ContinuousMultilinearMap.curryLeft
          ((-(2 * ↑π * I)) ^ Nat.succ n •
            ∫ (x_1 : E),
              ContinuousMultilinearMap.compContinuousLinearMap
                (ContinuousMultilinearMap.mkPiRing ℝ (Fin (Nat.succ n)) (((vectorFourierIntegrand x) f) x_1)) fun x =>
                (innerSL ℝ) x_1))
        Set.univ x) ∧
    ContinuousOn
      (fun x =>
        (-(2 * ↑π * I)) ^ (n + 1) •
          ∫ (x_1 : E),
            ContinuousMultilinearMap.compContinuousLinearMap
              (ContinuousMultilinearMap.mkPiRing ℝ (Fin (n + 1)) (((vectorFourierIntegrand x) f) x_1)) fun x =>
              (innerSL ℝ) x_1)
      Set.univ
Tactic:
refine And.intro ?_ ?_
State after:
case succ.refine_2.refine_1
E' : Type ?u.1044983
ι : 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
f : 𝓢(E, F)
n : ℕ
IH :
  HasFTaylorSeriesUpTo (↑n) (fun ξ => ∫ (x : E), ((vectorFourierIntegrand ξ) f) x) fun ξ n =>
    (-(2 * ↑π * I)) ^ n •
      ∫ (x : E),
        ContinuousMultilinearMap.compContinuousLinearMap
          (ContinuousMultilinearMap.mkPiRing ℝ (Fin n) (((vectorFourierIntegrand ξ) f) x)) fun x_1 => (innerSL ℝ) x
⊢ ∀ x ∈ Set.univ,
    HasFDerivWithinAt
      (fun y =>
        (-(2 * ↑π * I)) ^ n •
          ∫ (x : E),
            ContinuousMultilinearMap.compContinuousLinearMap
              (ContinuousMultilinearMap.mkPiRing ℝ (Fin n) (((vectorFourierIntegrand y) f) x)) fun x_1 => (innerSL ℝ) x)
      (ContinuousMultilinearMap.curryLeft
        ((-(2 * ↑π * I)) ^ Nat.succ n •
          ∫ (x_1 : E),
            ContinuousMultilinearMap.compContinuousLinearMap
              (ContinuousMultilinearMap.mkPiRing ℝ (Fin (Nat.succ n)) (((vectorFourierIntegrand x) f) x_1)) fun x =>
              (innerSL ℝ) x_1))
      Set.univ x

case succ.refine_2.refine_2
E' : Type ?u.1044983
ι : 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
f : 𝓢(E, F)
n : ℕ
IH :
  HasFTaylorSeriesUpTo (↑n) (fun ξ => ∫ (x : E), ((vectorFourierIntegrand ξ) f) x) fun ξ n =>
    (-(2 * ↑π * I)) ^ n •
      ∫ (x : E),
        ContinuousMultilinearMap.compContinuousLinearMap
          (ContinuousMultilinearMap.mkPiRing ℝ (Fin n) (((vectorFourierIntegrand ξ) f) x)) fun x_1 => (innerSL ℝ) x
⊢ ContinuousOn
    (fun x =>
      (-(2 * ↑π * I)) ^ (n + 1) •
        ∫ (x_1 : E),
          ContinuousMultilinearMap.compContinuousLinearMap
            (ContinuousMultilinearMap.mkPiRing ℝ (Fin (n + 1)) (((vectorFourierIntegrand x) f) x_1)) fun x =>
            (innerSL ℝ) x_1)
    Set.univ

State before:
case succ.refine_2.refine_1
E' : Type ?u.1044983
ι : 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
f : 𝓢(E, F)
n : ℕ
IH :
  HasFTaylorSeriesUpTo (↑n) (fun ξ => ∫ (x : E), ((vectorFourierIntegrand ξ) f) x) fun ξ n =>
    (-(2 * ↑π * I)) ^ n •
      ∫ (x : E),
        ContinuousMultilinearMap.compContinuousLinearMap
          (ContinuousMultilinearMap.mkPiRing ℝ (Fin n) (((vectorFourierIntegrand ξ) f) x)) fun x_1 => (innerSL ℝ) x
⊢ ∀ x ∈ Set.univ,
    HasFDerivWithinAt
      (fun y =>
        (-(2 * ↑π * I)) ^ n •
          ∫ (x : E),
            ContinuousMultilinearMap.compContinuousLinearMap
              (ContinuousMultilinearMap.mkPiRing ℝ (Fin n) (((vectorFourierIntegrand y) f) x)) fun x_1 => (innerSL ℝ) x)
      (ContinuousMultilinearMap.curryLeft
        ((-(2 * ↑π * I)) ^ Nat.succ n •
          ∫ (x_1 : E),
            ContinuousMultilinearMap.compContinuousLinearMap
              (ContinuousMultilinearMap.mkPiRing ℝ (Fin (Nat.succ n)) (((vectorFourierIntegrand x) f) x_1)) fun x =>
              (innerSL ℝ) x_1))
      Set.univ x
Tactic:
intro ξ _
State after:
case succ.refine_2.refine_1
E' : Type ?u.1044983
ι : 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
f : 𝓢(E, F)
n : ℕ
IH :
  HasFTaylorSeriesUpTo (↑n) (fun ξ => ∫ (x : E), ((vectorFourierIntegrand ξ) f) x) fun ξ n =>
    (-(2 * ↑π * I)) ^ n •
      ∫ (x : E),
        ContinuousMultilinearMap.compContinuousLinearMap
          (ContinuousMultilinearMap.mkPiRing ℝ (Fin n) (((vectorFourierIntegrand ξ) f) x)) fun x_1 => (innerSL ℝ) x
ξ : E
a✝ : ξ ∈ Set.univ
⊢ HasFDerivWithinAt
    (fun y =>
      (-(2 * ↑π * I)) ^ n •
        ∫ (x : E),
          ContinuousMultilinearMap.compContinuousLinearMap
            (ContinuousMultilinearMap.mkPiRing ℝ (Fin n) (((vectorFourierIntegrand y) f) x)) fun x_1 => (innerSL ℝ) x)
    (ContinuousMultilinearMap.curryLeft
      ((-(2 * ↑π * I)) ^ Nat.succ n •
        ∫ (x : E),
          ContinuousMultilinearMap.compContinuousLinearMap
            (ContinuousMultilinearMap.mkPiRing ℝ (Fin (Nat.succ n)) (((vectorFourierIntegrand ξ) f) x)) fun x_1 =>
            (innerSL ℝ) x))
    Set.univ ξ

State before:
case succ.refine_2.refine_1
E' : Type ?u.1044983
ι : 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
f : 𝓢(E, F)
n : ℕ
IH :
  HasFTaylorSeriesUpTo (↑n) (fun ξ => ∫ (x : E), ((vectorFourierIntegrand ξ) f) x) fun ξ n =>
    (-(2 * ↑π * I)) ^ n •
      ∫ (x : E),
        ContinuousMultilinearMap.compContinuousLinearMap
          (ContinuousMultilinearMap.mkPiRing ℝ (Fin n) (((vectorFourierIntegrand ξ) f) x)) fun x_1 => (innerSL ℝ) x
ξ : E
a✝ : ξ ∈ Set.univ
⊢ HasFDerivWithinAt
    (fun y =>
      (-(2 * ↑π * I)) ^ n •
        ∫ (x : E),
          ContinuousMultilinearMap.compContinuousLinearMap
            (ContinuousMultilinearMap.mkPiRing ℝ (Fin n) (((vectorFourierIntegrand y) f) x)) fun x_1 => (innerSL ℝ) x)
    (ContinuousMultilinearMap.curryLeft
      ((-(2 * ↑π * I)) ^ Nat.succ n •
        ∫ (x : E),
          ContinuousMultilinearMap.compContinuousLinearMap
            (ContinuousMultilinearMap.mkPiRing ℝ (Fin (Nat.succ n)) (((vectorFourierIntegrand ξ) f) x)) fun x_1 =>
            (innerSL ℝ) x))
    Set.univ ξ
Tactic:
sorry
State after:
no goals

State before:
case succ.refine_2.refine_2
E' : Type ?u.1044983
ι : 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
f : 𝓢(E, F)
n : ℕ
IH :
  HasFTaylorSeriesUpTo (↑n) (fun ξ => ∫ (x : E), ((vectorFourierIntegrand ξ) f) x) fun ξ n =>
    (-(2 * ↑π * I)) ^ n •
      ∫ (x : E),
        ContinuousMultilinearMap.compContinuousLinearMap
          (ContinuousMultilinearMap.mkPiRing ℝ (Fin n) (((vectorFourierIntegrand ξ) f) x)) fun x_1 => (innerSL ℝ) x
⊢ ContinuousOn
    (fun x =>
      (-(2 * ↑π * I)) ^ (n + 1) •
        ∫ (x_1 : E),
          ContinuousMultilinearMap.compContinuousLinearMap
            (ContinuousMultilinearMap.mkPiRing ℝ (Fin (n + 1)) (((vectorFourierIntegrand x) f) x_1)) fun x =>
            (innerSL ℝ) x_1)
    Set.univ
Tactic:
rw [← continuous_iff_continuousOn_univ]
State after:
case succ.refine_2.refine_2
E' : Type ?u.1044983
ι : 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
f : 𝓢(E, F)
n : ℕ
IH :
  HasFTaylorSeriesUpTo (↑n) (fun ξ => ∫ (x : E), ((vectorFourierIntegrand ξ) f) x) fun ξ n =>
    (-(2 * ↑π * I)) ^ n •
      ∫ (x : E),
        ContinuousMultilinearMap.compContinuousLinearMap
          (ContinuousMultilinearMap.mkPiRing ℝ (Fin n) (((vectorFourierIntegrand ξ) f) x)) fun x_1 => (innerSL ℝ) x
⊢ Continuous fun x =>
    (-(2 * ↑π * I)) ^ (n + 1) •
      ∫ (x_1 : E),
        ContinuousMultilinearMap.compContinuousLinearMap
          (ContinuousMultilinearMap.mkPiRing ℝ (Fin (n + 1)) (((vectorFourierIntegrand x) f) x_1)) fun x =>
          (innerSL ℝ) x_1

State before:
case succ.refine_2.refine_2
E' : Type ?u.1044983
ι : 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
f : 𝓢(E, F)
n : ℕ
IH :
  HasFTaylorSeriesUpTo (↑n) (fun ξ => ∫ (x : E), ((vectorFourierIntegrand ξ) f) x) fun ξ n =>
    (-(2 * ↑π * I)) ^ n •
      ∫ (x : E),
        ContinuousMultilinearMap.compContinuousLinearMap
          (ContinuousMultilinearMap.mkPiRing ℝ (Fin n) (((vectorFourierIntegrand ξ) f) x)) fun x_1 => (innerSL ℝ) x
⊢ Continuous fun x =>
    (-(2 * ↑π * I)) ^ (n + 1) •
      ∫ (x_1 : E),
        ContinuousMultilinearMap.compContinuousLinearMap
          (ContinuousMultilinearMap.mkPiRing ℝ (Fin (n + 1)) (((vectorFourierIntegrand x) f) x_1)) fun x =>
          (innerSL ℝ) x_1
Tactic:
refine Continuous.const_smul ?_ _
State after:
case succ.refine_2.refine_2
E' : Type ?u.1044983
ι : 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
f : 𝓢(E, F)
n : ℕ
IH :
  HasFTaylorSeriesUpTo (↑n) (fun ξ => ∫ (x : E), ((vectorFourierIntegrand ξ) f) x) fun ξ n =>
    (-(2 * ↑π * I)) ^ n •
      ∫ (x : E),
        ContinuousMultilinearMap.compContinuousLinearMap
          (ContinuousMultilinearMap.mkPiRing ℝ (Fin n) (((vectorFourierIntegrand ξ) f) x)) fun x_1 => (innerSL ℝ) x
⊢ Continuous fun x =>
    ∫ (x_1 : E),
      ContinuousMultilinearMap.compContinuousLinearMap
        (ContinuousMultilinearMap.mkPiRing ℝ (Fin (n + 1)) (((vectorFourierIntegrand x) f) x_1)) fun x =>
        (innerSL ℝ) x_1

State before:
case succ.refine_2.refine_2
E' : Type ?u.1044983
ι : 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
f : 𝓢(E, F)
n : ℕ
IH :
  HasFTaylorSeriesUpTo (↑n) (fun ξ => ∫ (x : E), ((vectorFourierIntegrand ξ) f) x) fun ξ n =>
    (-(2 * ↑π * I)) ^ n •
      ∫ (x : E),
        ContinuousMultilinearMap.compContinuousLinearMap
          (ContinuousMultilinearMap.mkPiRing ℝ (Fin n) (((vectorFourierIntegrand ξ) f) x)) fun x_1 => (innerSL ℝ) x
⊢ Continuous fun x =>
    ∫ (x_1 : E),
      ContinuousMultilinearMap.compContinuousLinearMap
        (ContinuousMultilinearMap.mkPiRing ℝ (Fin (n + 1)) (((vectorFourierIntegrand x) f) x_1)) fun x =>
        (innerSL ℝ) x_1
Tactic:
sorry
State after:
no goals