equiv_lpPiLp_norm — Mathlib

English

For a finite index α, the norm of the lpPiLp image equals the norm of the original lp element; i.e., ‖Equiv.lpPiLp f‖ = ‖f‖.

Русский

Для конечного α нормa образа через lpPiLp равна норме исходного элемента lp: ‖Equiv.lpPiLp f‖ = ‖f‖.

LaTeX

$$$\|\mathrm{Equiv.lpPiLp} f\| = \|f\|$$$

Lean4

theorem equiv_lpPiLp_norm [Fintype α] (f : lp E p) : ‖Equiv.lpPiLp f‖ = ‖f‖ :=
  by
  rcases p.trichotomy with (rfl | rfl | h)
  · simp [Equiv.lpPiLp, PiLp.norm_eq_card, lp.norm_eq_card_dsupport]
  · rw [PiLp.norm_eq_ciSup, lp.norm_eq_ciSup]; rfl
  · rw [PiLp.norm_eq_sum h, lp.norm_eq_tsum_rpow h, tsum_fintype]; rfl

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