internlm/Lean-Github huggingface dataset:
Theorem: ContinuousOn.const_isBigOWithUniformlyOn_isCompact_rev
Proof state before:
case refine_2.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : TopologicalSpace ι
C : ι → E
c : F
inst✝¹ : NormedAddGroup E
inst✝ : SeminormedAddGroup F
hf : ContinuousOn C s
hC : ∀ i ∈ s, C i ≠ 0
l : Filter α
x✝ : ι × α
hx✝ : x✝ ∈ s ×ˢ Set.univ
hs : IsCompact ((fun a => ‖a‖) '' (C '' s))
h_sInf : IsGLB ((fun a => ‖a‖) '' (C '' s)) (sInf ((fun a => ‖a‖) '' (C '' s)))
w✝ : E
hnormCx : (fun a => ‖a‖) w✝ = sInf ((fun a => ‖a‖) '' (C '' s))
x : ι
hx : x ∈ s
hCx : C x = w✝
⊢ 0 < sInf (norm '' (C '' s))
Tactic:
rewrite [← hnormCx, ← hCx]
Proof state after:
case refine_2.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : TopologicalSpace ι
C : ι → E
c : F
inst✝¹ : NormedAddGroup E
inst✝ : SeminormedAddGroup F
hf : ContinuousOn C s
hC : ∀ i ∈ s, C i ≠ 0
l : Filter α
x✝ : ι × α
hx✝ : x✝ ∈ s ×ˢ Set.univ
hs : IsCompact ((fun a => ‖a‖) '' (C '' s))
h_sInf : IsGLB ((fun a => ‖a‖) '' (C '' s)) (sInf ((fun a => ‖a‖) '' (C '' s)))
w✝ : E
hnormCx : (fun a => ‖a‖) w✝ = sInf ((fun a => ‖a‖) '' (C '' s))
x : ι
hx : x ∈ s
hCx : C x = w✝
⊢ 0 < (fun a => ‖a‖) (C x)
Theorem: ContinuousOn.const_isBigOWithUniformlyOn_isCompact_rev
Proof state before:
case refine_2.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : TopologicalSpace ι
C : ι → E
c : F
inst✝¹ : NormedAddGroup E
inst✝ : SeminormedAddGroup F
hf : ContinuousOn C s
hC : ∀ i ∈ s, C i ≠ 0
l : Filter α
x✝ : ι × α
hx✝ : x✝ ∈ s ×ˢ Set.univ
hs : IsCompact ((fun a => ‖a‖) '' (C '' s))
h_sInf : IsGLB ((fun a => ‖a‖) '' (C '' s)) (sInf ((fun a => ‖a‖) '' (C '' s)))
w✝ : E
hnormCx : (fun a => ‖a‖) w✝ = sInf ((fun a => ‖a‖) '' (C '' s))
x : ι
hx : x ∈ s
hCx : C x = w✝
⊢ 0 < (fun a => ‖a‖) (C x)
Tactic:
exact (norm_ne_zero_iff.mpr (hC x hx)).symm.lt_of_le (norm_nonneg _)
Proof state after:
no goals
Theorem: Asymptotics.IsBigO.eventually_integrableOn
Proof state before:
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : MeasurableSpace ι
inst✝¹ : NormedAddCommGroup E
f : ι × α → E
g : α → F
μ : Measure ι
l : Filter α
inst✝ : Norm F
hf :
  f =O[𝓟 s ×ˢ l] fun x =>
    match x with
    | (_i, x) => g x
hfm : ∀ᶠ (x : α) in l, AEStronglyMeasurable (fun i => f (i, x)) (μ.restrict s)
hs : MeasurableSet s
hμ : μ s < ⊤
⊢ ∀ᶠ (x : α) in l, IntegrableOn (fun i => f (i, x)) s μ
Tactic:
obtain ⟨C, hC⟩ := hf.bound
Proof state after:
case intro
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : MeasurableSpace ι
inst✝¹ : NormedAddCommGroup E
f : ι × α → E
g : α → F
μ : Measure ι
l : Filter α
inst✝ : Norm F
hf :
  f =O[𝓟 s ×ˢ l] fun x =>
    match x with
    | (_i, x) => g x
