mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.MeasureTheory.Covering.VitaliFamily

Goal state before:
pp: X : Type u_1
inst✝ : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
⊢ ∀ (x : X),
    ∀ s ∈ v.setsAt x ∪ {s | MeasurableSet s ∧ (interior s).Nonempty ∧ ¬s ⊆ closedBall x δ}, (interior s).Nonempty

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Covering.VitaliFamily

Goal state before:
pp: X : Type u_1
inst✝ : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
⊢ ∀ (x : X),
    ∀ ε > 0, ∃ s ∈ v.setsAt x ∪ {s | MeasurableSet s ∧ (interior s).Nonempty ∧ ¬s ⊆ closedBall x δ}, s ⊆ closedBall x ε

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝⁴ : TopologicalSpace β
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
⊢ SuperpolynomialDecay l k f ↔ ∀ (z : ℕ), IsBoundedUnder (fun x1 x2 ↦ x1 ≤ x2) l fun a ↦ |k a ^ z * f a|

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝⁴ : TopologicalSpace β
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : ∀ (z : ℤ), Tendsto (fun a ↦ k a ^ z * f a) l (𝓝 0)
n : ℕ
⊢ Tendsto (fun a ↦ k a ^ n * f a) l (𝓝 0)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u v : ℕ → EReal
b : EReal
hb : b ≠ ⊤
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ v n + b
⊢ linearGrowthSup u ≤ linearGrowthSup v

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: u : ℕ → ℝ≥0∞
a : EReal
⊢ a ≤ expGrowthSup u ↔ ∀ b < a, ∃ᶠ (n : ℕ) in atTop, (b * ↑n).exp ≤ u n

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝⁴ : TopologicalSpace β
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℤ
hz : z < 0
this : Tendsto (fun a ↦ k a ^ z) l (𝓝 0)
⊢ Tendsto f l (𝓝 0)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝⁴ : TopologicalSpace β
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
⊢ SuperpolynomialDecay l k f ↔ ∀ (z : ℤ), Tendsto (fun a ↦ k a ^ z * f a) l (𝓝 0)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝⁴ : TopologicalSpace β
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hf : SuperpolynomialDecay l k f
z : ℤ
⊢ SuperpolynomialDecay l k fun a ↦ k a ^ z * f a

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: u : ℕ → ℝ≥0∞
a : EReal
h : ∃ᶠ (n : ℕ) in atTop, u n ≤ (a * ↑n).exp
⊢ expGrowthInf u ≤ a

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝⁴ : TopologicalSpace β
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hf : SuperpolynomialDecay l k f
⊢ SuperpolynomialDecay l k (k⁻¹ * f)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝⁴ : TopologicalSpace β
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k (k * f)
x : α
hx : k x ≠ 0
⊢ (k⁻¹ * (k * f)) x = f x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u v : ℕ → EReal
⊢ linearGrowthInf (u ⊓ v) = min (linearGrowthInf u) (linearGrowthInf v)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝⁴ : TopologicalSpace β
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
⊢ SuperpolynomialDecay l k (f * k) ↔ SuperpolynomialDecay l k f

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: α : Type u_1
u : α → ℕ → EReal
s : Set α
hs : s.Finite
⊢ linearGrowthInf (⨅ x ∈ s, u x) = ⨅ x ∈ s, linearGrowthInf (u x)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: u : ℕ → ℝ≥0∞
a : EReal
h : ∀ᶠ (n : ℕ) in atTop, (a * ↑n).exp ≤ u n
c : EReal
c_u : c < a
n : ℕ
hn : (a * ↑n).exp ≤ u n
⊢ (c * ↑n).exp ≤ (a * ↑n).exp

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: ι : Type u_1
inst✝ : Finite ι
u : ι → ℕ → EReal
⊢ linearGrowthInf (⨅ i, u i) = ⨅ i, linearGrowthInf (u i)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝⁴ : TopologicalSpace β
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
n : ℕ
⊢ SuperpolynomialDecay l k (k ^ n * f) ↔ SuperpolynomialDecay l k f

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝⁴ : TopologicalSpace β
inst✝³ : Field β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
n : ℕ
⊢ SuperpolynomialDecay l k (f * k ^ n) ↔ SuperpolynomialDecay l k f

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: u : ℕ → ℝ≥0∞
a : EReal
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ (a * ↑n).exp
c : EReal
c_u : c > a
n : ℕ
hn : u n ≤ (a * ↑n).exp
⊢ (a * ↑n).exp ≤ (c * ↑n).exp

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝ : NormedField β
⊢ (∀ (n : ℕ), Tendsto (fun a ↦ ‖k a ^ n * f a‖) l (𝓝 0)) ↔ SuperpolynomialDecay l (fun a ↦ ‖k a‖) fun a ↦ ‖f a‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u v : ℕ → EReal
⊢ linearGrowthSup (u ⊔ v) = max (linearGrowthSup u) (linearGrowthSup v)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: α : Type u_1
u : α → ℕ → EReal
s : Set α
hs : s.Finite
⊢ linearGrowthSup (⨆ x ∈ s, u x) = ⨆ x ∈ s, linearGrowthSup (u x)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: ι : Type u_1
inst✝ : Finite ι
u : ι → ℕ → EReal
⊢ linearGrowthSup (⨆ i, u i) = ⨆ i, linearGrowthSup (u i)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: a b : ℝ
h : a < b
⊢ ∀ᶠ (x : ℝ) in atTop, ∃ n, a * x ≤ ↑n ∧ ↑n ≤ b * x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: u : ℕ → ℝ≥0∞
a : EReal
h : ∃ᶠ (n : ℕ) in atTop, (a * ↑n).exp ≤ u n
c : EReal
c_u : c < a
n : ℕ
hn : (a * ↑n).exp ≤ u n
⊢ (c * ↑n).exp ≤ (a * ↑n).exp

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝³ : NormedField β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
h : ∀ (z : ℤ), Tendsto (fun a ↦ k a ^ z * f a) l (𝓝 0)
z : ℤ
x : α
⊢ (fun a ↦ k a ^ z)⁻¹ x = k x ^ (-z)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: a b : ℝ
h : a < b
hb : 0 ≤ b
⊢ ∀ᶠ (x : ℝ) in atTop, ∃ n, a * x ≤ ↑n ∧ ↑n ≤ b * x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: a b : EReal
hb : 0 ≤ b
h : ⊥ < b
⊢ ∀ᶠ (n : ℕ) in atTop, ∃ m, ⊥ * ↑n ≤ ↑m ∧ ↑m ≤ b * ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: a✝ b : EReal
a : ℝ
hb : 0 ≤ ⊤
h : ↑a < ⊤
⊢ ∀ᶠ (n : ℕ) in atTop, ∃ m, ↑a * ↑n ≤ ↑m ∧ ↑m ≤ ⊤ * ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: ⊢ expGrowthSup 0 = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: a✝ b✝ : EReal
a b : ℝ
hb : 0 ≤ ↑b
h : ↑a < ↑b
⊢ ∀ᶠ (n : ℕ) in atTop, ∃ m, ↑a * ↑n ≤ ↑m ∧ ↑m ≤ ↑b * ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: v : ℕ → ℕ
h : (linearGrowthInf fun n ↦ ↑(v n)) ≠ 0
M : ℕ
this : Tendsto (fun n ↦ ↑(v n)) atTop (𝓝 ⊤)
n : ℕ
⊢ ↑↑M < ↑(v n) → M ≤ v n

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: v : ℕ → ℕ
h : (linearGrowthInf fun n ↦ ↑(v n)) ≠ 0
⊢ Tendsto v atTop atTop

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: ⊢ expGrowthInf 0 = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u : ℕ → EReal
v : ℕ → ℕ
hu : 0 ≤ᶠ[atTop] u
hv : Tendsto v atTop atTop
⊢ 0 ≤ linearGrowthInf (u ∘ v)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: ⊢ expGrowthInf ⊤ = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝³ : NormedField β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
⊢ SuperpolynomialDecay l k f ↔ ∀ (z : ℤ), f =O[l] fun a ↦ k a ^ z

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝³ : NormedField β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℤ
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
⊢ Tendsto (fun x ↦ 1 / k x) l (𝓝 0)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: ⊢ expGrowthSup ⊤ = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝³ : NormedField β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
h : SuperpolynomialDecay l k f
z : ℤ
hk0 : ∀ᶠ (x : α) in l, k x ≠ 0
this : (fun x ↦ 1) =o[l] k
⊢ f =o[l] fun x ↦ k x * k x ^ (z - 1)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.SuperpolynomialDecay

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
k f : α → β
inst✝³ : NormedField β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hk : Tendsto k l atTop
⊢ SuperpolynomialDecay l k f ↔ ∀ (z : ℤ), f =o[l] fun a ↦ k a ^ z

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: b : ℝ≥0∞
⊢ (expGrowthInf fun n ↦ b ^ n) = b.log

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u : ℕ → EReal
v : ℕ → ℕ
hu : 0 ≤ᶠ[atTop] u
hv : Tendsto v atTop atTop
uv_0 : 0 ≤ linearGrowthInf (u ∘ v)
a : EReal
x✝¹ : a ∈ Set.Ioo 0 (linearGrowthInf fun n ↦ ↑(v n))
b : EReal
x✝ : b ∈ Set.Ioo 0 (linearGrowthInf u)
left✝ : 0 < a
a_v : a < linearGrowthInf fun n ↦ ↑(v n)
b_0 : 0 < b
b_u : b < linearGrowthInf u
b_uv : ∀ᶠ (a : ℕ) in atTop, b * ↑(v a) ≤ u (v a)
n : ℕ
b_uvn : b * ↑(v n) ≤ u (v n)
n_0 : 0 < n
a_vn : a * ↑n ≤ ↑(v n)
⊢ b * (a * ↑n) ≤ b * ↑(v n)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Covering.VitaliFamily

