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

Tactic:
refine le_trans ?_ hfg

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
⊢ ‖(∫ (v : V), 𝐞 (-inner v w) • f v) - ∫ (v : V), 𝐞 (-inner v w) • g v‖ ≤ ∫ (x : V), ‖f x - g x‖

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

Tactic:
simp only [sub_zero, sub_add_cancel]

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

Tactic:
refine
  ((Metric.tendsto_nhds.mp
          (tendsto_integral_exp_inner_smul_cocompact_of_continuous_compact_support hg_cont
            hg_supp))
        _ (div_pos hε two_pos)).mp
    (Eventually.of_forall fun w 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 : dist (∫ (v : V), 𝐞 (-inner v w) • g v) 0 < ε / 2
⊢ dist (∫ (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‖ ≤ ε / 2
⊢ ‖(∫ (v : V), 𝐞 (-inner v w) • f v) - 0‖ < ε

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

Tactic:
have : ‖(∫ v, 𝐞 (-⟪v, w⟫) • f v) - ∫ v, 𝐞 (-⟪v, w⟫) • g v‖ ≤ ε / 2 := by
  refine le_trans ?_ hfg
  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]
  exact VectorFourier.norm_fourierIntegral_le_integral_norm 𝐞 _ bilinFormOfRealInner (f - g) w

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

Tactic:
rw [add_halves] at 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‖ < ε