awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
g : α → F
l : Filter α
ι : Type u_4
inst_1 : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
inst_2 : Norm F
hf : f =O[𝓟 s ×ˢ l] (g ∘ Prod.snd)
hfm : ∀ᶠ (x : α) in l, AEStronglyMeasurable.{u_4, u_2} (β := E) (fun (i : ι) ↦ f (i, x)) (μ.restrict s)
hs : MeasurableSet s
hμ : LT.lt (α := ENNReal) ((μ : (a : Set ι) → ENNReal) s : ENNReal) (⊤ : ENNReal)
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖f x‖ ≤ C * ‖(g ∘ Prod.snd) x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht : ∀ y ∈ t, ‖f y‖ ≤ C * ‖(g ∘ Prod.snd) y‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
w : Set α
hwl : w ∈ l
hw : ∀ y ∈ w, AEStronglyMeasurable.{u_4, u_2} (β := E) (fun (i : ι) ↦ f (i, y)) (μ.restrict s)
x : α
hx : x ∈ w ∩ v
⊢ IsFiniteMeasure (μ.restrict s)

Tactic:
haveI : IsFiniteMeasure (μ.restrict s) := ⟨Measure.restrict_apply_univ s ▸ hμ⟩
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
g : α → F
l : Filter α
ι : Type u_4
inst_1 : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
inst_2 : Norm F
hf : f =O[𝓟 s ×ˢ l] (g ∘ Prod.snd)
hfm : ∀ᶠ (x : α) in l, AEStronglyMeasurable.{u_4, u_2} (β := E) (fun (i : ι) ↦ f (i, x)) (μ.restrict s)
hs : MeasurableSet s
hμ : LT.lt (α := ENNReal) ((μ : (a : Set ι) → ENNReal) s : ENNReal) (⊤ : ENNReal)
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖f x‖ ≤ C * ‖(g ∘ Prod.snd) x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht : ∀ y ∈ t, ‖f y‖ ≤ C * ‖(g ∘ Prod.snd) y‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
w : Set α
hwl : w ∈ l
hw : ∀ y ∈ w, AEStronglyMeasurable.{u_4, u_2} (β := E) (fun (i : ι) ↦ f (i, y)) (μ.restrict s)
x : α
hx : x ∈ w ∩ v
this : IsFiniteMeasure (μ.restrict s)
⊢ IntegrableOn.{u_4, u_2} (ε := E) (fun (i : ι) ↦ f (i, x)) s μ

Tactic:
Integrable.mono' (integrable_const (C * ‖g x‖)) (hw x hx.1) ?_

Premises used: Norm.norm, HMul.hMul, MeasureTheory.Integrable.mono', MeasureTheory.IntegrableOn, And.left, MeasureTheory.integrable_const
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
g : α → F
l : Filter α
ι : Type u_4
inst_1 : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
inst_2 : Norm F
hf : f =O[𝓟 s ×ˢ l] (g ∘ Prod.snd)
hfm : ∀ᶠ (x : α) in l, AEStronglyMeasurable.{u_4, u_2} (β := E) (fun (i : ι) ↦ f (i, x)) (μ.restrict s)
hs : MeasurableSet s
hμ : LT.lt (α := ENNReal) ((μ : (a : Set ι) → ENNReal) s : ENNReal) (⊤ : ENNReal)
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖f x‖ ≤ C * ‖(g ∘ Prod.snd) x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht : ∀ y ∈ t, ‖f y‖ ≤ C * ‖(g ∘ Prod.snd) y‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
w : Set α
hwl : w ∈ l
hw : ∀ y ∈ w, AEStronglyMeasurable.{u_4, u_2} (β := E) (fun (i : ι) ↦ f (i, y)) (μ.restrict s)
x : α
hx : x ∈ w ∩ v
this : IsFiniteMeasure (μ.restrict s)
refine : ∀ᵐ (a : ι) ∂μ.restrict s, ‖f (a, x)‖ ≤ C * ‖g x‖
⊢ IntegrableOn.{u_4, u_2} (ε := E) (fun (i : ι) ↦ f (i, x)) s μ

