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

State before:
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
n : ℕ
f : 𝓢(E, F)
x ξ : E
dξ : Fin n → E
⊢ (iteratedFDeriv ℝ n (fun ξ => ((vectorFourierIntegrand ξ) f) x) ξ) dξ =
    (-(2 * ↑π * I)) ^ n • (∏ i : Fin n, ⟪x, dξ i⟫_ℝ) • ((vectorFourierIntegrand ξ) f) x
Tactic:
induction n generalizing ξ with
| zero => simp
| succ n IH =>
  rw [iteratedFDeriv_succ_apply_left]
  rw [← fderiv_continuousMultilinear_apply_const_apply
    (contDiff_vectorFourierIntegrand.differentiable_iteratedFDeriv (WithTop.coe_lt_top _) _)]
  simp_rw [IH]
  rw [fderiv_const_smul ((differentiable_vectorFourierIntegrand _).const_smul _)]
  simp
  rw [pow_succ']
  rw [← smul_smul]
  refine congrArg _ ?_
  rw [smul_comm]
  rw [fderiv_const_smul (differentiable_vectorFourierIntegrand _)]
  simp [-neg_smul, -smul_neg]
  rw [Fin.prod_univ_succ]
  simp only [Fin.tail]
  rw [mul_comm ⟪x, dξ 0⟫]
  rw [← smul_smul]
  refine congrArg _ ?_
  rw [fderiv_vectorFourierIntegrand]
  rw [fderivVectorFourierIntegrandCLM_apply]
  rw [smul_comm]
  simp [← smul_smul]
State after:
no goals

State before:
case zero
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
dξ : Fin Nat.zero → E
⊢ (iteratedFDeriv ℝ Nat.zero (fun ξ => ((vectorFourierIntegrand ξ) f) x) ξ) dξ =
    (-(2 * ↑π * I)) ^ Nat.zero • (∏ i : Fin Nat.zero, ⟪x, dξ i⟫_ℝ) • ((vectorFourierIntegrand ξ) f) x
Tactic:
simp
State after:
no goals

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
⊢ (iteratedFDeriv ℝ (Nat.succ n) (fun ξ => ((vectorFourierIntegrand ξ) f) x) ξ) dξ =
    (-(2 * ↑π * I)) ^ Nat.succ n • (∏ i : Fin (Nat.succ n), ⟪x, dξ i⟫_ℝ) • ((vectorFourierIntegrand ξ) f) x
Tactic:
rw [iteratedFDeriv_succ_apply_left]
State after:
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
⊢ ((fderiv ℝ (iteratedFDeriv ℝ n fun ξ => ((vectorFourierIntegrand ξ) f) x) ξ) (dξ 0)) (Fin.tail dξ) =
    (-(2 * ↑π * I)) ^ Nat.succ n • (∏ i : Fin (Nat.succ n), ⟪x, dξ i⟫_ℝ) • ((vectorFourierIntegrand ξ) f) x

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
⊢ ((fderiv ℝ (iteratedFDeriv ℝ n fun ξ => ((vectorFourierIntegrand ξ) f) x) ξ) (dξ 0)) (Fin.tail dξ) =
    (-(2 * ↑π * I)) ^ Nat.succ n • (∏ i : Fin (Nat.succ n), ⟪x, dξ i⟫_ℝ) • ((vectorFourierIntegrand ξ) f) x
Tactic:
rw [← fderiv_continuousMultilinear_apply_const_apply
  (contDiff_vectorFourierIntegrand.differentiable_iteratedFDeriv (WithTop.coe_lt_top _) _)]
State after:
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
⊢ (fderiv ℝ (fun y => (iteratedFDeriv ℝ n (fun ξ => ((vectorFourierIntegrand ξ) f) x) y) (Fin.tail dξ)) ξ) (dξ 0) =
    (-(2 * ↑π * I)) ^ Nat.succ n • (∏ i : Fin (Nat.succ n), ⟪x, dξ i⟫_ℝ) • ((vectorFourierIntegrand ξ) f) x

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
⊢ (fderiv ℝ (fun y => (iteratedFDeriv ℝ n (fun ξ => ((vectorFourierIntegrand ξ) f) x) y) (Fin.tail dξ)) ξ) (dξ 0) =
    (-(2 * ↑π * I)) ^ Nat.succ n • (∏ i : Fin (Nat.succ n), ⟪x, dξ i⟫_ℝ) • ((vectorFourierIntegrand ξ) f) x
Tactic:
simp_rw [IH]
State after:
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
⊢ (fderiv ℝ (fun y => (-(2 * ↑π * I)) ^ n • (∏ i : Fin n, ⟪x, Fin.tail dξ i⟫_ℝ) • ((vectorFourierIntegrand y) f) x) ξ)
      (dξ 0) =
    (-(2 * ↑π * I)) ^ Nat.succ n • (∏ i : Fin (Nat.succ n), ⟪x, dξ i⟫_ℝ) • ((vectorFourierIntegrand ξ) f) x

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
⊢ (fderiv ℝ (fun y => (-(2 * ↑π * I)) ^ n • (∏ i : Fin n, ⟪x, Fin.tail dξ i⟫_ℝ) • ((vectorFourierIntegrand y) f) x) ξ)
      (dξ 0) =
    (-(2 * ↑π * I)) ^ Nat.succ n • (∏ i : Fin (Nat.succ n), ⟪x, dξ i⟫_ℝ) • ((vectorFourierIntegrand ξ) f) x
Tactic:
rw [fderiv_const_smul ((differentiable_vectorFourierIntegrand _).const_smul _)]
State after:
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
⊢ ((-(2 * ↑π * I)) ^ n • fderiv ℝ (fun y => (∏ i : Fin n, ⟪x, Fin.tail dξ i⟫_ℝ) • ((vectorFourierIntegrand y) f) x) ξ)
      (dξ 0) =
    (-(2 * ↑π * I)) ^ Nat.succ n • (∏ i : Fin (Nat.succ n), ⟪x, dξ i⟫_ℝ) • ((vectorFourierIntegrand ξ) f) x

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
⊢ ((-(2 * ↑π * I)) ^ n • fderiv ℝ (fun y => (∏ i : Fin n, ⟪x, Fin.tail dξ i⟫_ℝ) • ((vectorFourierIntegrand y) f) x) ξ)
      (dξ 0) =
    (-(2 * ↑π * I)) ^ Nat.succ n • (∏ i : Fin (Nat.succ n), ⟪x, dξ i⟫_ℝ) • ((vectorFourierIntegrand ξ) f) x
Tactic:
simp
State after:
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
⊢ (-(2 * ↑π * I)) ^ n •
      (fderiv ℝ (fun y => (∏ i : Fin n, ⟪x, Fin.tail dξ i⟫_ℝ) • ((vectorFourierIntegrand y) f) x) ξ) (dξ 0) =
    (-(2 * ↑π * I)) ^ Nat.succ n • (∏ i : Fin (Nat.succ n), ⟪x, dξ i⟫_ℝ) • ((vectorFourierIntegrand ξ) f) x

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
⊢ (-(2 * ↑π * I)) ^ n •
      (fderiv ℝ (fun y => (∏ i : Fin n, ⟪x, Fin.tail dξ i⟫_ℝ) • ((vectorFourierIntegrand y) f) x) ξ) (dξ 0) =
    (-(2 * ↑π * I)) ^ Nat.succ n • (∏ i : Fin (Nat.succ n), ⟪x, dξ i⟫_ℝ) • ((vectorFourierIntegrand ξ) f) x
Tactic:
rw [pow_succ']
State after:
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
⊢ (-(2 * ↑π * I)) ^ n •
      (fderiv ℝ (fun y => (∏ i : Fin n, ⟪x, Fin.tail dξ i⟫_ℝ) • ((vectorFourierIntegrand y) f) x) ξ) (dξ 0) =
    ((-(2 * ↑π * I)) ^ n * -(2 * ↑π * I)) • (∏ i : Fin (Nat.succ n), ⟪x, dξ i⟫_ℝ) • ((vectorFourierIntegrand ξ) f) x

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
⊢ (-(2 * ↑π * I)) ^ n •
      (fderiv ℝ (fun y => (∏ i : Fin n, ⟪x, Fin.tail dξ i⟫_ℝ) • ((vectorFourierIntegrand y) f) x) ξ) (dξ 0) =
    ((-(2 * ↑π * I)) ^ n * -(2 * ↑π * I)) • (∏ i : Fin (Nat.succ n), ⟪x, dξ i⟫_ℝ) • ((vectorFourierIntegrand ξ) f) x
Tactic:
rw [← smul_smul]
State after:
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
⊢ (-(2 * ↑π * I)) ^ n •
      (fderiv ℝ (fun y => (∏ i : Fin n, ⟪x, Fin.tail dξ i⟫_ℝ) • ((vectorFourierIntegrand y) f) x) ξ) (dξ 0) =
    (-(2 * ↑π * I)) ^ n • -(2 * ↑π * I) • (∏ i : Fin (Nat.succ n), ⟪x, dξ i⟫_ℝ) • ((vectorFourierIntegrand ξ) f) x

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
⊢ (-(2 * ↑π * I)) ^ n •
      (fderiv ℝ (fun y => (∏ i : Fin n, ⟪x, Fin.tail dξ i⟫_ℝ) • ((vectorFourierIntegrand y) f) x) ξ) (dξ 0) =
    (-(2 * ↑π * I)) ^ n • -(2 * ↑π * I) • (∏ i : Fin (Nat.succ n), ⟪x, dξ i⟫_ℝ) • ((vectorFourierIntegrand ξ) f) x
Tactic:
refine congrArg _ ?_
State after:
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
⊢ (fderiv ℝ (fun y => (∏ i : Fin n, ⟪x, Fin.tail dξ i⟫_ℝ) • ((vectorFourierIntegrand y) f) x) ξ) (dξ 0) =
    -(2 * ↑π * I) • (∏ i : Fin (Nat.succ n), ⟪x, dξ i⟫_ℝ) • ((vectorFourierIntegrand ξ) f) x

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
⊢ (fderiv ℝ (fun y => (∏ i : Fin n, ⟪x, Fin.tail dξ i⟫_ℝ) • ((vectorFourierIntegrand y) f) x) ξ) (dξ 0) =
    -(2 * ↑π * I) • (∏ i : Fin (Nat.succ n), ⟪x, dξ i⟫_ℝ) • ((vectorFourierIntegrand ξ) f) x
Tactic:
rw [smul_comm]
State after:
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
⊢ (fderiv ℝ (fun y => (∏ i : Fin n, ⟪x, Fin.tail dξ i⟫_ℝ) • ((vectorFourierIntegrand y) f) x) ξ) (dξ 0) =
    (∏ i : Fin (Nat.succ n), ⟪x, dξ i⟫_ℝ) • -(2 * ↑π * I) • ((vectorFourierIntegrand ξ) f) x

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
⊢ (fderiv ℝ (fun y => (∏ i : Fin n, ⟪x, Fin.tail dξ i⟫_ℝ) • ((vectorFourierIntegrand y) f) x) ξ) (dξ 0) =
    (∏ i : Fin (Nat.succ n), ⟪x, dξ i⟫_ℝ) • -(2 * ↑π * I) • ((vectorFourierIntegrand ξ) f) x
Tactic:
rw [fderiv_const_smul (differentiable_vectorFourierIntegrand _)]
State after:
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
⊢ ((∏ i : Fin n, ⟪x, Fin.tail dξ i⟫_ℝ) • fderiv ℝ (fun ξ => ((vectorFourierIntegrand ξ) f) x) ξ) (dξ 0) =
    (∏ i : Fin (Nat.succ n), ⟪x, dξ i⟫_ℝ) • -(2 * ↑π * I) • ((vectorFourierIntegrand ξ) f) x

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
⊢ ((∏ i : Fin n, ⟪x, Fin.tail dξ i⟫_ℝ) • fderiv ℝ (fun ξ => ((vectorFourierIntegrand ξ) f) x) ξ) (dξ 0) =
    (∏ i : Fin (Nat.succ n), ⟪x, dξ i⟫_ℝ) • -(2 * ↑π * I) • ((vectorFourierIntegrand ξ) f) x
Tactic:
simp [-neg_smul, -smul_neg]
State after:
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
⊢ (∏ i : Fin n, ⟪x, Fin.tail dξ i⟫_ℝ) • (fderiv ℝ (fun ξ => ((vectorFourierIntegrand ξ) f) x) ξ) (dξ 0) =
    (∏ i : Fin (Nat.succ n), ⟪x, dξ i⟫_ℝ) • -(2 * ↑π * I) • ((vectorFourierIntegrand ξ) f) x

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
⊢ (∏ i : Fin n, ⟪x, Fin.tail dξ i⟫_ℝ) • (fderiv ℝ (fun ξ => ((vectorFourierIntegrand ξ) f) x) ξ) (dξ 0) =
    (∏ i : Fin (Nat.succ n), ⟪x, dξ i⟫_ℝ) • -(2 * ↑π * I) • ((vectorFourierIntegrand ξ) f) x
Tactic:
rw [Fin.prod_univ_succ]
State after:
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
⊢ (∏ i : Fin n, ⟪x, Fin.tail dξ i⟫_ℝ) • (fderiv ℝ (fun ξ => ((vectorFourierIntegrand ξ) f) x) ξ) (dξ 0) =
    (⟪x, dξ 0⟫_ℝ * ∏ i : Fin n, ⟪x, dξ (Fin.succ i)⟫_ℝ) • -(2 * ↑π * I) • ((vectorFourierIntegrand ξ) f) x

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
⊢ (∏ i : Fin n, ⟪x, Fin.tail dξ i⟫_ℝ) • (fderiv ℝ (fun ξ => ((vectorFourierIntegrand ξ) f) x) ξ) (dξ 0) =
    (⟪x, dξ 0⟫_ℝ * ∏ i : Fin n, ⟪x, dξ (Fin.succ i)⟫_ℝ) • -(2 * ↑π * I) • ((vectorFourierIntegrand ξ) f) x
Tactic:
simp only [Fin.tail]
State after:
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_1 : Fin n, ⟪x, dξ (Fin.succ x_1)⟫_ℝ) • (fderiv ℝ (fun ξ => ((vectorFourierIntegrand ξ) f) x) ξ) (dξ 0) =
    (⟪x, dξ 0⟫_ℝ * ∏ x_1 : Fin n, ⟪x, dξ (Fin.succ x_1)⟫_ℝ) • -(2 * ↑π * I) • ((vectorFourierIntegrand ξ) f) x

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_1 : Fin n, ⟪x, dξ (Fin.succ x_1)⟫_ℝ) • (fderiv ℝ (fun ξ => ((vectorFourierIntegrand ξ) f) x) ξ) (dξ 0) =
    (⟪x, dξ 0⟫_ℝ * ∏ x_1 : Fin n, ⟪x, dξ (Fin.succ x_1)⟫_ℝ) • -(2 * ↑π * I) • ((vectorFourierIntegrand ξ) f) x
