mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Log.Monotone

Goal state before:
pp: ⊢ StrictAntiOn (fun x ↦ x * log x) (Icc 0 (rexp (-1)))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 0 < t
⊢ MonotoneOn (cfcₙ (p.rpowIntegrand₀₁ t)) (Ici 0)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: A : Type u_1
inst✝² : NonUnitalCStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 0 < t
⊢ ConcaveOn ℝ (Ici 0) (cfcₙ (p.rpowIntegrand₀₁ t))

Tactic:
by

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

Goal state before:
pp: b : ℝ
hb : 1 < b
⊢ StrictAntiOn (logb b) (Iio 0)

Tactic:
by

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

Goal state before:
pp: b : ℝ
b_lt_one : b < 1
⊢ b ≠ 1

Tactic:
by

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

Goal state before:
pp: b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
h : 0 < x
h₁ : 0 < y
⊢ log y ≤ log x ↔ y ≤ x

Tactic:
log_le_log_iff h₁ h

Goal state after:
b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
h : 0 < x
h₁ : 0 < y
⊢ y ≤ x ↔ y ≤ x
Module: Mathlib.Analysis.SpecialFunctions.Log.Monotone

Goal state before:
pp: x : ℝ
hex : x ∈ Ici (rexp 1)
y : ℝ
hey : y ∈ Ici (rexp 1)
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
⊢ 1 ≤ log x

Tactic:
by

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

Goal state before:
pp: b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
h : 0 < x
h₁ : 0 < y
⊢ logb b x ≤ logb b y ↔ y ≤ x

Tactic:
by

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

Goal state before:
pp: b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
hxy : x < y
⊢ logb b y < logb b x

Tactic:
by

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

Goal state before:
pp: b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
hy : 0 < y
⊢ logb b x < logb b y ↔ y < x

Tactic:
by

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

Goal state before:
pp: b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
⊢ logb b x ≤ y ↔ b ^ y ≤ x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq

Goal state before:
pp: ε x : ℝ
⊢ -ε.mulExpNegMulSq (-x) = ε.mulExpNegMulSq x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq

Goal state before:
pp: x : ℝ
⊢ mulExpNegMulSq 1 x ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq

Goal state before:
pp: x : ℝ
⊢ -1 ≤ mulExpNegMulSq 1 x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq

Goal state before:
pp: ε : ℝ
⊢ Continuous fun x ↦ rexp (-(ε * x * x))

Tactic:
by

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

Goal state before:
pp: x : ℝ
hex : x ∈ Ici (rexp 1)
y : ℝ
hey : y ∈ Ici (rexp 1)
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
hlogx : 1 ≤ log x
⊢ 0 ≤ y / x - 1

Tactic:
by

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

Goal state before:
pp: b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
⊢ logb b x < y ↔ b ^ y < x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq

Goal state before:
pp: ε y : ℝ
⊢ DifferentiableAt ℝ (fun x ↦ rexp (-(ε * x * x))) y

Tactic:
by

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

Goal state before:
pp: b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hy : 0 < y
⊢ x ≤ logb b y ↔ y ≤ b ^ x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq

Goal state before:
pp: ε y : ℝ
⊢ -(ε * 1 * y + ε * y * 1) = -2 * ε * y

Tactic:
by

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

Goal state before:
pp: b x y : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hy : 0 < y
⊢ x < logb b y ↔ y < b ^ x

Tactic:
by

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

Goal state before:
pp: b x : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
⊢ 0 < logb b x ↔ x < 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq

Goal state before:
pp: ε y : ℝ
⊢ HasDerivAt ε.mulExpNegMulSq (rexp (-(ε * y * y)) + y * (rexp (-(ε * y * y)) * (-2 * ε * y))) y

Tactic:
by

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

Goal state before:
pp: x : ℝ
hex : x ∈ Ici (rexp 1)
y : ℝ
hey : y ∈ Ici (rexp 1)
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
hlogx : 1 ≤ log x
hyx : 0 ≤ y / x - 1
⊢ log y - log x = log (y / x)

Tactic:
by

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

Goal state before:
pp: b x : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
hx' : x < 1
⊢ 0 < logb b x