Tactic:
refine Integrable.mono' (integrable_const (C * ‖g x‖)) (hw x hx.1) ?_

Premises used: Norm.norm, HMul.hMul, MeasureTheory.Integrable.mono', And.left, MeasureTheory.integrable_const
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
g : α → F
l : Filter α
ι : Type u_4
inst_1 : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
inst_2 : Norm F
hf : f =O[𝓟 s ×ˢ l] (g ∘ Prod.snd)
hfm : ∀ᶠ (x : α) in l, AEStronglyMeasurable.{u_4, u_2} (β := E) (fun (i : ι) ↦ f (i, x)) (μ.restrict s)
hs : MeasurableSet s
hμ : LT.lt (α := ENNReal) ((μ : (a : Set ι) → ENNReal) s : ENNReal) (⊤ : ENNReal)
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖f x‖ ≤ C * ‖(g ∘ Prod.snd) x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht : ∀ y ∈ t, ‖f y‖ ≤ C * ‖(g ∘ Prod.snd) y‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
w : Set α
hwl : w ∈ l
hw : ∀ y ∈ w, AEStronglyMeasurable.{u_4, u_2} (β := E) (fun (i : ι) ↦ f (i, y)) (μ.restrict s)
x : α
hx : x ∈ w ∩ v
this : IsFiniteMeasure (μ.restrict s)
h : ∀ a ∈ s, ‖f (a, x)‖ ≤ C * ‖g x‖
⊢ ∀ᵐ (a : ι) ∂μ.restrict s, ‖f (a, x)‖ ≤ C * ‖g x‖

Tactic:
filter_upwards [MeasureTheory.self_mem_ae_restrict hs]

Premises used: MeasureTheory.self_mem_ae_restrict
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
g : α → F
l : Filter α
ι : Type u_4
inst_1 : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
inst_2 : Norm F
hf : f =O[𝓟 s ×ˢ l] (g ∘ Prod.snd)
hfm : ∀ᶠ (x : α) in l, AEStronglyMeasurable.{u_4, u_2} (β := E) (fun (i : ι) ↦ f (i, x)) (μ.restrict s)
hs : MeasurableSet s
hμ : LT.lt (α := ENNReal) ((μ : (a : Set ι) → ENNReal) s : ENNReal) (⊤ : ENNReal)
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖f x‖ ≤ C * ‖(g ∘ Prod.snd) x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht : ∀ y ∈ t, ‖f y‖ ≤ C * ‖(g ∘ Prod.snd) y‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
w : Set α
hwl : w ∈ l
hw : ∀ y ∈ w, AEStronglyMeasurable.{u_4, u_2} (β := E) (fun (i : ι) ↦ f (i, y)) (μ.restrict s)
x : α
hx : x ∈ w ∩ v
this : IsFiniteMeasure (μ.restrict s)
y : ι
hy : y ∈ s
⊢ ‖f (y, x)‖ ≤ C * ‖g x‖

Tactic:
ht (y, x) <| huv ⟨hu hy, hx.2⟩

Premises used: Prod.mk, And.right, And.intro
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
g : α → F
l : Filter α
ι : Type u_4
inst_1 : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
inst_2 : Norm F
hf : f =O[𝓟 s ×ˢ l] (g ∘ Prod.snd)
hfm : ∀ᶠ (x : α) in l, AEStronglyMeasurable.{u_4, u_2} (β := E) (fun (i : ι) ↦ f (i, x)) (μ.restrict s)
hs : MeasurableSet s
hμ : LT.lt (α := ENNReal) ((μ : (a : Set ι) → ENNReal) s : ENNReal) (⊤ : ENNReal)
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖f x‖ ≤ C * ‖(g ∘ Prod.snd) x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht : ∀ y ∈ t, ‖f y‖ ≤ C * ‖(g ∘ Prod.snd) y‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
w : Set α
hwl : w ∈ l
hw : ∀ y ∈ w, AEStronglyMeasurable.{u_4, u_2} (β := E) (fun (i : ι) ↦ f (i, y)) (μ.restrict s)
x : α
hx : x ∈ w ∩ v
this : IsFiniteMeasure (μ.restrict s)
y : ι
hy : y ∈ s
⊢ ‖f (y, x)‖ ≤ C * ‖g x‖

