mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic

Goal state before:
pp: X : Type u_1
inst✝ : MetricSpace X
D : DeloneSet X
x y : X
hy : y ∈ D.carrier
hdist : (x, y) ∈ {(x, y) | edist x y ≤ ↑D.coveringRadius}
⊢ dist x y ≤ ↑D.coveringRadius

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic

Goal state before:
pp: X : Type u_1
inst✝ : MetricSpace X
D : DeloneSet X
x : X
⊢ ∃ y ∈ D, dist x y ≤ ↑D.coveringRadius

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic

Goal state before:
pp: X : Type u_1
inst✝ : MetricSpace X
D : DeloneSet X
r : ℝ≥0
hr : r ≤ D.packingRadius / 2
x y z : X
hx : x ∈ D
hy : y ∈ D
hxz : x ∈ ball z ↑r
hyz : y ∈ ball z ↑r
hne : ¬x = y
⊢ dist x z + dist y z < ↑r + ↑r

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic

Goal state before:
pp: X : Type u_1
inst✝ : MetricSpace X
D : DeloneSet X
r : ℝ≥0
hr : r ≤ D.packingRadius / 2
x y z : X
hx : x ∈ D
hy : y ∈ D
hxz : x ∈ ball z ↑r
hyz : y ∈ ball z ↑r
hne : ¬x = y
⊢ ↑r + ↑r ≤ ↑D.packingRadius

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic

Goal state before:
pp: X : Type u_1
inst✝ : MetricSpace X
D : DeloneSet X
r : ℝ≥0
hr : r ≤ D.packingRadius / 2
x y z : X
hx : x ∈ D
hy : y ∈ D
hxz : x ∈ ball z ↑r
hyz : y ∈ ball z ↑r
⊢ x = y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic

Goal state before:
pp: X : Type u_1
inst✝ : MetricSpace X
D : DeloneSet X
hK1 hK2 : 0 < 1
hA : AntilipschitzWith 1 ⇑(Equiv.refl X)
hL : LipschitzWith 1 ⇑(Equiv.refl X)
⊢ mapBilipschitz (Equiv.refl X) 1 1 hK1 hK2 hA hL D = D

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp

Goal state before:
pp: ⊢ exp 0 = 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp

Goal state before:
pp: x : EReal
⊢ x.exp = 0 ↔ x = ⊥

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp

Goal state before:
pp: x : EReal
⊢ x.exp = ∞ ↔ x = ⊤

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: ⊢ log 1 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: x : ℝ
⊢ (ENNReal.ofReal x).log = if x ≤ 0 then ⊥ else ↑(Real.log x)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: x : ℝ
hx : 0 < x
⊢ (ENNReal.ofReal x).log = ↑(Real.log x)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: x : ℝ≥0∞
h : x ≠ 0
h' : x ≠ ∞
⊢ x.log = ↑(Real.log x.toReal)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: x : ℝ≥0∞
h : 0 < x.toReal
⊢ x.log = ↑(Real.log x.toReal)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: x : ℝ≥0
h : x ≠ 0
⊢ (↑x).log = ↑(Real.log ↑x)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp

Goal state before:
pp: ⊢ StrictMono exp

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Z : Type u_3
inst✝ : MetricSpace Z
D : DeloneSet X
f : X ≃ Y
g : Y ≃ Z
K₁f K₂f K₁g K₂g : ℝ≥0
hf₁_pos : 0 < K₁f
hf₂_pos : 0 < K₂f
hg₁_pos : 0 < K₁g
hg₂_pos : 0 < K₂g
hf_anti : AntilipschitzWith K₁f ⇑f
hf_lip : LipschitzWith K₂f ⇑f
hg_anti : AntilipschitzWith K₁g ⇑g
hg_lip : LipschitzWith K₂g ⇑g
⊢ mapBilipschitz g K₁g K₂g hg₁_pos hg₂_pos hg_anti hg_lip (mapBilipschitz f K₁f K₂f hf₁_pos hf₂_pos hf_anti hf_lip D) =
    mapBilipschitz (f.trans g) (K₁f * K₁g) (K₂g * K₂f) ⋯ ⋯ ⋯ ⋯ D

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : X ≃ᵢ Y
D : DeloneSet X
⊢ D.packingRadius = (mapBilipschitz f.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).packingRadius

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp

Goal state before:
pp: x : EReal
⊢ (-x).exp = x.exp⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : X ≃ᵢ Y
D : DeloneSet X
⊢ D.coveringRadius = (mapBilipschitz f.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).coveringRadius

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : X ≃ᵢ Y
D : DeloneSet Y
⊢ D.packingRadius = (mapBilipschitz f.symm.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).packingRadius

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : X ≃ᵢ Y
D : DeloneSet Y
⊢ D.coveringRadius = (mapBilipschitz f.symm.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).coveringRadius

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: ⊢ StrictMono log

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: ⊢ Function.Surjective log

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : X ≃ᵢ Y
D : DeloneSet X
⊢ (fun D ↦
        (mapBilipschitz f.symm.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).copy (⇑f.symm '' D.carrier) D.packingRadius D.coveringRadius ⋯ ⋯
          ⋯)
      ((fun D ↦ (mapBilipschitz f.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).copy (⇑f '' D.carrier) D.packingRadius D.coveringRadius ⋯ ⋯ ⋯)
        D) =
    D

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.ERealExp

Goal state before:
pp: x y : EReal
⊢ (x + y).exp = x.exp * y.exp

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp

Goal state before:
pp: x : EReal
⊢ x.exp.log = x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp

Goal state before:
pp: x : ℝ≥0∞
⊢ x.log.exp = x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp

Goal state before:
pp: x : EReal
n : ℕ
⊢ (↑n * x).exp = x.exp ^ n

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp

Goal state before:
pp: x : EReal
y : ℝ
⊢ (x * ↑y).exp = x.exp ^ y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp

Goal state before:
pp: x : ℝ≥0∞
y : ℝ
⊢ x ^ y = (↑y * x.log).exp

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp

Goal state before:
pp: ⊢ ∀ {a b : ℝ≥0∞},
    { toFun := log, invFun := exp, left_inv := ⋯, right_inv := ⋯ } a ≤
        { toFun := log, invFun := exp, left_inv := ⋯, right_inv := ⋯ } b ↔
      a ≤ b

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp

Goal state before:
pp: ⊢ Filter.Tendsto exp (𝓝 0) (𝓝 1)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝¹ : MetricSpace X
inst✝ : MetricSpace Y
f : X ≃ᵢ Y
D : DeloneSet Y
⊢ (fun D ↦ (mapBilipschitz f.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).copy (⇑f '' D.carrier) D.packingRadius D.coveringRadius ⋯ ⋯ ⋯)
      ((fun D ↦
          (mapBilipschitz f.symm.toEquiv 1 1 ⋯ ⋯ ⋯ ⋯ D).copy (⇑f.symm '' D.carrier) D.packingRadius D.coveringRadius ⋯ ⋯
            ⋯)
        D) =
    D

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp

Goal state before:
pp: b : ℝ≥0∞
hb : 1 < b
⊢ Filter.Tendsto (fun x ↦ b ^ x) Filter.atTop (𝓝 ∞)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic

Goal state before:
pp: X : Type u_1
inst✝ : MetricSpace X
D : DeloneSet X
⊢ (mapIsometry (IsometryEquiv.refl X)) D = D

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp

Goal state before:
pp: b : ℝ≥0∞
hb : b < 1
⊢ Filter.Tendsto (fun x ↦ b ^ x) Filter.atTop (𝓝 0)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.AperiodicOrder.Delone.Basic

Goal state before:
pp: X : Type u_1
Y : Type u_2
inst✝² : MetricSpace X
inst✝¹ : MetricSpace Y
Z : Type u_3
inst✝ : MetricSpace Z
D : DeloneSet X
f : X ≃ᵢ Y
g : Y ≃ᵢ Z
⊢ (mapIsometry (f.trans g)) D = (mapIsometry g) ((mapIsometry f) D)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: x y : ℝ≥0∞
⊢ (x * y).log = x.log + y.log

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp

Goal state before:
pp: b : ℝ≥0∞
hb : 1 < b
⊢ Filter.Tendsto (fun x ↦ b ^ x) Filter.atBot (𝓝 0)

Tactic:
by

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

Goal state before:
pp: u v : ℕ → EReal
h : ∃ᶠ (n : ℕ) in atTop, u n ≤ v n
n : ℕ
u_v : u n ≤ v n
⊢ u n / ↑n ≤ v n / ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLogExp

Goal state before:
pp: b : ℝ≥0∞
hb : b < 1
⊢ Filter.Tendsto (fun x ↦ b ^ x) Filter.atBot (𝓝 ∞)

Tactic:
by

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

Goal state before:
pp: u : ℕ → EReal
a b : EReal
x✝¹ : b > a
n : ℕ
x✝ : 1 ≤ n
⊢ 0 < ↑n

Tactic:
by

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

