internlm/Lean-Github huggingface dataset:
Theorem: SchwartzMap.vectorFourierIntegrand_hasTemperateGrowth_smul
Proof state before:
E' : Type ?u.1666239
ι : 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
g : E → ℝ
hg : Function.HasTemperateGrowth g
⊢ ↑(Real.fourierChar (Multiplicative.ofAdd (-⟪x, ξ⟫_ℝ))) • ((hasTemperateGrowth_smul hg) f) x =
    g x • ↑(Real.fourierChar (Multiplicative.ofAdd (-⟪x, ξ⟫_ℝ))) • f x
Tactic:
simp only [hasTemperateGrowth_smul_apply]
Proof state after:
E' : Type ?u.1666239
ι : 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
g : E → ℝ
hg : Function.HasTemperateGrowth g
⊢ ↑(Real.fourierChar (Multiplicative.ofAdd (-⟪x, ξ⟫_ℝ))) • g x • f x =
    g x • ↑(Real.fourierChar (Multiplicative.ofAdd (-⟪x, ξ⟫_ℝ))) • f x
Theorem: SchwartzMap.vectorFourierIntegrand_hasTemperateGrowth_smul
Proof state before:
E' : Type ?u.1666239
ι : 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
g : E → ℝ
hg : Function.HasTemperateGrowth g
⊢ ↑(Real.fourierChar (Multiplicative.ofAdd (-⟪x, ξ⟫_ℝ))) • g x • f x =
    g x • ↑(Real.fourierChar (Multiplicative.ofAdd (-⟪x, ξ⟫_ℝ))) • f x
Tactic:
rw [smul_comm]
Proof state after:
no goals
Theorem: SchwartzMap.iteratedFDeriv_integral_vectorFourierIntegrand_apply
Proof state before:
E' : Type ?u.1677399
ι : 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
⊢ (iteratedFDeriv ℝ n (fun ξ => ∫ (x : E), ((vectorFourierIntegrand ξ) f) x) ξ) m =
    (-(2 * ↑π * I)) ^ n • ∫ (x : E), (∏ i : Fin n, ⟪x, m i⟫_ℝ) • ((vectorFourierIntegrand ξ) f) x
Tactic:
induction n generalizing f ξ with
| zero => simp
| succ n IH =>
  rw [iteratedFDeriv_succ_apply_left]
  rw [← fderiv_continuousMultilinear_apply_const_apply
    (ContDiff.differentiable_iteratedFDeriv (WithTop.coe_lt_top n)
      contDiff_integral_vectorFourierIntegrand ξ)]
  simp_rw [IH]
  simp only [Fin.tail]
  simp_rw [← vectorFourierIntegrand_hasTemperateGrowth_smul
    (Function.hasTemperateGrowth_prod_univ_inner_const fun i : Fin n ↦ m i.succ)]
  rw [fderiv_const_smul (differentiable_integral_vectorFourierIntegrand _)]
  rw [ContinuousLinearMap.smul_apply, pow_succ', mul_smul]
  refine congrArg _ ?_
  rw [fderiv_integral_vectorFourierIntegrand', ← neg_smul, ContinuousLinearMap.smul_apply]
  refine congrArg _ ?_
  rw [ContinuousLinearMap.integral_apply (by exact integrable _)]  refine congrArg _ ?_
  funext x
  rw [Fin.prod_univ_succ]
  simp only [vectorFourierIntegrand_apply, ContinuousLinearMap.smul_apply, innerSL_smul_apply,
    hasTemperateGrowth_smul_apply]
  simp [smul_comm (_ : ℂ), smul_smul]
Proof state after:
no goals
Theorem: SchwartzMap.iteratedFDeriv_integral_vectorFourierIntegrand_apply
Proof state before:
case zero
E' : Type ?u.1677399
ι : Type u_1
𝕜 : Type u_2
𝕜' : Type u_3
R : Type u_4
M : ι → Type u_5
D : Type u_6
E : Type u_7
F : Type u_8
G : Type u_9
inst✝²² : DecidableEq ι
inst✝²¹ : Fintype ι
inst✝²⁰ : NontriviallyNormedField 𝕜
inst✝¹⁹ : (i : ι) → NormedAddCommGroup (M i)
inst✝¹⁸ : (i : ι) → NormedSpace ℝ (M i)
inst✝¹⁷ : NormedAddCommGroup D
inst✝¹⁶ : NormedSpace ℝ D
inst✝¹⁵ : NormedAddCommGroup E
inst✝¹⁴ : InnerProductSpace ℝ E
inst✝¹³ : NormedAddCommGroup E'
inst✝¹² : InnerProductSpace ℝ E'
inst✝¹¹ : NormedAddCommGroup F
inst✝¹⁰ : NormedSpace ℂ F
inst✝⁹ : NormedSpace 𝕜 F
inst✝⁸ : NormedAddCommGroup G
inst✝⁷ : NormedSpace ℝ G
inst✝⁶ : MeasurableSpace E
inst✝⁵ : FiniteDimensional ℝ E
inst✝⁴ : BorelSpace E
inst✝³ : MeasurableSpace E'
inst✝² : FiniteDimensional ℝ E'
inst✝¹ : BorelSpace E'
inst✝ : CompleteSpace F
f : 𝓢(E, F)
ξ : E
m : Fin Nat.zero → E
⊢ (iteratedFDeriv ℝ Nat.zero (fun ξ => ∫ (x : E), ((vectorFourierIntegrand ξ) f) x) ξ) m =
    (-(2 * ↑π * I)) ^ Nat.zero • ∫ (x : E), (∏ i : Fin Nat.zero, ⟪x, m i⟫_ℝ) • ((vectorFourierIntegrand ξ) f) x
Tactic:
simp
Proof state after:
no goals
Theorem: SchwartzMap.iteratedFDeriv_integral_vectorFourierIntegrand_apply
Proof state before:
case succ
E' : Type ?u.1677399
ι : 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), (∏ i : Fin n, ⟪x, m i⟫_ℝ) • ((vectorFourierIntegrand ξ) f) x
f : 𝓢(E, F)
ξ : E
m : Fin (Nat.succ n) → E
⊢ (iteratedFDeriv ℝ (Nat.succ n) (fun ξ => ∫ (x : E), ((vectorFourierIntegrand ξ) f) x) ξ) m =
    (-(2 * ↑π * I)) ^ Nat.succ n • ∫ (x : E), (∏ i : Fin (Nat.succ n), ⟪x, m i⟫_ℝ) • ((vectorFourierIntegrand ξ) f) x
Tactic:
rw [iteratedFDeriv_succ_apply_left]
Proof state after:
case succ
E' : Type ?u.1677399
ι : 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), (∏ i : Fin n, ⟪x, m i⟫_ℝ) • ((vectorFourierIntegrand ξ) f) x
f : 𝓢(E, F)
ξ : E
m : Fin (Nat.succ n) → E
⊢ ((fderiv ℝ (iteratedFDeriv ℝ n fun ξ => ∫ (x : E), ((vectorFourierIntegrand ξ) f) x) ξ) (m 0)) (Fin.tail m) =
    (-(2 * ↑π * I)) ^ Nat.succ n • ∫ (x : E), (∏ i : Fin (Nat.succ n), ⟪x, m i⟫_ℝ) • ((vectorFourierIntegrand ξ) f) x