hfm : ∀ᶠ (x : α) in l, AEStronglyMeasurable (fun i => f (i, x)) (μ.restrict s)
hs : MeasurableSet s
hμ : μ s < ⊤
C : ℝ
hC :
  ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l,
    ‖f x‖ ≤
      C *
        ‖match x with
          | (_i, x) => g x‖
⊢ ∀ᶠ (x : α) in l, IntegrableOn (fun i => f (i, x)) s μ
Theorem: Asymptotics.IsBigO.eventually_integrableOn
Proof state before:
case intro
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : MeasurableSpace ι
inst✝¹ : NormedAddCommGroup E
f : ι × α → E
g : α → F
μ : Measure ι
l : Filter α
inst✝ : Norm F
hf :
  f =O[𝓟 s ×ˢ l] fun x =>
    match x with
    | (_i, x) => g x
hfm : ∀ᶠ (x : α) in l, AEStronglyMeasurable (fun i => f (i, x)) (μ.restrict s)
hs : MeasurableSet s
hμ : μ s < ⊤
C : ℝ
hC :
  ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l,
    ‖f x‖ ≤
      C *
        ‖match x with
          | (_i, x) => g x‖
⊢ ∀ᶠ (x : α) in l, IntegrableOn (fun i => f (i, x)) s μ
Tactic:
obtain ⟨t, htl, ht⟩ := hC.exists_mem
Proof state after:
case intro.intro.intro
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : MeasurableSpace ι
inst✝¹ : NormedAddCommGroup E
f : ι × α → E
g : α → F
μ : Measure ι
l : Filter α
inst✝ : Norm F
hf :
  f =O[𝓟 s ×ˢ l] fun x =>
    match x with
    | (_i, x) => g x
hfm : ∀ᶠ (x : α) in l, AEStronglyMeasurable (fun i => f (i, x)) (μ.restrict s)
hs : MeasurableSet s
hμ : μ s < ⊤
C : ℝ
hC :
  ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l,
    ‖f x‖ ≤
      C *
        ‖match x with
          | (_i, x) => g x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht :
  ∀ y ∈ t,
    ‖f y‖ ≤
      C *
        ‖match y with
          | (_i, x) => g x‖
⊢ ∀ᶠ (x : α) in l, IntegrableOn (fun i => f (i, x)) s μ
Theorem: Asymptotics.IsBigO.eventually_integrableOn
Proof state before:
case intro.intro.intro
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : MeasurableSpace ι
inst✝¹ : NormedAddCommGroup E
f : ι × α → E
g : α → F
μ : Measure ι
l : Filter α
inst✝ : Norm F
hf :
  f =O[𝓟 s ×ˢ l] fun x =>
    match x with
    | (_i, x) => g x
hfm : ∀ᶠ (x : α) in l, AEStronglyMeasurable (fun i => f (i, x)) (μ.restrict s)
hs : MeasurableSet s
hμ : μ s < ⊤
C : ℝ
hC :
  ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l,
    ‖f x‖ ≤
      C *
        ‖match x with
          | (_i, x) => g x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht :
  ∀ y ∈ t,
    ‖f y‖ ≤
      C *
        ‖match y with
          | (_i, x) => g x‖
⊢ ∀ᶠ (x : α) in l, IntegrableOn (fun i => f (i, x)) s μ
Tactic:
obtain ⟨u, hu, v, hv, huv⟩ := Filter.mem_prod_iff.mp htl
Proof state after:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : MeasurableSpace ι
inst✝¹ : NormedAddCommGroup E
f : ι × α → E
g : α → F
μ : Measure ι
l : Filter α
inst✝ : Norm F
hf :
  f =O[𝓟 s ×ˢ l] fun x =>
    match x with
    | (_i, x) => g x
hfm : ∀ᶠ (x : α) in l, AEStronglyMeasurable (fun i => f (i, x)) (μ.restrict s)
hs : MeasurableSet s
hμ : μ s < ⊤
C : ℝ
hC :
  ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l,
    ‖f x‖ ≤
      C *
        ‖match x with
          | (_i, x) => g x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht :
  ∀ y ∈ t,
    ‖f y‖ ≤
      C *
        ‖match y with
          | (_i, x) => g x‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
