-- Mathlib/MeasureTheory/Integral/Asymptotics.lean
theorem IsBigO.integrableAtFilter [IsMeasurablyGenerated l]
    (hf : f =O[l] g) (hfm : StronglyMeasurableAtFilter f l μ) (hg : IntegrableAtFilter g l μ) :
    IntegrableAtFilter f l μ

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
f : α → E
g : α → F
l : Filter α
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup F
μ : Measure α
inst✝ : l.IsMeasurablyGenerated
hf : f =O[l] g
hfm : StronglyMeasurableAtFilter f l μ
hg : IntegrableAtFilter g l μ
⊢ IntegrableAtFilter f l μ

Tactic:
obtain ⟨C, hC⟩ := hf.bound

Result:
case intro
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
f : α → E
g : α → F
l : Filter α
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup F
μ : Measure α
inst✝ : l.IsMeasurablyGenerated
hf : f =O[l] g
hfm : StronglyMeasurableAtFilter f l μ
hg : IntegrableAtFilter g l μ
C : ℝ
hC : ∀ᶠ (x : α) in l, ‖f x‖ ≤ C * ‖g x‖
⊢ IntegrableAtFilter f l μ

Proof state:
case intro
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
f : α → E
g : α → F
l : Filter α
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup F
μ : Measure α
inst✝ : l.IsMeasurablyGenerated
hf : f =O[l] g
hfm : StronglyMeasurableAtFilter f l μ
hg : IntegrableAtFilter g l μ
C : ℝ
hC : ∀ᶠ (x : α) in l, ‖f x‖ ≤ C * ‖g x‖
⊢ IntegrableAtFilter f l μ

Tactic:
obtain ⟨s, hsl, hsm, hfg, hf, hg⟩ :=
  (hC.smallSets.and <| hfm.eventually.and hg.eventually).exists_measurable_mem_of_smallSets

Result:
case intro.intro.intro.intro.intro.intro
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
f : α → E
g : α → F
l : Filter α
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup F
μ : Measure α
inst✝ : l.IsMeasurablyGenerated
hf✝ : f =O[l] g
hfm : StronglyMeasurableAtFilter f l μ
hg✝ : IntegrableAtFilter g l μ
C : ℝ
hC : ∀ᶠ (x : α) in l, ‖f x‖ ≤ C * ‖g x‖
s : Set α
hsl : s ∈ l
hsm : MeasurableSet s
hfg : ∀ x ∈ s, ‖f x‖ ≤ C * ‖g x‖
hf : AEStronglyMeasurable f (μ.restrict s)
hg : IntegrableOn g s μ
⊢ IntegrableAtFilter f l μ

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
f : α → E
g : α → F
l : Filter α
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup F
μ : Measure α
inst✝ : l.IsMeasurablyGenerated
hf✝ : f =O[l] g
hfm : StronglyMeasurableAtFilter f l μ
hg✝ : IntegrableAtFilter g l μ
C : ℝ
hC : ∀ᶠ (x : α) in l, ‖f x‖ ≤ C * ‖g x‖
s : Set α
hsl : s ∈ l
hsm : MeasurableSet s
hfg : ∀ x ∈ s, ‖f x‖ ≤ C * ‖g x‖
hf : AEStronglyMeasurable f (μ.restrict s)
hg : IntegrableOn g s μ
⊢ ∀ᵐ (a : α) ∂μ.restrict s, ‖f a‖ ≤ ‖C * ‖g a‖‖

Tactic:
refine (ae_restrict_mem hsm).mono fun x hx ↦ ?_

Result:
case intro.intro.intro.intro.intro.intro
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
f : α → E
g : α → F
l : Filter α
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup F
μ : Measure α
inst✝ : l.IsMeasurablyGenerated
hf✝ : f =O[l] g
hfm : StronglyMeasurableAtFilter f l μ
hg✝ : IntegrableAtFilter g l μ
C : ℝ
hC : ∀ᶠ (x : α) in l, ‖f x‖ ≤ C * ‖g x‖
s : Set α
hsl : s ∈ l
hsm : MeasurableSet s
hfg : ∀ x ∈ s, ‖f x‖ ≤ C * ‖g x‖
hf : AEStronglyMeasurable f (μ.restrict s)
hg : IntegrableOn g s μ
x : α
hx : x ∈ s
⊢ ‖f x‖ ≤ ‖C * ‖g x‖‖

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
f : α → E
g : α → F
l : Filter α
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup F
μ : Measure α
inst✝ : l.IsMeasurablyGenerated
hf✝ : f =O[l] g
hfm : StronglyMeasurableAtFilter f l μ
hg✝ : IntegrableAtFilter g l μ
C : ℝ
hC : ∀ᶠ (x : α) in l, ‖f x‖ ≤ C * ‖g x‖
s : Set α
hsl : s ∈ l
hsm : MeasurableSet s
hfg : ∀ x ∈ s, ‖f x‖ ≤ C * ‖g x‖
hf : AEStronglyMeasurable f (μ.restrict s)
hg : IntegrableOn g s μ
x : α
hx : x ∈ s
⊢ ‖f x‖ ≤ ‖C * ‖g x‖‖

Tactic:
exact (hfg x hx).trans (le_abs_self _)

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
f : α → E
g : α → F
l : Filter α
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup F
μ : Measure α
inst✝ : l.IsMeasurablyGenerated
hf✝ : f =O[l] g
hfm : StronglyMeasurableAtFilter f l μ
hg✝ : IntegrableAtFilter g l μ
C : ℝ
hC : ∀ᶠ (x : α) in l, ‖f x‖ ≤ C * ‖g x‖
s : Set α
hsl : s ∈ l
hsm : MeasurableSet s
hfg : ∀ x ∈ s, ‖f x‖ ≤ C * ‖g x‖
hf : AEStronglyMeasurable f (μ.restrict s)
hg : IntegrableOn g s μ
⊢ IntegrableAtFilter f l μ

Tactic:
refine ⟨s, hsl, (hg.norm.const_mul C).mono hf ?_⟩

Result:
case intro.intro.intro.intro.intro.intro
α : Type u_1
E : Type u_2
F : Type u_3
inst✝³ : NormedAddCommGroup E
f : α → E
g : α → F
l : Filter α
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup F
μ : Measure α
inst✝ : l.IsMeasurablyGenerated
hf✝ : f =O[l] g
hfm : StronglyMeasurableAtFilter f l μ
hg✝ : IntegrableAtFilter g l μ
C : ℝ
hC : ∀ᶠ (x : α) in l, ‖f x‖ ≤ C * ‖g x‖
s : Set α
hsl : s ∈ l
hsm : MeasurableSet s
hfg : ∀ x ∈ s, ‖f x‖ ≤ C * ‖g x‖
hf : AEStronglyMeasurable f (μ.restrict s)
hg : IntegrableOn g s μ
⊢ ∀ᵐ (a : α) ∂μ.restrict s, ‖f a‖ ≤ ‖C * ‖g a‖‖