English
If f is locally integrable and symmetric in norm, and f = O[atTop] g with g integrable atTop, then f is integrable.
Русский
Если f локально интегрируема и симметрична по норме, и f = O[atTop] g, где g интегрируема, то f интегрируемо.
LaTeX
$$$\\mathrm{LocallyIntegrable}\\ f \\Rightarrow (\\text{symmetry of }\\|f\\|) \\Rightarrow \\mathrm{IsBigO}\\ f g \\Rightarrow \\mathrm{Integrable} f$$$
Lean4
/-- If `f` is locally integrable, `‖f(-x)‖ = ‖f(x)‖`, and `f =O[atTop] g`, for some
`g` integrable at `atTop`, then `f` is integrable. -/
theorem integrable_of_isBigO_atTop_of_norm_isNegInvariant [IsMeasurablyGenerated (atTop (α := α))] [MeasurableNeg α]
[μ.IsNegInvariant] (hf : LocallyIntegrable f μ) (hsymm : norm ∘ f =ᵐ[μ] norm ∘ f ∘ Neg.neg) (ho : f =O[atTop] g)
(hg : IntegrableAtFilter g atTop μ) : Integrable f μ :=
by
have h_int := (hf.locallyIntegrableOn (Ici 0)).integrableOn_of_isBigO_atTop ho hg
rw [← integrableOn_univ, ← Iic_union_Ici_of_le le_rfl, integrableOn_union]
refine ⟨?_, h_int⟩
have h_map_neg : (μ.restrict (Ici 0)).map Neg.neg = μ.restrict (Iic 0) :=
by
conv => rhs; rw [← Measure.map_neg_eq_self μ, measurableEmbedding_neg.restrict_map]
simp
rw [IntegrableOn, ← h_map_neg, measurableEmbedding_neg.integrable_map_iff]
refine h_int.congr' ?_ hsymm.restrict
refine AEStronglyMeasurable.comp_aemeasurable ?_ measurable_neg.aemeasurable
exact h_map_neg ▸ hf.aestronglyMeasurable.restrict
