-- Mathlib/Analysis/Fourier/RiemannLebesgueLemma.lean
theorem tendsto_integral_exp_smul_cocompact (μ : Measure V) [μ.IsAddHaarMeasure] :
    Tendsto (fun w : V →L[ℝ] ℝ => ∫ v, 𝐞 (-w v) • f v ∂μ) (cocompact (V →L[ℝ] ℝ)) (𝓝 0)

Proof state:
E : Type u_1
V : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℂ E
f : V → E
inst✝⁹ : AddCommGroup V
inst✝⁸ : TopologicalSpace V
inst✝⁷ : IsTopologicalAddGroup V
inst✝⁶ : T2Space V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : Module ℝ V
inst✝² : ContinuousSMul ℝ V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
V' : Type := EuclideanSpace ℝ (Fin (finrank ℝ V))
A : V ≃L[ℝ] V'
⊢ Tendsto (fun w => ∫ (v : V), 𝐞 (-w v) • f v ∂μ) (cocompact (V →L[ℝ] ℝ)) (𝓝 0)

Tactic:
borelize V'

Result:
E : Type u_1
V : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℂ E
f : V → E
inst✝⁹ : AddCommGroup V
inst✝⁸ : TopologicalSpace V
inst✝⁷ : IsTopologicalAddGroup V
inst✝⁶ : T2Space V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : Module ℝ V
inst✝² : ContinuousSMul ℝ V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
V' : Type := EuclideanSpace ℝ (Fin (finrank ℝ V))
A : V ≃L[ℝ] V'
this✝¹ : MeasurableSpace V' := borel V'
this✝ : BorelSpace V'
⊢ Tendsto (fun w => ∫ (v : V), 𝐞 (-w v) • f v ∂μ) (cocompact (V →L[ℝ] ℝ)) (𝓝 0)

Proof state:
case h.e'_3.h.e_f.h.e_a.h.e_6.h.e_a
E : Type u_1
V : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℂ E
f : V → E
inst✝⁹ : AddCommGroup V
inst✝⁸ : TopologicalSpace V
inst✝⁷ : IsTopologicalAddGroup V
inst✝⁶ : T2Space V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : Module ℝ V
inst✝² : ContinuousSMul ℝ V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
V' : Type := EuclideanSpace ℝ (Fin (finrank ℝ V))
A : V ≃L[ℝ] V'
this✝¹ : MeasurableSpace V' := borel V'
this✝ : BorelSpace V'
Aₘ : V ≃ᵐ V' := A.toHomeomorph.toMeasurableEquiv
Adual : (V →L[ℝ] ℝ) ≃L[ℝ] V' →L[ℝ] ℝ := A.arrowCongrSL (ContinuousLinearEquiv.refl ℝ ℝ)
this : (Measure.map (⇑Aₘ) μ).IsAddHaarMeasure
w : V →L[ℝ] ℝ
v : V
⊢ w v = (Adual.toHomeomorph.toCocompactMap.toFun w) (Aₘ v)

Tactic:
apply congr_arg w

Result:
case h.e'_3.h.e_f.h.e_a.h.e_6.h.e_a
E : Type u_1
V : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℂ E
f : V → E
inst✝⁹ : AddCommGroup V
inst✝⁸ : TopologicalSpace V
inst✝⁷ : IsTopologicalAddGroup V
inst✝⁶ : T2Space V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : Module ℝ V
inst✝² : ContinuousSMul ℝ V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
V' : Type := EuclideanSpace ℝ (Fin (finrank ℝ V))
A : V ≃L[ℝ] V'
this✝¹ : MeasurableSpace V' := borel V'
this✝ : BorelSpace V'
Aₘ : V ≃ᵐ V' := A.toHomeomorph.toMeasurableEquiv
Adual : (V →L[ℝ] ℝ) ≃L[ℝ] V' →L[ℝ] ℝ := A.arrowCongrSL (ContinuousLinearEquiv.refl ℝ ℝ)
this : (Measure.map (⇑Aₘ) μ).IsAddHaarMeasure
w : V →L[ℝ] ℝ
v : V
⊢ v = ↑↑A.symm (Aₘ v)

Proof state:
E : Type u_1
V : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℂ E
f : V → E
inst✝⁹ : AddCommGroup V
inst✝⁸ : TopologicalSpace V
inst✝⁷ : IsTopologicalAddGroup V
inst✝⁶ : T2Space V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : Module ℝ V
inst✝² : ContinuousSMul ℝ V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
V' : Type := EuclideanSpace ℝ (Fin (finrank ℝ V))
⊢ Tendsto (fun w => ∫ (v : V), 𝐞 (-w v) • f v ∂μ) (cocompact (V →L[ℝ] ℝ)) (𝓝 0)

Tactic:
have A : V ≃L[ℝ] V' := toEuclidean

Result:
E : Type u_1
V : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℂ E
f : V → E
inst✝⁹ : AddCommGroup V
inst✝⁸ : TopologicalSpace V
inst✝⁷ : IsTopologicalAddGroup V
inst✝⁶ : T2Space V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : Module ℝ V
inst✝² : ContinuousSMul ℝ V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
V' : Type := EuclideanSpace ℝ (Fin (finrank ℝ V))
A : V ≃L[ℝ] V'
⊢ Tendsto (fun w => ∫ (v : V), 𝐞 (-w v) • f v ∂μ) (cocompact (V →L[ℝ] ℝ)) (𝓝 0)

Proof state:
case h.e'_3.h.e_f.h.e_a.e_a
E : Type u_1
V : Type u_2
inst✝¹¹ : NormedAddCommGroup E
inst✝¹⁰ : NormedSpace ℂ E
f : V → E
inst✝⁹ : AddCommGroup V
inst✝⁸ : TopologicalSpace V
inst✝⁷ : IsTopologicalAddGroup V
inst✝⁶ : T2Space V
inst✝⁵ : MeasurableSpace V
inst✝⁴ : BorelSpace V
inst✝³ : Module ℝ V
inst✝² : ContinuousSMul ℝ V
inst✝¹ : FiniteDimensional ℝ V
μ : Measure V
inst✝ : μ.IsAddHaarMeasure
V' : Type := EuclideanSpace ℝ (Fin (finrank ℝ V))
A : V ≃L[ℝ] V'
this✝¹ : MeasurableSpace V' := borel V'
this✝ : BorelSpace V'
Aₘ : V ≃ᵐ V' := A.toHomeomorph.toMeasurableEquiv
Adual : (V →L[ℝ] ℝ) ≃L[ℝ] V' →L[ℝ] ℝ := A.arrowCongrSL (ContinuousLinearEquiv.refl ℝ ℝ)
this : (Measure.map (⇑Aₘ) μ).IsAddHaarMeasure
w : V →L[ℝ] ℝ
v : V
⊢ v = A.symm (Aₘ v)

Tactic:
exact (ContinuousLinearEquiv.symm_apply_apply A v).symm

Result:
no goals