internlm/Lean-Github huggingface dataset:
Theorem: SchwartzMap.iteratedFDeriv_vectorFourierIntegrand_apply
Proof state before:
case succ
E' : Type ?u.1454638
ι : 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
n : ℕ
IH :
  ∀ {ξ : E} {dξ : Fin n → E},
    (iteratedFDeriv ℝ n (fun ξ => ((vectorFourierIntegrand ξ) f) x) ξ) dξ =
      (-(2 * ↑π * I)) ^ n • (∏ i : Fin n, ⟪x, dξ i⟫_ℝ) • ((vectorFourierIntegrand ξ) f) x
ξ : E
dξ : Fin (Nat.succ n) → E
⊢ -(⟪x, dξ 0⟫_ℝ • (2 * ↑π * I) • ((vectorFourierIntegrand ξ) f) x) =
    ⟪x, dξ 0⟫_ℝ • -(2 * ↑π * I) • ((vectorFourierIntegrand ξ) f) x
Tactic:
simp [← smul_smul]
Proof state after:
no goals
Theorem: SchwartzMap.iteratedFDeriv_vectorFourierIntegrand
Proof state before:
E' : Type ?u.1516574
ι : 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
n : ℕ
f : 𝓢(E, F)
x ξ : E
⊢ iteratedFDeriv ℝ n (fun ξ => ((vectorFourierIntegrand ξ) f) x) ξ =
    (-(2 * ↑π * I)) ^ n •
      ContinuousMultilinearMap.compContinuousLinearMap
        (ContinuousMultilinearMap.mkPiRing ℝ (Fin n) (((vectorFourierIntegrand ξ) f) x)) fun x_1 => (innerSL ℝ) x
Tactic:
ext
Proof state after:
case H
E' : Type ?u.1516574
ι : 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
n : ℕ
f : 𝓢(E, F)
x ξ : E
x✝ : Fin n → E
⊢ (iteratedFDeriv ℝ n (fun ξ => ((vectorFourierIntegrand ξ) f) x) ξ) x✝ =
    ((-(2 * ↑π * I)) ^ n •
        ContinuousMultilinearMap.compContinuousLinearMap
          (ContinuousMultilinearMap.mkPiRing ℝ (Fin n) (((vectorFourierIntegrand ξ) f) x)) fun x_1 => (innerSL ℝ) x)
      x✝
Theorem: SchwartzMap.iteratedFDeriv_vectorFourierIntegrand
Proof state before:
case H
E' : Type ?u.1516574
ι : 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
n : ℕ
f : 𝓢(E, F)
x ξ : E
x✝ : Fin n → E
⊢ (iteratedFDeriv ℝ n (fun ξ => ((vectorFourierIntegrand ξ) f) x) ξ) x✝ =
    ((-(2 * ↑π * I)) ^ n •
        ContinuousMultilinearMap.compContinuousLinearMap
          (ContinuousMultilinearMap.mkPiRing ℝ (Fin n) (((vectorFourierIntegrand ξ) f) x)) fun x_1 => (innerSL ℝ) x)
      x✝
Tactic:
simp [iteratedFDeriv_vectorFourierIntegrand_apply]
Proof state after:
no goals
Theorem: SchwartzMap.integral_iteratedFDeriv_vectorFourierIntegrand_apply
Proof state before:
E' : Type ?u.1537740
ι : 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
n : ℕ
f : 𝓢(E, F)
ξ : E
m : Fin n → E
⊢ ∫ (x : E), (iteratedFDeriv ℝ n (fun x_1 => ((vectorFourierIntegrand x_1) f) x) ξ) m =
    (-(2 * ↑π * I)) ^ n • ∫ (x : E), (∏ i : Fin n, ⟪x, m i⟫_ℝ) • ((vectorFourierIntegrand ξ) f) x
Tactic:
simp only [iteratedFDeriv_vectorFourierIntegrand]
Proof state after:
E' : Type ?u.1537740
ι : 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
n : ℕ
f : 𝓢(E, F)
ξ : E
m : Fin n → E
⊢ ∫ (x : E),
      ((-(2 * ↑π * I)) ^ n •
          ContinuousMultilinearMap.compContinuousLinearMap
            (ContinuousMultilinearMap.mkPiRing ℝ (Fin n) (((vectorFourierIntegrand ξ) f) x)) fun x_1 => (innerSL ℝ) x)
        m =
    (-(2 * ↑π * I)) ^ n • ∫ (x : E), (∏ i : Fin n, ⟪x, m i⟫_ℝ) • ((vectorFourierIntegrand ξ) f) x