Goal state before:
pp: u : ℕ → EReal
a : EReal
⊢ linearGrowthInf u ≤ a ↔ ∀ b > a, ∃ᶠ (n : ℕ) in atTop, u n ≤ b * ↑n

Tactic:
by

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

Goal state before:
pp: u : ℕ → EReal
a b : EReal
x✝¹ : b < a
n : ℕ
x✝ : 1 ≤ n
⊢ ↑n > 0

Tactic:
by

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

Goal state before:
pp: u : ℕ → EReal
a : EReal
⊢ a ≤ linearGrowthInf u ↔ ∀ b < a, ∀ᶠ (n : ℕ) in atTop, b * ↑n ≤ u n

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: x : ℝ≥0∞
y : ℝ
⊢ (x ^ y).log = ↑y * x.log

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: x : ℝ≥0∞
n : ℕ
⊢ (x ^ n).log = ↑n * x.log

Tactic:
by

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

Goal state before:
pp: u : ℕ → EReal
a : EReal
⊢ linearGrowthSup u ≤ a ↔ ∀ b > a, ∀ᶠ (n : ℕ) in atTop, u n ≤ b * ↑n

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog

Goal state before:
pp: x : ℝ≥0∞
⊢ x⁻¹.log = -x.log

Tactic:
by

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

Goal state before:
pp: u : ℕ → EReal
a : EReal
⊢ a ≤ linearGrowthSup u ↔ ∀ b < a, ∃ᶠ (n : ℕ) in atTop, b * ↑n ≤ u n

Tactic:
by

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

Goal state before:
pp: u : ℕ → EReal
a : EReal
h : ∃ᶠ (n : ℕ) in atTop, u n ≤ a * ↑n
c : EReal
c_u : c > a
n : ℕ
hn : u n ≤ a * ↑n
⊢ a * ↑n ≤ c * ↑n

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: n : ℕ
n_pos : 0 < n
⊢ 0 < ↑n

Tactic:
by

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

Goal state before:
pp: ⊢ linearGrowthSup ⊥ = ⊥

Tactic:
by

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

Goal state before:
pp: ⊢ linearGrowthInf ⊥ = ⊥

Tactic:
by

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

Goal state before:
pp: ⊢ linearGrowthInf ⊤ = ⊤

Tactic:
by

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

Goal state before:
pp: ⊢ linearGrowthSup ⊤ = ⊤

Tactic:
by

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

Goal state before:
pp: u : ℕ → EReal
h : 0 < linearGrowthInf u
⊢ Tendsto u atTop (𝓝 ⊤)

Tactic:
by

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

Goal state before:
pp: u v : ℕ → EReal
⊢ linearGrowthInf u + linearGrowthInf v ≤ linearGrowthInf (u + v)

Tactic:
by

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

Goal state before:
pp: u v : ℕ → EReal
h : linearGrowthSup u ≠ ⊥ ∨ linearGrowthInf v ≠ ⊤
h' : linearGrowthSup u ≠ ⊤ ∨ linearGrowthInf v ≠ ⊥
⊢ linearGrowthInf (u + v) ≤ linearGrowthSup u + linearGrowthInf v

Tactic:
by

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

Goal state before:
pp: u v : ℕ → EReal
h : linearGrowthInf u ≠ ⊥ ∨ linearGrowthSup v ≠ ⊤
h' : linearGrowthInf u ≠ ⊤ ∨ linearGrowthSup v ≠ ⊥
⊢ linearGrowthInf (u + v) ≤ linearGrowthInf u + linearGrowthSup v

Tactic:
by

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

Goal state before:
pp: u v : ℕ → EReal
⊢ linearGrowthSup u + linearGrowthInf v ≤ linearGrowthSup (u + v)

Tactic:
by

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

Goal state before:
pp: u v : ℕ → EReal
⊢ linearGrowthInf u + linearGrowthSup v ≤ linearGrowthSup (u + v)

Tactic:
by

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

Goal state before:
pp: u v : ℕ → EReal
h : linearGrowthSup u ≠ ⊥ ∨ linearGrowthSup v ≠ ⊤
h' : linearGrowthSup u ≠ ⊤ ∨ linearGrowthSup v ≠ ⊥
⊢ linearGrowthSup (u + v) ≤ linearGrowthSup u + linearGrowthSup v

Tactic:
by

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

Goal state before:
pp: u : ℕ → EReal
⊢ linearGrowthInf (-u) = -linearGrowthSup u

Tactic:
by

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

Goal state before:
pp: u : ℕ → EReal
⊢ linearGrowthSup (-u) = -linearGrowthInf u