Goal state before:
pp: X : Type u_1
inst✝ : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
s : Set X
f : X → Set (Set X)
fset : ∀ x ∈ s, f x ⊆ v.setsAt x ∪ {s | MeasurableSet s ∧ (interior s).Nonempty ∧ ¬s ⊆ closedBall x δ}
ffine : ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε
g : X → Set (Set X) := fun x ↦ f x ∩ v.setsAt x
⊢ ∀ x ∈ s, ∀ ε > 0, ∃ t ∈ g x, t ⊆ closedBall x ε

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u : ℕ → EReal
v : ℕ → ℕ
hu : 0 ≤ᶠ[atTop] u
hv : Tendsto v atTop atTop
⊢ (linearGrowthInf fun n ↦ ↑(v n)) * linearGrowthInf u ≤ linearGrowthInf (u ∘ v)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: b : ℝ≥0∞
⊢ (expGrowthSup fun n ↦ b ^ n) = b.log

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: u v : ℕ → ℝ≥0∞
⊢ expGrowthInf u + expGrowthInf v ≤ expGrowthInf (u * v)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: u v : ℕ → ℝ≥0∞
h : expGrowthSup u ≠ ⊥ ∨ expGrowthInf v ≠ ⊤
h' : expGrowthSup u ≠ ⊤ ∨ expGrowthInf v ≠ ⊥
⊢ expGrowthInf (u * v) ≤ expGrowthSup u + expGrowthInf v

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Covering.VitaliFamily

