internlm/Lean-Github huggingface dataset:
Theorem: SchwartzMap.realintegral_vectorFourierIntegrand_pderivCLM_single
Proof state before:
E' : Type ?u.1249490
ι : 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
i : ι
f : 𝓢(ι → ℝ, F)
ξ : ι → ℝ
h_mem : ∀ (j : ι), j ∈ Finset.univ \ {i} ↔ j ≠ i
⊢ ∫ (x : { j // ¬j = i } → ℝ) (u : ℝ),
      ↑(Real.fourierChar (Multiplicative.ofAdd (-∑ x_1 : { x // ¬x = i }, x x_1 * ξ ↑x_1))) •
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(u * ξ i)))) •
          (fderiv ℝ (⇑f) ((Equiv.piSplitAt i fun a => ℝ).symm (u, x))) (Pi.single i 1) =
    (2 * ↑π * I * ↑(ξ i)) • 𝓕ₙ (⇑f) ξ
Tactic:
simp only [integral_smul]
Proof state after:
E' : Type ?u.1249490
ι : 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
i : ι
f : 𝓢(ι → ℝ, F)
ξ : ι → ℝ
h_mem : ∀ (j : ι), j ∈ Finset.univ \ {i} ↔ j ≠ i
⊢ ∫ (x : { j // ¬j = i } → ℝ),
      ↑(Real.fourierChar (Multiplicative.ofAdd (-∑ x_1 : { x // ¬x = i }, x x_1 * ξ ↑x_1))) •
        ∫ (a : ℝ),
          ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ i)))) •
            (fderiv ℝ (⇑f) ((Equiv.piSplitAt i fun a => ℝ).symm (a, x))) (Pi.single i 1) =
    (2 * ↑π * I * ↑(ξ i)) • 𝓕ₙ (⇑f) ξ
Theorem: SchwartzMap.realintegral_vectorFourierIntegrand_pderivCLM_single
Proof state before:
E' : Type ?u.1249490
ι : 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
i : ι
f : 𝓢(ι → ℝ, F)
ξ : ι → ℝ
h_mem : ∀ (j : ι), j ∈ Finset.univ \ {i} ↔ j ≠ i
⊢ ∫ (x : { j // ¬j = i } → ℝ),
      ↑(Real.fourierChar (Multiplicative.ofAdd (-∑ x_1 : { x // ¬x = i }, x x_1 * ξ ↑x_1))) •
        ∫ (a : ℝ),
          ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ i)))) •
            (fderiv ℝ (⇑f) ((Equiv.piSplitAt i fun a => ℝ).symm (a, x))) (Pi.single i 1) =
    (2 * ↑π * I * ↑(ξ i)) • 𝓕ₙ (⇑f) ξ
Tactic:
simp only [← deriv_comp_update (f.differentiableAt)]
Proof state after:
E' : Type ?u.1249490
ι : 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
i : ι
f : 𝓢(ι → ℝ, F)
ξ : ι → ℝ
h_mem : ∀ (j : ι), j ∈ Finset.univ \ {i} ↔ j ≠ i
⊢ ∫ (x : { j // ¬j = i } → ℝ),
      ↑(Real.fourierChar (Multiplicative.ofAdd (-∑ x_1 : { x // ¬x = i }, x x_1 * ξ ↑x_1))) •
        ∫ (a : ℝ),
          ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ i)))) •
            deriv (fun u => f (Function.update ((Equiv.piSplitAt i fun a => ℝ).symm (a, x)) i u))
              ((Equiv.piSplitAt i fun a => ℝ).symm (a, x) i) =
    (2 * ↑π * I * ↑(ξ i)) • 𝓕ₙ (⇑f) ξ
Theorem: SchwartzMap.realintegral_vectorFourierIntegrand_pderivCLM_single
Proof state before:
E' : Type ?u.1249490
ι : 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
i : ι
f : 𝓢(ι → ℝ, F)
ξ : ι → ℝ
h_mem : ∀ (j : ι), j ∈ Finset.univ \ {i} ↔ j ≠ i
⊢ ∫ (x : { j // ¬j = i } → ℝ),
      ↑(Real.fourierChar (Multiplicative.ofAdd (-∑ x_1 : { x // ¬x = i }, x x_1 * ξ ↑x_1))) •
        ∫ (a : ℝ),
          ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ i)))) •
            deriv (fun u => f (Function.update ((Equiv.piSplitAt i fun a => ℝ).symm (a, x)) i u))
              ((Equiv.piSplitAt i fun a => ℝ).symm (a, x) i) =
    (2 * ↑π * I * ↑(ξ i)) • 𝓕ₙ (⇑f) ξ
Tactic:
simp only [Equiv.piSplitAt_symm_apply (j := i), dite_true]
Proof state after:
E' : Type ?u.1249490
ι : 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
i : ι
f : 𝓢(ι → ℝ, F)
ξ : ι → ℝ
h_mem : ∀ (j : ι), j ∈ Finset.univ \ {i} ↔ j ≠ i
⊢ ∫ (x : { j // ¬j = i } → ℝ),
      ↑(Real.fourierChar (Multiplicative.ofAdd (-∑ x_1 : { x // ¬x = i }, x x_1 * ξ ↑x_1))) •
        ∫ (a : ℝ),
          ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ i)))) •
            deriv (fun u => f (Function.update ((Equiv.piSplitAt i fun a => ℝ).symm (a, x)) i u)) a =
    (2 * ↑π * I * ↑(ξ i)) • 𝓕ₙ (⇑f) ξ
Theorem: SchwartzMap.realintegral_vectorFourierIntegrand_pderivCLM_single
Proof state before:
E' : Type ?u.1249490
ι : 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
i : ι
f : 𝓢(ι → ℝ, F)
ξ : ι → ℝ
h_mem : ∀ (j : ι), j ∈ Finset.univ \ {i} ↔ j ≠ i
⊢ ∫ (x : { j // ¬j = i } → ℝ),
      ↑(Real.fourierChar (Multiplicative.ofAdd (-∑ x_1 : { x // ¬x = i }, x x_1 * ξ ↑x_1))) •
        ∫ (a : ℝ),
          ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ i)))) •
            deriv (fun u => f (Function.update ((Equiv.piSplitAt i fun a => ℝ).symm (a, x)) i u)) a =
    (2 * ↑π * I * ↑(ξ i)) • 𝓕ₙ (⇑f) ξ
Tactic:
simp only [Function.update_piSplitAt_symm]
Proof state after:
E' : Type ?u.1249490
ι : 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
i : ι
f : 𝓢(ι → ℝ, F)
ξ : ι → ℝ
h_mem : ∀ (j : ι), j ∈ Finset.univ \ {i} ↔ j ≠ i
⊢ ∫ (x : { j // ¬j = i } → ℝ),
      ↑(Real.fourierChar (Multiplicative.ofAdd (-∑ x_1 : { x // ¬x = i }, x x_1 * ξ ↑x_1))) •
        ∫ (a : ℝ),
          ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ i)))) •
            deriv (fun u => f ((Equiv.piSplitAt i fun a => ℝ).symm (u, x))) a =
    (2 * ↑π * I * ↑(ξ i)) • 𝓕ₙ (⇑f) ξ
Theorem: SchwartzMap.realintegral_vectorFourierIntegrand_pderivCLM_single
Proof state before:
E' : Type ?u.1249490
ι : 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
i : ι
f : 𝓢(ι → ℝ, F)
ξ : ι → ℝ
h_mem : ∀ (j : ι), j ∈ Finset.univ \ {i} ↔ j ≠ i
⊢ ∫ (x : { j // ¬j = i } → ℝ),
      ↑(Real.fourierChar (Multiplicative.ofAdd (-∑ x_1 : { x // ¬x = i }, x x_1 * ξ ↑x_1))) •
        ∫ (a : ℝ),
          ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ i)))) •
            deriv (fun u => f ((Equiv.piSplitAt i fun a => ℝ).symm (u, x))) a =
    (2 * ↑π * I * ↑(ξ i)) • 𝓕ₙ (⇑f) ξ
Tactic:
conv =>
  lhs; arg 2; intro x; rhs
  conv =>
    arg 2; intro y; rhs; arg 1; intro u
    rw [← Equiv.piSplitAt_symm_zero_add_single]
    rw [← compConstAddCLM_apply]
    rw [← compSingleCLM_apply]
  rw [← Real.fourierIntegral_def]
  rw [realFourierIntegral_deriv]
Proof state after:
E' : Type ?u.1249490
ι : 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
i : ι
f : 𝓢(ι → ℝ, F)
ξ : ι → ℝ
h_mem : ∀ (j : ι), j ∈ Finset.univ \ {i} ↔ j ≠ i
⊢ ∫ (x : { j // ¬j = i } → ℝ),
      ↑(Real.fourierChar (Multiplicative.ofAdd (-∑ x_1 : { x // ¬x = i }, x x_1 * ξ ↑x_1))) •
        (2 * ↑π * I * ↑(ξ i)) •
          𝓕 (fun x_1 => ((compSingleCLM i) ((compConstAddCLM ((Equiv.piSplitAt i fun a => ℝ).symm (0, x))) f)) x_1)
            (ξ i) =
    (2 * ↑π * I * ↑(ξ i)) • 𝓕ₙ (⇑f) ξ
Theorem: SchwartzMap.realintegral_vectorFourierIntegrand_pderivCLM_single
Proof state before:
E' : Type ?u.1249490
ι : 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
i : ι
f : 𝓢(ι → ℝ, F)
ξ : ι → ℝ
h_mem : ∀ (j : ι), j ∈ Finset.univ \ {i} ↔ j ≠ i
⊢ ∫ (x : { j // ¬j = i } → ℝ),
      ↑(Real.fourierChar (Multiplicative.ofAdd (-∑ x_1 : { x // ¬x = i }, x x_1 * ξ ↑x_1))) •
        (2 * ↑π * I * ↑(ξ i)) •
          𝓕 (fun x_1 => ((compSingleCLM i) ((compConstAddCLM ((Equiv.piSplitAt i fun a => ℝ).symm (0, x))) f)) x_1)
            (ξ i) =
    (2 * ↑π * I * ↑(ξ i)) • 𝓕ₙ (⇑f) ξ
Tactic:
simp only [compConstAddCLM_apply, compSingleCLM_apply]
Proof state after:
E' : Type ?u.1249490
ι : 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
i : ι
f : 𝓢(ι → ℝ, F)
ξ : ι → ℝ
h_mem : ∀ (j : ι), j ∈ Finset.univ \ {i} ↔ j ≠ i
⊢ ∫ (x : { j // ¬j = i } → ℝ),
      ↑(Real.fourierChar (Multiplicative.ofAdd (-∑ x_1 : { x // ¬x = i }, x x_1 * ξ ↑x_1))) •
        (2 * ↑π * I * ↑(ξ i)) • 𝓕 (fun x_1 => f ((Equiv.piSplitAt i fun a => ℝ).symm (0, x) + Pi.single i x_1)) (ξ i) =
    (2 * ↑π * I * ↑(ξ i)) • 𝓕ₙ (⇑f) ξ
Theorem: SchwartzMap.realintegral_vectorFourierIntegrand_pderivCLM_single
Proof state before:
E' : Type ?u.1249490
ι : 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
i : ι
f : 𝓢(ι → ℝ, F)
ξ : ι → ℝ
h_mem : ∀ (j : ι), j ∈ Finset.univ \ {i} ↔ j ≠ i
⊢ ∫ (x : { j // ¬j = i } → ℝ),
      ↑(Real.fourierChar (Multiplicative.ofAdd (-∑ x_1 : { x // ¬x = i }, x x_1 * ξ ↑x_1))) •
        (2 * ↑π * I * ↑(ξ i)) • 𝓕 (fun x_1 => f ((Equiv.piSplitAt i fun a => ℝ).symm (0, x) + Pi.single i x_1)) (ξ i) =
    (2 * ↑π * I * ↑(ξ i)) • 𝓕ₙ (⇑f) ξ
Tactic:
conv => lhs; arg 2; intro x; rw [smul_comm]
Proof state after:
E' : Type ?u.1249490
ι : 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
i : ι
f : 𝓢(ι → ℝ, F)
ξ : ι → ℝ
h_mem : ∀ (j : ι), j ∈ Finset.univ \ {i} ↔ j ≠ i
⊢ ∫ (x : { j // ¬j = i } → ℝ),
      (2 * ↑π * I * ↑(ξ i)) •
        ↑(Real.fourierChar (Multiplicative.ofAdd (-∑ x_1 : { x // ¬x = i }, x x_1 * ξ ↑x_1))) •
          𝓕 (fun x_1 => f ((Equiv.piSplitAt i fun a => ℝ).symm (0, x) + Pi.single i x_1)) (ξ i) =
    (2 * ↑π * I * ↑(ξ i)) • 𝓕ₙ (⇑f) ξ
Theorem: SchwartzMap.realintegral_vectorFourierIntegrand_pderivCLM_single
Proof state before:
E' : Type ?u.1249490
ι : 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
i : ι
f : 𝓢(ι → ℝ, F)
ξ : ι → ℝ
h_mem : ∀ (j : ι), j ∈ Finset.univ \ {i} ↔ j ≠ i
⊢ ∫ (x : { j // ¬j = i } → ℝ),
      (2 * ↑π * I * ↑(ξ i)) •
        ↑(Real.fourierChar (Multiplicative.ofAdd (-∑ x_1 : { x // ¬x = i }, x x_1 * ξ ↑x_1))) •
          𝓕 (fun x_1 => f ((Equiv.piSplitAt i fun a => ℝ).symm (0, x) + Pi.single i x_1)) (ξ i) =
    (2 * ↑π * I * ↑(ξ i)) • 𝓕ₙ (⇑f) ξ
Tactic:
rw [integral_smul]
Proof state after:
E' : Type ?u.1249490
ι : 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
i : ι
f : 𝓢(ι → ℝ, F)
ξ : ι → ℝ
h_mem : ∀ (j : ι), j ∈ Finset.univ \ {i} ↔ j ≠ i
⊢ (2 * ↑π * I * ↑(ξ i)) •
      ∫ (a : { j // ¬j = i } → ℝ),
        ↑(Real.fourierChar (Multiplicative.ofAdd (-∑ x : { x // ¬x = i }, a x * ξ ↑x))) •
          𝓕 (fun x => f ((Equiv.piSplitAt i fun a => ℝ).symm (0, a) + Pi.single i x)) (ξ i) =
    (2 * ↑π * I * ↑(ξ i)) • 𝓕ₙ (⇑f) ξ
Theorem: SchwartzMap.realintegral_vectorFourierIntegrand_pderivCLM_single
Proof state before:
E' : Type ?u.1249490
ι : 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
i : ι
f : 𝓢(ι → ℝ, F)
ξ : ι → ℝ
h_mem : ∀ (j : ι), j ∈ Finset.univ \ {i} ↔ j ≠ i
⊢ (2 * ↑π * I * ↑(ξ i)) •
      ∫ (a : { j // ¬j = i } → ℝ),
        ↑(Real.fourierChar (Multiplicative.ofAdd (-∑ x : { x // ¬x = i }, a x * ξ ↑x))) •
          𝓕 (fun x => f ((Equiv.piSplitAt i fun a => ℝ).symm (0, a) + Pi.single i x)) (ξ i) =
    (2 * ↑π * I * ↑(ξ i)) • 𝓕ₙ (⇑f) ξ
Tactic:
refine congrArg _ ?_
Proof state after:
E' : Type ?u.1249490
ι : 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
i : ι
f : 𝓢(ι → ℝ, F)
ξ : ι → ℝ
h_mem : ∀ (j : ι), j ∈ Finset.univ \ {i} ↔ j ≠ i
⊢ ∫ (a : { j // ¬j = i } → ℝ),
      ↑(Real.fourierChar (Multiplicative.ofAdd (-∑ x : { x // ¬x = i }, a x * ξ ↑x))) •
        𝓕 (fun x => f ((Equiv.piSplitAt i fun a => ℝ).symm (0, a) + Pi.single i x)) (ξ i) =
    𝓕ₙ (⇑f) ξ