integrableOn_peak_smul_of_integrableOn_of_continuousWithinAt

theorem integrableOn_peak_smul_of_integrableOn_of_continuousWithinAt : ∀ {α : Type u_1} {E : Type u_2} {ι : Type u_3} {hm : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace α] [inst_1 : BorelSpace α] [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace ℝ E] {g : α → E} {l : Filter ι} {x₀ : α} {s t : Set α} {φ : ι → α → ℝ} {a : E}, MeasurableSet s → t ∈ nhdsWithin x₀ s → (∀ (u : Set α), IsOpen u → x₀ ∈ u → TendstoUniformlyOn φ 0 l (s \ u)) → Filter.Tendsto (fun i => ∫ (x : α) in t, φ i x ∂μ) l (nhds 1) → (∀ᶠ (i : ι) in l, MeasureTheory.AEStronglyMeasurable (φ i) (μ.restrict s)) → MeasureTheory.IntegrableOn g s μ → Filter.Tendsto g (nhdsWithin x₀ s) (nhds a) → ∀ᶠ (i : ι) in l, MeasureTheory.IntegrableOn (fun x => φ i x • g x) s μ

This theorem, `integrableOn_peak_smul_of_integrableOn_of_continuousWithinAt`, states that if we have a sequence of peak functions `φᵢ` which converges uniformly to zero away from a point `x₀`, and a function `g` which is integrable and tends towards a limit at `x₀`, then the product function `φᵢ • g` will eventually be integrable. More formally, the conditions are: * `s` is a measurable set. * `t` is in the neighborhood within `s` of `x₀`. * For any open set `u` containing `x₀`, `φ` tends towards zero uniformly on `s` without `u`. * The integral of `φᵢ` over `t` tends towards 1. * `φᵢ` is almost everywhere strongly measurable on `s` eventually with respect to a filter `l`. * `g` is integrable on `s`. * `g` tends towards a limit `a` within `s` of `x₀`. Under all these conditions, the theorem asserts that `φᵢ • g` will be eventually integrable on `s` with respect to the filter `l`.

More concisely: If `{φᵢ}` is a uniformly convergent sequence of integrable peak functions to zero away from `x₀`, and `g` is an integrable, limit-approaching function at `x₀`, then the product `φᵢ • g` is eventually integrable.