internlm/Lean-Github huggingface dataset:
Theorem: SchwartzMap.Real.intervalIntegral_fourierIntegrand_deriv_sub_smul_fourierIntegrand
Proof state before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ a b : ℝ
this :
  ∫ (x : ℝ) in a..b,
      (-ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x +
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (⇑f) x =
    ↑(Real.fourierChar (Multiplicative.ofAdd (-(b * ξ)))) • f b -
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • f a
x : ℝ
a✝ : x ∈ Set.uIcc a b
⊢ (fun x =>
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (fun y => f y) x -
          (2 * ↑π * I * ↑ξ) • ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • f x)
      x =
    (fun x =>
        (-ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x +
          ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (⇑f) x)
      x
Tactic:
simp only
Proof state after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ a b : ℝ
this :
  ∫ (x : ℝ) in a..b,
      (-ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x +
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (⇑f) x =
    ↑(Real.fourierChar (Multiplicative.ofAdd (-(b * ξ)))) • f b -
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • f a
x : ℝ
a✝ : x ∈ Set.uIcc a b
⊢ ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (fun y => f y) x -
      (2 * ↑π * I * ↑ξ) • ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • f x =
    (-ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x +
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (⇑f) x
Theorem: SchwartzMap.Real.intervalIntegral_fourierIntegrand_deriv_sub_smul_fourierIntegrand
Proof state before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ a b : ℝ
this :
  ∫ (x : ℝ) in a..b,
      (-ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x +
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (⇑f) x =
    ↑(Real.fourierChar (Multiplicative.ofAdd (-(b * ξ)))) • f b -
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • f a
x : ℝ
a✝ : x ∈ Set.uIcc a b
⊢ ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (fun y => f y) x -
      (2 * ↑π * I * ↑ξ) • ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • f x =
    (-ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x +
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (⇑f) x
Tactic:
rw [sub_eq_neg_add, add_left_inj]
Proof state after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ a b : ℝ
this :
  ∫ (x : ℝ) in a..b,
      (-ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x +
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (⇑f) x =
    ↑(Real.fourierChar (Multiplicative.ofAdd (-(b * ξ)))) • f b -
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • f a
x : ℝ
a✝ : x ∈ Set.uIcc a b
⊢ -((2 * ↑π * I * ↑ξ) • ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • f x) =
    (-ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x
Theorem: SchwartzMap.Real.intervalIntegral_fourierIntegrand_deriv_sub_smul_fourierIntegrand
Proof state before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ a b : ℝ
this :
  ∫ (x : ℝ) in a..b,
      (-ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x +
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (⇑f) x =
    ↑(Real.fourierChar (Multiplicative.ofAdd (-(b * ξ)))) • f b -
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • f a
x : ℝ
a✝ : x ∈ Set.uIcc a b
⊢ -((2 * ↑π * I * ↑ξ) • ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • f x) =
    (-ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x
Tactic:
simp only [neg_smul, neg_inj]
Proof state after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ a b : ℝ
this :
  ∫ (x : ℝ) in a..b,
      (-ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x +
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (⇑f) x =
    ↑(Real.fourierChar (Multiplicative.ofAdd (-(b * ξ)))) • f b -
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • f a
x : ℝ
a✝ : x ∈ Set.uIcc a b
⊢ (2 * ↑π * I * ↑ξ) • ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • f x =
    (ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x
Theorem: SchwartzMap.Real.intervalIntegral_fourierIntegrand_deriv_sub_smul_fourierIntegrand
Proof state before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ a b : ℝ
this :
  ∫ (x : ℝ) in a..b,
      (-ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x +
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (⇑f) x =
    ↑(Real.fourierChar (Multiplicative.ofAdd (-(b * ξ)))) • f b -
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • f a
x : ℝ
a✝ : x ∈ Set.uIcc a b
⊢ (2 * ↑π * I * ↑ξ) • ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • f x =
    (ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x
Tactic:
rw [Complex.real_smul, smul_smul]
Proof state after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ a b : ℝ
this :
  ∫ (x : ℝ) in a..b,
      (-ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x +
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (⇑f) x =
    ↑(Real.fourierChar (Multiplicative.ofAdd (-(b * ξ)))) • f b -
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • f a
x : ℝ
a✝ : x ∈ Set.uIcc a b
⊢ (2 * ↑π * I * ↑ξ * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ))))) • f x =
    (↑ξ * (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x
Theorem: SchwartzMap.Real.intervalIntegral_fourierIntegrand_deriv_sub_smul_fourierIntegrand
Proof state before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ a b : ℝ
this :
  ∫ (x : ℝ) in a..b,
      (-ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x +
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (⇑f) x =
    ↑(Real.fourierChar (Multiplicative.ofAdd (-(b * ξ)))) • f b -
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • f a
x : ℝ
a✝ : x ∈ Set.uIcc a b
⊢ (2 * ↑π * I * ↑ξ * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ))))) • f x =
    (↑ξ * (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x
Tactic:
exact congrArg₂ _ (by ring) rfl
Proof state after:
no goals
Theorem: SchwartzMap.Real.intervalIntegral_fourierIntegrand_deriv_sub_smul_fourierIntegrand
Proof state before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ a b : ℝ
⊢ ContinuousOn (fun x => deriv (⇑f) x) (Set.uIcc a b)
Tactic:
simpa [derivCLM_apply ℝ] using (derivCLM ℝ f).continuous.continuousOn
Proof state after:
no goals
Theorem: SchwartzMap.Real.intervalIntegral_fourierIntegrand_deriv_sub_smul_fourierIntegrand
Proof state before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ a b : ℝ
this :
  ∫ (x : ℝ) in a..b,
      (-ξ • (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))) • f x +
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (⇑f) x =
    ↑(Real.fourierChar (Multiplicative.ofAdd (-(b * ξ)))) • f b -
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • f a
x : ℝ
a✝ : x ∈ Set.uIcc a b
⊢ 2 * ↑π * I * ↑ξ * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) =
    ↑ξ * (2 * ↑π * I * ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))))
Tactic:
ring
Proof state after:
no goals
Theorem: SchwartzMap.Real.fourierIntegral_deriv
Proof state before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ 𝓕 (fun x => deriv (fun y => f y) x) ξ = (2 * ↑π * I * ↑ξ) • 𝓕 (fun x => f x) ξ
Tactic:
rw [← sub_eq_zero]
Proof state after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ 𝓕 (fun x => deriv (fun y => f y) x) ξ - (2 * ↑π * I * ↑ξ) • 𝓕 (fun x => f x) ξ = 0
Theorem: SchwartzMap.Real.fourierIntegral_deriv
Proof state before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ 𝓕 (fun x => deriv (fun y => f y) x) ξ - (2 * ↑π * I * ↑ξ) • 𝓕 (fun x => f x) ξ = 0
Tactic:
simp only [Real.fourierIntegral_def]
Proof state after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ (∫ (v : ℝ), ↑(Real.fourierChar (Multiplicative.ofAdd (-(v * ξ)))) • deriv (fun y => f y) v) -
      (2 * ↑π * I * ↑ξ) • ∫ (v : ℝ), ↑(Real.fourierChar (Multiplicative.ofAdd (-(v * ξ)))) • f v =
    0
Theorem: SchwartzMap.Real.fourierIntegral_deriv
Proof state before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ (∫ (v : ℝ), ↑(Real.fourierChar (Multiplicative.ofAdd (-(v * ξ)))) • deriv (fun y => f y) v) -
      (2 * ↑π * I * ↑ξ) • ∫ (v : ℝ), ↑(Real.fourierChar (Multiplicative.ofAdd (-(v * ξ)))) • f v =
    0
Tactic:
rw [← integral_smul]
Proof state after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ (∫ (v : ℝ), ↑(Real.fourierChar (Multiplicative.ofAdd (-(v * ξ)))) • deriv (fun y => f y) v) -
      ∫ (a : ℝ), (2 * ↑π * I * ↑ξ) • ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • f a =
    0
Theorem: SchwartzMap.Real.fourierIntegral_deriv
Proof state before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ (∫ (v : ℝ), ↑(Real.fourierChar (Multiplicative.ofAdd (-(v * ξ)))) • deriv (fun y => f y) v) -
      ∫ (a : ℝ), (2 * ↑π * I * ↑ξ) • ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • f a =
    0
Tactic:
simp only [← derivCLM_apply (𝕜 := ℝ)]
Proof state after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ (∫ (v : ℝ), ↑(Real.fourierChar (Multiplicative.ofAdd (-(v * ξ)))) • ((derivCLM ℝ) f) v) -
      ∫ (a : ℝ), (2 * ↑π * I * ↑ξ) • ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • f a =
    0
Theorem: SchwartzMap.Real.fourierIntegral_deriv
Proof state before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ (∫ (v : ℝ), ↑(Real.fourierChar (Multiplicative.ofAdd (-(v * ξ)))) • ((derivCLM ℝ) f) v) -
      ∫ (a : ℝ), (2 * ↑π * I * ↑ξ) • ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • f a =
    0
Tactic:
rw [← integral_sub (integrable_fourierIntegrand _ ξ) ((integrable_fourierIntegrand f ξ).smul' _)]
Proof state after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ ∫ (a : ℝ),
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • ((derivCLM ℝ) f) a -
        (2 * ↑π * I * ↑ξ) • ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • f a =
    0
Theorem: SchwartzMap.Real.fourierIntegral_deriv
Proof state before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ ∫ (a : ℝ),
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • ((derivCLM ℝ) f) a -
        (2 * ↑π * I * ↑ξ) • ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • f a =
    0
Tactic:
have h_cover : AECover volume Filter.atTop (fun i => Set.Ioc (-i) i : ℕ → Set ℝ)
Proof state after:
case h_cover
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ AECover volume Filter.atTop fun i => Set.Ioc (-↑i) ↑i

F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
h_cover : AECover volume Filter.atTop fun i => Set.Ioc (-↑i) ↑i
⊢ ∫ (a : ℝ),
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • ((derivCLM ℝ) f) a -
        (2 * ↑π * I * ↑ξ) • ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • f a =
    0
Theorem: SchwartzMap.Real.fourierIntegral_deriv
Proof state before:
case h_cover
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
⊢ AECover volume Filter.atTop fun i => Set.Ioc (-↑i) ↑i

F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
h_cover : AECover volume Filter.atTop fun i => Set.Ioc (-↑i) ↑i
⊢ ∫ (a : ℝ),
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • ((derivCLM ℝ) f) a -
        (2 * ↑π * I * ↑ξ) • ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • f a =
    0
Tactic:
. refine aecover_Ioc ?_ ?_ <;> simp [Filter.tendsto_neg_atBot_iff, tendsto_nat_cast_atTop_atTop]
Proof state after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
h_cover : AECover volume Filter.atTop fun i => Set.Ioc (-↑i) ↑i
⊢ ∫ (a : ℝ),
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • ((derivCLM ℝ) f) a -
        (2 * ↑π * I * ↑ξ) • ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • f a =
    0
Theorem: SchwartzMap.Real.fourierIntegral_deriv
Proof state before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
h_cover : AECover volume Filter.atTop fun i => Set.Ioc (-↑i) ↑i
⊢ ∫ (a : ℝ),
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • ((derivCLM ℝ) f) a -
        (2 * ↑π * I * ↑ξ) • ↑(Real.fourierChar (Multiplicative.ofAdd (-(a * ξ)))) • f a =
    0
Tactic:
refine AECover.integral_eq_of_tendsto h_cover _
  (.sub (integrable_fourierIntegrand _ ξ) ((integrable_fourierIntegrand f ξ).smul' _)) ?_
Proof state after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
h_cover : AECover volume Filter.atTop fun i => Set.Ioc (-↑i) ↑i
⊢ Filter.Tendsto
    (fun n =>
      ∫ (x : ℝ) in Set.Ioc (-↑n) ↑n,
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • ((derivCLM ℝ) f) x -
          (2 * ↑π * I * ↑ξ) • ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • f x)
    Filter.atTop (nhds 0)
Theorem: SchwartzMap.Real.fourierIntegral_deriv
Proof state before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
h_cover : AECover volume Filter.atTop fun i => Set.Ioc (-↑i) ↑i
⊢ Filter.Tendsto
    (fun n =>
      ∫ (x : ℝ) in Set.Ioc (-↑n) ↑n,
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • ((derivCLM ℝ) f) x -
          (2 * ↑π * I * ↑ξ) • ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • f x)
    Filter.atTop (nhds 0)
Tactic:
simp only [← intervalIntegral.integral_of_le (neg_le_self_iff.mpr (Nat.cast_nonneg _))]
Proof state after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
h_cover : AECover volume Filter.atTop fun i => Set.Ioc (-↑i) ↑i
⊢ Filter.Tendsto
    (fun n =>
      ∫ (x : ℝ) in -↑n..↑n,
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • ((derivCLM ℝ) f) x -
          (2 * ↑π * I * ↑ξ) • ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • f x)
    Filter.atTop (nhds 0)
Theorem: SchwartzMap.Real.fourierIntegral_deriv
Proof state before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
h_cover : AECover volume Filter.atTop fun i => Set.Ioc (-↑i) ↑i
⊢ Filter.Tendsto
    (fun n =>
      ∫ (x : ℝ) in -↑n..↑n,
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • ((derivCLM ℝ) f) x -
          (2 * ↑π * I * ↑ξ) • ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • f x)
    Filter.atTop (nhds 0)
Tactic:
simp only [derivCLM_apply]
Proof state after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
h_cover : AECover volume Filter.atTop fun i => Set.Ioc (-↑i) ↑i
⊢ Filter.Tendsto
    (fun n =>
      ∫ (x : ℝ) in -↑n..↑n,
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (⇑f) x -
          (2 * ↑π * I * ↑ξ) • ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • f x)
    Filter.atTop (nhds 0)
Theorem: SchwartzMap.Real.fourierIntegral_deriv
Proof state before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
h_cover : AECover volume Filter.atTop fun i => Set.Ioc (-↑i) ↑i
⊢ Filter.Tendsto
    (fun n =>
      ∫ (x : ℝ) in -↑n..↑n,
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • deriv (⇑f) x -
          (2 * ↑π * I * ↑ξ) • ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • f x)
    Filter.atTop (nhds 0)
Tactic:
simp only [intervalIntegral_fourierIntegrand_deriv_sub_smul_fourierIntegrand]
Proof state after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
h_cover : AECover volume Filter.atTop fun i => Set.Ioc (-↑i) ↑i
⊢ Filter.Tendsto
    (fun n =>
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(↑n * ξ)))) • f ↑n -
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(-↑n * ξ)))) • f (-↑n))
    Filter.atTop (nhds 0)
Theorem: SchwartzMap.Real.fourierIntegral_deriv
Proof state before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
h_cover : AECover volume Filter.atTop fun i => Set.Ioc (-↑i) ↑i
⊢ Filter.Tendsto
    (fun n =>
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(↑n * ξ)))) • f ↑n -
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(-↑n * ξ)))) • f (-↑n))
    Filter.atTop (nhds 0)
Tactic:
rw [← Function.comp_def (g := (fun n : ℕ ↦ (n : ℝ)))
  (fun x : ℝ ↦ Real.fourierChar[-(x * ξ)] • f x - Real.fourierChar[-(-x * ξ)] • f (-x))]
Proof state after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
h_cover : AECover volume Filter.atTop fun i => Set.Ioc (-↑i) ↑i
⊢ Filter.Tendsto
    ((fun x =>
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • f x -
          ↑(Real.fourierChar (Multiplicative.ofAdd (-(-x * ξ)))) • f (-x)) ∘
      fun n => ↑n)
    Filter.atTop (nhds 0)
Theorem: SchwartzMap.Real.fourierIntegral_deriv
Proof state before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
h_cover : AECover volume Filter.atTop fun i => Set.Ioc (-↑i) ↑i
⊢ Filter.Tendsto
    ((fun x =>
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • f x -
          ↑(Real.fourierChar (Multiplicative.ofAdd (-(-x * ξ)))) • f (-x)) ∘
      fun n => ↑n)
    Filter.atTop (nhds 0)
Tactic:
refine Filter.Tendsto.comp ?_ tendsto_nat_cast_atTop_atTop
Proof state after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
h_cover : AECover volume Filter.atTop fun i => Set.Ioc (-↑i) ↑i
⊢ Filter.Tendsto
    (fun x =>
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • f x -
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(-x * ξ)))) • f (-x))
    Filter.atTop (nhds 0)