Tactic:
by

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

Goal state before:
pp: x : ℝ
hex : x ∈ Ici (rexp 1)
y : ℝ
hey : y ∈ Ici (rexp 1)
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
hlogx : 1 ≤ log x
hyx : 0 ≤ y / x - 1
⊢ log x * (y / x - 1) = log x / x * y - log x

Tactic:
by

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

Goal state before:
pp: b x : ℝ
b_pos : 0 < b
b_lt_one : b < 1
h : 0 < x
⊢ logb b x < 0 ↔ 1 < x

Tactic:
by

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

Goal state before:
pp: ⊢ AntitoneOn (fun x ↦ log x / x) (Ici (rexp 1))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq

Goal state before:
pp: ε : ℝ
hε : 0 < ε
x : ℝ
⊢ rexp (-(ε * x * x)) + x * (rexp (-(ε * x * x)) * (-2 * ε * x)) = rexp (-(ε * x * x)) * (1 - 2 * (ε * x * x))

Tactic:
by

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

Goal state before:
pp: b x : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
⊢ 0 ≤ logb b x ↔ x ≤ 1

Tactic:
by

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

Goal state before:
pp: b x : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
hx' : x ≤ 1
⊢ 0 ≤ logb b x

Tactic:
by

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

Goal state before:
pp: a : ℝ
ha : 0 < a
x : ℝ
hex : x ∈ Ici (rexp a⁻¹)
y : ℝ
x✝ : y ∈ Ici (rexp a⁻¹)
hxy : x ≤ y
⊢ (fun x ↦ log x / x ^ a) y ≤ (fun x ↦ log x / x ^ a) x

Tactic:
simp only

Goal state after:
a : ℝ
ha : 0 < a
x : ℝ
hex : x ∈ Ici (rexp a⁻¹)
y : ℝ
x✝ : y ∈ Ici (rexp a⁻¹)
hxy : x ≤ y
⊢ log y / y ^ a ≤ log x / x ^ a
Module: Mathlib.Analysis.SpecialFunctions.Log.Base

Goal state before:
pp: b x : ℝ
b_pos : 0 < b
b_lt_one : b < 1
hx : 0 < x
⊢ logb b x ≤ 0 ↔ 1 ≤ x

Tactic:
by

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

Goal state before:
pp: a : ℝ
ha : 0 < a
x : ℝ
hex : x ∈ Ici (rexp a⁻¹)
y : ℝ
x✝ : y ∈ Ici (rexp a⁻¹)
hxy : x ≤ y
x_pos : 0 < x
⊢ 0 < y

Tactic:
by

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

Goal state before:
pp: b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
⊢ StrictMonoOn (logb b) (Iio 0)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq

Goal state before:
pp: ε : ℝ
hε : 0 < ε
x : ℝ
y : ℝ := ε * x * x
heq : rexp (-y) + x * (rexp (-y) * (-2 * ε * x)) = rexp (-y) * (1 - 2 * y)
hy : y = ε * x * x
⊢ 0 ≤ y

Tactic:
rw [hy, mul_assoc]

Goal state after:
ε : ℝ
hε : 0 < ε
x : ℝ
y : ℝ := ε * x * x
heq : rexp (-y) + x * (rexp (-y) * (-2 * ε * x)) = rexp (-y) * (1 - 2 * y)
hy : y = ε * x * x
⊢ 0 ≤ ε * (x * x)
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq

Goal state before:
pp: ε : ℝ
hε : 0 < ε
x : ℝ
y : ℝ := ε * x * x
heq : rexp (-y) + x * (rexp (-y) * (-2 * ε * x)) = rexp (-y) * (1 - 2 * y)
hy : y = ε * x * x
⊢ 0 ≤ y

Tactic:
by

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

Goal state before:
pp: b : ℝ
b_pos : 0 < b
b_lt_one : b < 1
⊢ Tendsto (logb b) atTop atBot

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq

Goal state before:
pp: ε : ℝ
hε : 0 < ε
x : ℝ
y : ℝ := ε * x * x
heq : rexp (-y) + x * (rexp (-y) * (-2 * ε * x)) = rexp (-y) * (1 - 2 * y)
hy : y = ε * x * x
hynonneg : 0 ≤ y
⊢ 0 ≤ 2 * y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq

