sumPiLpEquivProdLpPiLp — Mathlib

English

There is a canonical isometric equivalence between PiLp p on a Sigma-indexed family and a nested PiLp curry construction.

Русский

Существует каноническое изометрическое эквивалентное отображение между PiLp p на семействе с сигма-индексацией и вложенной конструкцией карри для PiLp.

LaTeX

$$$\text{PiLpCurry}_{\mathbb{K}}(p,\alpha) : PiLp(p, (i:\Sigma κ)\mapsto α_i) \simeq_{LinIso} PiLp(p, (i\mapsto PiLp(p, α_i)))$$$

Lean4

/-- `LinearEquiv.sumPiEquivProdPi` for `PiLp`, as an isometry. -/
@[simps! +simpRhs]
def sumPiLpEquivProdLpPiLp :
    WithLp p (Π i, α i) ≃ₗᵢ[𝕜] WithLp p (WithLp p (Π i, α (.inl i)) × WithLp p (Π i, α (.inr i)))
    where
  toLinearEquiv :=
    WithLp.linearEquiv p _ _ ≪≫ₗ LinearEquiv.sumPiEquivProdPi _ _ _ α ≪≫ₗ
        LinearEquiv.prodCongr (WithLp.linearEquiv p _ _).symm (WithLp.linearEquiv _ _ _).symm ≪≫ₗ
      (WithLp.linearEquiv p _ _).symm
  norm_map' :=
    (WithLp.linearEquiv p 𝕜 _).symm.surjective.forall.2 fun x =>
      by
      obtain rfl | hp := p.dichotomy
      · simp [← Finset.univ_disjSum_univ, Finset.sup_disjSum, Pi.norm_def]
      · have : 0 < p.toReal := by positivity
        have hpt : p ≠ ⊤ := (toReal_pos_iff_ne_top p).mp this
        simp_rw [← coe_nnnorm];
        congr 1 -- convert to nnnorm to avoid needing positivity arguments

        simp [nnnorm_eq_sum hpt, WithLp.prod_nnnorm_eq_add hpt, NNReal.rpow_inv_rpow this.ne']

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