fourierPowSMulRight_apply — Mathlib

English

If f is AEStronglyMeasurable (almost everywhere strongly measurable) and μ is a measure on V, then the map v ↦ fourierPowSMulRight L f v is AEStronglyMeasurable with respect to μ.

Русский

Если f тождественно измерима почти всюду, то v ↦ fourierPowSMulRight L f v измерима почти всюду относительно μ.

LaTeX

$$$\\text{AEStronglyMeasurable}(v \\mapsto \\text{fourierPowSMulRight } L f v)\\; μ$$$

Lean4

@[simp 1100]
theorem fourierPowSMulRight_apply {f : V → E} {v : V} {n : ℕ} {m : Fin n → W} :
    fourierPowSMulRight L f v n m = (-(2 * π * I)) ^ n • (∏ i, L v (m i)) • f v := by simp [fourierPowSMulRight]

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