Goal state before:
pp: X : Type u_1
inst✝ : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
⊢ ∀ (s : Set X) (f : X → Set (Set X)),
    (∀ x ∈ s, f x ⊆ v.setsAt x ∪ {s | MeasurableSet s ∧ (interior s).Nonempty ∧ ¬s ⊆ closedBall x δ}) →
      (∀ x ∈ s, ∀ ε > 0, ∃ t ∈ f x, t ⊆ closedBall x ε) →
        ∃ t, (∀ p ∈ t, p.1 ∈ s) ∧ (t.PairwiseDisjoint fun p ↦ p.2) ∧ (∀ p ∈ t, p.2 ∈ f p.1) ∧ μ (s \ ⋃ p ∈ t, p.2) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u : ℕ → EReal
v : ℕ → ℕ
hu : ∃ᶠ (n : ℕ) in atTop, 0 ≤ u n
hv₀ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ 0
hv₁ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ ⊤
hv₂ : Tendsto v atTop atTop
v_0 : 0 < linearGrowthSup fun n ↦ ↑(v n)
a : EReal
v_a : a > linearGrowthSup fun n ↦ ↑(v n)
b : EReal
u_b : b > linearGrowthSup u
⊢ 0 ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Covering.VitaliFamily

Goal state before:
pp: X : Type u_1
inst✝ : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
ι : Sort u_2
p : ι → Prop
s : ι → Set X
x : X
h : (𝓝 x).HasBasis p s
⊢ (v.filterAt x).HasBasis p fun i ↦ {t | t ∈ v.setsAt x ∧ t ⊆ s i}

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Covering.VitaliFamily

