internlm/Lean-Github huggingface dataset:
Theorem: SchwartzMap.hasFTaylorSeriesUpTo_integral_vectorFourierIntegrand
Proof 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]
Proof 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
Theorem: SchwartzMap.hasFTaylorSeriesUpTo_integral_vectorFourierIntegrand
Proof 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]
Proof 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
Theorem: SchwartzMap.hasFTaylorSeriesUpTo_integral_vectorFourierIntegrand
Proof 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
Proof state after:
no goals
Theorem: SchwartzMap.hasFTaylorSeriesUpTo_integral_vectorFourierIntegrand
Proof 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
Proof state after:
no goals
Theorem: SchwartzMap.hasFTaylorSeriesUpTo_integral_vectorFourierIntegrand
Proof 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]
Proof 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
Theorem: SchwartzMap.hasFTaylorSeriesUpTo_integral_vectorFourierIntegrand
Proof 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 ?_ _
Proof 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
Theorem: SchwartzMap.hasFTaylorSeriesUpTo_integral_vectorFourierIntegrand
Proof 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
Proof state after:
no goals
Theorem: SchwartzMap.fderiv_fourierChar_inner
Proof state before:
E' : Type ?u.1098054
ι : 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
x ξ dξ : E
⊢ (fderiv ℝ (fun ξ => ↑(Real.fourierChar (Multiplicative.ofAdd (-⟪x, ξ⟫_ℝ)))) ξ) dξ =
    -(2 * ↑π * I * ↑⟪x, dξ⟫_ℝ * ↑(Real.fourierChar (Multiplicative.ofAdd (-⟪x, ξ⟫_ℝ))))
Tactic:
change fderiv ℝ ((fun u : ℝ => Real.fourierChar[u]) ∘ (fun ξ : E => -⟪x, ξ⟫)) ξ dξ = _
Proof state after:
E' : Type ?u.1098054
ι : 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
x ξ dξ : E
⊢ (fderiv ℝ ((fun u => ↑(Real.fourierChar (Multiplicative.ofAdd u))) ∘ fun ξ => -⟪x, ξ⟫_ℝ) ξ) dξ =
    -(2 * ↑π * I * ↑⟪x, dξ⟫_ℝ * ↑(Real.fourierChar (Multiplicative.ofAdd (-⟪x, ξ⟫_ℝ))))
Theorem: SchwartzMap.fderiv_fourierChar_inner
Proof state before:
E' : Type ?u.1098054
ι : 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
x ξ dξ : E
⊢ (ContinuousLinearMap.comp (fderiv ℝ (fun u => ↑(Real.fourierChar (Multiplicative.ofAdd u))) (-⟪x, ξ⟫_ℝ))
        (fderiv ℝ (fun ξ => -⟪x, ξ⟫_ℝ) ξ))
      dξ =
    -(2 * ↑π * I * ↑⟪x, dξ⟫_ℝ * ↑(Real.fourierChar (Multiplicative.ofAdd (-⟪x, ξ⟫_ℝ))))
Tactic:
rw [ContinuousLinearMap.comp_apply]
Proof state after:
E' : Type ?u.1098054
ι : 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
x ξ dξ : E
⊢ (fderiv ℝ (fun u => ↑(Real.fourierChar (Multiplicative.ofAdd u))) (-⟪x, ξ⟫_ℝ))
      ((fderiv ℝ (fun ξ => -⟪x, ξ⟫_ℝ) ξ) dξ) =
    -(2 * ↑π * I * ↑⟪x, dξ⟫_ℝ * ↑(Real.fourierChar (Multiplicative.ofAdd (-⟪x, ξ⟫_ℝ))))
Theorem: SchwartzMap.fderiv_fourierChar_inner
Proof state before:
E' : Type ?u.1098054
ι : 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
x ξ dξ : E
⊢ (fderiv ℝ (fun u => ↑(Real.fourierChar (Multiplicative.ofAdd u))) (-⟪x, ξ⟫_ℝ))
      ((fderiv ℝ (fun ξ => -⟪x, ξ⟫_ℝ) ξ) dξ) =
    -(2 * ↑π * I * ↑⟪x, dξ⟫_ℝ * ↑(Real.fourierChar (Multiplicative.ofAdd (-⟪x, ξ⟫_ℝ))))
Tactic:
simp
Proof state after:
E' : Type ?u.1098054
ι : 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
x ξ dξ : E
⊢ (fderiv ℝ (fun u => ↑(Real.fourierChar (Multiplicative.ofAdd u))) (-⟪x, ξ⟫_ℝ)) ((fderiv ℝ (fun y => ⟪x, y⟫_ℝ) ξ) dξ) =
    2 * ↑π * I * ↑⟪x, dξ⟫_ℝ * ↑(Real.fourierChar (Multiplicative.ofAdd (-⟪x, ξ⟫_ℝ)))