Theorem: SchwartzMap.iteratedFDeriv_integral_vectorFourierIntegrand_apply'
Proof state before:
case succ
E' : Type ?u.1736571
ι : 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 : ℕ
IH :
  ∀ {f : 𝓢(E, F)} {ξ : E} {m : Fin n → E},
    (iteratedFDeriv ℝ n (fun ξ => ∫ (x : E), ((vectorFourierIntegrand ξ) f) x) ξ) m =
      (-(2 * ↑π * I)) ^ n •
        ∫ (x : E),
          ((vectorFourierIntegrand ξ)
              ((hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => ∏ i : Fin n, ⟪x, m i⟫_ℝ)) f))
            x
f : 𝓢(E, F)
ξ : E
m : Fin (Nat.succ n) → E
⊢ (∫ (x : E),
        ((vectorFourierIntegrand ξ)
            (innerSL_smul
              ((hasTemperateGrowth_smul
                  (_ : Function.HasTemperateGrowth fun x => ∏ x_1 : Fin n, ⟪x, m (Fin.succ x_1)⟫_ℝ))
                f)))
          x)
      (m 0) =
    ∫ (x : E),
      ((vectorFourierIntegrand ξ)
          ((hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => ∏ i : Fin (Nat.succ n), ⟪x, m i⟫_ℝ)) f))
        x
Tactic:
rw [ContinuousLinearMap.integral_apply (by exact integrable _)]
Proof state after:
case succ
E' : Type ?u.1736571
ι : 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 : ℕ
IH :
  ∀ {f : 𝓢(E, F)} {ξ : E} {m : Fin n → E},
    (iteratedFDeriv ℝ n (fun ξ => ∫ (x : E), ((vectorFourierIntegrand ξ) f) x) ξ) m =
      (-(2 * ↑π * I)) ^ n •
        ∫ (x : E),
          ((vectorFourierIntegrand ξ)
              ((hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => ∏ i : Fin n, ⟪x, m i⟫_ℝ)) f))
            x
f : 𝓢(E, F)
ξ : E
m : Fin (Nat.succ n) → E
⊢ ∫ (a : E),
      (((vectorFourierIntegrand ξ)
            (innerSL_smul
              ((hasTemperateGrowth_smul
                  (_ : Function.HasTemperateGrowth fun x => ∏ x_1 : Fin n, ⟪x, m (Fin.succ x_1)⟫_ℝ))
                f)))
          a)
        (m 0) =
    ∫ (x : E),
      ((vectorFourierIntegrand ξ)
          ((hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => ∏ i : Fin (Nat.succ n), ⟪x, m i⟫_ℝ)) f))
        x