Goal state before:
pp: ε : ℝ
hε : 0 < ε
x : ℝ
⊢ ‖deriv ε.mulExpNegMulSq x‖ ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq

Goal state before:
pp: ε : ℝ
hε : 0 < ε
x : ℝ
⊢ ‖deriv ε.mulExpNegMulSq x‖₊ ≤ 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq

Goal state before:
pp: ε : ℝ
hε : 0 < ε
⊢ LipschitzWith 1 ε.mulExpNegMulSq

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq

Goal state before:
pp: ε : ℝ
hε : 0 < ε
x : ℝ
⊢ ε.mulExpNegMulSq x = (√ε)⁻¹ * mulExpNegMulSq 1 (√ε * x)

Tactic:
by

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

Goal state before:
pp: a : ℝ
ha : 0 < a
x : ℝ
hex : x ∈ Ici (rexp a⁻¹)
y : ℝ
x✝ : y ∈ Ici (rexp a⁻¹)
hxy : x ≤ y
x_pos : 0 < x
y_pos : 0 < y
z : ℝ
hz : z ∈ Ici (rexp a⁻¹)
⊢ z ^ a ∈ {b | rexp 1 ≤ b}

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq

Goal state before:
pp: ε : ℝ
hε : 0 < ε
x : ℝ
⊢ 0 < (√ε)⁻¹

Tactic:
by

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

Goal state before:
pp: a : ℝ
ha : 0 < a
⊢ AntitoneOn (fun x ↦ log x / x ^ a) (Ici (rexp a⁻¹))

Tactic:
by

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

Goal state before:
pp: ⊢ AntitoneOn (fun x ↦ log x / √x) (Ici (rexp 2))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq

Goal state before:
pp: ε : ℝ
hε : 0 < ε
x : ℝ
⊢ |ε.mulExpNegMulSq x| ≤ (√ε)⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq

Goal state before:
pp: ε : ℝ
hε : 0 < ε
x y : ℝ
⊢ dist (ε.mulExpNegMulSq x) (ε.mulExpNegMulSq y) ≤ 2 * (√ε)⁻¹

Tactic:
by

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

Goal state before:
pp: b : ℕ
r : ℝ
hr : 0 ≤ r
⊢ ⌊logb (↑b) r⌋ = Int.log b r

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq

Goal state before:
pp: ε : ℝ
hε : 0 < ε
x y : ℝ
⊢ dist (ε.mulExpNegMulSq x) (ε.mulExpNegMulSq y) ≤ dist x y

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq

Goal state before:
pp: x : ℝ
⊢ x = (fun ε ↦ ε.mulExpNegMulSq x) 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq

Goal state before:
pp: x : ℝ
this : x = (fun ε ↦ ε.mulExpNegMulSq x) 0
⊢ Continuous fun ε ↦ rexp (-(ε * x * x))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq

Goal state before:
pp: x : ℝ
⊢ Tendsto (fun ε ↦ ε.mulExpNegMulSq x) (𝓝 0) (𝓝 x)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq

Goal state before:
pp: ε : ℝ
E : Type u_1
inst✝ : TopologicalSpace E
x : E
g : E →ᵇ ℝ
hε : 0 ≤ ε
⊢ |(ε.mulExpNegMulSq ∘ ⇑g) x| ≤ ‖g‖

Tactic:
by

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

Goal state before:
pp: b : ℕ
r : ℝ
hr : 0 ≤ r
⊢ ⌈logb (↑b) r⌉ = Int.clog b r

Tactic:
by

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

Goal state before:
pp: n b : ℕ
hn : n ≠ 0
⊢ 0 ≤ ↑n

Tactic:
by

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

Goal state before:
pp: n b : ℕ
hn : n ≠ 0
⊢ 1 < ↑(b + 1 + 1)

Tactic:
simp [Nat.cast_add_one_pos]

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

Goal state before:
pp: n b : ℕ
hn : n ≠ 0
⊢ 1 < ↑(b + 1 + 1)

