proposition: Lemma Lnorm_counting p (f : R^nat) : (0 < p)%R -> 'N_p%:E [f] = (\sum_(k <oo) (`| f k | `^ p)%:E) `^ p^-1.
proof: Proof. move=> p0; rewrite unlock gt_eqF// ge0_integral_count// => k. by rewrite lee_fin powR_ge0. Qed.
imports: HB(structures) mathcomp(all_ssreflect ssralg ssrnum ssrint interval finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop ) signed reals ereal topology normedtype sequences real_interval esum measure lebesgue_measure lebesgue_integral numfun exp convex itv