internlm/Lean-Github huggingface dataset:
Theorem: MeasureTheory.Asymptotics.IsBigO.set_integral_isBigO
Proof state before:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁸ : MeasurableSpace α
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
f✝ : α → E
g : α → F
a b : α
μ✝ : Measure α
l : Filter α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : SecondCountableTopology α
ι : Type u_4
inst✝³ : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
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
E : Type u_2
F : Type u_3
inst✝⁸ : MeasurableSpace α
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
f✝ : α → E
g : α → F
a b : α
μ✝ : Measure α
l : Filter α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : SecondCountableTopology α
ι : Type u_4
inst✝³ : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
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: MeasureTheory.Asymptotics.IsBigO.set_integral_isBigO
Proof state before:
case intro.intro.intro.intro.intro.intro.intro
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁸ : MeasurableSpace α
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
f✝ : α → E
g : α → F
a b : α
μ✝ : Measure α
l : Filter α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : SecondCountableTopology α
ι : Type u_4
inst✝³ : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
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
E : Type u_2
F : Type u_3
inst✝⁸ : MeasurableSpace α
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
f✝ : α → E
g : α → F
a b : α
μ✝ : Measure α
l : Filter α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : SecondCountableTopology α
ι : Type u_4
inst✝³ : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
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
E : Type u_2
F : Type u_3
inst✝⁸ : MeasurableSpace α
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
f✝ : α → E
g : α → F
a b : α
μ✝ : Measure α
l : Filter α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : SecondCountableTopology α
ι : Type u_4
inst✝³ : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
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: MeasureTheory.Asymptotics.IsBigO.set_integral_isBigO
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.refine_1
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁸ : MeasurableSpace α
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
f✝ : α → E
g : α → F
a b : α
μ✝ : Measure α
l : Filter α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : SecondCountableTopology α
ι : Type u_4
inst✝³ : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
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
E : Type u_2
F : Type u_3
inst✝⁸ : MeasurableSpace α
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
f✝ : α → E
g : α → F
a b : α
μ✝ : Measure α
l : Filter α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : SecondCountableTopology α
ι : Type u_4
inst✝³ : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
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: MeasureTheory.Asymptotics.IsBigO.set_integral_isBigO
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.refine_1
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁸ : MeasurableSpace α
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
f✝ : α → E
g : α → F
a b : α
μ✝ : Measure α
l : Filter α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : SecondCountableTopology α
ι : Type u_4
inst✝³ : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
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: MeasureTheory.Asymptotics.IsBigO.set_integral_isBigO
Proof state before:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁸ : MeasurableSpace α
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
f✝ : α → E
g : α → F
a b : α
μ✝ : Measure α
l : Filter α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : SecondCountableTopology α
ι : Type u_4
inst✝³ : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
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) univ < ⊤
Tactic:
convert hμ using 1
Proof state after:
case h.e'_3
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁸ : MeasurableSpace α
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
f✝ : α → E
g : α → F
a b : α
μ✝ : Measure α
l : Filter α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : SecondCountableTopology α
ι : Type u_4
inst✝³ : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
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) univ = μ s
Theorem: MeasureTheory.Asymptotics.IsBigO.set_integral_isBigO
Proof state before:
case h.e'_3
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁸ : MeasurableSpace α
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
f✝ : α → E
g : α → F
a b : α
μ✝ : Measure α
l : Filter α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : SecondCountableTopology α
ι : Type u_4
inst✝³ : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
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) univ = μ s
Tactic:
exact Measure.restrict_apply_univ s
Proof state after:
no goals
Theorem: MeasureTheory.Asymptotics.IsBigO.set_integral_isBigO
Proof state before:
case intro.intro.intro.intro.intro.intro.intro.refine_2
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁸ : MeasurableSpace α
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
f✝ : α → E
g : α → F
a b : α
μ✝ : Measure α
l : Filter α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : SecondCountableTopology α
ι : Type u_4
inst✝³ : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
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
E : Type u_2
F : Type u_3
inst✝⁸ : MeasurableSpace α
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
f✝ : α → E
g : α → F
a b : α
μ✝ : Measure α
l : Filter α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : SecondCountableTopology α
ι : Type u_4
inst✝³ : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
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: MeasureTheory.Asymptotics.IsBigO.set_integral_isBigO
Proof state before:
case h
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁸ : MeasurableSpace α
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
f✝ : α → E
g : α → F
a b : α
μ✝ : Measure α
l : Filter α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : SecondCountableTopology α
ι : Type u_4
inst✝³ : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
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
E : Type u_2
F : Type u_3
inst✝⁸ : MeasurableSpace α
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
f✝ : α → E
g : α → F
a b : α
μ✝ : Measure α
l : Filter α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : SecondCountableTopology α
ι : Type u_4
inst✝³ : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
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: MeasureTheory.Asymptotics.IsBigO.set_integral_isBigO
Proof state before:
case h
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁸ : MeasurableSpace α
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
f✝ : α → E
g : α → F
a b : α
μ✝ : Measure α
l : Filter α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : SecondCountableTopology α
ι : Type u_4
inst✝³ : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
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
E : Type u_2
F : Type u_3
inst✝⁸ : MeasurableSpace α
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
f✝ : α → E
g : α → F
a b : α
μ✝ : Measure α
l : Filter α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : SecondCountableTopology α
ι : Type u_4
inst✝³ : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
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: MeasureTheory.Asymptotics.IsBigO.set_integral_isBigO
Proof state before:
case h
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁸ : MeasurableSpace α
inst✝⁷ : NormedAddCommGroup E
inst✝⁶ : NormedAddCommGroup F
f✝ : α → E
g : α → F
a b : α
μ✝ : Measure α
l : Filter α
inst✝⁵ : TopologicalSpace α
inst✝⁴ : SecondCountableTopology α
ι : Type u_4
inst✝³ : MeasurableSpace ι
f : ι × α → E
s : Set ι
μ : Measure ι
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: ArithmeticFunction.IsMultiplicative.mult_lcm_eq_of_ne_zero
Proof state before:
R : Type u_1
inst✝ : CommGroupWithZero R
f : ArithmeticFunction R
h_mult : f.IsMultiplicative
x y : ℕ
hf : f (x.gcd y) ≠ 0
⊢ f (x.lcm y) = f x * f y / f (x.gcd y)
Tactic:
rw [←h_mult.lcm_apply_mul_gcd_apply]
Proof state after:
R : Type u_1
inst✝ : CommGroupWithZero R
f : ArithmeticFunction R
h_mult : f.IsMultiplicative
x y : ℕ
hf : f (x.gcd y) ≠ 0
⊢ f (x.lcm y) = f (x.lcm y) * f (x.gcd y) / f (x.gcd y)
Theorem: ArithmeticFunction.IsMultiplicative.mult_lcm_eq_of_ne_zero
Proof state before:
R : Type u_1
inst✝ : CommGroupWithZero R
f : ArithmeticFunction R
h_mult : f.IsMultiplicative
x y : ℕ
hf : f (x.gcd y) ≠ 0
⊢ f (x.lcm y) = f (x.lcm y) * f (x.gcd y) / f (x.gcd y)
Tactic:
field_simp
Proof state after:
no goals
Theorem: ArithmeticFunction.IsMultiplicative.prod_factors_of_mult
Proof state before:
R : Type u_1
f : ArithmeticFunction ℝ
h_mult : f.IsMultiplicative
l : ℕ
hl : Squarefree l
⊢ ∏ a ∈ l.primeFactors, f a = f l
Tactic:
rw [←IsMultiplicative.map_prod_of_subset_primeFactors h_mult l _ Finset.Subset.rfl,
  Nat.prod_primeFactors_of_squarefree hl]
