-- 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:
case pos
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
⊢ ∀ᶠ (x : V) in cocompact V, dist (∫ (v : V), 𝐞 (-inner v x) • f v) 0 < ε

Tactic:
obtain ⟨g, hg_supp, hfg, hg_cont, -⟩ :=
  hfi.exists_hasCompactSupport_integral_sub_le (div_pos hε two_pos)

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
⊢ ∀ᶠ (x : V) in cocompact V, dist (∫ (v : V), 𝐞 (-inner v x) • f v) 0 < ε

Proof state:
case h.e.h.e'_3.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
⊢ ∫ (v : V), 𝐞 (-inner v w) • f v = 0

Tactic:
apply integral_undef

Result:
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

Proof state:
case neg
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
⊢ Tendsto (fun w => ∫ (v : V), 𝐞 (-inner v w) • f v) (cocompact V) (𝓝 0)

Tactic:
convert tendsto_const_nhds (x := (0 : E)) with w

Result:
case h.e.h.e'_3.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
⊢ ∫ (v : V), 𝐞 (-inner v w) • f v = 0

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 : ‖(∫ (v : V), 𝐞 (-inner v w) • g v) - 0‖ < ε / 2
this :
  ‖(∫ (v : V), 𝐞 (-inner v w) • f v) - ∫ (v : V), 𝐞 (-inner v w) • g v‖ + ‖(∫ (v : V), 𝐞 (-inner v w) • g v) - 0‖ < ε
⊢ ‖(∫ (v : V), 𝐞 (-inner v w) • f v) - 0‖ < ε

Tactic:
refine ((le_of_eq ?_).trans (norm_add_le _ _)).trans_lt this

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
this :
  ‖(∫ (v : V), 𝐞 (-inner v w) • f v) - ∫ (v : V), 𝐞 (-inner v w) • g v‖ + ‖(∫ (v : V), 𝐞 (-inner v w) • g v) - 0‖ < ε
⊢ ‖(∫ (v : V), 𝐞 (-inner v w) • f v) - 0‖ =
    ‖((∫ (v : V), 𝐞 (-inner v w) • f v) - ∫ (v : V), 𝐞 (-inner v w) • g v) + ((∫ (v : V), 𝐞 (-inner v w) • g 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
⊢ Tendsto (fun w => ∫ (v : V), 𝐞 (-inner v w) • f v) (cocompact V) (𝓝 0)

Tactic:
by_cases hfi : Integrable f

Result:
case pos
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
⊢ Tendsto (fun w => ∫ (v : V), 𝐞 (-inner v w) • f v) (cocompact V) (𝓝 0)

case neg
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
⊢ Tendsto (fun w => ∫ (v : V), 𝐞 (-inner v w) • f v) (cocompact V) (𝓝 0)

Proof state:
case pos
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
⊢ Tendsto (fun w => ∫ (v : V), 𝐞 (-inner v w) • f v) (cocompact V) (𝓝 0)

Tactic:
refine Metric.tendsto_nhds.mpr fun ε hε => ?_

Result:
case pos
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
⊢ ∀ᶠ (x : V) in cocompact V, dist (∫ (v : V), 𝐞 (-inner v x) • f v) 0 < ε

Proof state:
case pos
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
⊢ Tendsto (fun w => ∫ (v : V), 𝐞 (-inner v w) • f v) (cocompact V) (𝓝 0)

case neg
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
⊢ Tendsto (fun w => ∫ (v : V), 𝐞 (-inner v w) • f v) (cocompact V) (𝓝 0)

Tactic:
swap

Result:
case neg
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
⊢ Tendsto (fun w => ∫ (v : V), 𝐞 (-inner v w) • f v) (cocompact V) (𝓝 0)

case pos
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
⊢ Tendsto (fun w => ∫ (v : V), 𝐞 (-inner v w) • f v) (cocompact V) (𝓝 0)