Goal state before:
pp: X : Type u_1
inst✝ : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
x : X
s : Set (Set X)
⊢ s ∈ v.filterAt x ↔ ∃ ε > 0, ∀ t ∈ v.setsAt x, t ⊆ closedBall x ε → t ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: u v : ℕ → ℝ≥0∞
h : expGrowthInf u ≠ ⊥ ∨ expGrowthSup v ≠ ⊤
h' : expGrowthInf u ≠ ⊤ ∨ expGrowthSup v ≠ ⊥
⊢ expGrowthInf (u * v) ≤ expGrowthInf u + expGrowthSup v

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Covering.VitaliFamily

Goal state before:
pp: X : Type u_1
inst✝ : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
ι : Type u_2
l : Filter ι
f : ι → Set X
x : X
⊢ Tendsto f l (v.filterAt x) ↔ (∀ᶠ (i : ι) in l, f i ∈ v.setsAt x) ∧ ∀ ε > 0, ∀ᶠ (i : ι) in l, f i ⊆ closedBall x ε

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Covering.VitaliFamily

Goal state before:
pp: X : Type u_1
inst✝ : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
x : X
⊢ ∀ᶠ (t : Set X) in v.filterAt x, MeasurableSet t

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: u v : ℕ → ℝ≥0∞
⊢ expGrowthSup u + expGrowthInf v ≤ expGrowthSup (u * v)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: u v : ℕ → ℝ≥0∞
⊢ expGrowthInf u + expGrowthSup v ≤ expGrowthSup (u * v)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Covering.VitaliFamily

Goal state before:
pp: X : Type u_1
inst✝ : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
x : X
P : Set X → Prop
⊢ (∃ᶠ (t : Set X) in v.filterAt x, P t) ↔ ∀ ε > 0, ∃ t ∈ v.setsAt x, t ⊆ closedBall x ε ∧ P t

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Covering.VitaliFamily

Goal state before:
pp: X : Type u_1
inst✝ : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
x : X
this : {t | MeasurableSet t → (interior t).Nonempty → ¬t ⊆ closedBall x δ → t ∈ v.setsAt x} ∈ (𝓝 x).smallSets
⊢ (v.enlarge δ δpos).filterAt x = v.filterAt x

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Covering.VitaliFamily

Goal state before:
pp: X : Type u_1
inst✝ : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
δ : ℝ
δpos : 0 < δ
⊢ (v.enlarge δ δpos).filterAt = v.filterAt

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: u v : ℕ → ℝ≥0∞
h : expGrowthSup u ≠ ⊥ ∨ expGrowthSup v ≠ ⊤
h' : expGrowthSup u ≠ ⊤ ∨ expGrowthSup v ≠ ⊥
⊢ expGrowthSup (u * v) ≤ expGrowthSup u + expGrowthSup v

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Covering.VitaliFamily

