English
Applying the curry isometry to a function corresponds to the curry construction on the function values.
Русский
Применение карри-изометрии к функции эквивалентно карри-конструкции на значениях функции.
LaTeX
$$$\text{piLpCurry}(p, \alpha)(f) = \text{toLp}(p, \lambda i. (toLp)(p, \Sigma.curry (toLp f) i))$$$
Lean4
@[simp]
theorem nnnorm_toLp_single (i : ι) (b : β i) : ‖toLp p (Pi.single i b)‖₊ = ‖b‖₊ :=
by
haveI : Nonempty ι := ⟨i⟩
induction p generalizing hp with
| top =>
simp_rw [nnnorm_eq_ciSup, toLp_apply]
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, nnnorm_zero]
exact zero_le _
· rw [Pi.single_eq_same]
| coe p =>
have hp0 : (p : ℝ) ≠ 0 := mod_cast (zero_lt_one.trans_le <| Fact.out (p := 1 ≤ (p : ℝ≥0∞))).ne'
rw [nnnorm_eq_sum ENNReal.coe_ne_top, ENNReal.coe_toReal, Fintype.sum_eq_single i, toLp_apply, Pi.single_eq_same, ←
NNReal.rpow_mul, one_div, mul_inv_cancel₀ hp0, NNReal.rpow_one]
intro j hij
rw [toLp_apply, Pi.single_eq_of_ne hij, nnnorm_zero, NNReal.zero_rpow hp0]