Tactic:
by

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

Goal state before:
pp: n b : ℕ
hn : n ≠ 0
⊢ 1 ≤ n

Tactic:
by

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

Goal state before:
pp: b n : ℕ
⊢ ⌊logb ↑b ↑n⌋₊ = Nat.log b n

Tactic:
by

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

Goal state before:
pp: b n : ℕ
⊢ ⌈logb ↑b ↑n⌉₊ = Nat.clog b n

Tactic:
by

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

Goal state before:
pp: a b : ℕ
⊢ ↑(Nat.log b a) ≤ logb ↑b ↑a

Tactic:
by

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

Goal state before:
pp: n : ℕ
⊢ ↑n.log2 ≤ logb 2 ↑n

Tactic:
by

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

Goal state before:
pp: b x : ℝ
⊢ logb b x = 0 ↔ b = 0 ∨ b = 1 ∨ b = -1 ∨ x = 0 ∨ x = 1 ∨ x = -1

Tactic:
by

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

Goal state before:
pp: b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
this : ∀ {b : ℝ}, b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1 → 0 < b → Tendsto (fun x ↦ |logb b x|) atTop atTop
hb₀ : ¬0 < b
⊢ -b ≠ -1 ∧ -b ≠ 0 ∧ -b ≠ 1

Tactic:
by

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

Goal state before:
pp: b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
this : ∀ {b : ℝ}, b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1 → 0 < b → Tendsto (fun x ↦ |logb b x|) atTop atTop
hb₀ : ¬0 < b
⊢ 0 < -b

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
f : X →ᵇ ℝ≥0
x : X
⊢ f x ≤ nndist 0 f

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
f : X →ᵇ ℝ≥0
x : X
⊢ f x ≤ nndist 0 f

Tactic:
by
  convert! nndist_coe_le_nndist x
  simp only [coe_zero, Pi.zero_apply, NNReal.nndist_zero_eq_val]

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

Goal state before:
pp: b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
this : ∀ {b : ℝ}, b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1 → 0 < b → Tendsto (fun x ↦ |logb b x|) atTop atTop
hb₀ : ¬0 < b
⊢ ∀ (x : ℝ), |logb (-b) x| = |logb b x|

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: X : Type u_1
inst✝ : TopologicalSpace X
f : X →ᵇ ℝ≥0
x : X
⊢ ↑(f x) ≤ edist 0 f

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : MeasurableSpace X
f : X →ᵇ ℝ≥0
μ : Measure X
⊢ ∫⁻ (a : X), ↑(nndist 0 f) ∂μ ≤ edist 0 f * μ Set.univ

Tactic:
by

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

Goal state before:
pp: b✝ b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
hb₀ : 0 < b
this : ∀ {b : ℝ}, b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1 → 0 < b → 1 < b → Tendsto (fun x ↦ |logb b x|) atTop atTop
hb₁ : ¬1 < b
⊢ b⁻¹ ≠ -1 ∧ b⁻¹ ≠ 0 ∧ b⁻¹ ≠ 1

Tactic:
by

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

Goal state before:
pp: b✝ b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
hb₀ : 0 < b
this : ∀ {b : ℝ}, b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1 → 0 < b → 1 < b → Tendsto (fun x ↦ |logb b x|) atTop atTop
hb₁ : ¬1 < b
⊢ 0 < b⁻¹

Tactic:
by

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

Goal state before:
pp: b✝ b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
hb₀ : 0 < b
this : ∀ {b : ℝ}, b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1 → 0 < b → 1 < b → Tendsto (fun x ↦ |logb b x|) atTop atTop
hb₁ : ¬1 < b
⊢ b < 1

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
f : X →ᵇ ℝ≥0
⊢ ∫⁻ (x : X), ↑(f x) ∂μ < ∞

Tactic:
by

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