Proof state after:
no goals
Theorem: Aux.sum_over_dvd_ite
Proof state before:
α : Type u_1
inst✝ : Ring α
P : ℕ
hP : P ≠ 0
n : ℕ
hn : n ∣ P
f : ℕ → α
⊢ ∑ d ∈ n.divisors, f d = ∑ d ∈ P.divisors, if d ∣ n then f d else 0
Tactic:
rw [←Finset.sum_filter, Nat.divisors_filter_dvd_of_dvd hP hn]
Proof state after:
no goals
Theorem: Aux.sum_intro
Proof state before:
α : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq α
s : Finset α
f : α → M
d : α
hd : d ∈ s
⊢ f d = ∑ k ∈ s, if k = d then f k else 0
Tactic:
trans (∑ k in s, if k = d then f d else 0)
Proof state after:
α : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq α
s : Finset α
f : α → M
d : α
hd : d ∈ s
⊢ f d = ∑ k ∈ s, if k = d then f d else 0

α : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq α
s : Finset α
f : α → M
d : α
hd : d ∈ s
⊢ (∑ k ∈ s, if k = d then f d else 0) = ∑ k ∈ s, if k = d then f k else 0
Theorem: Aux.sum_intro
Proof state before:
α : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq α
s : Finset α
f : α → M
d : α
hd : d ∈ s
⊢ (∑ k ∈ s, if k = d then f d else 0) = ∑ k ∈ s, if k = d then f k else 0
Tactic:
apply sum_congr rfl
Proof state after:
α : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq α
s : Finset α
f : α → M
d : α
hd : d ∈ s
⊢ ∀ x ∈ s, (if x = d then f d else 0) = if x = d then f x else 0
Theorem: Aux.sum_intro
Proof state before:
α : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq α
s : Finset α
f : α → M
d : α
hd : d ∈ s
⊢ ∀ x ∈ s, (if x = d then f d else 0) = if x = d then f x else 0
Tactic:
intro k _
Proof state after:
α : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq α
s : Finset α
f : α → M
d : α
hd : d ∈ s
k : α
a✝ : k ∈ s
⊢ (if k = d then f d else 0) = if k = d then f k else 0
Theorem: Aux.sum_intro
Proof state before:
α : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq α
s : Finset α
f : α → M
d : α
hd : d ∈ s
k : α
a✝ : k ∈ s
⊢ (if k = d then f d else 0) = if k = d then f k else 0
Tactic:
apply if_ctx_congr Iff.rfl _ (fun _ => rfl)
Proof state after:
α : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq α
s : Finset α
f : α → M
d : α
hd : d ∈ s
k : α
a✝ : k ∈ s
⊢ k = d → f d = f k
Theorem: Aux.sum_intro
Proof state before:
α : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq α
s : Finset α
f : α → M
d : α
hd : d ∈ s
k : α
a✝ : k ∈ s
⊢ k = d → f d = f k
Tactic:
intro h
Proof state after:
α : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq α
s : Finset α
f : α → M
d : α
hd : d ∈ s
k : α
a✝ : k ∈ s
h : k = d
⊢ f d = f k
Theorem: Aux.sum_intro
Proof state before:
α : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq α
s : Finset α
f : α → M
d : α
hd : d ∈ s
k : α
a✝ : k ∈ s
h : k = d
⊢ f d = f k
Tactic:
rw [h]
Proof state after:
no goals
Theorem: Aux.sum_intro
Proof state before:
α : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq α
s : Finset α
f : α → M
d : α
hd : d ∈ s
⊢ f d = ∑ k ∈ s, if k = d then f d else 0
Tactic:
rw [sum_eq_single_of_mem d hd]
Proof state after:
α : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq α
s : Finset α
f : α → M
d : α
hd : d ∈ s
⊢ f d = if d = d then f d else 0

α : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq α
s : Finset α
f : α → M
d : α
hd : d ∈ s
⊢ ∀ b ∈ s, b ≠ d → (if b = d then f d else 0) = 0
Theorem: Aux.sum_intro
Proof state before:
α : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq α
s : Finset α
f : α → M
d : α
hd : d ∈ s
⊢ f d = if d = d then f d else 0

α : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq α
s : Finset α
f : α → M
d : α
hd : d ∈ s
⊢ ∀ b ∈ s, b ≠ d → (if b = d then f d else 0) = 0
Tactic:
rw [if_pos rfl]
Proof state after:
α : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq α
s : Finset α
f : α → M
d : α
hd : d ∈ s
⊢ ∀ b ∈ s, b ≠ d → (if b = d then f d else 0) = 0
Theorem: Aux.sum_intro
Proof state before:
α : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq α
s : Finset α
f : α → M
d : α
hd : d ∈ s
⊢ ∀ b ∈ s, b ≠ d → (if b = d then f d else 0) = 0
Tactic:
intro _ _ h
Proof state after:
α : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq α
s : Finset α
f : α → M
d : α
hd : d ∈ s
b✝ : α
a✝ : b✝ ∈ s
h : b✝ ≠ d
⊢ (if b✝ = d then f d else 0) = 0
Theorem: Aux.sum_intro
Proof state before:
α : Type u_1
M : Type u_2
inst✝¹ : AddCommMonoid M
inst✝ : DecidableEq α
s : Finset α
f : α → M
d : α
hd : d ∈ s
b✝ : α
a✝ : b✝ ∈ s
h : b✝ ≠ d
⊢ (if b✝ = d then f d else 0) = 0
Tactic:
rw [if_neg h]
Proof state after:
no goals
Theorem: Aux.ite_sum_zero
Proof state before:
p : Prop
inst✝ : Decidable p
s : Finset ℕ
f : ℕ → ℝ
⊢ (if p then ∑ x ∈ s, f x else 0) = ∑ x ∈ s, if p then f x else 0
Tactic:
split_ifs <;> simp
Proof state after:
no goals