Tactic:
rw [mul_comm ⟪x, dξ 0⟫]
State after:
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_1 : Fin n, ⟪x, dξ (Fin.succ x_1)⟫_ℝ) • (fderiv ℝ (fun ξ => ((vectorFourierIntegrand ξ) f) x) ξ) (dξ 0) =
    ((∏ x_1 : Fin n, ⟪x, dξ (Fin.succ x_1)⟫_ℝ) * ⟪x, dξ 0⟫_ℝ) • -(2 * ↑π * I) • ((vectorFourierIntegrand ξ) f) x

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_1 : Fin n, ⟪x, dξ (Fin.succ x_1)⟫_ℝ) • (fderiv ℝ (fun ξ => ((vectorFourierIntegrand ξ) f) x) ξ) (dξ 0) =
    ((∏ x_1 : Fin n, ⟪x, dξ (Fin.succ x_1)⟫_ℝ) * ⟪x, dξ 0⟫_ℝ) • -(2 * ↑π * I) • ((vectorFourierIntegrand ξ) f) x
Tactic:
rw [← smul_smul]
State after:
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_1 : Fin n, ⟪x, dξ (Fin.succ x_1)⟫_ℝ) • (fderiv ℝ (fun ξ => ((vectorFourierIntegrand ξ) f) x) ξ) (dξ 0) =
    (∏ x_1 : Fin n, ⟪x, dξ (Fin.succ x_1)⟫_ℝ) • ⟪x, dξ 0⟫_ℝ • -(2 * ↑π * I) • ((vectorFourierIntegrand ξ) f) x

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_1 : Fin n, ⟪x, dξ (Fin.succ x_1)⟫_ℝ) • (fderiv ℝ (fun ξ => ((vectorFourierIntegrand ξ) f) x) ξ) (dξ 0) =
    (∏ x_1 : Fin n, ⟪x, dξ (Fin.succ x_1)⟫_ℝ) • ⟪x, dξ 0⟫_ℝ • -(2 * ↑π * I) • ((vectorFourierIntegrand ξ) f) x