Tactic:
by

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

Goal state before:
pp: u : ℕ → ℝ≥0∞
⊢ expGrowthInf u = linearGrowthInf (log ∘ u)

Tactic:
by

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

Goal state before:
pp: u : ℕ → ℝ≥0∞
⊢ expGrowthSup u = linearGrowthSup (log ∘ u)

Tactic:
by

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

Goal state before:
pp: u v : ℕ → ℝ≥0∞
h : ∃ᶠ (n : ℕ) in atTop, u n ≤ v n
n : ℕ
u_v : u n ≤ v n
⊢ (u n).log / ↑n ≤ (v n).log / ↑n

Tactic:
by

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

Goal state before:
pp: u : ℕ → ℝ≥0∞
a b : EReal
x✝¹ : b > a
n : ℕ
x✝ : 1 ≤ n
⊢ 0 < ↑n

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace β
inst✝ : CommSemiring β
l : Filter α
k : α → β
z : ℕ
⊢ Tendsto (fun a ↦ k a ^ z * 0 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 g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : CommSemiring β
inst✝ : ContinuousAdd β
hf : SuperpolynomialDecay l k f
hg : SuperpolynomialDecay l k g
z : ℕ
⊢ Tendsto (fun a ↦ k a ^ z * (f + g) 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 g : α → β
inst✝² : TopologicalSpace β
inst✝¹ : CommSemiring β
inst✝ : ContinuousMul β
hf : SuperpolynomialDecay l k f
hg : SuperpolynomialDecay l k g
z : ℕ
⊢ Tendsto (fun a ↦ k a ^ z * (f * g) a) l (𝓝 0)

Tactic:
by

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

Goal state before:
pp: u : ℕ → ℝ≥0∞
a : EReal
⊢ expGrowthInf u ≤ a ↔ ∀ b > a, ∃ᶠ (n : ℕ) in atTop, u n ≤ (b * ↑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✝² : TopologicalSpace β
inst✝¹ : CommSemiring β
inst✝ : ContinuousMul β
hf : SuperpolynomialDecay l k f
c : β
z : ℕ
⊢ Tendsto (fun a ↦ k a ^ z * (fun n ↦ f n * c) 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✝ : CommSemiring β
hf : SuperpolynomialDecay l k f
z : ℕ
s : Set β
hs : IsOpen[inst✝¹] s
hs0 : 0 ∈ s
x : α
hx : x ∈ (fun a ↦ k a ^ (z + 1) * f a) ⁻¹' s
⊢ x ∈ (fun a ↦ k a ^ z * (k * f) a) ⁻¹' s

Tactic:
by

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

Goal state before:
pp: u : ℕ → ℝ≥0∞
a b : EReal
x✝¹ : b < a
n : ℕ
x✝ : 1 ≤ n
⊢ ↑n > 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✝ : CommSemiring β
hf : SuperpolynomialDecay l k f
n : ℕ
⊢ SuperpolynomialDecay l k (k ^ n * 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✝ : CommSemiring β
hf : SuperpolynomialDecay l k f
n : ℕ
⊢ SuperpolynomialDecay l k (k ^ n * f)

Tactic:
by
  induction n with
  | zero => simpa only [one_mul, pow_zero] using hf
  | succ n hn => simpa only [pow_succ', mul_assoc] using hn.param_mul

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✝² : CommSemiring β
inst✝¹ : ContinuousAdd β
inst✝ : ContinuousMul β
hf : SuperpolynomialDecay l k f
p✝ p q : β[X]
hp : SuperpolynomialDecay l k fun x ↦ eval (k x) p * f x
hq : SuperpolynomialDecay l k fun x ↦ eval (k x) q * f x
⊢ SuperpolynomialDecay l k fun x ↦ eval (k x) (p + q) * f 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✝² : CommSemiring β
inst✝¹ : ContinuousAdd β
inst✝ : ContinuousMul β
hf : SuperpolynomialDecay l k f
p : β[X]
n : ℕ
c : β
⊢ SuperpolynomialDecay l k fun x ↦ eval (k x) ((monomial n) c) * f x

Tactic:
by

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

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

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
⊢ 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 g g' : α → β
inst✝⁴ : TopologicalSpace β
inst✝³ : CommSemiring β
inst✝² : PartialOrder β
inst✝¹ : IsOrderedRing β
inst✝ : OrderTopology β
hk : 0 ≤ᶠ[l] k
hg : SuperpolynomialDecay l k g
hg' : SuperpolynomialDecay l k g'
hfg : g ≤ᶠ[l] f
hfg' : f ≤ᶠ[l] g'
z : ℕ
x : α
hx : g x ≤ f x
hx' : 0 ≤ k x
⊢ k x ^ z * g x ≤ k x ^ z * f 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 g g' : α → β
inst✝⁴ : TopologicalSpace β
inst✝³ : CommSemiring β
inst✝² : PartialOrder β
inst✝¹ : IsOrderedRing β
inst✝ : OrderTopology β
hk : 0 ≤ᶠ[l] k
hg : SuperpolynomialDecay l k g
hg' : SuperpolynomialDecay l k g'
hfg : g ≤ᶠ[l] f
hfg' : f ≤ᶠ[l] g'
z : ℕ
⊢ ∀ᶠ (b : α) in l, k b ^ z * g b ≤ k b ^ z * f b

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝⁴ : TopologicalSpace β
inst✝³ : CommSemiring β
inst✝² : PartialOrder β
inst✝¹ : IsOrderedRing β
inst✝ : OrderTopology β
hk : 0 ≤ᶠ[l] k
hg : SuperpolynomialDecay l k g
hg' : SuperpolynomialDecay l k g'
hfg : g ≤ᶠ[l] f
hfg' : f ≤ᶠ[l] g'
z : ℕ
x : α
hx : f x ≤ g' x
hx' : 0 ≤ k x
⊢ k x ^ z * f x ≤ k x ^ z * g' 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 μ
f : X → Set (Set X)
s : Set X
h : v.FineSubfamilyOn f s
inst✝ : SecondCountableTopology X
ρ : Measure X
hρ : ρ ≪ μ
⊢ s ⊆ (s \ ⋃ p ∈ h.index, h.covering p) ∪ ⋃ p ∈ h.index, h.covering p

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
k f g g' : α → β
inst✝⁴ : TopologicalSpace β
inst✝³ : CommSemiring β
inst✝² : PartialOrder β
inst✝¹ : IsOrderedRing β
inst✝ : OrderTopology β
hk : 0 ≤ᶠ[l] k
hg : SuperpolynomialDecay l k g
hg' : SuperpolynomialDecay l k g'
hfg : g ≤ᶠ[l] f
hfg' : f ≤ᶠ[l] g'
z : ℕ
⊢ ∀ᶠ (b : α) in l, k b ^ z * f b ≤ k b ^ z * g' b

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✝³ : CommRing β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
⊢ (∀ (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.SuperpolynomialDecay

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
k f g : α → β
inst✝⁴ : TopologicalSpace β
inst✝³ : CommRing β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hf : ∀ (n : ℕ), Tendsto (fun a ↦ |k a ^ n * f a|) l (𝓝 0)
hfg : abs ∘ g ≤ᶠ[l] abs ∘ f
z : ℕ
x : α
hx : (abs ∘ g) x ≤ (abs ∘ f) x
⊢ |k x ^ z| * |g x| ≤ |k x ^ z| * |f 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 μ
f : X → Set (Set X)
s : Set X
h : v.FineSubfamilyOn f s
inst✝ : SecondCountableTopology X
ρ : Measure X
hρ : ρ ≪ μ
⊢ ρ (s \ ⋃ p ∈ h.index, h.covering p) + ρ (⋃ p ∈ h.index, h.covering p) = ∑' (p : ↑h.index), ρ (h.covering ↑p)

Tactic:
by

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

Goal state before:
pp: α : Type u_1
β : Type u_2
l : Filter α
k f g : α → β
inst✝⁴ : TopologicalSpace β
inst✝³ : CommRing β
inst✝² : LinearOrder β
inst✝¹ : IsStrictOrderedRing β
inst✝ : OrderTopology β
hf : SuperpolynomialDecay l k f
hfg : abs ∘ g ≤ᶠ[l] abs ∘ f
⊢ SuperpolynomialDecay l k g

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✝ : ContinuousMul β
c : β
hc0 : c ≠ 0
h : SuperpolynomialDecay l k fun n ↦ f n * c
x : α
⊢ f x * c * c⁻¹ = f 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✝ : ContinuousMul β
c : β
hc0 : c ≠ 0
h : SuperpolynomialDecay l k fun n ↦ c * f n
x : α
⊢ c⁻¹ * (c * f x) = f 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 < δ
⊢ ∀ (x : X), ∀ s ∈ v.setsAt x ∪ {s | MeasurableSet s ∧ (interior s).Nonempty ∧ ¬s ⊆ closedBall x δ}, MeasurableSet s

Tactic:
by

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

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

Tactic:
by

Goal state after: