Prove CLT assuming Lévy continuity theorem

[hanwenzhu]

This PR proves CLT (central_limit) assuming Lévy continuity, plus some other pending results.

The current remaining TODOs for a sorryless proof are:

• Lévy continuity theorem charFun_tendsto_iff_measure_tendsto (which would be the bulk of the proof of CLT)
  • Characteristic functions, separating algebras, etc (feat: separation of FiniteMeasure by StarSubalgebra or characteristic functions leanprover-community/mathlib4#19761)
  • Tight families of measures (also see feat : define pre-tight and tight measures leanprover-community/mathlib4#12394)
  • Prokhorov’s theorem (I am also not completely sure if this is actually needed)
    • depends on Riesz-Markov-Kakutani (in a Mathlib PR)
• Taylor's theorem on ℝ → ℝ, Peano form
• ProbabilityMeasure.ext_of_charFun_eq (Mathlib#19761)
• An analysis result tendsto_one_plus_div_pow_exp'

I will be away for the next few days (feel free to make any edits directly to the PR).

I have not been able to set up the blueprint environment, probably because of something wrong on my end. I will need to link the results here to the blueprint.

[RemyDegenne]

This is great!
I will merge the PR here, but you should also really PR everything you can to Mathlib (and feel free to PR any code I wrote too if you need it).

I'll update the blueprint.