fourierPowSMulRight — Mathlib

English

The value of fourierPowSMulRight L f v n on an argument m is the scalar -(2π i)^n times the product over i of L(v, m_i) times f(v).

Русский

Значение fourierPowSMulRight на аргументе m равно -(2π i)^n умножить на произведение по i от L(v, m_i) и f(v).

LaTeX

$$$\\text{fourierPowSMulRight } L f v n = (-(2 \\pi i))^n \\cdot \\left( \\prod_{i=1}^n L(v, m_i) \\right) \\cdot f(v)$$$

Lean4

theorem _root_.MeasureTheory.AEStronglyMeasurable.fourierPowSMulRight (hf : AEStronglyMeasurable f μ) (n : ℕ) :
    AEStronglyMeasurable (fun v ↦ fourierPowSMulRight L f v n) μ :=
  by
  simp_rw [fourierPowSMulRight_eq_comp]
  apply AEStronglyMeasurable.const_smul'
  apply (smulRightL ℝ (fun (_ : Fin n) ↦ W) E).continuous₂.comp_aestronglyMeasurable₂ _ hf
  apply Continuous.aestronglyMeasurable
  exact Continuous.comp (map_continuous _) (continuous_pi (fun _ ↦ L.continuous))

Похожие утверждения