Goal state before:
pp: X : Type u_1
inst✝ : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
f : X → Set (Set X)
s : Set X
⊢ v.FineSubfamilyOn f s ↔ ∀ x ∈ s, ∃ᶠ (t : Set X) in v.filterAt x, t ∈ f x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u : ℕ → EReal
v : ℕ → ℕ
hu : ∃ᶠ (n : ℕ) in atTop, 0 ≤ u n
hv₀ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ 0
hv₁ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ ⊤
hv₂ : Tendsto v atTop atTop
v_0 : 0 < linearGrowthSup fun n ↦ ↑(v n)
a : EReal
v_a : a > linearGrowthSup fun n ↦ ↑(v n)
b : EReal
u_b : b > linearGrowthSup u
b_0 : 0 ≤ b
uv_b : ∀ᶠ (n : ℕ) in atTop, u (v n) ≤ b * ↑(v n)
n : ℕ
uvn_b : u (v n) ≤ b * ↑(v n)
n_0 : 0 < n
vn_a : ↑(v n) ≤ a * ↑n
⊢ b * ↑(v n) ≤ b * (a * ↑n)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: u : ℕ → ℝ≥0∞
⊢ expGrowthInf u⁻¹ = -expGrowthSup u

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Covering.VitaliFamily

Goal state before:
pp: X : Type u_1
inst✝ : PseudoMetricSpace X
m0 : MeasurableSpace X
μ : Measure X
v : VitaliFamily μ
f : X → Set (Set X)
s : Set X
h : ∀ x ∈ s, ∃ᶠ (t : Set X) in v.filterAt x, t ∈ f x
⊢ v.FineSubfamilyOn f s

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u : ℕ → EReal
v : ℕ → ℕ
hu : ∃ᶠ (n : ℕ) in atTop, 0 ≤ u n
hv₀ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ 0
hv₁ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ ⊤
hv₂ : Tendsto v atTop atTop
⊢ linearGrowthSup (u ∘ v) ≤ (linearGrowthSup fun n ↦ ↑(v n)) * linearGrowthSup u

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: u : ℕ → ℝ≥0∞
⊢ expGrowthSup u⁻¹ = -expGrowthInf u

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u : ℕ → EReal
h : Monotone u
h' : u ≠ ⊥
⊢ 0 ≤ linearGrowthInf u

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
h' : u ≠ ⊥
hv : Tendsto v atTop atTop
⊢ 0 ≤ linearGrowthInf (u ∘ v)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.ExpGrowth

Goal state before:
pp: u v : ℕ → ℝ≥0∞
b : ℝ≥0∞
hb : b ≠ ∞
h : ∀ᶠ (n : ℕ) in atTop, u n ≤ b * v n
⊢ expGrowthInf u ≤ expGrowthInf v

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ 0
hv₁ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ ⊤
u_0 : ¬u = ⊥
v_0 : 0 < linearGrowthSup fun n ↦ ↑(v n)
a : EReal
v_a : a > linearGrowthSup fun n ↦ ↑(v n)
b : EReal
u_b : b > linearGrowthInf u
a_0 : 0 < a
b_0 : 0 < b
a_top : a ≠ ⊤
a' : EReal
v_a' : (linearGrowthSup fun n ↦ ↑(v n)) < a'
a_a' : a' < a
a_0' : 0 < a'
a_a_inv' : a⁻¹ < a'⁻¹
⊢ ∀ᶠ (n : ℕ) in atTop, ↑(v n) ≤ a' * ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Asymptotics.LinearGrowth

