Theorem: SchwartzMap.Real.fourierIntegral_deriv (ForML/SchwartzRealFourier.lean)

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]
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

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]
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

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]
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

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 (𝕜 := ℝ)]
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

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' _)]
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

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 ℝ)
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

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]
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

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' _)) ?_
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)

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 _))]
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)

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]
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)

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]
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)

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))]
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)

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
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)

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]
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))

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]
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))

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 ?_ ?_
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)

State before:
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)
Tactic:
. exact Filter.Tendsto.mono_left (zero_at_infty _) atTop_le_cocompact
State after:
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)

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
Tactic:
refine aecover_Ioc ?_ ?_ <;> simp [Filter.tendsto_neg_atBot_iff, tendsto_nat_cast_atTop_atTop]
State after:
no goals

State before:
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)
Tactic:
exact Filter.Tendsto.mono_left (zero_at_infty _) atTop_le_cocompact
State after:
no goals

State before:
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)
Tactic:
refine Filter.Tendsto.comp ?_ Filter.tendsto_neg_atTop_atBot
State after:
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
    (⇑((hasTemperateGrowth_smul
          (_ : Function.HasTemperateGrowth fun x => ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ))))))
        f))
    Filter.atBot (nhds 0)

State before:
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
    (⇑((hasTemperateGrowth_smul
          (_ : Function.HasTemperateGrowth fun x => ↑(Real.fourierChar (Multiplicative.ofAdd (-(x * ξ))))))
        f))
    Filter.atBot (nhds 0)
Tactic:
exact Filter.Tendsto.mono_left (zero_at_infty _) atBot_le_cocompact
State after:
no goals