piLpCongrRight — Mathlib

English

A family of coordinatewise linear isometric equivalences yields a linear isometric equivalence between PiLp spaces.

Русский

Семейство покоординатных линейно-изометрических эквивалентностей задаёт линейно-изометрическое эквивалент между пространствами PiLp.

LaTeX

$$$\PiLp(p,\alpha) \simeq_{\mathrm{LinIso}} \PiLp(p,\beta)\quad\text{where } \alpha_i\simeq\beta_i$$

Lean4

/-- A family of linearly isometric equivalences in the codomain induces an isometric equivalence
between Pi types with the Lp norm.

This is the isometry version of `LinearEquiv.piCongrRight`. -/
protected def _root_.LinearIsometryEquiv.piLpCongrRight (e : ∀ i, α i ≃ₗᵢ[𝕜] β i) : PiLp p α ≃ₗᵢ[𝕜] PiLp p β
    where
  toLinearEquiv :=
    WithLp.linearEquiv _ _ _ ≪≫ₗ (LinearEquiv.piCongrRight fun i => (e i).toLinearEquiv) ≪≫ₗ
      (WithLp.linearEquiv _ _ _).symm
  norm_map' :=
    (WithLp.linearEquiv p 𝕜 _).symm.surjective.forall.2 fun x =>
      by
      simp only [LinearEquiv.trans_apply, WithLp.linearEquiv_symm_apply, WithLp.linearEquiv_apply]
      obtain rfl | hp := p.dichotomy
      ·
        simp_rw [PiLp.norm_toLp, Pi.norm_def, LinearEquiv.piCongrRight_apply, LinearIsometryEquiv.coe_toLinearEquiv,
          LinearIsometryEquiv.nnnorm_map, ofLp_apply, toLp_apply]
      · have : 0 < p.toReal := zero_lt_one.trans_le <| by norm_cast
        simp only [PiLp.norm_eq_sum this, toLp_apply, LinearEquiv.piCongrRight_apply,
          LinearIsometryEquiv.coe_toLinearEquiv, LinearIsometryEquiv.norm_map, ofLp_apply, toLp_apply]

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