English
If f is locally integrable and ‖f(−x)‖ = ‖f(x)‖ almost everywhere, and f = O[atTop] g with g integrable atTop, then f is integrable.
Русский
Если f локально интегрируемо и ‖f(−x)‖ = ‖f(x)‖ почти повсеместно, и f = O[atTop] g, где g интегрируема на atTop, то f интегрируемо.
LaTeX
$$$\\mathrm{LocallyIntegrable}\\; f\\; \\Rightarrow \\; (\\|f(-x)\\|=\\|f(x)\\|)\\implies \\mathrm{IntegrableAtFilter}\\ g \\Rightarrow \\mathrm{Integrable}\\ f$$$
Lean4
/-- If `f` is locally integrable, `f` has a bottom element, and `f =O[atTop] g`, for some
`g` integrable at `atTop`, then `f` is integrable. -/
theorem integrable_of_isBigO_atTop [IsMeasurablyGenerated (atTop (α := α))] [OrderBot α] (hf : LocallyIntegrable f μ)
(ho : f =O[atTop] g) (hg : IntegrableAtFilter g atTop μ) : Integrable f μ :=
by
refine integrable_iff_integrableAtFilter_atTop.mpr ⟨ho.integrableAtFilter ?_ hg, hf⟩
exact hf.aestronglyMeasurable.stronglyMeasurableAtFilter
