Asymptotics of integral

Stream: mathlib4

[Weiyi Wang]

Should there be some theorems about ∫ f ~ ∫ g given f ~ g,where ~ is one of Asymptotics.IsLittleO, Asymptotics.IsBigO etc? (Or maybe there are and I just didn't find them?)

To ensure I didn't just make up false statements, I managed to prove a specialized version for my own use (with a non-mathlib-ready 100-line proof)

import Mathlib.MeasureTheory.Integral.SetIntegral
import Mathlib.MeasureTheory.Measure.Lebesgue.Basic
import Mathlib.Order.CompletePartialOrder

open Asymptotics Filter MeasureTheory

theorem Asymptotics.IsLittleO.integral {f g : ℝ → ℝ}
    (hfg : f =o[atTop] g)
    (hg_tendsto : Tendsto g atTop atTop)
    {a : ℝ}
    (hf_integrable : ∀ x ≥ a, IntegrableOn f (Set.Ioc a x))
    (hg_integrable : ∀ x ≥ a, IntegrableOn g (Set.Ioc a x)):
    (∫ t in Set.Ioc a ·, f t) =o[atTop] (∫ t in Set.Ioc a ·, ‖g t‖) := sorry

I don't know how much this can be generalized.

[Weiyi Wang]

I managed to drop the norm on g t with another hundred of lines :sweat_smile:

[Weiyi Wang]

Anyway, I have them pushed here https://github.com/wwylele/biased-bisect-lean/blob/5b8a76cadfa8cc387fe131d59c51de39fcf55666/BiasedBisect/MathlibMeasureTheoryIntegralAsymptotics.lean#L1

[Etienne Marion]

The hypothesis hg_tendsto seems strange. I think better assumptions are that g has constant sign near infinity and f is not integrable on Ioi a.

[Weiyi Wang]

The hg_tendsto serves another purpose, which is to ensure the integral doesn't just converge to constants on both sides (and thus break IsLittleO). This likely can be weakened to requiring the integral to tends to infinity, but I haven't got time to think deeply in it

[Etienne Marion]

I know this is the purpose of hg_tendsto, but my point is that it can be generalized (this was your original question)

[Weiyi Wang]

ah sorry, I misread your message

[Weiyi Wang]

requiring f not integrable on Ioi a seems also too strict. This should also work when f integrate to a finite value on Ioi, while g grows unbounded. Maybe requiring g not integrable on Ioi (& the consistent sign condition) is good enough?

[Etienne Marion]

I think it would be good enough yes. I have always seen it formulated with f not integrable because it implies that g is not too and if f is integrable but g is not then you likely are not interested in comparing their asymptotic behaviour. So g not integrable is more general, in practice I don't know if it would make much difference.

[Weiyi Wang]

Another thing that I don't know enough about is whether this can be generalized to arbitrary filter (e.g. integrating around a pole of a function). And if it does still work that way, my current approach of the proof won't work...

[Etienne Marion]

I’m pretty sure it is still true with Ioo a b instead of Ioi a

[Weiyi Wang]

I am thinking more about this. Can I generalize this to arbitrary type other than ℝ, which might not even have an order? I think what I want to express is having an "end point" of the set being integrated to be in the filter, or maybe integrating along complement sets of sets in the filter. Not sure what is the best way to express this in mathlib

[Aaron Liu]

(deleted)

[Weiyi Wang]

:thinking: Maybe I should use what improper integral uses https://leanprover-community.github.io/mathlib4_docs/Mathlib/MeasureTheory/Integral/IntegralEqImproper.html#MeasureTheory.AECover

[Etienne Marion]

Maybe the cocompact filter

[Weiyi Wang]

Hmm, I don't see how cocompact helps (nor do I fully understand it). I think what I want is, given a Filter a that appears in the IsBigO hypothesis, I want to translate it to a Filter (Set a) for IsBigO on the integration. When elements in the Filter a "contracts" to its limit (say, b), elements in the Filter (Set a) should expand with its boundary approaching b. I don't know how to precisely express this. I tried Filter.smallSets but it doesn't seem to do what I want

[Weiyi Wang]

Meanwhile, this is what I think the base theorem should look like assuming a partial order (I might be missing some measurability conditions)

theorem Asympotitics.IsBigOWith.integral
    [NormedAddCommGroup E] [NormedSpace ℝ E] [MeasurableSpace α] [PartialOrder α]
    {c : ℝ} {l : Filter α} {f : α → E} {g : α → ℝ}
    (hfg: IsBigOWith c l f g) (μ : Measure α)
    (hf: ∃ᶠ a in l, IntegrableOn f (Set.Iic a) μ)
    (hg: ∃ᶠ a in l, IntegrableOn g (Set.Iic a) μ)
    (hg_tendsto: Tendsto (fun a ↦ ∫ x in (Set.Iic a), g x ∂μ) l atTop):
    ∀ c' > c, IsBigOWith c' l
      (fun a ↦ ∫ x in (Set.Iic a), f x ∂μ) (fun a ↦ ∫ x in (Set.Iic a), g x ∂μ) :=

[Weiyi Wang]

hmm probably not... Even on real numbers, I feel I can come up with some pathological filters that break things. The problem is I don't know how to specify the contraint between the filter and the integral set (the set should grow while the filter shrinks). Maybe I should just focus on the atTop case and the case of a one-side neighborhood of a point

[Weiyi Wang]

At least I have a somewhat general version for atTop with slightly better proof now https://github.com/wwylele/biased-bisect-lean/blob/2cf6c592327453a7608d2c713b2099304facbdcd/BiasedBisect/MathlibMeasureTheoryIntegralAsymptotics.lean#L15