Tactic:
exact ht (y, x) <| huv ⟨hu hy, hx.2⟩

Premises used: Prod.mk, And.intro
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
g : α → F
l : Filter α
ι : Type u_4
inst_1 : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
hf : f =O[𝓟 s ×ˢ l] (g ∘ Prod.snd)
hs : MeasurableSet s
hμ : LT.lt (α := ENNReal) ((μ : (a : Set ι) → ENNReal) s : ENNReal) (⊤ : ENNReal)
obtain :
  ∀ (C : ℝ) (hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖f x‖ ≤ C * ‖(g ∘ Prod.snd) x‖),
    IsBigO.{u_1, u_2, u_3} (E := E) l (fun (x : α) ↦ ∫ (i : ι) in s, f (i, x) ∂μ) g
⊢ IsBigO.{u_1, u_2, u_3} (E := E) l (fun (x : α) ↦ ∫ (i : ι) in s, f (i, x) ∂μ) g

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

Premises used: Asymptotics.IsBigO.bound
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
g : α → F
l : Filter α
ι : Type u_4
inst_1 : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
hf : f =O[𝓟 s ×ˢ l] (g ∘ Prod.snd)
hs : MeasurableSet s
hμ : LT.lt (α := ENNReal) ((μ : (a : Set ι) → ENNReal) s : ENNReal) (⊤ : ENNReal)
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖f x‖ ≤ C * ‖(g ∘ Prod.snd) x‖
obtain :
  ∀ (t : Set (ι × α)) (htl : t ∈ 𝓟 s ×ˢ l) (ht : ∀ y ∈ t, ‖f y‖ ≤ C * ‖(g ∘ Prod.snd) y‖),
    IsBigO.{u_1, u_2, u_3} (E := E) l (fun (x : α) ↦ ∫ (i : ι) in s, f (i, x) ∂μ) g
⊢ IsBigO.{u_1, u_2, u_3} (E := E) l (fun (x : α) ↦ ∫ (i : ι) in s, f (i, x) ∂μ) g

Tactic:
obtain ⟨t, htl, ht⟩ := hC.exists_mem

Premises used: Filter.Eventually.exists_mem
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
g : α → F
l : Filter α
ι : Type u_4
inst_1 : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
hf : f =O[𝓟 s ×ˢ l] (g ∘ Prod.snd)
hs : MeasurableSet s
hμ : LT.lt (α := ENNReal) ((μ : (a : Set ι) → ENNReal) s : ENNReal) (⊤ : ENNReal)
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖f x‖ ≤ C * ‖(g ∘ Prod.snd) x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht : ∀ y ∈ t, ‖f y‖ ≤ C * ‖(g ∘ Prod.snd) y‖
obtain :
  ∀ (u : Set ι) (hu : u ∈ 𝓟 s) (v : Set α) (hv : v ∈ l) (huv : u ×ˢ v ⊆ t),
    IsBigO.{u_1, u_2, u_3} (E := E) l (fun (x : α) ↦ ∫ (i : ι) in s, f (i, x) ∂μ) g
⊢ IsBigO.{u_1, u_2, u_3} (E := E) l (fun (x : α) ↦ ∫ (i : ι) in s, f (i, x) ∂μ) g

Tactic:
obtain ⟨u, hu, v, hv, huv⟩ := Filter.mem_prod_iff.mp htl

Premises used: Iff.mp, Filter.mem_prod_iff
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
g : α → F
l : Filter α
ι : Type u_4
inst_1 : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
hf : f =O[𝓟 s ×ˢ l] (g ∘ Prod.snd)
hs : MeasurableSet s
hμ : LT.lt (α := ENNReal) ((μ : (a : Set ι) → ENNReal) s : ENNReal) (⊤ : ENNReal)
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖f x‖ ≤ C * ‖(g ∘ Prod.snd) x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht : ∀ y ∈ t, ‖f y‖ ≤ C * ‖(g ∘ Prod.snd) y‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
⊢ IsBigO.{u_1, u_2, u_3} (E := E) l (fun (x : α) ↦ ∫ (i : ι) in s, f (i, x) ∂μ) g

