Directional integration by parts on a fundamental parallelepiped
ProvedZSpan.norm_setIntegral_fundamentalDomain_cexp_mul_le_inv_pow_mul_setIntegral_norm_of_hasDerivAtLet be a finite-dimensional real normed space, equipped with a Borel measurable structure and an additive Haar measure , let be a basis of indexed by a finite type , and let be a continuous linear form. Let satisfy , and let be a sequence of continuous functions such that for every and every the function of a real variable has derivative at , and such that for every , every and every index one has , i.e. each product is invariant under translation by each basis vector. Then for every natural number ,
where ZSpan.fundamentalDomain b is the fundamental parallelepiped of the lattice spanned by , and the inverse is taken in (so the factor is when ).
This is the standard decay estimate for Fourier coefficients of smooth functions on a torus, here in a directional form: differentiation is performed only along the single vector , and only the products , not the character and the functions separately, are assumed periodic under the lattice. It is used to bound Whittaker coefficients of automorphic forms, via AutomorphicForm.exists_norm_whittakerCoefficient_le_mul_of_hasDerivAt_unipotentGL2_of_forall_norm_le.
import Mathlib set_option maxHeartbeats 4000000 set_option synthInstance.maxHeartbeats 400000 set_option backward.isDefEq.respectTransparency.types false set_option autoImplicit false open MeasureTheory
theorem ZSpan.norm_setIntegral_fundamentalDomain_cexp_mul_le_inv_pow_mul_setIntegral_norm_of_hasDerivAt
{ι E : Type*} [Fintype ι] [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E]
[MeasurableSpace E] [BorelSpace E] (b : Module.Basis ι ℝ E) (μ : Measure E) [μ.IsAddHaarMeasure]
(ℓ : E →L[ℝ] ℝ) (v : E) (hv : ℓ v ≠ 0)
(Hs : ℕ → E → ℂ) (hcont : ∀ j, Continuous (Hs j))
(hderiv : ∀ (j : ℕ) (x : E), HasDerivAt (fun t : ℝ => Hs j (x + t • v)) (Hs (j + 1) x) 0)
(hper : ∀ (j : ℕ) (x : E) (i : ι),
Complex.exp (2 * Real.pi * Complex.I * ℓ (x + b i)) * Hs j (x + b i) =
Complex.exp (2 * Real.pi * Complex.I * ℓ x) * Hs j x)
(M : ℕ) :
‖∫ x in ZSpan.fundamentalDomain b, Complex.exp (2 * Real.pi * Complex.I * ℓ x) * Hs 0 x ∂μ‖ ≤
((2 * Real.pi * |ℓ v|)⁻¹) ^ M * ∫ x in ZSpan.fundamentalDomain b, ‖Hs M x‖ ∂μ := by sorry