Theorem: SchwartzMap.iteratedFDeriv_integral_vectorFourierIntegrand_apply
Proof state before:
case succ
E' : Type ?u.1677399
ι : 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), (∏ i : Fin n, ⟪x, m i⟫_ℝ) • ((vectorFourierIntegrand ξ) f) x
f : 𝓢(E, F)
ξ : E
m : Fin (Nat.succ n) → E
⊢ ((fderiv ℝ (iteratedFDeriv ℝ n fun ξ => ∫ (x : E), ((vectorFourierIntegrand ξ) f) x) ξ) (m 0)) (Fin.tail m) =
    (-(2 * ↑π * I)) ^ Nat.succ n • ∫ (x : E), (∏ i : Fin (Nat.succ n), ⟪x, m i⟫_ℝ) • ((vectorFourierIntegrand ξ) f) x
Tactic:
rw [← fderiv_continuousMultilinear_apply_const_apply
  (ContDiff.differentiable_iteratedFDeriv (WithTop.coe_lt_top n)
    contDiff_integral_vectorFourierIntegrand ξ)]
Proof state after:
case succ
E' : Type ?u.1677399
ι : 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), (∏ i : Fin n, ⟪x, m i⟫_ℝ) • ((vectorFourierIntegrand ξ) f) x
f : 𝓢(E, F)
ξ : E
m : Fin (Nat.succ n) → E
⊢ (fderiv ℝ (fun y => (iteratedFDeriv ℝ n (fun ξ => ∫ (x : E), ((vectorFourierIntegrand ξ) f) x) y) (Fin.tail m)) ξ)
      (m 0) =
    (-(2 * ↑π * I)) ^ Nat.succ n • ∫ (x : E), (∏ i : Fin (Nat.succ n), ⟪x, m i⟫_ℝ) • ((vectorFourierIntegrand ξ) f) x
Theorem: SchwartzMap.iteratedFDeriv_integral_vectorFourierIntegrand_apply
Proof state before:
case succ
E' : Type ?u.1677399
ι : 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), (∏ i : Fin n, ⟪x, m i⟫_ℝ) • ((vectorFourierIntegrand ξ) f) x
f : 𝓢(E, F)
ξ : E
m : Fin (Nat.succ n) → E
⊢ (fderiv ℝ (fun y => (iteratedFDeriv ℝ n (fun ξ => ∫ (x : E), ((vectorFourierIntegrand ξ) f) x) y) (Fin.tail m)) ξ)
      (m 0) =
    (-(2 * ↑π * I)) ^ Nat.succ n • ∫ (x : E), (∏ i : Fin (Nat.succ n), ⟪x, m i⟫_ℝ) • ((vectorFourierIntegrand ξ) f) x