⊢ ∀ᶠ (x : α) in l, IntegrableOn (fun i => f (i, x)) s μ
Theorem: Asymptotics.IsBigO.eventually_integrableOn
Proof state before:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : MeasurableSpace ι
inst✝¹ : NormedAddCommGroup E
f : ι × α → E
g : α → F
μ : Measure ι
l : Filter α
inst✝ : Norm F
hf :
  f =O[𝓟 s ×ˢ l] fun x =>
    match x with
    | (_i, x) => g x
hfm : ∀ᶠ (x : α) in l, AEStronglyMeasurable (fun i => f (i, x)) (μ.restrict s)
hs : MeasurableSet s
hμ : μ s < ⊤
C : ℝ
hC :
  ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l,
    ‖f x‖ ≤
      C *
        ‖match x with
          | (_i, x) => g x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht :
  ∀ y ∈ t,
    ‖f y‖ ≤
      C *
        ‖match y with
          | (_i, x) => g x‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
⊢ ∀ᶠ (x : α) in l, IntegrableOn (fun i => f (i, x)) s μ
Tactic:
obtain ⟨w, hwl, hw⟩ := hfm.exists_mem
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : MeasurableSpace ι
inst✝¹ : NormedAddCommGroup E
f : ι × α → E
g : α → F
μ : Measure ι
l : Filter α
inst✝ : Norm F
hf :
  f =O[𝓟 s ×ˢ l] fun x =>
    match x with
    | (_i, x) => g x
hfm : ∀ᶠ (x : α) in l, AEStronglyMeasurable (fun i => f (i, x)) (μ.restrict s)
hs : MeasurableSet s
hμ : μ s < ⊤
C : ℝ
hC :
  ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l,
    ‖f x‖ ≤
      C *
        ‖match x with
          | (_i, x) => g x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht :
  ∀ y ∈ t,
    ‖f y‖ ≤
      C *
        ‖match y with
          | (_i, x) => g x‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
w : Set α
hwl : w ∈ l
hw : ∀ y ∈ w, AEStronglyMeasurable (fun i => f (i, y)) (μ.restrict s)
⊢ ∀ᶠ (x : α) in l, IntegrableOn (fun i => f (i, x)) s μ
Theorem: Asymptotics.IsBigO.eventually_integrableOn
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : MeasurableSpace ι
inst✝¹ : NormedAddCommGroup E
f : ι × α → E
g : α → F
μ : Measure ι
l : Filter α
inst✝ : Norm F
hf :
  f =O[𝓟 s ×ˢ l] fun x =>
    match x with
    | (_i, x) => g x
hfm : ∀ᶠ (x : α) in l, AEStronglyMeasurable (fun i => f (i, x)) (μ.restrict s)
hs : MeasurableSet s
hμ : μ s < ⊤
C : ℝ
hC :
  ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l,
    ‖f x‖ ≤
      C *
        ‖match x with
          | (_i, x) => g x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht :
  ∀ y ∈ t,
    ‖f y‖ ≤
      C *
        ‖match y with
          | (_i, x) => g x‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
w : Set α
hwl : w ∈ l
hw : ∀ y ∈ w, AEStronglyMeasurable (fun i => f (i, y)) (μ.restrict s)
⊢ ∀ᶠ (x : α) in l, IntegrableOn (fun i => f (i, x)) s μ
Tactic:
refine eventually_iff_exists_mem.mpr ⟨w ∩ v, inter_mem hwl hv, fun x hx ↦ ?_⟩
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : MeasurableSpace ι
inst✝¹ : NormedAddCommGroup E
f : ι × α → E
g : α → F
μ : Measure ι
l : Filter α
inst✝ : Norm F
hf :
  f =O[𝓟 s ×ˢ l] fun x =>
    match x with
    | (_i, x) => g x
hfm : ∀ᶠ (x : α) in l, AEStronglyMeasurable (fun i => f (i, x)) (μ.restrict s)
hs : MeasurableSet s
hμ : μ s < ⊤
C : ℝ
hC :
  ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l,
    ‖f x‖ ≤
      C *
        ‖match x with
          | (_i, x) => g x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht :
  ∀ y ∈ t,
    ‖f y‖ ≤
      C *
        ‖match y with
          | (_i, x) => g x‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
w : Set α
hwl : w ∈ l
hw : ∀ y ∈ w, AEStronglyMeasurable (fun i => f (i, y)) (μ.restrict s)
x : α
hx : x ∈ w ∩ v
⊢ IntegrableOn (fun i => f (i, x)) s μ
Theorem: Asymptotics.IsBigO.eventually_integrableOn
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : MeasurableSpace ι
inst✝¹ : NormedAddCommGroup E
f : ι × α → E
g : α → F
μ : Measure ι
l : Filter α
inst✝ : Norm F
hf :
  f =O[𝓟 s ×ˢ l] fun x =>
    match x with
    | (_i, x) => g x
hfm : ∀ᶠ (x : α) in l, AEStronglyMeasurable (fun i => f (i, x)) (μ.restrict s)
hs : MeasurableSet s
hμ : μ s < ⊤
C : ℝ
hC :
  ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l,
    ‖f x‖ ≤
      C *
        ‖match x with
          | (_i, x) => g x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht :
  ∀ y ∈ t,
    ‖f y‖ ≤
      C *
        ‖match y with
          | (_i, x) => g x‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
w : Set α
hwl : w ∈ l
hw : ∀ y ∈ w, AEStronglyMeasurable (fun i => f (i, y)) (μ.restrict s)
x : α
hx : x ∈ w ∩ v
⊢ IntegrableOn (fun i => f (i, x)) s μ
Tactic:
haveI : IsFiniteMeasure (μ.restrict s) :=
  ⟨by convert hμ using 1; exact Measure.restrict_apply_univ s⟩
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : MeasurableSpace ι
inst✝¹ : NormedAddCommGroup E
f : ι × α → E
g : α → F
μ : Measure ι
l : Filter α
inst✝ : Norm F
hf :
  f =O[𝓟 s ×ˢ l] fun x =>
    match x with
    | (_i, x) => g x
hfm : ∀ᶠ (x : α) in l, AEStronglyMeasurable (fun i => f (i, x)) (μ.restrict s)
hs : MeasurableSet s
hμ : μ s < ⊤
C : ℝ
hC :
  ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l,
    ‖f x‖ ≤
      C *
        ‖match x with
          | (_i, x) => g x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht :
  ∀ y ∈ t,
    ‖f y‖ ≤
      C *
        ‖match y with
          | (_i, x) => g x‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
w : Set α
hwl : w ∈ l
hw : ∀ y ∈ w, AEStronglyMeasurable (fun i => f (i, y)) (μ.restrict s)
x : α
hx : x ∈ w ∩ v
this : IsFiniteMeasure (μ.restrict s)
⊢ IntegrableOn (fun i => f (i, x)) s μ
Theorem: Asymptotics.IsBigO.eventually_integrableOn
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : MeasurableSpace ι
inst✝¹ : NormedAddCommGroup E
f : ι × α → E
g : α → F
μ : Measure ι
l : Filter α
inst✝ : Norm F
hf :
  f =O[𝓟 s ×ˢ l] fun x =>
    match x with
    | (_i, x) => g x
hfm : ∀ᶠ (x : α) in l, AEStronglyMeasurable (fun i => f (i, x)) (μ.restrict s)
hs : MeasurableSet s
hμ : μ s < ⊤
C : ℝ
hC :
  ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l,
    ‖f x‖ ≤
      C *
        ‖match x with
          | (_i, x) => g x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht :
  ∀ y ∈ t,
    ‖f y‖ ≤
      C *
        ‖match y with
          | (_i, x) => g x‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
w : Set α
hwl : w ∈ l
hw : ∀ y ∈ w, AEStronglyMeasurable (fun i => f (i, y)) (μ.restrict s)
x : α
hx : x ∈ w ∩ v
this : IsFiniteMeasure (μ.restrict s)
⊢ IntegrableOn (fun i => f (i, x)) s μ
Tactic:
refine Integrable.mono' (integrable_const (C * ‖g x‖)) (hw x hx.1) ?_
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : MeasurableSpace ι
inst✝¹ : NormedAddCommGroup E
f : ι × α → E
g : α → F
μ : Measure ι
l : Filter α
inst✝ : Norm F
hf :
  f =O[𝓟 s ×ˢ l] fun x =>
    match x with
    | (_i, x) => g x
hfm : ∀ᶠ (x : α) in l, AEStronglyMeasurable (fun i => f (i, x)) (μ.restrict s)
hs : MeasurableSet s
hμ : μ s < ⊤
C : ℝ
hC :
  ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l,
    ‖f x‖ ≤
      C *
        ‖match x with
          | (_i, x) => g x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht :
  ∀ y ∈ t,
    ‖f y‖ ≤
      C *
        ‖match y with
          | (_i, x) => g x‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
w : Set α
hwl : w ∈ l
hw : ∀ y ∈ w, AEStronglyMeasurable (fun i => f (i, y)) (μ.restrict s)
x : α
hx : x ∈ w ∩ v
this : IsFiniteMeasure (μ.restrict s)
⊢ ∀ᵐ (a : ι) ∂μ.restrict s, ‖f (a, x)‖ ≤ C * ‖g x‖
Theorem: Asymptotics.IsBigO.eventually_integrableOn
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : MeasurableSpace ι
inst✝¹ : NormedAddCommGroup E
f : ι × α → E
g : α → F
μ : Measure ι
l : Filter α
inst✝ : Norm F
hf :
  f =O[𝓟 s ×ˢ l] fun x =>
    match x with
    | (_i, x) => g x
hfm : ∀ᶠ (x : α) in l, AEStronglyMeasurable (fun i => f (i, x)) (μ.restrict s)
hs : MeasurableSet s
hμ : μ s < ⊤
C : ℝ
hC :
  ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l,
    ‖f x‖ ≤
      C *
        ‖match x with
          | (_i, x) => g x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht :
  ∀ y ∈ t,
    ‖f y‖ ≤
      C *
        ‖match y with
          | (_i, x) => g x‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
w : Set α
hwl : w ∈ l
hw : ∀ y ∈ w, AEStronglyMeasurable (fun i => f (i, y)) (μ.restrict s)
x : α
hx : x ∈ w ∩ v
this : IsFiniteMeasure (μ.restrict s)
⊢ ∀ᵐ (a : ι) ∂μ.restrict s, ‖f (a, x)‖ ≤ C * ‖g x‖
Tactic:
filter_upwards [MeasureTheory.self_mem_ae_restrict hs]
Proof state after:
case h
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : MeasurableSpace ι
inst✝¹ : NormedAddCommGroup E
f : ι × α → E
g : α → F
μ : Measure ι
l : Filter α
inst✝ : Norm F
hf :
  f =O[𝓟 s ×ˢ l] fun x =>
    match x with
    | (_i, x) => g x
hfm : ∀ᶠ (x : α) in l, AEStronglyMeasurable (fun i => f (i, x)) (μ.restrict s)
hs : MeasurableSet s
hμ : μ s < ⊤
C : ℝ
hC :
  ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l,
    ‖f x‖ ≤
      C *
        ‖match x with
          | (_i, x) => g x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht :
  ∀ y ∈ t,
    ‖f y‖ ≤
      C *
        ‖match y with
          | (_i, x) => g x‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
w : Set α
hwl : w ∈ l
hw : ∀ y ∈ w, AEStronglyMeasurable (fun i => f (i, y)) (μ.restrict s)
x : α
hx : x ∈ w ∩ v
this : IsFiniteMeasure (μ.restrict s)
⊢ ∀ a ∈ s, ‖f (a, x)‖ ≤ C * ‖g x‖
Theorem: Asymptotics.IsBigO.eventually_integrableOn
Proof state before:
case h
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : MeasurableSpace ι
inst✝¹ : NormedAddCommGroup E
f : ι × α → E
g : α → F
μ : Measure ι
l : Filter α
inst✝ : Norm F
hf :
  f =O[𝓟 s ×ˢ l] fun x =>
    match x with
    | (_i, x) => g x
hfm : ∀ᶠ (x : α) in l, AEStronglyMeasurable (fun i => f (i, x)) (μ.restrict s)
hs : MeasurableSet s
hμ : μ s < ⊤
C : ℝ
hC :
  ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l,
    ‖f x‖ ≤
      C *
        ‖match x with
          | (_i, x) => g x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht :
  ∀ y ∈ t,
    ‖f y‖ ≤
      C *
        ‖match y with
          | (_i, x) => g x‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
w : Set α
hwl : w ∈ l
hw : ∀ y ∈ w, AEStronglyMeasurable (fun i => f (i, y)) (μ.restrict s)
x : α
hx : x ∈ w ∩ v
this : IsFiniteMeasure (μ.restrict s)
⊢ ∀ a ∈ s, ‖f (a, x)‖ ≤ C * ‖g x‖
Tactic:
intro y hy
Proof state after:
case h
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : MeasurableSpace ι
inst✝¹ : NormedAddCommGroup E
f : ι × α → E
g : α → F
μ : Measure ι
l : Filter α
inst✝ : Norm F
hf :
  f =O[𝓟 s ×ˢ l] fun x =>
    match x with
    | (_i, x) => g x
hfm : ∀ᶠ (x : α) in l, AEStronglyMeasurable (fun i => f (i, x)) (μ.restrict s)
hs : MeasurableSet s
hμ : μ s < ⊤
C : ℝ
hC :
  ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l,
    ‖f x‖ ≤
      C *
        ‖match x with
          | (_i, x) => g x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht :
  ∀ y ∈ t,
    ‖f y‖ ≤
      C *
        ‖match y with
          | (_i, x) => g x‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
w : Set α
hwl : w ∈ l
hw : ∀ y ∈ w, AEStronglyMeasurable (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‖
Theorem: Asymptotics.IsBigO.eventually_integrableOn
Proof state before:
case h
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : MeasurableSpace ι
inst✝¹ : NormedAddCommGroup E
f : ι × α → E
g : α → F
μ : Measure ι
l : Filter α
inst✝ : Norm F
hf :
  f =O[𝓟 s ×ˢ l] fun x =>
    match x with
    | (_i, x) => g x
hfm : ∀ᶠ (x : α) in l, AEStronglyMeasurable (fun i => f (i, x)) (μ.restrict s)
hs : MeasurableSet s
hμ : μ s < ⊤
C : ℝ
hC :
  ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l,
    ‖f x‖ ≤
      C *
        ‖match x with
          | (_i, x) => g x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht :
  ∀ y ∈ t,
    ‖f y‖ ≤
      C *
        ‖match y with
          | (_i, x) => g x‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
w : Set α
hwl : w ∈ l
hw : ∀ y ∈ w, AEStronglyMeasurable (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⟩
Proof state after:
no goals
Theorem: Asymptotics.IsBigO.eventually_integrableOn
Proof state before:
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : MeasurableSpace ι
inst✝¹ : NormedAddCommGroup E
f : ι × α → E
g : α → F
μ : Measure ι
l : Filter α
inst✝ : Norm F
hf :
  f =O[𝓟 s ×ˢ l] fun x =>
    match x with
    | (_i, x) => g x
hfm : ∀ᶠ (x : α) in l, AEStronglyMeasurable (fun i => f (i, x)) (μ.restrict s)
hs : MeasurableSet s
hμ : μ s < ⊤
C : ℝ
hC :
  ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l,
    ‖f x‖ ≤
      C *
        ‖match x with
          | (_i, x) => g x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht :
  ∀ y ∈ t,
    ‖f y‖ ≤
      C *
        ‖match y with
          | (_i, x) => g x‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
w : Set α
hwl : w ∈ l
hw : ∀ y ∈ w, AEStronglyMeasurable (fun i => f (i, y)) (μ.restrict s)
x : α
hx : x ∈ w ∩ v
⊢ (μ.restrict s) Set.univ < ⊤
Tactic:
convert hμ using 1
Proof state after:
case h.e'_3
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : MeasurableSpace ι
inst✝¹ : NormedAddCommGroup E
f : ι × α → E
g : α → F
μ : Measure ι
l : Filter α
inst✝ : Norm F
hf :
  f =O[𝓟 s ×ˢ l] fun x =>
    match x with
    | (_i, x) => g x
hfm : ∀ᶠ (x : α) in l, AEStronglyMeasurable (fun i => f (i, x)) (μ.restrict s)
hs : MeasurableSet s
hμ : μ s < ⊤
C : ℝ
hC :
  ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l,
    ‖f x‖ ≤
      C *
        ‖match x with
          | (_i, x) => g x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht :
  ∀ y ∈ t,
    ‖f y‖ ≤
      C *
        ‖match y with
          | (_i, x) => g x‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
w : Set α
hwl : w ∈ l
hw : ∀ y ∈ w, AEStronglyMeasurable (fun i => f (i, y)) (μ.restrict s)
x : α
hx : x ∈ w ∩ v
⊢ (μ.restrict s) Set.univ = μ s
Theorem: Asymptotics.IsBigO.eventually_integrableOn
Proof state before:
case h.e'_3
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝² : MeasurableSpace ι
inst✝¹ : NormedAddCommGroup E
f : ι × α → E
g : α → F
μ : Measure ι
l : Filter α
inst✝ : Norm F
hf :
  f =O[𝓟 s ×ˢ l] fun x =>
    match x with
    | (_i, x) => g x
hfm : ∀ᶠ (x : α) in l, AEStronglyMeasurable (fun i => f (i, x)) (μ.restrict s)
hs : MeasurableSet s
hμ : μ s < ⊤
C : ℝ
hC :
  ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l,
    ‖f x‖ ≤
      C *
        ‖match x with
          | (_i, x) => g x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht :
  ∀ y ∈ t,
    ‖f y‖ ≤
      C *
        ‖match y with
          | (_i, x) => g x‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
w : Set α
hwl : w ∈ l
hw : ∀ y ∈ w, AEStronglyMeasurable (fun i => f (i, y)) (μ.restrict s)
x : α
hx : x ∈ w ∩ v
⊢ (μ.restrict s) Set.univ = μ s
Tactic:
exact Measure.restrict_apply_univ s
Proof state after:
no goals
Theorem: Asymptotics.IsBigO.set_integral_isBigO
Proof state before:
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝⁴ : MeasurableSpace ι
inst✝³ : NormedAddCommGroup E
f : ι × α → E
g : α → F
μ : Measure ι
l : Filter α
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
hf :
  f =O[𝓟 s ×ˢ l] fun x =>
    match x with
    | (_i, x) => g x
hs : MeasurableSet s
hμ : μ s < ⊤
⊢ (fun x => ∫ (i : ι) in s, f (i, x) ∂μ) =O[l] g
Tactic:
obtain ⟨C, hC⟩ := hf.bound
Proof state after:
case intro
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝⁴ : MeasurableSpace ι
inst✝³ : NormedAddCommGroup E
f : ι × α → E
g : α → F
μ : Measure ι
l : Filter α
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
hf :
  f =O[𝓟 s ×ˢ l] fun x =>
    match x with
    | (_i, x) => g x
hs : MeasurableSet s
hμ : μ s < ⊤
C : ℝ
hC :
  ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l,
    ‖f x‖ ≤
      C *
        ‖match x with
          | (_i, x) => g x‖
⊢ (fun x => ∫ (i : ι) in s, f (i, x) ∂μ) =O[l] g
Theorem: Asymptotics.IsBigO.set_integral_isBigO
Proof state before:
case intro
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝⁴ : MeasurableSpace ι
inst✝³ : NormedAddCommGroup E
f : ι × α → E
g : α → F
μ : Measure ι
l : Filter α
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
hf :
  f =O[𝓟 s ×ˢ l] fun x =>
    match x with
    | (_i, x) => g x
hs : MeasurableSet s
hμ : μ s < ⊤
C : ℝ
hC :
  ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l,
    ‖f x‖ ≤
      C *
        ‖match x with
          | (_i, x) => g x‖
⊢ (fun x => ∫ (i : ι) in s, f (i, x) ∂μ) =O[l] g
Tactic:
obtain ⟨t, htl, ht⟩ := hC.exists_mem
Proof state after:
case intro.intro.intro
α : Type u_1
ι : Type u_2
E : Type u_3
F : Type u_4
s : Set ι
inst✝⁴ : MeasurableSpace ι
inst✝³ : NormedAddCommGroup E
f : ι × α → E
g : α → F
μ : Measure ι
l : Filter α
inst✝² : NormedSpace ℝ E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
hf :
  f =O[𝓟 s ×ˢ l] fun x =>
    match x with
    | (_i, x) => g x
hs : MeasurableSet s
hμ : μ s < ⊤
C : ℝ
hC :
  ∀ᶠ (x : ι × α) in 𝓟 s ×ˢ l,
    ‖f x‖ ≤
      C *
        ‖match x with
          | (_i, x) => g x‖
t : Set (ι × α)
htl : t ∈ 𝓟 s ×ˢ l
ht :
  ∀ y ∈ t,
    ‖f y‖ ≤
      C *
        ‖match y with
          | (_i, x) => g x‖
⊢ (fun x => ∫ (i : ι) in s, f (i, x) ∂μ) =O[l] g