Tactic:
isBigO_iff.mpr ⟨C * μ.real s, eventually_iff_exists_mem.mpr ⟨v, hv, fun x hx ↦ ?_⟩⟩

Premises used: Iff.mpr, HMul.hMul, Asymptotics.isBigO_iff, MeasureTheory.Measure.real, And.intro, Exists.intro, Filter.eventually_iff_exists_mem
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
g : α → F
l : Filter α
ι : Type u_4
inst_1 : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
hf : f =O[𝓟 s ×ˢ l] (g ∘ Prod.snd)
hs : MeasurableSet s
hμ : LT.lt (α := ENNReal) ((μ : (a : Set ι) → ENNReal) s : ENNReal) (⊤ : ENNReal)
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖f x‖ ≤ C * ‖(g ∘ Prod.snd) x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht : ∀ y ∈ t, ‖f y‖ ≤ C * ‖(g ∘ Prod.snd) y‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
refine : ∀ (x : α) (hx : x ∈ v), norm.{u_2} (E := E) (∫ (i : ι) in s, f (i, x) ∂μ) ≤ C * μ.real s * ‖g x‖
⊢ IsBigO.{u_1, u_2, u_3} (E := E) l (fun (x : α) ↦ ∫ (i : ι) in s, f (i, x) ∂μ) g

Tactic:
refine isBigO_iff.mpr ⟨C * μ.real s, eventually_iff_exists_mem.mpr ⟨v, hv, fun x hx ↦ ?_⟩⟩

Premises used: Iff.mpr, HMul.hMul, Asymptotics.isBigO_iff, MeasureTheory.Measure.real, And.intro, Exists.intro, Filter.eventually_iff_exists_mem
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
g : α → F
l : Filter α
ι : Type u_4
inst_1 : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
hf : f =O[𝓟 s ×ˢ l] (g ∘ Prod.snd)
hs : MeasurableSet s
hμ : LT.lt (α := ENNReal) ((μ : (a : Set ι) → ENNReal) s : ENNReal) (⊤ : ENNReal)
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖f x‖ ≤ C * ‖(g ∘ Prod.snd) x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht : ∀ y ∈ t, ‖f y‖ ≤ C * ‖(g ∘ Prod.snd) y‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
x : α
hx : x ∈ v
rw : norm.{u_2} (E := E) (∫ (i : ι) in s, f (i, x) ∂μ) ≤ ∫ (x_1 : ι) in s, ‖g x‖ • C ∂μ
⊢ norm.{u_2} (E := E) (∫ (i : ι) in s, f (i, x) ∂μ) ≤ C * μ.real s * ‖g x‖

Tactic:
rw [mul_assoc, ← smul_eq_mul _ ‖g x‖, ← MeasureTheory.measureReal_restrict_apply_univ,
    ← integral_const, mul_comm, ← smul_eq_mul, ← integral_smul_const]

Premises used: Norm.norm, integral_smul_const, mul_assoc, MeasureTheory.integral_const, mul_comm, MeasureTheory.measureReal_restrict_apply_univ, smul_eq_mul
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
g : α → F
l : Filter α
ι : Type u_4
inst_1 : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
hf : f =O[𝓟 s ×ˢ l] (g ∘ Prod.snd)
hs : MeasurableSet s
hμ : LT.lt (α := ENNReal) ((μ : (a : Set ι) → ENNReal) s : ENNReal) (⊤ : ENNReal)
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖f x‖ ≤ C * ‖(g ∘ Prod.snd) x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht : ∀ y ∈ t, ‖f y‖ ≤ C * ‖(g ∘ Prod.snd) y‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
x : α
hx : x ∈ v
rw : LT.lt (α := ENNReal) ((μ : (a : Set ι) → ENNReal) s : ENNReal) (⊤ : ENNReal)
⊢ LT.lt (α := ENNReal) ((μ.restrict s : (a : Set ι) → ENNReal) univ : ENNReal) (⊤ : ENNReal)

