-- Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean
theorem tendsto_integral_exp_inner_smul_cocompact :
    Tendsto (fun w : V => ∫ v, 𝐞 (-⟪v, w⟫) • f v) (cocompact V) (𝓝 0)

Proof state:
E : Type u_1
V : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
f : V → E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : FiniteDimensional ℝ V
hfi : Integrable f volume
ε : ℝ
hε : ε > 0
g : V → E
hg_supp : HasCompactSupport g
hfg : ∫ (x : V), ‖f x - g x‖ ≤ ε / 2
hg_cont : Continuous g
w : V
hI : ‖(∫ (v : V), 𝐞 (-inner v w) • g v) - 0‖ < ε / 2
⊢ ‖∫ (a : V), 𝐞 (-inner a w) • (f - g) a ∂volume‖ ≤ ∫ (x : V), ‖(f - g) x‖

Tactic:
exact VectorFourier.norm_fourierIntegral_le_integral_norm 𝐞 _ bilinFormOfRealInner (f - g) w

Result:
no goals

Proof state:
E : Type u_1
V : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
f : V → E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : FiniteDimensional ℝ V
hfi : Integrable f volume
ε : ℝ
hε : ε > 0
g : V → E
hg_supp : HasCompactSupport g
hfg : ∫ (x : V), ‖f x - g x‖ ≤ ε / 2
hg_cont : Continuous g
w : V
hI : ‖(∫ (v : V), 𝐞 (-inner v w) • g v) - 0‖ < ε / 2
⊢ ‖(∫ (v : V), 𝐞 (-inner v w) • f v) - ∫ (v : V), 𝐞 (-inner v w) • g v‖ ≤ ∫ (x : V), ‖f x - g x‖

Tactic:
simp_rw [← integral_sub ((Real.fourierIntegral_convergent_iff w).2 hfi)
  ((Real.fourierIntegral_convergent_iff w).2 (hg_cont.integrable_of_hasCompactSupport hg_supp)),
  ← smul_sub, ← Pi.sub_apply]

Result:
E : Type u_1
V : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
f : V → E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : FiniteDimensional ℝ V
hfi : Integrable f volume
ε : ℝ
hε : ε > 0
g : V → E
hg_supp : HasCompactSupport g
hfg : ∫ (x : V), ‖f x - g x‖ ≤ ε / 2
hg_cont : Continuous g
w : V
hI : ‖(∫ (v : V), 𝐞 (-inner v w) • g v) - 0‖ < ε / 2
⊢ ‖∫ (a : V), 𝐞 (-inner a w) • (f - g) a ∂volume‖ ≤ ∫ (x : V), ‖(f - g) x‖

Proof state:
case h.e.h.e'_3.h.h
E : Type u_1
V : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
f : V → E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : FiniteDimensional ℝ V
hfi : ¬Integrable f volume
w : V
⊢ ¬Integrable (fun a => 𝐞 (-inner a w) • f a) volume

Tactic:
rwa [Real.fourierIntegral_convergent_iff]

Result:
no goals

Proof state:
case pos.intro.intro.intro.intro
E : Type u_1
V : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
f : V → E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : FiniteDimensional ℝ V
hfi : Integrable f volume
ε : ℝ
hε : ε > 0
g : V → E
hg_supp : HasCompactSupport g
hfg : ∫ (x : V), ‖f x - g x‖ ≤ ε / 2
hg_cont : Continuous g
w : V
hI : dist (∫ (v : V), 𝐞 (-inner v w) • g v) 0 < ε / 2
⊢ dist (∫ (v : V), 𝐞 (-inner v w) • f v) 0 < ε

Tactic:
rw [dist_eq_norm] at hI ⊢

Result:
case pos.intro.intro.intro.intro
E : Type u_1
V : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℂ E
f : V → E
inst✝⁴ : NormedAddCommGroup V
inst✝³ : MeasurableSpace V
inst✝² : BorelSpace V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : FiniteDimensional ℝ V
hfi : Integrable f volume
ε : ℝ
hε : ε > 0
g : V → E
hg_supp : HasCompactSupport g
hfg : ∫ (x : V), ‖f x - g x‖ ≤ ε / 2
hg_cont : Continuous g
w : V
hI : ‖(∫ (v : V), 𝐞 (-inner v w) • g v) - 0‖ < ε / 2
⊢ ‖(∫ (v : V), 𝐞 (-inner v w) • f v) - 0‖ < ε