lpMeasSubgroupToLpTrim_add — Mathlib

English

The trim-to-Lp map preserves addition: lpMeasSubgroupToLpTrim of f+g equals the sum of the trims.

Русский

Перенос через обрезку сохраняет сложение: lpMeasSubgroupToLpTrim(f+g) = lpMeasSubgroupToLpTrim(f) + lpMeasSubgroupToLpTrim(g).

LaTeX

$$$lpMeasSubgroupToLpTrim\ F\ p\ μ hm (f+g) = lpMeasSubgroupToLpTrim\ F\ p\ μ hm f + lpMeasSubgroupToLpTrim\ F\ p\ μ hm g$$$

Lean4

theorem lpMeasSubgroupToLpTrim_add (hm : m ≤ m0) (f g : lpMeasSubgroup F m p μ) :
    lpMeasSubgroupToLpTrim F p μ hm (f + g) = lpMeasSubgroupToLpTrim F p μ hm f + lpMeasSubgroupToLpTrim F p μ hm g :=
  by
  ext1
  grw [Lp.coeFn_add]
  refine (Lp.stronglyMeasurable _).ae_eq_trim_of_stronglyMeasurable hm ?_ ?_
  · exact (Lp.stronglyMeasurable _).add (Lp.stronglyMeasurable _)
  grw [lpMeasSubgroupToLpTrim_ae_eq, lpMeasSubgroupToLpTrim_ae_eq, lpMeasSubgroupToLpTrim_ae_eq, ← Lp.coeFn_add]
  rfl

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