English
Under mild assumptions, the map single p i preserves distances: Isometry( lp.single p i ).
Русский
При некоторых условиях отображение single сохраняет расстояния: Isometry( lp.single p i ).
LaTeX
$$$\text{Isometry}(\text{lp.single } p i).$$$
Lean4
@[simp]
protected theorem norm_single (hp : 0 < p) (i : α) (x : E i) : ‖lp.single p i x‖ = ‖x‖ :=
by
haveI : Nonempty α := ⟨i⟩
induction p with
| top =>
simp only [norm_eq_ciSup, lp.coeFn_single]
refine ciSup_eq_of_forall_le_of_forall_lt_exists_gt (fun j => ?_) fun n hn => ⟨i, hn.trans_eq ?_⟩
· obtain rfl | hij := Decidable.eq_or_ne i j
· rw [Pi.single_eq_same]
· rw [Pi.single_eq_of_ne' hij, _root_.norm_zero]
exact norm_nonneg _
· rw [Pi.single_eq_same]
| coe p =>
have : 0 < (p : ℝ≥0∞).toReal := by simpa using hp
rw [norm_eq_tsum_rpow this, tsum_eq_single i, lp.coeFn_single, one_div, Real.rpow_rpow_inv _ this.ne',
Pi.single_eq_same]
· exact norm_nonneg _
· intro j hji
rw [lp.coeFn_single, Pi.single_eq_of_ne hji, _root_.norm_zero, Real.zero_rpow this.ne']