Theorem: SchwartzMap.integral_iteratedFDeriv_vectorFourierIntegrand_apply
Proof state before:
E' : Type ?u.1537740
ι : 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
n : ℕ
f : 𝓢(E, F)
ξ : E
m : Fin n → E
⊢ ∫ (x : E),
      ((-(2 * ↑π * I)) ^ n •
          ContinuousMultilinearMap.compContinuousLinearMap
            (ContinuousMultilinearMap.mkPiRing ℝ (Fin n) (((vectorFourierIntegrand ξ) f) x)) fun x_1 => (innerSL ℝ) x)
        m =
    (-(2 * ↑π * I)) ^ n • ∫ (x : E), (∏ i : Fin n, ⟪x, m i⟫_ℝ) • ((vectorFourierIntegrand ξ) f) x
Tactic:
simp [integral_smul]
Proof state after:
no goals
Theorem: SchwartzMap.integral_iteratedFDeriv_vectorFourierIntegrand_apply'
Proof state before:
E' : Type ?u.1560826
ι : 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
n : ℕ
f : 𝓢(E, F)
ξ : E
m : Fin n → E
⊢ (∫ (x : E), iteratedFDeriv ℝ n (fun x_1 => ((vectorFourierIntegrand x_1) f) x) ξ) m =
    (-(2 * ↑π * I)) ^ n • ∫ (x : E), (∏ i : Fin n, ⟪x, m i⟫_ℝ) • ((vectorFourierIntegrand ξ) f) x
Tactic:
simp only [iteratedFDeriv_vectorFourierIntegrand]
Proof state after:
E' : Type ?u.1560826
ι : 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
n : ℕ
f : 𝓢(E, F)
ξ : E
m : Fin n → E
⊢ (∫ (x : E),
        (-(2 * ↑π * I)) ^ n •
          ContinuousMultilinearMap.compContinuousLinearMap
            (ContinuousMultilinearMap.mkPiRing ℝ (Fin n) (((vectorFourierIntegrand ξ) f) x)) fun x_1 => (innerSL ℝ) x)
      m =
    (-(2 * ↑π * I)) ^ n • ∫ (x : E), (∏ i : Fin n, ⟪x, m i⟫_ℝ) • ((vectorFourierIntegrand ξ) f) x
Theorem: SchwartzMap.integral_iteratedFDeriv_vectorFourierIntegrand_apply'
Proof state before:
E' : Type ?u.1560826
ι : 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
n : ℕ
f : 𝓢(E, F)
ξ : E
m : Fin n → E
⊢ (∫ (x : E),
        (-(2 * ↑π * I)) ^ n •
          ContinuousMultilinearMap.compContinuousLinearMap
            (ContinuousMultilinearMap.mkPiRing ℝ (Fin n) (((vectorFourierIntegrand ξ) f) x)) fun x_1 => (innerSL ℝ) x)
      m =
    (-(2 * ↑π * I)) ^ n • ∫ (x : E), (∏ i : Fin n, ⟪x, m i⟫_ℝ) • ((vectorFourierIntegrand ξ) f) x
Tactic:
rw [integral_smul, ContinuousMultilinearMap.smul_apply]
Proof state after:
E' : Type ?u.1560826
ι : 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
n : ℕ
f : 𝓢(E, F)
ξ : E
m : Fin n → E
⊢ (-(2 * ↑π * I)) ^ n •
      (∫ (a : E),
          ContinuousMultilinearMap.compContinuousLinearMap
            (ContinuousMultilinearMap.mkPiRing ℝ (Fin n) (((vectorFourierIntegrand ξ) f) a)) fun x => (innerSL ℝ) a)
        m =
    (-(2 * ↑π * I)) ^ n • ∫ (x : E), (∏ i : Fin n, ⟪x, m i⟫_ℝ) • ((vectorFourierIntegrand ξ) f) x