Theorem: SchwartzMap.Real.fourierIntegral_deriv
Proof state before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
h_cover : AECover volume Filter.atTop fun i => Set.Ioc (-↑i) ↑i
⊢ Filter.Tendsto
    (fun x =>
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • f x -
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(-x * ξ)))) • f (-x))
    Filter.atTop (nhds 0)
Tactic:
rw [← sub_zero 0]
Proof state after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
h_cover : AECover volume Filter.atTop fun i => Set.Ioc (-↑i) ↑i
⊢ Filter.Tendsto
    (fun x =>
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • f x -
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(-x * ξ)))) • f (-x))
    Filter.atTop (nhds (0 - 0))
Theorem: SchwartzMap.Real.fourierIntegral_deriv
Proof state before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
h_cover : AECover volume Filter.atTop fun i => Set.Ioc (-↑i) ↑i
⊢ Filter.Tendsto
    (fun x =>
      ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ)))) • f x -
        ↑(Real.fourierChar (Multiplicative.ofAdd (-(-x * ξ)))) • f (-x))
    Filter.atTop (nhds (0 - 0))
Tactic:
simp only [fourierIntegrand_eq_hasTemperateGrowth_smul]
Proof state after:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
h_cover : AECover volume Filter.atTop fun i => Set.Ioc (-↑i) ↑i
⊢ Filter.Tendsto
    (fun x =>
      ((hasTemperateGrowth_smul
              (_ : Function.HasTemperateGrowth fun x => ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ))))))
            f)
          x -
        ((hasTemperateGrowth_smul
              (_ : Function.HasTemperateGrowth fun x => ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ))))))
            f)
          (-x))
    Filter.atTop (nhds (0 - 0))
