Converting infinite sums to integrals

Stream: Is there code for X?

[Cookie Guy]

Is there a way for me to argue about a sum by noticing it is in the form of a reimann integral?

Like something like.

(hf : ContinuousOn f (Set.Icc a b)) : Filter.Tendsto (fun (n : ℕ) => ((b - a) / n : ℝ) * ∑ k ∈ Finset.Icc 1 n, f (a + k * (b - a) / n : ℝ)) Filter.atTop (nhds (∫ x in a..b, f x))

I cant find a theorem in athlib for me to argue about things like this

[Weiyi Wang]

I would start by looking into files around https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/BoxIntegral/Basic.html

[Weiyi Wang]

Them there is docs#MeasureTheory.ContinuousOn.hasBoxIntegral that connects two notion of integral

[Cookie Guy]

Yes, but I still do not know how to convert this box integral into a sum. My best guess is BoxIntegral.HasIntegral.sum, but im still not sure how to use it to prove this.

[Weiyi Wang]

I think it is docs#BoxIntegral.HasIntegral.tendsto