Tactic:
rw [Measure.restrict_apply_univ s]

Premises used: MeasureTheory.Measure.restrict_apply_univ
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
g : α → F
l : Filter α
ι : Type u_4
inst_1 : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
hf : f =O[𝓟 s ×ˢ l] (g ∘ Prod.snd)
hs : MeasurableSet s
hμ : LT.lt (α := ENNReal) ((μ : (a : Set ι) → ENNReal) s : ENNReal) (⊤ : ENNReal)
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖f x‖ ≤ C * ‖(g ∘ Prod.snd) x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht : ∀ y ∈ t, ‖f y‖ ≤ C * ‖(g ∘ Prod.snd) y‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
x : α
hx : x ∈ v
⊢ LT.lt (α := ENNReal) ((μ : (a : Set ι) → ENNReal) s : ENNReal) (⊤ : ENNReal)

Tactic:
hμ
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
g : α → F
l : Filter α
ι : Type u_4
inst_1 : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
hf : f =O[𝓟 s ×ˢ l] (g ∘ Prod.snd)
hs : MeasurableSet s
hμ : LT.lt (α := ENNReal) ((μ : (a : Set ι) → ENNReal) s : ENNReal) (⊤ : ENNReal)
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖f x‖ ≤ C * ‖(g ∘ Prod.snd) x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht : ∀ y ∈ t, ‖f y‖ ≤ C * ‖(g ∘ Prod.snd) y‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
x : α
hx : x ∈ v
⊢ LT.lt (α := ENNReal) ((μ : (a : Set ι) → ENNReal) s : ENNReal) (⊤ : ENNReal)

Tactic:
exact hμ
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
g : α → F
l : Filter α
ι : Type u_4
inst_1 : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
hf : f =O[𝓟 s ×ˢ l] (g ∘ Prod.snd)
hs : MeasurableSet s
hμ : LT.lt (α := ENNReal) ((μ : (a : Set ι) → ENNReal) s : ENNReal) (⊤ : ENNReal)
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖f x‖ ≤ C * ‖(g ∘ Prod.snd) x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht : ∀ y ∈ t, ‖f y‖ ≤ C * ‖(g ∘ Prod.snd) y‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
x : α
hx : x ∈ v
⊢ IsFiniteMeasure (μ.restrict s)

Tactic:
haveI : IsFiniteMeasure (μ.restrict s) := ⟨by rw [Measure.restrict_apply_univ s]; exact hμ⟩
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
g : α → F
l : Filter α
ι : Type u_4
inst_1 : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
hf : f =O[𝓟 s ×ˢ l] (g ∘ Prod.snd)
hs : MeasurableSet s
hμ : LT.lt (α := ENNReal) ((μ : (a : Set ι) → ENNReal) s : ENNReal) (⊤ : ENNReal)
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖f x‖ ≤ C * ‖(g ∘ Prod.snd) x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht : ∀ y ∈ t, ‖f y‖ ≤ C * ‖(g ∘ Prod.snd) y‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
x : α
hx : x ∈ v
this : IsFiniteMeasure (μ.restrict s)
⊢ norm.{u_2} (E := E) (∫ (i : ι) in s, f (i, x) ∂μ) ≤ ∫ (x_1 : ι) in s, ‖g x‖ • C ∂μ

