piLpCurry — Mathlib

English

Congruence with the identity (relabeling by identity) yields the identity isomorphism.

Русский

Конгруентность с идентичностью эквивалентна тождественному изоморфизму.

LaTeX

$$$\text{piLpCongrRight}(p,\text{id}) = \text{refl}$$$

Lean4

/-- `LinearEquiv.piCurry` for `PiLp`, as an isometry. -/
def _root_.LinearIsometryEquiv.piLpCurry : PiLp p (fun i : Sigma _ => α i.1 i.2) ≃ₗᵢ[𝕜] PiLp p (fun i => PiLp p (α i))
    where
  toLinearEquiv :=
    WithLp.linearEquiv _ _ _ ≪≫ₗ LinearEquiv.piCurry 𝕜 α ≪≫ₗ
        (LinearEquiv.piCongrRight fun _ => (WithLp.linearEquiv _ _ _).symm) ≪≫ₗ
      (WithLp.linearEquiv _ _ _).symm
  norm_map' :=
    (WithLp.linearEquiv p 𝕜 _).symm.surjective.forall.2 fun x =>
      by
      simp_rw [← coe_nnnorm, NNReal.coe_inj]
      dsimp only [WithLp.linearEquiv_symm_apply]
      obtain rfl | hp := eq_or_ne p ⊤
      · simp_rw [← PiLp.nnnorm_ofLp, Pi.nnnorm_def, ← PiLp.nnnorm_ofLp, Pi.nnnorm_def]
        dsimp [Sigma.curry]
        rw [← Finset.univ_sigma_univ, Finset.sup_sigma]
      · have : 0 < p.toReal := (toReal_pos_iff_ne_top _).mpr hp
        simp_rw [PiLp.nnnorm_eq_sum hp, toLp_apply]
        dsimp [Sigma.curry]
        simp_rw [one_div, NNReal.rpow_inv_rpow this.ne', ← Finset.univ_sigma_univ, Finset.sum_sigma]

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