Tactic:
simp_rw [IH]
Proof state after:
case succ
E' : Type ?u.1677399
ι : 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), (∏ i : Fin n, ⟪x, m i⟫_ℝ) • ((vectorFourierIntegrand ξ) f) x
f : 𝓢(E, F)
ξ : E
m : Fin (Nat.succ n) → E
⊢ (fderiv ℝ
        (fun y =>
          (-(2 * ↑π * I)) ^ n • ∫ (x : E), (∏ i : Fin n, ⟪x, Fin.tail m i⟫_ℝ) • ((vectorFourierIntegrand y) f) x)
        ξ)
      (m 0) =
    (-(2 * ↑π * I)) ^ Nat.succ n • ∫ (x : E), (∏ i : Fin (Nat.succ n), ⟪x, m i⟫_ℝ) • ((vectorFourierIntegrand ξ) f) x
Theorem: SchwartzMap.iteratedFDeriv_integral_vectorFourierIntegrand_apply
Proof state before:
case succ
E' : Type ?u.1677399
ι : 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), (∏ i : Fin n, ⟪x, m i⟫_ℝ) • ((vectorFourierIntegrand ξ) f) x
f : 𝓢(E, F)
ξ : E
m : Fin (Nat.succ n) → E
⊢ (fderiv ℝ
        (fun y =>
          (-(2 * ↑π * I)) ^ n • ∫ (x : E), (∏ i : Fin n, ⟪x, Fin.tail m i⟫_ℝ) • ((vectorFourierIntegrand y) f) x)
        ξ)
      (m 0) =
    (-(2 * ↑π * I)) ^ Nat.succ n • ∫ (x : E), (∏ i : Fin (Nat.succ n), ⟪x, m i⟫_ℝ) • ((vectorFourierIntegrand ξ) f) x
Tactic:
simp only [Fin.tail]
Proof state after:
case succ
E' : Type ?u.1677399
ι : 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), (∏ i : Fin n, ⟪x, m i⟫_ℝ) • ((vectorFourierIntegrand ξ) f) x
f : 𝓢(E, F)
ξ : E
m : Fin (Nat.succ n) → E
⊢ (fderiv ℝ
        (fun y =>
          (-(2 * ↑π * I)) ^ n • ∫ (x : E), (∏ x_1 : Fin n, ⟪x, m (Fin.succ x_1)⟫_ℝ) • ((vectorFourierIntegrand y) f) x)
        ξ)
      (m 0) =
    (-(2 * ↑π * I)) ^ Nat.succ n • ∫ (x : E), (∏ i : Fin (Nat.succ n), ⟪x, m i⟫_ℝ) • ((vectorFourierIntegrand ξ) f) x
Theorem: SchwartzMap.iteratedFDeriv_integral_vectorFourierIntegrand_apply
Proof state before:
case succ
E' : Type ?u.1677399
ι : 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), (∏ i : Fin n, ⟪x, m i⟫_ℝ) • ((vectorFourierIntegrand ξ) f) x
f : 𝓢(E, F)
ξ : E
m : Fin (Nat.succ n) → E
⊢ (fderiv ℝ
        (fun ξ =>
          ∫ (x : E),
            ((vectorFourierIntegrand ξ)
                ((hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => ∏ i : Fin n, ⟪x, m (Fin.succ i)⟫_ℝ))
                  f))
              x)
        ξ)
      (m 0) =
    -(2 * ↑π * I) • ∫ (x : E), (∏ i : Fin (Nat.succ n), ⟪x, m i⟫_ℝ) • ((vectorFourierIntegrand ξ) f) x
Tactic:
rw [fderiv_integral_vectorFourierIntegrand', ← neg_smul, ContinuousLinearMap.smul_apply]
Proof state after:
case succ
E' : Type ?u.1677399
ι : 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), (∏ i : Fin n, ⟪x, m i⟫_ℝ) • ((vectorFourierIntegrand ξ) f) x
f : 𝓢(E, F)
ξ : E
m : Fin (Nat.succ n) → E
⊢ -(2 * ↑π * I) •
      (∫ (x : E),
          ((vectorFourierIntegrand ξ)
              (innerSL_smul
                ((hasTemperateGrowth_smul (_ : Function.HasTemperateGrowth fun x => ∏ i : Fin n, ⟪x, m (Fin.succ i)⟫_ℝ))
                  f)))
            x)
        (m 0) =
    -(2 * ↑π * I) • ∫ (x : E), (∏ i : Fin (Nat.succ n), ⟪x, m i⟫_ℝ) • ((vectorFourierIntegrand ξ) f) x