English
If f is continuous on t, t is measurable, t is separable (in the topological sense), and a ∈ t, then f is integrable at nhdsWithin a t with respect to μ.
Русский
Если f непрерывна на t, t измеримо, t сепарабельно, и a ∈ t, то f интегрируема в окрестности nhdsWithin a t по μ.
LaTeX
$$$\\text{IntegrableAtFilter } f (\\nhdsWithin a t) \\ μ$ under the given hypotheses.$$
Lean4
theorem integrableAt_nhdsWithin_of_isSeparable [TopologicalSpace α] [PseudoMetrizableSpace α] [OpensMeasurableSpace α]
{μ : Measure α} [IsLocallyFiniteMeasure μ] {a : α} {t : Set α} {f : α → E} (hft : ContinuousOn f t)
(ht : MeasurableSet t) (h't : TopologicalSpace.IsSeparable t) (ha : a ∈ t) : IntegrableAtFilter f (𝓝[t] a) μ :=
haveI : (𝓝[t] a).IsMeasurablyGenerated := ht.nhdsWithin_isMeasurablyGenerated _
(hft a ha).integrableAtFilter ⟨_, self_mem_nhdsWithin, hft.aestronglyMeasurable_of_isSeparable ht h't⟩
(μ.finiteAt_nhdsWithin _ _)
