lpMeasSubgroupToLpTrim_norm_map — Mathlib

English

The norm is preserved by lpMeasSubgroupToLpTrim: the norm of the trimmed image equals the norm of the original element.

Русский

Норма сохраняется отображением lpMeasSubgroupToLpTrim: норма образа обрезанного элемента равна норме исходного элемента.

LaTeX

$$$\|lpMeasSubgroupToLpTrim\ F\ p\ μ hm f\| = \|f\|$$$

Lean4

/-- `lpMeasSubgroupToLpTrim` preserves the norm. -/
theorem lpMeasSubgroupToLpTrim_norm_map [hp : Fact (1 ≤ p)] (hm : m ≤ m0) (f : lpMeasSubgroup F m p μ) :
    ‖lpMeasSubgroupToLpTrim F p μ hm f‖ = ‖f‖ :=
  by
  rw [Lp.norm_def, eLpNorm_trim hm (Lp.stronglyMeasurable _), eLpNorm_congr_ae (lpMeasSubgroupToLpTrim_ae_eq hm _), ←
    Lp.norm_def]
  congr

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