Sum as integral

Stream: Is there code for X?

[Vincent Beffara]

There is docs#lintegral_count' but do we have this?

lemma integral_count {α : Type*} [fintype α] {f : α → ℝ} :
  ∫ a, f a ∂(@count α ⊤) = ∑ a, f a :=
begin
  simp [count],
  rw integral_finset_sum_measure,
  { congr, funext i, apply integral_dirac', exact measurable_from_top.strongly_measurable },
  { refine λ i hi, ⟨measurable_from_top.ae_strongly_measurable, _⟩,
    rw [has_finite_integral, lintegral_dirac' _ measurable_from_top],
    simp only [ennreal.coe_lt_top] }
end

[Vincent Beffara]

And then,

lemma l2 {α : Type*} [fintype α] (f : α → ℝ) :
  mem_ℒp f 2 (@count α ⊤) :=
begin
  refine ⟨measurable_from_top.ae_strongly_measurable, _⟩,
  simp [snorm, snorm', count],
  apply @ennreal.rpow_lt_top_of_nonneg _ (2⁻¹) (by norm_num),
  apply lt_top_iff_ne_top.mp,
  simp [ennreal.sum_lt_top, lintegral_dirac' _ measurable_from_top],
end

and we can get Cauchy-Schwarz for sums from the L2 version, but in any case mapping sums to (Bochner) integral might be of more general use.

[Jason KY.]

I don't think we have these and they will very useful to have!