mathlib

59694bd0 - feat(measure_theory/integral/peak_function): convergence of integral against a sequence of peak functions (#18327)

feat(measure_theory/integral/peak_function): convergence of integral against a sequence of peak functions (#18327) If a sequence of peak functions `φᵢ` converges uniformly to zero away from a point `x₀`, and `g` is integrable and continuous at `x₀`, then `∫ φᵢ • g` converges to `g x₀`. We prove this statement and some consequences of it (notably to sequences which are the successive powers of a given function). Co-authored-by: David Loeffler <d.loeffler.01@cantab.net> Co-authored-by: loefflerd <d.loeffler.01@cantab.net>