Goal state before:
pp: case neg.inr
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ 0
hv₁ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ ⊤
u_0 : ¬u = ⊥
v_0 : 0 < linearGrowthSup fun n ↦ ↑(v n)
a : EReal
v_a : a > linearGrowthSup fun n ↦ ↑(v n)
b : EReal
u_b : b > linearGrowthInf u
a_0 : 0 < a
b_0 : 0 < b
a_top : a ≠ ⊤
a' : EReal
a_a' : a' < a
a_0' : 0 < a'
a_a_inv' : a⁻¹ < a'⁻¹
v_a' : ∀ᶠ (n : ℕ) in atTop, ↑(v n) ≤ a' * ↑n
⊢ (∀ᶠ (n : ℕ) in atTop, ↑(v n) ≤ a' * ↑n) → ∃ᶠ (n : ℕ) in atTop, (u ∘ v) n ≤ a * b * ↑n

Tactic:
rw [← frequently_imp_distrib]

Goal state after:
case neg.inr
u : ℕ → EReal
v : ℕ → ℕ
h : Monotone u
hv₀ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ 0
hv₁ : (linearGrowthSup fun n ↦ ↑(v n)) ≠ ⊤
u_0 : ¬u = ⊥
v_0 : 0 < linearGrowthSup fun n ↦ ↑(v n)
a : EReal
v_a : a > linearGrowthSup fun n ↦ ↑(v n)
b : EReal
u_b : b > linearGrowthInf u
a_0 : 0 < a
b_0 : 0 < b
a_top : a ≠ ⊤
a' : EReal
a_a' : a' < a
a_0' : 0 < a'
a_a_inv' : a⁻¹ < a'⁻¹
v_a' : ∀ᶠ (n : ℕ) in atTop, ↑(v n) ≤ a' * ↑n
⊢ ∃ᶠ (x : ℕ) in atTop, ↑(v x) ≤ a' * ↑x → (u ∘ v) x ≤ a * b * ↑x
Module: Mathlib.MeasureTheory.Function.AEMeasurableOrder

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : s.Countable
s_dense : Dense s
f : α → β
h :
  ∀ p ∈ s,
    ∀ q ∈ s, p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ μ (u ∩ v) = 0
this : Encodable ↑s
⊢ ∀ (p q : β),
    ∃ u v,
      MeasurableSet u ∧
        MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ (p ∈ s → q ∈ s → p < q → μ (u ∩ v) = 0)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.AEMeasurableOrder

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : s.Countable
s_dense : Dense s
f : α → β
h :
  ∀ p ∈ s,
    ∀ q ∈ s, p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ μ (u ∩ v) = 0
this : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p ↦ ⋂ q ∈ s ∩ Ioi p, u p q
⊢ ∀ (i : β), MeasurableSet (u' i)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Function.AEMeasurableOrder

Goal state before:
pp: α : Type u_1
m : MeasurableSpace α
μ : Measure α
β : Type u_2
inst✝⁶ : CompleteLinearOrder β
inst✝⁵ : DenselyOrdered β
inst✝⁴ : TopologicalSpace β
inst✝³ : OrderTopology β
inst✝² : SecondCountableTopology β
inst✝¹ : MeasurableSpace β
inst✝ : BorelSpace β
s : Set β
s_count : s.Countable
s_dense : Dense s
f : α → β
h :
  ∀ p ∈ s,
    ∀ q ∈ s, p < q → ∃ u v, MeasurableSet u ∧ MeasurableSet v ∧ {x | f x < p} ⊆ u ∧ {x | q < f x} ⊆ v ∧ μ (u ∩ v) = 0
this : Encodable ↑s
u v : β → β → Set α
huv :
  ∀ (p q : β),
    MeasurableSet (u p q) ∧
      MeasurableSet (v p q) ∧
        {x | f x < p} ⊆ u p q ∧ {x | q < f x} ⊆ v p q ∧ (p ∈ s → q ∈ s → p < q → μ (u p q ∩ v p q) = 0)
u' : β → Set α := fun p ↦ ⋂ q ∈ s ∩ Ioi p, u p q
u'_meas : ∀ (i : β), MeasurableSet (u' i)
f' : α → β := fun x ↦ ⨅ i, (u' ↑i).piecewise (fun x ↦ ↑i) (fun x ↦ ⊤) x
⊢ Measurable f'

Tactic:
by

Goal state after: