English
If integrability conditions hold, then the FourierPowSMulRight function is integrable, and its integral satisfies a dominated convergence bound matching the Fourier transform structure.
Русский
При выполнении условий интегрируемости функция FourierPowSMulRight интегрируема и её интеграл удовлетворяет ограничению доминирования.
LaTeX
$$$\\int \\text{fourierPowSMulRight } L f(v)\\, d\\mu(v) \\quad \\text{is finite under dominance }$$$
Lean4
theorem norm_fourierPowSMulRight_le (f : V → E) (v : V) (n : ℕ) :
‖fourierPowSMulRight L f v n‖ ≤ (2 * π * ‖L‖) ^ n * ‖v‖ ^ n * ‖f v‖ :=
by
apply ContinuousMultilinearMap.opNorm_le_bound (by positivity) (fun m ↦ ?_)
calc
‖fourierPowSMulRight L f v n m‖ = (2 * π) ^ n * ((∏ x : Fin n, |(L v) (m x)|) * ‖f v‖) := by
simp [abs_of_nonneg pi_nonneg, norm_smul]
_ ≤ (2 * π) ^ n * ((∏ x : Fin n, ‖L‖ * ‖v‖ * ‖m x‖) * ‖f v‖) :=
by
gcongr with i _hi
exact L.le_opNorm₂ v (m i)
_ = (2 * π * ‖L‖) ^ n * ‖v‖ ^ n * ‖f v‖ * ∏ i : Fin n, ‖m i‖ := by simp [Finset.prod_mul_distrib, mul_pow]; ring