Tactic:
refine congrArg _ ?_
State after:
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
⊢ (fderiv ℝ (fun ξ => ((vectorFourierIntegrand ξ) f) x) ξ) (dξ 0) =
    ⟪x, dξ 0⟫_ℝ • -(2 * ↑π * I) • ((vectorFourierIntegrand ξ) f) x

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
⊢ (fderiv ℝ (fun ξ => ((vectorFourierIntegrand ξ) f) x) ξ) (dξ 0) =
    ⟪x, dξ 0⟫_ℝ • -(2 * ↑π * I) • ((vectorFourierIntegrand ξ) f) x
Tactic:
rw [fderiv_vectorFourierIntegrand]
State after:
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
⊢ (((fderivVectorFourierIntegrandCLM ξ) f) x) (dξ 0) = ⟪x, dξ 0⟫_ℝ • -(2 * ↑π * I) • ((vectorFourierIntegrand ξ) f) x

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
⊢ (((fderivVectorFourierIntegrandCLM ξ) f) x) (dξ 0) = ⟪x, dξ 0⟫_ℝ • -(2 * ↑π * I) • ((vectorFourierIntegrand ξ) f) x
Tactic:
rw [fderivVectorFourierIntegrandCLM_apply]
State after:
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
⊢ -((2 * ↑π * I) • ⟪x, dξ 0⟫_ℝ • ((vectorFourierIntegrand ξ) f) x) =
    ⟪x, dξ 0⟫_ℝ • -(2 * ↑π * I) • ((vectorFourierIntegrand ξ) f) x

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
⊢ -((2 * ↑π * I) • ⟪x, dξ 0⟫_ℝ • ((vectorFourierIntegrand ξ) f) x) =
    ⟪x, dξ 0⟫_ℝ • -(2 * ↑π * I) • ((vectorFourierIntegrand ξ) f) x
Tactic:
rw [smul_comm]
State after:
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

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]
State after:
no goals