Goal state before:
pp: b✝ b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
hb₀ : 0 < b
this : ∀ {b : ℝ}, b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1 → 0 < b → 1 < b → Tendsto (fun x ↦ |logb b x|) atTop atTop
hb₁ : ¬1 < b
⊢ ∀ (x : ℝ), |logb b⁻¹ x| = |logb b x|

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : OpensMeasurableSpace X
f : X →ᵇ ℝ≥0
⊢ Integrable (NNReal.toReal ∘ ⇑f) μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : MeasurableSpace X
μ : Measure X
inst✝¹ : IsFiniteMeasure μ
inst✝ : OpensMeasurableSpace X
f : X →ᵇ ℝ
⊢ ∫ (x : X), f x ∂μ = ∫ (x : X), ↑(f.nnrealPart x) ∂μ - ∫ (x : X), ↑((-f).nnrealPart x) ∂μ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
f : X →ᵇ ℝ≥0
μ : Measure X
⊢ AEStronglyMeasurable (fun x ↦ ↑(f x)) μ

Tactic:
by

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

Goal state before:
pp: b : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
⊢ Tendsto (fun x ↦ |logb b x|) atTop atTop

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
f : X →ᵇ ℝ≥0
μ : Measure X
⊢ ∀ (x : X), 0 x ≤ (fun x ↦ ↑(f x)) x

Tactic:
by

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

Goal state before:
pp: b x : ℝ
hb₀ : 0 < b
hb : b ≠ 1
⊢ ContinuousAt (logb b) x ↔ x ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: X : Type u_1
inst✝² : TopologicalSpace X
inst✝¹ : MeasurableSpace X
inst✝ : OpensMeasurableSpace X
f : X →ᵇ ℝ≥0
μ : Measure X
⊢ (∫⁻ (x : X), ↑(f x) ∂μ).toReal = ∫ (x : X), ↑(f x) ∂μ

Tactic:
by

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

Goal state before:
pp: b : ℝ
α : Type u_1
s : Finset α
f : α → ℝ
hf : ∀ x ∈ s, f x ≠ 0
⊢ logb b (∏ i ∈ s, f i) = ∑ i ∈ s, logb b (f i)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: X : Type u_1
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
μ : Measure X
E : Type u_2
inst✝ : NormedAddCommGroup E
f : X →ᵇ E
⊢ ∫⁻ (x : X), ↑‖f x‖₊ ∂μ ≤ ∫⁻ (x : X), ↑‖f‖₊ ∂μ

Tactic:
by

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

Goal state before:
pp: b : ℝ
n : ℕ
⊢ logb b ↑n = n.factorization.sum fun p t ↦ ↑t * logb b ↑p

Tactic:
by

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

Goal state before:
pp: b a c : ℝ
n : ℕ
ha : a ≠ 0
h : log b ≠ 0
⊢ a * log b ^ n ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: X : Type u_1
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
μ : Measure X
E : Type u_2
inst✝ : NormedAddCommGroup E
f : X →ᵇ E
⊢ ∫⁻ (x : X), ↑‖f‖₊ ∂μ = ↑‖f‖₊ * μ Set.univ

Tactic:
by

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

Goal state before:
pp: b a c : ℝ
n : ℕ
ha : a ≠ 0
h : log b ≠ 0
x : ℝ
⊢ log x ^ n / (a * log b ^ n * x + c * log b ^ n) = logb b x ^ n / (a * x + c)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: X : Type u_1
inst✝² : MeasurableSpace X
inst✝¹ : TopologicalSpace X
μ : Measure X
E : Type u_2
inst✝ : NormedAddCommGroup E
f : X →ᵇ E
⊢ ∫⁻ (x : X), ↑‖f x‖₊ ∂μ ≤ ↑‖f‖₊ * μ Set.univ

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: X : Type u_1
inst✝⁷ : MeasurableSpace X
inst✝⁶ : TopologicalSpace X
μ : Measure X
E : Type u_2
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : OpensMeasurableSpace X
inst✝³ : SecondCountableTopology E
inst✝² : MeasurableSpace E
inst✝¹ : BorelSpace E
inst✝ : IsFiniteMeasure μ
f : X →ᵇ E
⊢ Integrable (⇑f) μ

Tactic:
by

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

