internlm/Lean-Github huggingface dataset:
Theorem: Asymptotics.IsBigO.set_integral_isBigO
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✝² : 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
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✝² : 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‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
⊢ (fun x => ∫ (i : ι) in s, f (i, x) ∂μ) =O[l] g
Theorem: Asymptotics.IsBigO.set_integral_isBigO
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✝² : 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‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
⊢ (fun x => ∫ (i : ι) in s, f (i, x) ∂μ) =O[l] g
Tactic:
refine isBigO_iff.mpr ⟨C * (μ s).toReal, eventually_iff_exists_mem.mpr ⟨v, hv, fun x hx ↦ ?_⟩⟩
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✝² : 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‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
x : α
hx : x ∈ v
⊢ ‖∫ (i : ι) in s, f (i, x) ∂μ‖ ≤ C * (μ s).toReal * ‖g x‖
Theorem: Asymptotics.IsBigO.set_integral_isBigO
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✝² : 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‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
x : α
hx : x ∈ v
⊢ ‖∫ (i : ι) in s, f (i, x) ∂μ‖ ≤ C * (μ s).toReal * ‖g x‖
Tactic:
rewrite [mul_assoc, ← smul_eq_mul (a' := ‖g x‖), ← MeasureTheory.Measure.restrict_apply_univ,
  ← integral_const, mul_comm, ← smul_eq_mul, ← integral_smul_const]
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✝² : 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‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
x : α
hx : x ∈ v
⊢ ‖∫ (i : ι) in s, f (i, x) ∂μ‖ ≤ ∫ (x_1 : ι) in s, ‖g x‖ • C ∂μ
Theorem: Asymptotics.IsBigO.set_integral_isBigO
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✝² : 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‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
x : α
hx : x ∈ v
⊢ ‖∫ (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 _) ?_ ?_
Proof state after:
case intro.intro.intro.intro.intro.intro.intro.refine_1
α : 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‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
x : α
hx : x ∈ v
⊢ Integrable (fun x_1 => ‖g x‖ • C) (μ.restrict s)

case intro.intro.intro.intro.intro.intro.intro.refine_2
α : 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‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
x : α
hx : x ∈ v
⊢ (fun a => ‖f (a, x)‖) ≤ᶠ[ae (μ.restrict s)] fun x_1 => ‖g x‖ • C
Theorem: Asymptotics.IsBigO.set_integral_isBigO
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.refine_1
α : 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‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
x : α
hx : x ∈ v
⊢ Integrable (fun x_1 => ‖g x‖ • C) (μ.restrict 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.refine_1
α : 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‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
x : α
hx : x ∈ v
this : IsFiniteMeasure (μ.restrict s)
⊢ Integrable (fun x_1 => ‖g x‖ • C) (μ.restrict s)
Theorem: Asymptotics.IsBigO.set_integral_isBigO
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.refine_1
α : 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‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
x : α
hx : x ∈ v
this : IsFiniteMeasure (μ.restrict s)
⊢ Integrable (fun x_1 => ‖g x‖ • C) (μ.restrict s)
Tactic:
exact integrable_const _
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 < ⊤
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 : α
hx : x ∈ 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✝² : 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‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
x : α
hx : x ∈ v
⊢ (μ.restrict s) Set.univ = μ s
Theorem: Asymptotics.IsBigO.set_integral_isBigO
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✝² : 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‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
x : α
hx : x ∈ 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:
case intro.intro.intro.intro.intro.intro.intro.refine_2
α : 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‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
x : α
hx : x ∈ v
⊢ (fun a => ‖f (a, x)‖) ≤ᶠ[ae (μ.restrict s)] fun x_1 => ‖g x‖ • C
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✝² : 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‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
x : α
hx : x ∈ v
⊢ ∀ a ∈ s, ‖f (a, x)‖ ≤ ‖g x‖ • C
Theorem: Asymptotics.IsBigO.set_integral_isBigO
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✝² : 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‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
x : α
hx : x ∈ v
⊢ ∀ a ∈ s, ‖f (a, x)‖ ≤ ‖g x‖ • C
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✝² : 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‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
x : α
hx : x ∈ v
y : ι
hy : y ∈ s
⊢ ‖f (y, x)‖ ≤ ‖g x‖ • C
Theorem: Asymptotics.IsBigO.set_integral_isBigO
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✝² : 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‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
x : α
hx : x ∈ v
y : ι
hy : y ∈ s
⊢ ‖f (y, x)‖ ≤ ‖g x‖ • C
Tactic:
rewrite [smul_eq_mul, mul_comm]
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✝² : 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‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
x : α
hx : x ∈ v
y : ι
hy : y ∈ s
⊢ ‖f (y, x)‖ ≤ C * ‖g x‖
Theorem: Asymptotics.IsBigO.set_integral_isBigO
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✝² : 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‖
u : Set ι
hu : u ∈ 𝓟 s
v : Set α
hv : v ∈ l
huv : u ×ˢ v ⊆ t
x : α
hx : x ∈ v
y : ι
hy : y ∈ s
⊢ ‖f (y, x)‖ ≤ C * ‖g x‖
Tactic:
exact ht (y, x) <| huv ⟨hu hy, hx⟩
Proof state after:
no goals
Theorem: smooth_urysohn_support_Ioo
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
⊢ ∃ Ψ,
    ContDiff ℝ ⊤ Ψ ∧
      HasCompactSupport Ψ ∧ (Icc b c).indicator 1 ≤ Ψ ∧ Ψ ≤ (Ioo a d).indicator 1 ∧ Function.support Ψ = Ioo a d
Tactic:
have := exists_msmooth_zero_iff_one_iff_of_isClosed
  (modelWithCornersSelf ℝ ℝ) (s := Set.Iic a ∪ Set.Ici d) (t := Set.Icc b c)
  (IsClosed.union isClosed_Iic isClosed_Ici)
  (isClosed_Icc)
  (by
    simp_rw [Set.disjoint_union_left, Set.disjoint_iff, Set.subset_def, Set.mem_inter_iff, Set.mem_Iic, Set.mem_Icc,
      Set.mem_empty_iff_false, and_imp, imp_false, not_le, Set.mem_Ici]
    constructor <;> intros <;> linarith)
Proof state after:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
this :
  ∃ f,
    Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) f ∧
      range f ⊆ Icc 0 1 ∧ (∀ (x : ℝ), x ∈ Iic a ∪ Ici d ↔ f x = 0) ∧ ∀ (x : ℝ), x ∈ Icc b c ↔ f x = 1
⊢ ∃ Ψ,
    ContDiff ℝ ⊤ Ψ ∧
      HasCompactSupport Ψ ∧ (Icc b c).indicator 1 ≤ Ψ ∧ Ψ ≤ (Ioo a d).indicator 1 ∧ Function.support Ψ = Ioo a d
Theorem: smooth_urysohn_support_Ioo
Proof state before:
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
this :
  ∃ f,
    Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) f ∧
      range f ⊆ Icc 0 1 ∧ (∀ (x : ℝ), x ∈ Iic a ∪ Ici d ↔ f x = 0) ∧ ∀ (x : ℝ), x ∈ Icc b c ↔ f x = 1
⊢ ∃ Ψ,
    ContDiff ℝ ⊤ Ψ ∧
      HasCompactSupport Ψ ∧ (Icc b c).indicator 1 ≤ Ψ ∧ Ψ ≤ (Ioo a d).indicator 1 ∧ Function.support Ψ = Ioo a d
Tactic:
rcases this with ⟨Ψ, hΨSmooth, hΨrange, hΨ0, hΨ1⟩
Proof state after:
case intro.intro.intro.intro
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ∈ Iic a ∪ Ici d ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), x ∈ Icc b c ↔ Ψ x = 1
⊢ ∃ Ψ,
    ContDiff ℝ ⊤ Ψ ∧
      HasCompactSupport Ψ ∧ (Icc b c).indicator 1 ≤ Ψ ∧ Ψ ≤ (Ioo a d).indicator 1 ∧ Function.support Ψ = Ioo a d
Theorem: smooth_urysohn_support_Ioo
Proof state before:
case intro.intro.intro.intro
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ∈ Iic a ∪ Ici d ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), x ∈ Icc b c ↔ Ψ x = 1
⊢ ∃ Ψ,
    ContDiff ℝ ⊤ Ψ ∧
      HasCompactSupport Ψ ∧ (Icc b c).indicator 1 ≤ Ψ ∧ Ψ ≤ (Ioo a d).indicator 1 ∧ Function.support Ψ = Ioo a d
Tactic:
simp only [Set.EqOn, Set.mem_setOf_eq, Set.mem_union, Set.mem_Iic, Set.mem_Ici,
  ContMDiffMap.coeFn_mk, Pi.zero_apply, Set.mem_Icc, Pi.one_apply, and_imp] at *
Proof state after:
case intro.intro.intro.intro
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
⊢ ∃ Ψ,
    ContDiff ℝ ⊤ Ψ ∧
      HasCompactSupport Ψ ∧ (Icc b c).indicator 1 ≤ Ψ ∧ Ψ ≤ (Ioo a d).indicator 1 ∧ Function.support Ψ = Ioo a d
Theorem: smooth_urysohn_support_Ioo
Proof state before:
case intro.intro.intro.intro
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
⊢ ∃ Ψ,
    ContDiff ℝ ⊤ Ψ ∧
      HasCompactSupport Ψ ∧ (Icc b c).indicator 1 ≤ Ψ ∧ Ψ ≤ (Ioo a d).indicator 1 ∧ Function.support Ψ = Ioo a d
Tactic:
use Ψ
Proof state after:
case h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
⊢ ContDiff ℝ ⊤ Ψ ∧
    HasCompactSupport Ψ ∧ (Icc b c).indicator 1 ≤ Ψ ∧ Ψ ≤ (Ioo a d).indicator 1 ∧ Function.support Ψ = Ioo a d
Theorem: smooth_urysohn_support_Ioo
Proof state before:
case h
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
⊢ ContDiff ℝ ⊤ Ψ ∧
    HasCompactSupport Ψ ∧ (Icc b c).indicator 1 ≤ Ψ ∧ Ψ ≤ (Ioo a d).indicator 1 ∧ Function.support Ψ = Ioo a d
Tactic:
constructor
Proof state after:
case h.left
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
⊢ ContDiff ℝ ⊤ Ψ

case h.right
n : ℕ
A a b c d u x y t σ' : ℝ
ψ Ψ✝ : ℝ → ℂ
F G : ℂ → ℂ
f : ℕ → ℂ
𝕜 : Type
inst✝ : _root_.RCLike 𝕜
h1 : a < b
h3 : c < d
Ψ : ℝ → ℝ
hΨSmooth : Smooth (modelWithCornersSelf ℝ ℝ) (modelWithCornersSelf ℝ ℝ) Ψ
hΨrange : range Ψ ⊆ Icc 0 1
hΨ0 : ∀ (x : ℝ), x ≤ a ∨ d ≤ x ↔ Ψ x = 0
hΨ1 : ∀ (x : ℝ), b ≤ x ∧ x ≤ c ↔ Ψ x = 1
⊢ HasCompactSupport Ψ ∧ (Icc b c).indicator 1 ≤ Ψ ∧ Ψ ≤ (Ioo a d).indicator 1 ∧ Function.support Ψ = Ioo a d