lpMeasSubgroupToLpTrim_neg — Mathlib

English

Negation commutes with the trim-to-Lp map: lpMeasSubgroupToLpTrim of -f equals the negation of the trim of f.

Русский

Отрицание коммутирует с отображением обрезки: lpMeasSubgroupToLpTrim(-f) = - lpMeasSubgroupToLpTrim(f).

LaTeX

$$$lpMeasSubgroupToLpTrim\ F\ p\ μ hm (-f) = - lpMeasSubgroupToLpTrim\ F\ p\ μ hm f$$$

Lean4

theorem lpMeasSubgroupToLpTrim_neg (hm : m ≤ m0) (f : lpMeasSubgroup F m p μ) :
    lpMeasSubgroupToLpTrim F p μ hm (-f) = -lpMeasSubgroupToLpTrim F p μ hm f :=
  by
  ext1
  grw [Lp.coeFn_neg]
  refine (Lp.stronglyMeasurable _).ae_eq_trim_of_stronglyMeasurable hm (Lp.stronglyMeasurable _).neg ?_
  grw [lpMeasSubgroupToLpTrim_ae_eq, lpMeasSubgroupToLpTrim_ae_eq, ← Lp.coeFn_neg]
  rfl

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