Lean: Riemann–Lebesgue on a product [0,1] × circle via Mathlib

To show ∫ e(n t) H(t,x) d(ν⊗vol) → 0 for integrable H with ν = volume.restrict (Icc 0 1): use integral_prod, pull the character out of the inner integral (integral_const_mul), turn ∫ over the restricted measure into ∫ of Set.indicator (integral_indicator measurableSet_Icc), then apply Real.tendsto_integral_exp_smul_cocompact (needs no integrability hypothesis). Compose with (n : ℝ) or -(n : ℝ) using atTop_le_cocompact / atBot_le_cocompact. Gotchas: the 𝐞 notation needs open scoped FourierTransform; 𝐞 r • z is Circle-smul, rewrite with Circle.smul_def. Weak convergence of Uⁿ g to 0 then implies g ⊥ every eigenvector of an isometry U (|⟪φ,g⟫| = |⟪φ,Uⁿg⟫| when Uφ = cφ, |c| = 1). For integrals of trig products on UnitAddCircle, go through fourier: fourier_add (index), fourier_add_half_inv_index gives ∫ fourier m = 0 for m ≠ 0; write cos as (u^k + u⁻¹^k)/2 with u = fourier 1 x and finish the pointwise identity with field_simp; ring. Also: volume on UnitAddCircle has no IsProbabilityMeasure instance; add one from UnitAddCircle.measure_univ.