Theorem: SchwartzMap.integral_iteratedFDeriv_vectorFourierIntegrand_apply'
Proof state before:
E' : Type ?u.1560826
ι : 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
n : ℕ
f : 𝓢(E, F)
ξ : E
m : Fin n → E
⊢ (-(2 * ↑π * I)) ^ n •
      (∫ (a : E),
          ContinuousMultilinearMap.compContinuousLinearMap
            (ContinuousMultilinearMap.mkPiRing ℝ (Fin n) (((vectorFourierIntegrand ξ) f) a)) fun x => (innerSL ℝ) a)
        m =
    (-(2 * ↑π * I)) ^ n • ∫ (x : E), (∏ i : Fin n, ⟪x, m i⟫_ℝ) • ((vectorFourierIntegrand ξ) f) x
Tactic:
refine congrArg _ ?_
Proof state after:
E' : Type ?u.1560826
ι : 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
n : ℕ
f : 𝓢(E, F)
ξ : E
m : Fin n → E
⊢ (∫ (a : E),
        ContinuousMultilinearMap.compContinuousLinearMap
          (ContinuousMultilinearMap.mkPiRing ℝ (Fin n) (((vectorFourierIntegrand ξ) f) a)) fun x => (innerSL ℝ) a)
      m =
    ∫ (x : E), (∏ i : Fin n, ⟪x, m i⟫_ℝ) • ((vectorFourierIntegrand ξ) f) x
Theorem: SchwartzMap.integral_iteratedFDeriv_vectorFourierIntegrand_apply'
Proof state before:
E' : Type ?u.1560826
ι : 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
n : ℕ
f : 𝓢(E, F)
ξ : E
m : Fin n → E
⊢ ∫ (x : E),
      (ContinuousMultilinearMap.compContinuousLinearMap
          (ContinuousMultilinearMap.mkPiRing ℝ (Fin n) (((vectorFourierIntegrand ξ) f) x)) fun x_1 => (innerSL ℝ) x)
        m =
    ∫ (x : E), (∏ i : Fin n, ⟪x, m i⟫_ℝ) • ((vectorFourierIntegrand ξ) f) x
Tactic:
simp
Proof state after:
no goals
Theorem: SchwartzMap.integral_iteratedFDeriv_vectorFourierIntegrand_apply'
Proof state before:
case hc.refine_1
E' : Type ?u.1560826
ι : 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
n : ℕ
f : 𝓢(E, F)
ξ : E
m : Fin n → E
⊢ AEStronglyMeasurable
    (fun a =>
      ContinuousMultilinearMap.compContinuousLinearMap
        (ContinuousMultilinearMap.mkPiRing ℝ (Fin n) (((vectorFourierIntegrand ξ) f) a)) fun x => (innerSL ℝ) a)
    volume
Tactic:
refine Continuous.aestronglyMeasurable ?_
Proof state after:
case hc.refine_1
E' : Type ?u.1560826
ι : 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
n : ℕ
f : 𝓢(E, F)
ξ : E
m : Fin n → E
⊢ Continuous fun a =>
    ContinuousMultilinearMap.compContinuousLinearMap
      (ContinuousMultilinearMap.mkPiRing ℝ (Fin n) (((vectorFourierIntegrand ξ) f) a)) fun x => (innerSL ℝ) a
Theorem: SchwartzMap.integral_iteratedFDeriv_vectorFourierIntegrand_apply'
Proof state before:
case hc.refine_1
E' : Type ?u.1560826
ι : 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
n : ℕ
f : 𝓢(E, F)
ξ : E
m : Fin n → E
⊢ Continuous fun a =>
    ContinuousMultilinearMap.compContinuousLinearMap
      (ContinuousMultilinearMap.mkPiRing ℝ (Fin n) (((vectorFourierIntegrand ξ) f) a)) fun x => (innerSL ℝ) a
Tactic:
simp only [← ContinuousMultilinearMap.compContinuousLinearMapL_apply]
Proof state after:
case hc.refine_1
E' : Type ?u.1560826
ι : 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
n : ℕ
f : 𝓢(E, F)
ξ : E
m : Fin n → E
⊢ Continuous fun a =>
    (ContinuousMultilinearMap.compContinuousLinearMapL fun x => (innerSL ℝ) a)
      (ContinuousMultilinearMap.mkPiRing ℝ (Fin n) (((vectorFourierIntegrand ξ) f) a))