lpMeasSubgroupToLpTrimIso — Mathlib

English

There is an isometric isomorphism between the subspace lpMeasSubgroup F m p μ and the Lp space Lp F p (μ.trim hm).

Русский

Существует изометрическое изоморфирование между подпространством lpMeasSubgroup и пространством Lp F p (μ.trim hm).

LaTeX

$$$lpMeasSubgroupToLpTrimIso\ F\ p\ μ hm : lpMeasSubgroup F m p μ \cong_i Lp F p (μ.trim hm)$$$

Lean4

/-- `lpMeasSubgroup` and `Lp F p (μ.trim hm)` are isometric. -/
noncomputable def lpMeasSubgroupToLpTrimIso [Fact (1 ≤ p)] (hm : m ≤ m0) : lpMeasSubgroup F m p μ ≃ᵢ Lp F p (μ.trim hm)
    where
  toFun := lpMeasSubgroupToLpTrim F p μ hm
  invFun := lpTrimToLpMeasSubgroup F p μ hm
  left_inv := lpMeasSubgroupToLpTrim_left_inv hm
  right_inv := lpMeasSubgroupToLpTrim_right_inv hm
  isometry_toFun := isometry_lpMeasSubgroupToLpTrim hm

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