English
A simplification of the previous norm identity showing how the norm-p power distributes over a finite subset of coordinates.
Русский
Упрощение предыдущего тождества нормы, демонстрирующее распределение нормы-степени по конечному подмножеству координат.
LaTeX
$$$\\|f\\|^{p.toReal} - \\|f - \\sum_{i\\in s} lp.single(p,i)(f(i))\\|^{p.toReal} = \\sum_{i\\in s} \\|f(i)\\|^{p.toReal}.$$$
Lean4
/-- The canonical finitely-supported approximations to an element `f` of `lp` converge to it, in the
`lp` topology. -/
protected theorem hasSum_single [Fact (1 ≤ p)] (hp : p ≠ ⊤) (f : lp E p) :
HasSum (fun i : α => lp.single p i (f i : E i)) f :=
by
have hp₀ : 0 < p := zero_lt_one.trans_le Fact.out
have hp' : 0 < p.toReal := ENNReal.toReal_pos hp₀.ne' hp
have := lp.hasSum_norm hp' f
rw [HasSum, Metric.tendsto_nhds] at this ⊢
intro ε hε
refine (this _ (Real.rpow_pos_of_pos hε p.toReal)).mono ?_
intro s hs
rw [← Real.rpow_lt_rpow_iff dist_nonneg (le_of_lt hε) hp']
rw [dist_comm] at hs
simp only [dist_eq_norm, Real.norm_eq_abs] at hs ⊢
have H : ‖(∑ i ∈ s, lp.single p i (f i : E i)) - f‖ ^ p.toReal = ‖f‖ ^ p.toReal - ∑ i ∈ s, ‖f i‖ ^ p.toReal := by
simpa only [coeFn_neg, Pi.neg_apply, lp.single_neg, Finset.sum_neg_distrib, neg_sub_neg, norm_neg,
_root_.norm_neg] using lp.norm_compl_sum_single hp' (-f) s
rw [← H] at hs
have :
|‖(∑ i ∈ s, lp.single p i (f i : E i)) - f‖ ^ p.toReal| = ‖(∑ i ∈ s, lp.single p i (f i : E i)) - f‖ ^ p.toReal :=
by simp only [Real.abs_rpow_of_nonneg (norm_nonneg _), abs_norm]
exact this ▸ hs
