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
⊢ ∫ (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) ξ
Tactic:
simp only [Real.fourierIntegral_def]
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))) •
        ∫ (v : ℝ),
          ↑(Real.fourierChar (Multiplicative.ofAdd (-(v * ξ i)))) •
            f ((Equiv.piSplitAt i fun a => ℝ).symm (0, a) + Pi.single i v) =
    𝓕ₙ (⇑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
⊢ ∫ (a : { j // ¬j = i } → ℝ),
      ↑(Real.fourierChar (Multiplicative.ofAdd (-∑ x : { x // ¬x = i }, a x * ξ ↑x))) •
        ∫ (v : ℝ),
          ↑(Real.fourierChar (Multiplicative.ofAdd (-(v * ξ i)))) •
            f ((Equiv.piSplitAt i fun a => ℝ).symm (0, a) + Pi.single i v) =
    𝓕ₙ (⇑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
⊢ ∫ (a : { j // ¬j = i } → ℝ) (a_1 : ℝ),
      ↑(Real.fourierChar (Multiplicative.ofAdd (-∑ x : { x // ¬x = i }, a x * ξ ↑x))) •
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(a_1 * ξ i)))) •
          f ((Equiv.piSplitAt i fun a => ℝ).symm (0, a) + Pi.single i a_1) =
    𝓕ₙ (⇑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
⊢ ∫ (a : { j // ¬j = i } → ℝ) (a_1 : ℝ),
      ↑(Real.fourierChar (Multiplicative.ofAdd (-∑ x : { x // ¬x = i }, a x * ξ ↑x))) •
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(a_1 * ξ i)))) •
          f ((Equiv.piSplitAt i fun a => ℝ).symm (0, a) + Pi.single i a_1) =
    𝓕ₙ (⇑f) ξ
Tactic:
simp only [smul_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
⊢ ∫ (a : { j // ¬j = i } → ℝ) (a_1 : ℝ),
      (↑(Real.fourierChar (Multiplicative.ofAdd (-∑ x : { x // ¬x = i }, a x * ξ ↑x))) *
          ↑(Real.fourierChar (Multiplicative.ofAdd (-(a_1 * ξ i))))) •
        f ((Equiv.piSplitAt i fun a => ℝ).symm (0, a) + Pi.single i a_1) =
    𝓕ₙ (⇑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
⊢ ∫ (a : { j // ¬j = i } → ℝ) (a_1 : ℝ),
      (↑(Real.fourierChar (Multiplicative.ofAdd (-∑ x : { x // ¬x = i }, a x * ξ ↑x))) *
          ↑(Real.fourierChar (Multiplicative.ofAdd (-(a_1 * ξ i))))) •
        f ((Equiv.piSplitAt i fun a => ℝ).symm (0, a) + Pi.single i a_1) =
    𝓕ₙ (⇑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)
ξ : ι → ℝ
h_mem : ∀ (j : ι), j ∈ Finset.univ \ {i} ↔ j ≠ i
⊢ ∫ (a : { j // ¬j = i } → ℝ) (a_1 : ℝ),
      (↑(Real.fourierChar (Multiplicative.ofAdd (-∑ x : { x // ¬x = i }, a x * ξ ↑x))) *
          ↑(Real.fourierChar (Multiplicative.ofAdd (-(a_1 * ξ i))))) •
        f ((Equiv.piSplitAt i fun a => ℝ).symm (0, a) + Pi.single i a_1) =
    ∫ (x : ι → ℝ), ↑(Real.fourierChar (Multiplicative.ofAdd (-∑ i : ι, x i * ξ i))) • f x
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
⊢ ∫ (a : { j // ¬j = i } → ℝ) (a_1 : ℝ),
      (↑(Real.fourierChar (Multiplicative.ofAdd (-∑ x : { x // ¬x = i }, a x * ξ ↑x))) *
          ↑(Real.fourierChar (Multiplicative.ofAdd (-(a_1 * ξ i))))) •
        f ((Equiv.piSplitAt i fun a => ℝ).symm (0, a) + Pi.single i a_1) =
    ∫ (x : { j // j ≠ i } → ℝ) (u : ℝ),
      ↑(Real.fourierChar (Multiplicative.ofAdd (-∑ i_1 : ι, (Equiv.piSplitAt i fun a => ℝ).symm (u, x) i_1 * ξ i_1))) •
        f ((Equiv.piSplitAt i fun a => ℝ).symm (u, x))
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
⊢ (fun a =>
      ∫ (a_1 : ℝ),
        (↑(Real.fourierChar (Multiplicative.ofAdd (-∑ x : { x // ¬x = i }, a x * ξ ↑x))) *
            ↑(Real.fourierChar (Multiplicative.ofAdd (-(a_1 * ξ i))))) •
          f ((Equiv.piSplitAt i fun a => ℝ).symm (0, a) + Pi.single i a_1)) =
    fun x =>
    ∫ (u : ℝ),
      ↑(Real.fourierChar (Multiplicative.ofAdd (-∑ i_1 : ι, (Equiv.piSplitAt i fun a => ℝ).symm (u, x) i_1 * ξ i_1))) •
        f ((Equiv.piSplitAt i fun a => ℝ).symm (u, x))
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
⊢ (fun a =>
      ∫ (a_1 : ℝ),
        (↑(Real.fourierChar (Multiplicative.ofAdd (-∑ x : { x // ¬x = i }, a x * ξ ↑x))) *
            ↑(Real.fourierChar (Multiplicative.ofAdd (-(a_1 * ξ i))))) •
          f ((Equiv.piSplitAt i fun a => ℝ).symm (0, a) + Pi.single i a_1)) =
    fun x =>
    ∫ (u : ℝ),
      ↑(Real.fourierChar (Multiplicative.ofAdd (-∑ i_1 : ι, (Equiv.piSplitAt i fun a => ℝ).symm (u, x) i_1 * ξ i_1))) •
        f ((Equiv.piSplitAt i fun a => ℝ).symm (u, x))
Tactic:
ext x
Proof state after:
case h
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 } → ℝ
⊢ ∫ (a : ℝ),
      (↑(Real.fourierChar (Multiplicative.ofAdd (-∑ x_1 : { x // ¬x = i }, x x_1 * ξ ↑x_1))) *
          ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ i))))) •
        f ((Equiv.piSplitAt i fun a => ℝ).symm (0, x) + Pi.single i a) =
    ∫ (u : ℝ),
      ↑(Real.fourierChar (Multiplicative.ofAdd (-∑ i_1 : ι, (Equiv.piSplitAt i fun a => ℝ).symm (u, x) i_1 * ξ i_1))) •
        f ((Equiv.piSplitAt i fun a => ℝ).symm (u, x))
Theorem: SchwartzMap.realintegral_vectorFourierIntegrand_pderivCLM_single
Proof state before:
case h
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 } → ℝ
⊢ ∫ (a : ℝ),
      (↑(Real.fourierChar (Multiplicative.ofAdd (-∑ x_1 : { x // ¬x = i }, x x_1 * ξ ↑x_1))) *
          ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ i))))) •
        f ((Equiv.piSplitAt i fun a => ℝ).symm (0, x) + Pi.single i a) =
    ∫ (u : ℝ),
      ↑(Real.fourierChar (Multiplicative.ofAdd (-∑ i_1 : ι, (Equiv.piSplitAt i fun a => ℝ).symm (u, x) i_1 * ξ i_1))) •
        f ((Equiv.piSplitAt i fun a => ℝ).symm (u, x))
Tactic:
refine congrArg _ ?_
Proof state after:
case h
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 } → ℝ
⊢ (fun a =>
      (↑(Real.fourierChar (Multiplicative.ofAdd (-∑ x_1 : { x // ¬x = i }, x x_1 * ξ ↑x_1))) *
          ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ i))))) •
        f ((Equiv.piSplitAt i fun a => ℝ).symm (0, x) + Pi.single i a)) =
    fun u =>
    ↑(Real.fourierChar (Multiplicative.ofAdd (-∑ i_1 : ι, (Equiv.piSplitAt i fun a => ℝ).symm (u, x) i_1 * ξ i_1))) •
      f ((Equiv.piSplitAt i fun a => ℝ).symm (u, x))
Theorem: SchwartzMap.realintegral_vectorFourierIntegrand_pderivCLM_single
Proof state before:
case h
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 } → ℝ
⊢ (fun a =>
      (↑(Real.fourierChar (Multiplicative.ofAdd (-∑ x_1 : { x // ¬x = i }, x x_1 * ξ ↑x_1))) *
          ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ i))))) •
        f ((Equiv.piSplitAt i fun a => ℝ).symm (0, x) + Pi.single i a)) =
    fun u =>
    ↑(Real.fourierChar (Multiplicative.ofAdd (-∑ i_1 : ι, (Equiv.piSplitAt i fun a => ℝ).symm (u, x) i_1 * ξ i_1))) •
      f ((Equiv.piSplitAt i fun a => ℝ).symm (u, x))
Tactic:
ext u
Proof state after:
case h.h
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))))) •
      f ((Equiv.piSplitAt i fun a => ℝ).symm (0, x) + Pi.single i u) =
    ↑(Real.fourierChar (Multiplicative.ofAdd (-∑ i_1 : ι, (Equiv.piSplitAt i fun a => ℝ).symm (u, x) i_1 * ξ i_1))) •
      f ((Equiv.piSplitAt i fun a => ℝ).symm (u, x))
Theorem: SchwartzMap.realintegral_vectorFourierIntegrand_pderivCLM_single
Proof state before:
case h.h.e_a.h.e_6.h
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 : ℝ
⊢ (Equiv.piSplitAt i fun a => ℝ).symm (0, x) + Pi.single i u = (Equiv.piSplitAt i fun a => ℝ).symm (u, x)
Tactic:
. rw [Equiv.piSplitAt_symm_zero_add_single]
Proof state after:
no goals