coeFn_mFourierLp — Mathlib

English

For a given p, mFourierLp p n equals mFourier n almost everywhere (with respect to volume).

Русский

Для данного p функция mFourierLp p n совпадает почти всюду с mFourier n (относительно объёма).

LaTeX

$$$ mFourierLp(p, n) =_a.e.^{\mathrm{volume}} mFourier(n) $$$

Lean4

theorem coeFn_mFourierLp (p : ℝ≥0∞) [Fact (1 ≤ p)] (n : d → ℤ) : mFourierLp p n =ᵐ[volume] mFourier n :=
  ContinuousMap.coeFn_toLp volume
    (mFourier n)
      -- shortcut instance: avoids `synthInstance.maxHeartbeats` issue in `span_mFourierLp_closure_eq_top`

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