Commit 2023-01-31 19:36 59694bd0

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).