Theorem: SchwartzMap.Real.fourierIntegral_deriv
Proof state before:
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
h_cover : AECover volume Filter.atTop fun i => Set.Ioc (-↑i) ↑i
⊢ Filter.Tendsto
    (fun x =>
      ((hasTemperateGrowth_smul
              (_ : Function.HasTemperateGrowth fun x => ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ))))))
            f)
          x -
        ((hasTemperateGrowth_smul
              (_ : Function.HasTemperateGrowth fun x => ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ))))))
            f)
          (-x))
    Filter.atTop (nhds (0 - 0))
Tactic:
refine Filter.Tendsto.sub ?_ ?_
Proof state after:
case refine_1
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
h_cover : AECover volume Filter.atTop fun i => Set.Ioc (-↑i) ↑i
⊢ Filter.Tendsto
    (fun x =>
      ((hasTemperateGrowth_smul
            (_ : Function.HasTemperateGrowth fun x => ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ))))))
          f)
        x)
    Filter.atTop (nhds 0)

case refine_2
F : Type u_1
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℂ F
inst✝ : CompleteSpace F
f : 𝓢(ℝ, F)
ξ : ℝ
h_cover : AECover volume Filter.atTop fun i => Set.Ioc (-↑i) ↑i
⊢ Filter.Tendsto
    (fun x =>
      ((hasTemperateGrowth_smul
            (_ : Function.HasTemperateGrowth fun x => ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ))))))
          f)
        (-x))
    Filter.atTop (nhds 0)