English
Permuting the index set by a finite equivalence e: ι ≃ ι' yields a linear isometric equivalence between the corresponding Lp spaces.
Русский
Перемещая индексы по фон-эквивалентности e: ι ≃ ι', получаем линейно-изометрическое эквивалентное отображение между соответствующими пространствами Lp.
LaTeX
$$$\text{If } e:\, ι \xrightarrow{\sim} ι',\; \PiLp(p,β) \cong_{\mathrm{LinIso}} \PiLp(p,β) \text{ along } e$$$
Lean4
/-- An equivalence of finite domains induces a linearly isometric equivalence of finitely supported
functions -/
def _root_.LinearIsometryEquiv.piLpCongrLeft (e : ι ≃ ι') : (PiLp p fun _ : ι => E) ≃ₗᵢ[𝕜] PiLp p fun _ : ι' => E
where
toLinearEquiv := LinearEquiv.piCongrLeft' 𝕜 (fun _ : ι => E) e
norm_map'
x' := by
rcases p.dichotomy with (rfl | h)
· simp_rw [norm_eq_ciSup]
exact e.symm.iSup_congr fun _ => rfl
· simp only [norm_eq_sum (zero_lt_one.trans_le h)]
congr 1
exact Fintype.sum_equiv e.symm _ _ fun _ => rfl