Goal state before:
pp: b a c : ℝ
n : ℕ
ha : a ≠ 0
⊢ Tendsto (fun x ↦ logb b x ^ n / (a * x + c)) atTop (𝓝 0)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: X : Type u_1
inst✝⁸ : MeasurableSpace X
inst✝⁷ : TopologicalSpace X
μ : Measure X
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : OpensMeasurableSpace X
inst✝⁴ : SecondCountableTopology E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure μ
f : X →ᵇ E
⊢ ∫ (x : X), ‖f‖ ∂μ = μ.real Set.univ • ‖f‖

Tactic:
by

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

Goal state before:
pp: b : ℝ
n : ℕ
⊢ (fun x ↦ logb b x ^ n) =o[atTop] id

Tactic:
by

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

Goal state before:
pp: b c : ℝ
hb : b ≠ -1 ∧ b ≠ 0 ∧ b ≠ 1
⊢ (fun x ↦ c) =o[atTop] logb b

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: X : Type u_1
inst✝⁸ : MeasurableSpace X
inst✝⁷ : TopologicalSpace X
μ : Measure X
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : OpensMeasurableSpace X
inst✝⁴ : SecondCountableTopology E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : IsFiniteMeasure μ
f : X →ᵇ E
⊢ ‖∫ (x : X), f x ∂μ‖ ≤ μ.real Set.univ * ‖f‖

Tactic:
by

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

Goal state before:
pp: b : ℝ
⊢ logb b =O[⊤] log

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: X : Type u_1
inst✝⁸ : MeasurableSpace X
inst✝⁷ : TopologicalSpace X
μ : Measure X
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : OpensMeasurableSpace X
inst✝⁴ : SecondCountableTopology E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℝ E
inst✝ : IsProbabilityMeasure μ
f : X →ᵇ E
⊢ ‖∫ (x : X), f x ∂μ‖ ≤ ‖f‖

Tactic:
by

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

Goal state before:
pp: c : ℝ
hc : c ≠ 0
⊢ (fun x ↦ log (c * x)) =ᶠ[atTop] fun x ↦ log c + log x

Tactic:
by

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

Goal state before:
pp: c : ℝ
⊢ (fun x ↦ log (c * x)) =O[atTop] log

Tactic:
by

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

Goal state before:
pp: c : ℝ
⊢ (fun x ↦ log (x * c)) =O[atTop] log

Tactic:
by

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

Goal state before:
pp: b c : ℝ
⊢ (fun x ↦ logb b (c * x)) =O[atTop] log

Tactic:
by

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

Goal state before:
pp: b c : ℝ
⊢ (fun x ↦ logb b (x * c)) =O[atTop] log

Tactic:
by

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

Goal state before:
pp: b y : ℝ
⊢ Tendsto (fun x ↦ logb b (x + y) - logb b x) atTop (𝓝 0)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: X : Type u_1
inst✝⁸ : MeasurableSpace X
inst✝⁷ : TopologicalSpace X
E : Type u_2
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : OpensMeasurableSpace X
inst✝⁴ : SecondCountableTopology E
inst✝³ : MeasurableSpace E
inst✝² : BorelSpace E
inst✝¹ : NormedSpace ℝ E
ι : Type u_3
μs : ι → Measure X
inst✝ : ∀ (i : ι), IsProbabilityMeasure (μs i)
f : X →ᵇ E
⊢ Bornology.IsBounded (Set.range fun i ↦ ∫ (x : X), f x ∂μs i)

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : MeasurableSpace X
inst✝¹ : OpensMeasurableSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
f : X →ᵇ ℝ
c : ℝ
⊢ ∫ (x : X), (f + const X c) x ∂μ = ∫ (x : X), f x ∂μ + μ.real Set.univ • c

Tactic:
by

Goal state after:
Module: Mathlib.MeasureTheory.Integral.BoundedContinuousFunction

Goal state before:
pp: X : Type u_1
inst✝³ : TopologicalSpace X
inst✝² : MeasurableSpace X
inst✝¹ : OpensMeasurableSpace X
μ : Measure X
inst✝ : IsFiniteMeasure μ
f : X →ᵇ ℝ
c : ℝ
⊢ ∫ (x : X), (const X c - f) x ∂μ = μ.real Set.univ • c - ∫ (x : X), f x ∂μ

Tactic:
by

Goal state after: