internlm/Lean-Github huggingface dataset:
Theorem: SchwartzMap.realFourierIntegral_deriv
Proof state before:
case refine_2.refine_2
E' : Type ?u.1169414
ι : 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 : 𝓢(ℝ, F)
ξ : ℝ
h_cover : AECover volume Filter.atTop fun i => Set.Ioc (-↑i) ↑i
⊢ Filter.Tendsto ((fun x => ((realFourierIntegrand ξ) f) (-x)) ∘ fun n => ↑n) Filter.atTop (nhds 0)
Tactic:
refine Filter.Tendsto.comp ?_ tendsto_nat_cast_atTop_atTop
Proof state after:
case refine_2.refine_2
E' : Type ?u.1169414
ι : 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 : 𝓢(ℝ, F)
ξ : ℝ
h_cover : AECover volume Filter.atTop fun i => Set.Ioc (-↑i) ↑i
⊢ Filter.Tendsto (fun x => ((realFourierIntegrand ξ) f) (-x)) Filter.atTop (nhds 0)
Theorem: SchwartzMap.realFourierIntegral_deriv
Proof state before:
case refine_2.refine_2
E' : Type ?u.1169414
ι : 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 : 𝓢(ℝ, F)
ξ : ℝ
h_cover : AECover volume Filter.atTop fun i => Set.Ioc (-↑i) ↑i
⊢ Filter.Tendsto (fun x => ((realFourierIntegrand ξ) f) (-x)) Filter.atTop (nhds 0)
Tactic:
simp_rw [← compNegEquiv_apply]
Proof state after:
case refine_2.refine_2
E' : Type ?u.1169414
ι : 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 : 𝓢(ℝ, F)
ξ : ℝ
h_cover : AECover volume Filter.atTop fun i => Set.Ioc (-↑i) ↑i
⊢ Filter.Tendsto (fun x => (compNegEquiv ((realFourierIntegrand ξ) f)) x) Filter.atTop (nhds 0)
Theorem: SchwartzMap.realFourierIntegral_deriv
Proof state before:
case refine_2.refine_2
E' : Type ?u.1169414
ι : 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 : 𝓢(ℝ, F)
ξ : ℝ
h_cover : AECover volume Filter.atTop fun i => Set.Ioc (-↑i) ↑i
⊢ Filter.Tendsto (fun x => (compNegEquiv ((realFourierIntegrand ξ) f)) x) Filter.atTop (nhds 0)
Tactic:
exact tendsto_atTop_zero_real (compNegEquiv (realFourierIntegrand ξ f))
Proof state after:
no goals
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)
ξ : ι → ℝ
⊢ 𝓕ₙ (⇑((pderivCLM ℝ (Pi.single i 1)) f)) ξ = (2 * ↑π * I * ↑(ξ i)) • 𝓕ₙ (⇑f) ξ
Tactic:
rw [RealVectorFourier.fourierIntegral_l2inner_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)
ξ : ι → ℝ
⊢ ∫ (x : ι → ℝ),
      ↑(Real.fourierChar (Multiplicative.ofAdd (-∑ i : ι, x i * ξ i))) • ((pderivCLM ℝ (Pi.single i 1)) f) x =
    (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)
ξ : ι → ℝ
⊢ ∫ (x : { j // j ≠ i } → ℝ) (u : ℝ),
      ↑(Real.fourierChar (Multiplicative.ofAdd (-∑ i_1 : ι, (Equiv.piSplitAt i fun a => ℝ).symm (u, x) i_1 * ξ i_1))) •
        ((pderivCLM ℝ (Pi.single i 1)) f) ((Equiv.piSplitAt i fun a => ℝ).symm (u, x)) =
    (2 * ↑π * I * ↑(ξ i)) • 𝓕ₙ (⇑f) ξ
Tactic:
have h_mem (j) : j ∈ Finset.univ \ {i} ↔ j ≠ i := by simp
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 } → ℝ) (u : ℝ),
      ↑(Real.fourierChar (Multiplicative.ofAdd (-∑ i_1 : ι, (Equiv.piSplitAt i fun a => ℝ).symm (u, x) i_1 * ξ i_1))) •
        ((pderivCLM ℝ (Pi.single i 1)) f) ((Equiv.piSplitAt i fun a => ℝ).symm (u, x)) =
    (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 } → ℝ) (u : ℝ),
      ↑(Real.fourierChar (Multiplicative.ofAdd (-∑ i_1 : ι, (Equiv.piSplitAt i fun a => ℝ).symm (u, x) i_1 * ξ i_1))) •
        ((pderivCLM ℝ (Pi.single i 1)) f) ((Equiv.piSplitAt i fun a => ℝ).symm (u, x)) =
    (2 * ↑π * I * ↑(ξ i)) • 𝓕ₙ (⇑f) ξ
Tactic:
conv => lhs; simp only [Finset.sum_eq_add_sum_diff_singleton (Finset.mem_univ i)]
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 } → ℝ) (u : ℝ),
      ↑(Real.fourierChar
            (Multiplicative.ofAdd
              (-((Equiv.piSplitAt i fun a => ℝ).symm (u, x) i * ξ i +
                  ∑ i_1 in Finset.univ \ {i}, (Equiv.piSplitAt i fun a => ℝ).symm (u, x) i_1 * ξ i_1)))) •
        ((pderivCLM ℝ (Pi.single i 1)) f) ((Equiv.piSplitAt i fun a => ℝ).symm (u, x)) =
    (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 } → ℝ) (u : ℝ),
      ↑(Real.fourierChar
            (Multiplicative.ofAdd
              (-((Equiv.piSplitAt i fun a => ℝ).symm (u, x) i * ξ i +
                  ∑ i_1 in Finset.univ \ {i}, (Equiv.piSplitAt i fun a => ℝ).symm (u, x) i_1 * ξ i_1)))) •
        ((pderivCLM ℝ (Pi.single i 1)) f) ((Equiv.piSplitAt i fun a => ℝ).symm (u, x)) =
    (2 * ↑π * I * ↑(ξ i)) • 𝓕ₙ (⇑f) ξ
Tactic:
simp only [dite_true, Finset.sum_subtype _ h_mem]
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 } → ℝ) (u : ℝ),
      ↑(Real.fourierChar
            (Multiplicative.ofAdd
              (-((Equiv.piSplitAt i fun a => ℝ).symm (u, x) i * ξ i +
                  ∑ a : { x // x ≠ i }, (Equiv.piSplitAt i fun a => ℝ).symm (u, x) ↑a * ξ ↑a)))) •
        ((pderivCLM ℝ (Pi.single i 1)) f) ((Equiv.piSplitAt i fun a => ℝ).symm (u, x)) =
    (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 } → ℝ) (u : ℝ),
      ↑(Real.fourierChar
            (Multiplicative.ofAdd
              (-((Equiv.piSplitAt i fun a => ℝ).symm (u, x) i * ξ i +
                  ∑ a : { x // x ≠ i }, (Equiv.piSplitAt i fun a => ℝ).symm (u, x) ↑a * ξ ↑a)))) •
        ((pderivCLM ℝ (Pi.single i 1)) f) ((Equiv.piSplitAt i fun a => ℝ).symm (u, x)) =
    (2 * ↑π * I * ↑(ξ i)) • 𝓕ₙ (⇑f) ξ
Tactic:
simp [Finset.sum_ite]
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 } → ℝ) (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) ξ
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:
conv => lhs; arg 2; intro x; arg 2; intro u; lhs; rw [← smul_eq_mul]
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 } → ℝ) (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) ξ
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 [smul_assoc]
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 } → ℝ) (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) ξ