Tactic:
(norm_integral_le_integral_norm _).trans <|
    integral_mono_of_nonneg (univ_mem' fun _ ↦ norm_nonneg _) (integrable_const _) ?_

Premises used: MeasureTheory.norm_integral_le_integral_norm, Prod.mk, MeasureTheory.integral_mono_of_nonneg, LE.le.trans, norm_nonneg, MeasureTheory.integrable_const, Filter.univ_mem'
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
g : α → F
l : Filter α
ι : Type u_4
inst_1 : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
hf : f =O[𝓟 s ×ˢ l] (g ∘ Prod.snd)
hs : MeasurableSet s
hμ : LT.lt (α := ENNReal) ((μ : (a : Set ι) → ENNReal) s : ENNReal) (⊤ : ENNReal)
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖f x‖ ≤ C * ‖(g ∘ Prod.snd) x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht : ∀ y ∈ t, ‖f y‖ ≤ C * ‖(g ∘ Prod.snd) y‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
x : α
hx : x ∈ v
this : IsFiniteMeasure (μ.restrict s)
refine : (ae (μ.restrict s)).EventuallyLE (β := ℝ) (fun (a : ι) ↦ ‖f (a, x)‖) fun (x_1 : ι) ↦ ‖g x‖ • C
⊢ norm.{u_2} (E := E) (∫ (i : ι) in s, f (i, x) ∂μ) ≤ ∫ (x_1 : ι) in s, ‖g x‖ • C ∂μ

Tactic:
refine (norm_integral_le_integral_norm _).trans <|
    integral_mono_of_nonneg (univ_mem' fun _ ↦ norm_nonneg _) (integrable_const _) ?_

Premises used: MeasureTheory.norm_integral_le_integral_norm, MeasureTheory.integral_mono_of_nonneg, LE.le.trans, MeasureTheory.integrable_const, Filter.univ_mem'
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
g : α → F
l : Filter α
ι : Type u_4
inst_1 : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
hf : f =O[𝓟 s ×ˢ l] (g ∘ Prod.snd)
hs : MeasurableSet s
hμ : LT.lt (α := ENNReal) ((μ : (a : Set ι) → ENNReal) s : ENNReal) (⊤ : ENNReal)
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖f x‖ ≤ C * ‖(g ∘ Prod.snd) x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht : ∀ y ∈ t, ‖f y‖ ≤ C * ‖(g ∘ Prod.snd) y‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
x : α
hx : x ∈ v
this : IsFiniteMeasure (μ.restrict s)
h : ∀ a ∈ s, ‖f (a, x)‖ ≤ ‖g x‖ • C
⊢ (ae (μ.restrict s)).EventuallyLE (β := ℝ) (fun (a : ι) ↦ ‖f (a, x)‖) fun (x_1 : ι) ↦ ‖g x‖ • C

Tactic:
filter_upwards [MeasureTheory.self_mem_ae_restrict hs]

Premises used: MeasureTheory.self_mem_ae_restrict
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
g : α → F
l : Filter α
ι : Type u_4
inst_1 : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
hf : f =O[𝓟 s ×ˢ l] (g ∘ Prod.snd)
hs : MeasurableSet s
hμ : LT.lt (α := ENNReal) ((μ : (a : Set ι) → ENNReal) s : ENNReal) (⊤ : ENNReal)
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖f x‖ ≤ C * ‖(g ∘ Prod.snd) x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht : ∀ y ∈ t, ‖f y‖ ≤ C * ‖(g ∘ Prod.snd) y‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
x : α
hx : x ∈ v
this : IsFiniteMeasure (μ.restrict s)
y : ι
hy : y ∈ s
h : ‖f (y, x)‖ ≤ C * ‖g x‖
⊢ ‖f (y, x)‖ ≤ ‖g x‖ • C

Tactic:
rw [smul_eq_mul, mul_comm]

Premises used: mul_comm, smul_eq_mul
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
g : α → F
l : Filter α
ι : Type u_4
inst_1 : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
hf : f =O[𝓟 s ×ˢ l] (g ∘ Prod.snd)
hs : MeasurableSet s
hμ : LT.lt (α := ENNReal) ((μ : (a : Set ι) → ENNReal) s : ENNReal) (⊤ : ENNReal)
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖f x‖ ≤ C * ‖(g ∘ Prod.snd) x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht : ∀ y ∈ t, ‖f y‖ ≤ C * ‖(g ∘ Prod.snd) y‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
x : α
hx : x ∈ v
this : IsFiniteMeasure (μ.restrict s)
y : ι
hy : y ∈ s
⊢ ‖f (y, x)‖ ≤ C * ‖g x‖

Tactic:
ht (y, x) <| huv ⟨hu hy, hx⟩

Premises used: Prod.mk, And.intro
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
g : α → F
l : Filter α
ι : Type u_4
inst_1 : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
inst_2 : NormedSpace ℝ E
inst_3 : NormedAddCommGroup F
hf : f =O[𝓟 s ×ˢ l] (g ∘ Prod.snd)
hs : MeasurableSet s
hμ : LT.lt (α := ENNReal) ((μ : (a : Set ι) → ENNReal) s : ENNReal) (⊤ : ENNReal)
C : ℝ
hC : ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l, ‖f x‖ ≤ C * ‖(g ∘ Prod.snd) x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht : ∀ y ∈ t, ‖f y‖ ≤ C * ‖(g ∘ Prod.snd) y‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
x : α
hx : x ∈ v
this : IsFiniteMeasure (μ.restrict s)
y : ι
hy : y ∈ s
⊢ ‖f (y, x)‖ ≤ C * ‖g x‖

Tactic:
exact ht (y, x) <| huv ⟨hu hy, hx⟩

Premises used: Prod.mk, And.intro
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : MeasurableSpace α
μ : Measure α
inst_4 : NormedAddCommGroup F
inst_5 : (cocompact α).IsMeasurablyGenerated
hf : LocallyIntegrable f μ
ho : f =O[cocompact α] g
hg : IntegrableAtFilter g (cocompact α) μ
⊢ Integrable f μ

Tactic:
integrable_iff_integrableAtFilter_cocompact.mpr ⟨ho.integrableAtFilter ?_ hg, hf⟩

Premises used: Asymptotics.IsBigO.integrableAtFilter, Iff.mpr, MeasureTheory.integrable_iff_integrableAtFilter_cocompact, And.intro
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : MeasurableSpace α
μ : Measure α
inst_4 : NormedAddCommGroup F
inst_5 : (cocompact α).IsMeasurablyGenerated
hf : LocallyIntegrable f μ
ho : f =O[cocompact α] g
hg : IntegrableAtFilter g (cocompact α) μ
refine : StronglyMeasurableAtFilter f (cocompact α) μ
⊢ Integrable f μ

Tactic:
refine integrable_iff_integrableAtFilter_cocompact.mpr ⟨ho.integrableAtFilter ?_ hg, hf⟩

Premises used: Asymptotics.IsBigO.integrableAtFilter, Iff.mpr, MeasureTheory.integrable_iff_integrableAtFilter_cocompact, And.intro
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : MeasurableSpace α
μ : Measure α
inst_4 : NormedAddCommGroup F
inst_5 : (cocompact α).IsMeasurablyGenerated
hf : LocallyIntegrable f μ
ho : f =O[cocompact α] g
hg : IntegrableAtFilter g (cocompact α) μ
⊢ StronglyMeasurableAtFilter f (cocompact α) μ

Tactic:
hf.aestronglyMeasurable.stronglyMeasurableAtFilter

Premises used: MeasureTheory.AEStronglyMeasurable.stronglyMeasurableAtFilter, MeasureTheory.LocallyIntegrable.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Integral.Asymptotics
Goal:
α : Type u_1
E : Type u_2
F : Type u_3
inst : NormedAddCommGroup E
f : α → E
g : α → F
inst_1 : TopologicalSpace α
inst_2 : SecondCountableTopology α
inst_3 : MeasurableSpace α
μ : Measure α
inst_4 : NormedAddCommGroup F
inst_5 : (cocompact α).IsMeasurablyGenerated
hf : LocallyIntegrable f μ
ho : f =O[cocompact α] g
hg : IntegrableAtFilter g (cocompact α) μ
⊢ StronglyMeasurableAtFilter f (cocompact α) μ

Tactic:
exact hf.aestronglyMeasurable.stronglyMeasurableAtFilter

Premises used: MeasureTheory.AEStronglyMeasurable.stronglyMeasurableAtFilter, MeasureTheory.LocallyIntegrable.aestronglyMeasurable