norm_fourierSMulRight — Mathlib

English

The norm of the Fourier-smoothed right translate at v is exactly (2π) times the norm of L v times the norm of f v; i.e., the magnitude of the right-hand piece scales by (2π)⋅‖L v‖⋅‖f(v)‖.

Русский

Норма правого переводного фурье-оператора равна (2π)·‖L v‖·‖f(v)‖.

LaTeX

$$$\\|\\mathrm{fourierSMulRight}(L,f)(v)\\| = (2\\pi)\\; \\|L v\\|\\; \\|f(v)\\|$$$

Lean4

theorem norm_fourierSMulRight (L : V →L[ℝ] W →L[ℝ] ℝ) (f : V → E) (v : V) :
    ‖fourierSMulRight L f v‖ = (2 * π) * ‖L v‖ * ‖f v‖ := by
  rw [fourierSMulRight, norm_smul _ (ContinuousLinearMap.smulRight (L v) (f v)), norm_neg, norm_mul, norm_mul, norm_I,
    mul_one, Complex.norm_of_nonneg pi_pos.le, Complex.norm_two, ContinuousLinearMap.norm_smulRight_apply, ← mul_assoc]

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