mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
s : ℂ
a : ℝ
ha : 0 < a
this : EqOn (fun t ↦ ↑t ^ (s - 1) • f (a * t)) (fun t ↦ ↑a ^ (1 - s) • (fun u ↦ ↑u ^ (s - 1) • f u) (a * t)) (Ioi 0)
⊢ ↑a ^ (-s) • ∫ (x : ℝ) in Ioi 0, ↑x ^ (s - 1) • f x = ↑a ^ (-s) • ∫ (t : ℝ) in Ioi 0, ↑t ^ (s - 1) • f t

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: case succ
z : ℂ
n : ℕ
ih : HasDerivAt (logTaylor (n + 1)) (∑ j ∈ Finset.range n, (-1) ^ j * z ^ j) z
⊢ HasDerivAt (logTaylor (n + 1) + fun z ↦ (-1) ^ (n + 1 + 1) * z ^ (n + 1) / ↑(n + 1))
    (∑ j ∈ Finset.range (n + 1), (-1) ^ j * z ^ j) z

Tactic:
]

Goal state after:
case succ
z : ℂ
n : ℕ
ih : HasDerivAt (logTaylor (n + 1)) (∑ j ∈ Finset.range n, (-1) ^ j * z ^ j) z
⊢ HasDerivAt (logTaylor (n + 1) + fun z ↦ (-1) ^ (n + 1 + 1) * z ^ (n + 1) / ↑(n + 1))
    (∑ j ∈ Finset.range (n + 1), (-1) ^ j * z ^ j) z
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv

Goal state before:
pp: s : ℂ
hs : 0 < s.re
⊢ HasDerivAt (mellin fun x ↦ ↑(rexp (-x))) (∫ (t : ℝ) in Ioi 0, ↑t ^ (s - 1) * (↑(Real.log t) * ↑(rexp (-t)))) s

Tactic:
]

Goal state after:
s : ℂ
hs : 0 < s.re
⊢ HasDerivAt (mellin fun x ↦ ↑(rexp (-x))) (∫ (t : ℝ) in Ioi 0, ↑t ^ (s - 1) * (↑(Real.log t) * ↑(rexp (-t)))) s
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
T : Set ℝ
hT : T ⊆ Ioi 0
hT' : MeasurableSet T
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
s : ℂ
this : AEStronglyMeasurable (fun t ↦ ↑t ^ (s - 1) • f t) (volume.restrict T)
⊢ IntegrableOn (fun a ↦ ‖↑a ^ (s - 1) • f a‖) T volume ↔ IntegrableOn (fun t ↦ t ^ (s.re - 1) * ‖f t‖) T volume

Tactic:
]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℝ → E
T : Set ℝ
hT : T ⊆ Ioi 0
hT' : MeasurableSet T
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
s : ℂ
this : AEStronglyMeasurable (fun t ↦ ↑t ^ (s - 1) • f t) (volume.restrict T)
⊢ IntegrableOn (fun a ↦ ‖↑a ^ (s - 1) • f a‖) T volume ↔ IntegrableOn (fun t ↦ t ^ (s.re - 1) * ‖f t‖) T volume
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv

Goal state before:
pp: case convert_3
s : ℂ
hs : 0 < s.re
⊢ (fun x ↦ ‖↑(rexp (-x))‖) =O[atTop] fun x ↦ x ^ (-(s.re + 1))

Tactic:
]

Goal state after:
case convert_3
s : ℂ
hs : 0 < s.re
⊢ (fun x ↦ ‖↑(rexp (-x))‖) =O[atTop] fun x ↦ x ^ (-(s.re + 1))
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv

Goal state before:
pp: case convert_4
s : ℂ
hs : 0 < s.re
⊢ Tendsto (fun x ↦ ↑(rexp (-x))) (𝓝[>] 0) (𝓝 ↑(rexp (-0)))

Tactic:
]

Goal state after:
case convert_4
s : ℂ
hs : 0 < s.re
⊢ Tendsto (fun x ↦ ↑(rexp (-x))) (𝓝[>] 0) (𝓝 ↑(rexp (-0)))
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: n : ℕ
z : ℂ
hz : 1 + z ∈ slitPlane
H : z = -1
⊢ False

Tactic:
]

Goal state after:
n : ℕ
z : ℂ
hz : 1 + z ∈ slitPlane
H : z = -1
⊢ False
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: t : ℝ
ht : 0 ≤ t ∧ t ≤ 1
z : ℂ
hz : ‖z‖ < 1
⊢ ‖(1 + ↑t * z)⁻¹‖ ≤ (1 - ‖z‖)⁻¹

Tactic:
]

Goal state after:
t : ℝ
ht : 0 ≤ t ∧ t ≤ 1
z : ℂ
hz : ‖z‖ < 1
⊢ ‖(1 + ↑t * z)⁻¹‖ ≤ (1 - ‖z‖)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: t : ℝ
ht : 0 ≤ t ∧ t ≤ 1
z : ℂ
hz : ‖z‖ < 1
⊢ ‖1 + ↑t * z‖⁻¹ ≤ (1 - ‖z‖)⁻¹

Tactic:
]

Goal state after:
t : ℝ
ht : 0 ≤ t ∧ t ≤ 1
z : ℂ
hz : ‖z‖ < 1
⊢ ‖1 + ↑t * z‖⁻¹ ≤ (1 - ‖z‖)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: t : ℝ
ht : 0 ≤ t ∧ t ≤ 1
z : ℂ
hz : ‖z‖ < 1
⊢ 1 - t * ‖z‖ = 1 - t * ‖z‖

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: t : ℝ
ht : 0 ≤ t ∧ t ≤ 1
z : ℂ
hz : ‖z‖ < 1
⊢ 1 - ‖-(↑t * z)‖ ≤ ‖1 - -(↑t * z)‖

Tactic:
]

Goal state after:
t : ℝ
ht : 0 ≤ t ∧ t ≤ 1
z : ℂ
hz : ‖z‖ < 1
⊢ 1 - ‖-(↑t * z)‖ ≤ ‖1 - -(↑t * z)‖
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: n : ℕ
z : ℂ
hz : ‖z‖ < 1
this : ContinuousOn (fun t ↦ (1 + t • z)⁻¹) (Set.uIcc 0 1)
⊢ IntervalIntegrable (fun t ↦ t ^ n * ‖(1 + ↑t * z)⁻¹‖) MeasureTheory.volume 0 1

Tactic:
]

Goal state after:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
this : ContinuousOn (fun t ↦ (1 + t • z)⁻¹) (Set.uIcc 0 1)
⊢ IntervalIntegrable (fun t ↦ t ^ n * ‖(1 + ↑t * z)⁻¹‖) MeasureTheory.volume 0 1
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
a s : ℝ
hf : f =O[atTop] fun x ↦ x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ (b : ℝ), e ≤ b → ‖f b‖ ≤ d * ‖b ^ (-a)‖
he' : 0 < max e 1
t : ℝ
ht : t ∈ Ioi (max e 1)
ht' : 0 < t
⊢ t ^ (s - 1) * ‖f t‖ ≤ t ^ (s - 1) * (d * ‖t ^ (-a)‖)

Tactic:
]

Goal state after:
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
a s : ℝ
hf : f =O[atTop] fun x ↦ x ^ (-a)
hs : s < a
d e : ℝ
he : ∀ (b : ℝ), e ≤ b → ‖f b‖ ≤ d * ‖b ^ (-a)‖
he' : 0 < max e 1
t : ℝ
ht : t ∈ Ioi (max e 1)
ht' : 0 < t
⊢ t ^ (s - 1) * ‖f t‖ ≤ t ^ (s - 1) * (d * ‖t ^ (-a)‖)
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (fun t ↦ t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
f : ℂ → ℂ := fun z ↦ log (1 + z) - logTaylor (n + 1) z
f' : ℂ → ℂ := fun z ↦ (-z) ^ n * (1 + z)⁻¹
t : ℝ
ht : t ∈ Set.Icc 0 1
⊢ HasDerivAt f (f' (↑t * z)) (↑t * z)

Tactic:
]

Goal state after:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (fun t ↦ t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
f : ℂ → ℂ := fun z ↦ log (1 + z) - logTaylor (n + 1) z
f' : ℂ → ℂ := fun z ↦ (-z) ^ n * (1 + z)⁻¹
t : ℝ
ht : t ∈ Set.Icc 0 1
⊢ HasDerivAt f (f' (↑t * z)) (↑t * z)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv

Goal state before:
pp: ⊢ Tendsto (fun z ↦ z * Gamma z) (𝓝[≠] 0) (𝓝 (Gamma (0 + 1)))

Tactic:
]

Goal state after:
⊢ Tendsto (fun z ↦ z * Gamma z) (𝓝[≠] 0) (𝓝 (Gamma (0 + 1)))
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv

Goal state before:
pp: ⊢ ¬ContinuousAt Gamma 0

Tactic:
]

Goal state after:
⊢ ¬ContinuousAt Gamma 0
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv

Goal state before:
pp: n : ℕ
ih : ContinuousAt Gamma (-(↑n + 1))
⊢ ContinuousAt Gamma (-↑n)

Tactic:
]

Goal state after:
n : ℕ
ih : ContinuousAt Gamma (-(↑n + 1))
⊢ ContinuousAt Gamma (-↑n)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv

Goal state before:
pp: n : ℕ
ih : ContinuousAt Gamma (-(↑n + 1))
⊢ ContinuousAt (fun s ↦ Gamma (s + 1)) (-(↑n + 1))

Tactic:
]

Goal state after:
n : ℕ
ih : ContinuousAt Gamma (-(↑n + 1))
⊢ ContinuousAt (fun s ↦ Gamma (s + 1)) (-(↑n + 1))
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv

Goal state before:
pp: case pos
m : ℕ
hs : -↑m ≠ 0
⊢ 0 = 0

pp: case pos
m : ℕ
hs : -↑m ≠ 0
⊢ 1 ≤ m

Tactic:
]

Goal state after:
case pos
m : ℕ
hs : -↑m ≠ 0
⊢ 1 ≤ m
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv

Goal state before:
pp: case pos
m : ℕ
hs : 1 ≤ m
⊢ 1 ≤ m

Tactic:
]

Goal state after:
case pos
m : ℕ
hs : 1 ≤ m
⊢ 1 ≤ m
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv

Goal state before:
pp: s : ℂ
hs : s ≠ 0
h : ∀ (m : ℕ), s ≠ -↑m
this : HasDerivWithinAt (fun s ↦ Gamma (s + 1)) (Gamma s + s * deriv Gamma s) {0}ᶜ s
⊢ deriv (fun x ↦ Gamma (x + 1)) s = Gamma s + s * deriv Gamma s

Tactic:
]

Goal state after:
s : ℂ
hs : s ≠ 0
h : ∀ (m : ℕ), s ≠ -↑m
this : HasDerivWithinAt (fun s ↦ Gamma (s + 1)) (Gamma s + s * deriv Gamma s) {0}ᶜ s
⊢ deriv (fun x ↦ Gamma (x + 1)) s = Gamma s + s * deriv Gamma s
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deriv

Goal state before:
pp: s : ℝ
hs : ∀ (m : ℕ), s ≠ -↑m
⊢ ∀ (m : ℕ), ¬s = -↑m

Tactic:
exact hs

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun c u x ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), x ∈ Ioi 0 → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ f c u x
c x : ℝ
hc : 0 < c
u : ℝ
hx : 0 < x
⊢ rexp (-x) * x ^ (u - 1) = rexp (-c * x * (1 / c)) * x ^ (c * (u - 1) * (1 / c))

Tactic:
]

Goal state after:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun c u x ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), x ∈ Ioi 0 → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ f c u x
c x : ℝ
hc : 0 < c
u : ℝ
hx : 0 < x
⊢ rexp (-x) * x ^ (u - 1) = rexp (-c * x * (1 / c)) * x ^ (c * (u - 1) * (1 / c))
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: case refine_2.hg
b : ℝ
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
hf : f =O[𝓝[>] 0] fun x ↦ x ^ (-b)
s : ℝ
hs : b < s
d : ℝ
left✝ : d > 0
ε : ℝ
hε : 0 < ε
hε' : ∀ ⦃y : ℝ⦄, dist y 0 < ε → y ∈ Ioi 0 → ‖f y‖ ≤ d * ‖y ^ (-b)‖
⊢ IntervalIntegrable (fun t ↦ t ^ (s - b - 1)) volume 0 ε

Tactic:
]

Goal state after:
case refine_2.hg
b : ℝ
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
hf : f =O[𝓝[>] 0] fun x ↦ x ^ (-b)
s : ℝ
hs : b < s
d : ℝ
left✝ : d > 0
ε : ℝ
hε : 0 < ε
hε' : ∀ ⦃y : ℝ⦄, dist y 0 < ε → y ∈ Ioi 0 → ‖f y‖ ≤ d * ‖y ^ (-b)‖
⊢ IntervalIntegrable (fun t ↦ t ^ (s - b - 1)) volume 0 ε
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: case refine_2.h
b : ℝ
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
hf : f =O[𝓝[>] 0] fun x ↦ x ^ (-b)
s : ℝ
hs : b < s
d : ℝ
left✝ : d > 0
ε : ℝ
hε : 0 < ε
hε' : ∀ ⦃y : ℝ⦄, dist y 0 < ε → y ∈ Ioi 0 → ‖f y‖ ≤ d * ‖y ^ (-b)‖
t : ℝ
ht : t ∈ Ioo 0 ε
⊢ ‖f t‖ * ‖t ^ (s - 1)‖ ≤ d * t ^ (s - b - 1)

Tactic:
]

Goal state after:
case refine_2.h
b : ℝ
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
hf : f =O[𝓝[>] 0] fun x ↦ x ^ (-b)
s : ℝ
hs : b < s
d : ℝ
left✝ : d > 0
ε : ℝ
hε : 0 < ε
hε' : ∀ ⦃y : ℝ⦄, dist y 0 < ε → y ∈ Ioi 0 → ‖f y‖ ≤ d * ‖y ^ (-b)‖
t : ℝ
ht : t ∈ Ioo 0 ε
⊢ ‖f t‖ * ‖t ^ (s - 1)‖ ≤ d * t ^ (s - b - 1)
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: case e'_2.e'_4
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 : ∀ x ∈ uIcc 0 (π / 2), HasDerivAt (fun y ↦ ↑(cos y) ^ n) (-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)) x
x : ℝ
⊢ ↑(cos x) ^ n * Complex.cos (2 * z * ↑x) = ↑(cos x) ^ n * Complex.cos (2 * z * ↑x)

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: case refine_2.h
b : ℝ
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
hf : f =O[𝓝[>] 0] fun x ↦ x ^ (-b)
s : ℝ
hs : b < s
d : ℝ
left✝ : d > 0
ε : ℝ
hε : 0 < ε
hε' : ∀ ⦃y : ℝ⦄, dist y 0 < ε → y ∈ Ioi 0 → ‖f y‖ ≤ d * ‖y ^ (-b)‖
t : ℝ
ht : t ∈ Ioo 0 ε
⊢ t < ε

Tactic:
]

Goal state after:
case refine_2.h
b : ℝ
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
hf : f =O[𝓝[>] 0] fun x ↦ x ^ (-b)
s : ℝ
hs : b < s
d : ℝ
left✝ : d > 0
ε : ℝ
hε : 0 < ε
hε' : ∀ ⦃y : ℝ⦄, dist y 0 < ε → y ∈ Ioi 0 → ‖f y‖ ≤ d * ‖y ^ (-b)‖
t : ℝ
ht : t ∈ Ioo 0 ε
⊢ t < ε
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (fun t ↦ t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
f : ℂ → ℂ := fun z ↦ log (1 + z) - logTaylor (n + 1) z
f' : ℂ → ℂ := fun z ↦ (-z) ^ n * (1 + z)⁻¹
hderiv : ∀ t ∈ Set.Icc 0 1, HasDerivAt f (f' (0 + ↑t * z)) (0 + ↑t * z)
hcont : ContinuousOn (fun t ↦ f' (0 + ↑t * z)) (Set.Icc 0 1)
H : log (1 + z) - logTaylor (n + 1) z = z * ∫ (t : ℝ) in 0..1, (-(↑t * z)) ^ n * (1 + ↑t * z)⁻¹
t : ℝ
ht₀ : 0 < t
ht₁ : t ≤ 1
⊢ t ^ n * ‖(1 + ↑t * z)⁻¹‖ ≤ t ^ n * (1 - ‖z‖)⁻¹

Tactic:
]

Goal state after:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (fun t ↦ t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
f : ℂ → ℂ := fun z ↦ log (1 + z) - logTaylor (n + 1) z
f' : ℂ → ℂ := fun z ↦ (-z) ^ n * (1 + z)⁻¹
hderiv : ∀ t ∈ Set.Icc 0 1, HasDerivAt f (f' (0 + ↑t * z)) (0 + ↑t * z)
hcont : ContinuousOn (fun t ↦ f' (0 + ↑t * z)) (Set.Icc 0 1)
H : log (1 + z) - logTaylor (n + 1) z = z * ∫ (t : ℝ) in 0..1, (-(↑t * z)) ^ n * (1 + ↑t * z)⁻¹
t : ℝ
ht₀ : 0 < t
ht₁ : t ≤ 1
⊢ t ^ n * ‖(1 + ↑t * z)⁻¹‖ ≤ t ^ n * (1 - ‖z‖)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun c u x ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), x ∈ Ioi 0 → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
c u : ℝ
hc : 0 < c
hu : 0 < u
⊢ 0 < c

Tactic:
]

Goal state after:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun c u x ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), x ∈ Ioi 0 → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
c u : ℝ
hc : 0 < c
hu : 0 < u
⊢ 0 < c
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (fun t ↦ t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
f : ℂ → ℂ := fun z ↦ log (1 + z) - logTaylor (n + 1) z
f' : ℂ → ℂ := fun z ↦ (-z) ^ n * (1 + z)⁻¹
hderiv : ∀ t ∈ Set.Icc 0 1, HasDerivAt f (f' (0 + ↑t * z)) (0 + ↑t * z)
hcont : ContinuousOn (fun t ↦ f' (0 + ↑t * z)) (Set.Icc 0 1)
H : log (1 + z) - logTaylor (n + 1) z = z * ∫ (t : ℝ) in 0..1, (-(↑t * z)) ^ n * (1 + ↑t * z)⁻¹
⊢ (1 - ‖z‖)⁻¹ * ((1 ^ (n + 1) - 0 ^ (n + 1)) / (↑n + 1)) = (1 - ‖z‖)⁻¹ / (↑n + 1)

Tactic:
]

Goal state after:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
help : IntervalIntegrable (fun t ↦ t ^ n * (1 - ‖z‖)⁻¹) MeasureTheory.volume 0 1
f : ℂ → ℂ := fun z ↦ log (1 + z) - logTaylor (n + 1) z
f' : ℂ → ℂ := fun z ↦ (-z) ^ n * (1 + z)⁻¹
hderiv : ∀ t ∈ Set.Icc 0 1, HasDerivAt f (f' (0 + ↑t * z)) (0 + ↑t * z)
hcont : ContinuousOn (fun t ↦ f' (0 + ↑t * z)) (Set.Icc 0 1)
H : log (1 + z) - logTaylor (n + 1) z = z * ∫ (t : ℝ) in 0..1, (-(↑t * z)) ^ n * (1 + ↑t * z)⁻¹
⊢ (1 - ‖z‖)⁻¹ * ((1 ^ (n + 1) - 0 ^ (n + 1)) / (↑n + 1)) = (1 - ‖z‖)⁻¹ / (↑n + 1)
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: case refine_2.h
b : ℝ
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
hf : f =O[𝓝[>] 0] fun x ↦ x ^ (-b)
s : ℝ
hs : b < s
d : ℝ
left✝ : d > 0
ε : ℝ
hε : 0 < ε
t : ℝ
hε' : ‖f t‖ ≤ d * ‖t ^ (-b)‖
ht : t ∈ Ioo 0 ε
⊢ d * t ^ (-b + (s - 1)) = d * t ^ (s - b - 1)

Tactic:
]

Goal state after:
case refine_2.h
b : ℝ
f : ℝ → ℝ
hfc : AEStronglyMeasurable f (volume.restrict (Ioi 0))
hf : f =O[𝓝[>] 0] fun x ↦ x ^ (-b)
s : ℝ
hs : b < s
d : ℝ
left✝ : d > 0
ε : ℝ
hε : 0 < ε
t : ℝ
hε' : ‖f t‖ ≤ d * ‖t ^ (-b)‖
ht : t ∈ Ioo 0 ε
⊢ d * t ^ (-b + (s - 1)) = d * t ^ (s - b - 1)
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: n : ℕ
⊢ ∃ c, ∀ᶠ (x : ℂ) in 𝓝 0, ‖log (1 + x) - logTaylor (n + 1) x‖ ≤ c * ‖x ^ (n + 1)‖

Tactic:
]

Goal state after:
n : ℕ
⊢ ∃ c, ∀ᶠ (x : ℂ) in 𝓝 0, ‖log (1 + x) - logTaylor (n + 1) x‖ ≤ c * ‖x ^ (n + 1)‖
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: n : ℕ
z : ℂ
hz1 : ‖z‖ < 1
hz12 : ‖z‖ < 1 / 2
⊢ ‖log (1 + z) - logTaylor (n + 1) z‖ ≤ 2 / (↑n + 1) * ‖z ^ (n + 1)‖

Tactic:
]

Goal state after:
n : ℕ
z : ℂ
hz1 : ‖z‖ < 1
hz12 : ‖z‖ < 1 / 2
⊢ ‖log (1 + z) - logTaylor (n + 1) z‖ ≤ 2 / (↑n + 1) * ‖z ^ (n + 1)‖
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: n : ℕ
z : ℂ
hz1 : ‖z‖ < 1
hz12 : ‖z‖ < 1 / 2
⊢ 2⁻¹ ≤ 1 - ‖z‖

Tactic:
]

Goal state after:
n : ℕ
z : ℂ
hz1 : ‖z‖ < 1
hz12 : ‖z‖ < 1 / 2
⊢ 2⁻¹ ≤ 1 - ‖z‖
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: n : ℕ
z : ℂ
hz1 : ‖z‖ < 1
hz12 : ‖z‖ < 1 / 2
this : (1 - ‖z‖)⁻¹ ≤ 2
⊢ (1 - ‖z‖)⁻¹ / (↑n + 1) * ‖z‖ ^ (n + 1) ≤ 2 / (↑n + 1) * ‖z‖ ^ (n + 1)

Tactic:
]

Goal state after:
n : ℕ
z : ℂ
hz1 : ‖z‖ < 1
hz12 : ‖z‖ < 1 / 2
this : (1 - ‖z‖)⁻¹ ≤ 2
⊢ (1 - ‖z‖)⁻¹ / (↑n + 1) * ‖z‖ ^ (n + 1) ≤ 2 / (↑n + 1) * ‖z‖ ^ (n + 1)
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: z : ℂ
hz : ‖z‖ < 1
⊢ ‖log (1 + z) - z + z‖ ≤ ‖z‖ ^ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖

Tactic:
]

Goal state after:
z : ℂ
hz : ‖z‖ < 1
⊢ ‖log (1 + z) - z + z‖ ≤ ‖z‖ ^ 2 * (1 - ‖z‖)⁻¹ / 2 + ‖z‖
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: z : ℂ
hz : ‖z‖ ≤ 1 / 2
⊢ 1 ≤ 2 * (1 - ‖z‖)

pp: z : ℂ
hz : ‖z‖ ≤ 1 / 2
⊢ 0 < 1 - ‖z‖

Tactic:
]

Goal state after:
z : ℂ
hz : ‖z‖ ≤ 1 / 2
⊢ 1 ≤ 2 * (1 - ‖z‖)

z : ℂ
hz : ‖z‖ ≤ 1 / 2
⊢ 0 < 1 - ‖z‖
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: case e'_3
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 : ∀ x ∈ uIcc 0 (π / 2), HasDerivAt (fun y ↦ ↑(cos y) ^ n) (-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)) x
⊢ ∫ (x : ℝ) in 0..π / 2, ↑n / (2 * z) * (Complex.sin (2 * z * ↑x) * ↑(sin x) * ↑(cos x) ^ (n - 1)) =
    ∫ (x : ℝ) in 0..π / 2, -(-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1) * (Complex.sin (2 * z * ↑x) / (2 * z)))

Tactic:
]

Goal state after:
case e'_3
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
der1 : ∀ x ∈ uIcc 0 (π / 2), HasDerivAt (fun y ↦ ↑(cos y) ^ n) (-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1)) x
⊢ ∫ (x : ℝ) in 0..π / 2, ↑n / (2 * z) * (Complex.sin (2 * z * ↑x) * ↑(sin x) * ↑(cos x) ^ (n - 1)) =
    ∫ (x : ℝ) in 0..π / 2, -(-↑n * ↑(sin x) * ↑(cos x) ^ (n - 1) * (Complex.sin (2 * z * ↑x) / (2 * z)))
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: case c0
z : ℂ
hz : ‖z‖ ≤ 1 / 2
hz3 : (1 - ‖z‖)⁻¹ ≤ 2
⊢ 0 ≤ 1 - ‖z‖

Tactic:
]

Goal state after:
case c0
z : ℂ
hz : ‖z‖ ≤ 1 / 2
hz3 : (1 - ‖z‖)⁻¹ ≤ 2
⊢ 0 ≤ 1 - ‖z‖
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: a b : ℝ
f : ℝ → ℝ
s : ℝ
hfc : LocallyIntegrableOn f (Ioi 0) volume
hf_top : f =O[atTop] fun x ↦ x ^ (-a)
hs_top : s < a
hf_bot : f =O[𝓝[>] 0] fun x ↦ x ^ (-b)
hs_bot : b < s
c1 : ℝ
hc1 : 0 < c1
hc1' : IntegrableOn (fun t ↦ t ^ (s - 1) * f t) (Ioi c1) volume
c2 : ℝ
hc2 : 0 < c2
hc2' : IntegrableOn (fun t ↦ t ^ (s - 1) * f t) (Ioc 0 c2) volume
⊢ Ioi 0 = Ioi 0

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: case h₁
z : ℂ
hz : ‖z‖ ≤ 1 / 2
hz3 : (1 - ‖z‖)⁻¹ ≤ 2
⊢ ‖z‖ * ‖z‖ ≤ ‖z‖ * (1 / 2)

Tactic:
]

Goal state after:
case h₁
z : ℂ
hz : ‖z‖ ≤ 1 / 2
hz3 : (1 - ‖z‖)⁻¹ ≤ 2
⊢ ‖z‖ * ‖z‖ ≤ ‖z‖ * (1 / 2)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.BohrMollerup

Goal state before:
pp: s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun c u x ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), x ∈ Ioi 0 → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
c u : ℝ
hc : 0 < c
hu : 0 < u
A : ENNReal.ofReal (1 / c) ≠ 0
B : ENNReal.ofReal (1 / c) ≠ ∞
⊢ Integrable (fun x ↦ ‖f c u x‖ ^ (1 / c)) (volume.restrict (Ioi 0))

pp: s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun c u x ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), x ∈ Ioi 0 → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
c u : ℝ
hc : 0 < c
hu : 0 < u
A : ENNReal.ofReal (1 / c) ≠ 0
B : ENNReal.ofReal (1 / c) ≠ ∞
⊢ AEStronglyMeasurable (f c u) (volume.restrict (Ioi 0))

Tactic:
]

Goal state after:
s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun c u x ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), x ∈ Ioi 0 → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
c u : ℝ
hc : 0 < c
hu : 0 < u
A : ENNReal.ofReal (1 / c) ≠ 0
B : ENNReal.ofReal (1 / c) ≠ ∞
⊢ Integrable (fun x ↦ ‖f c u x‖ ^ (1 / c)) (volume.restrict (Ioi 0))

s t a b : ℝ
hs : 0 < s
ht : 0 < t
ha : 0 < a
hb : 0 < b
hab : a + b = 1
f : ℝ → ℝ → ℝ → ℝ := fun c u x ↦ rexp (-c * x) * x ^ (c * (u - 1))
e : (1 / a).HolderConjugate (1 / b)
hab' : b = 1 - a
hst : 0 < a * s + b * t
posf : ∀ (c u x : ℝ), x ∈ Ioi 0 → 0 ≤ f c u x
posf' : ∀ (c u : ℝ), ∀ᵐ (x : ℝ) ∂volume.restrict (Ioi 0), 0 ≤ f c u x
fpow : ∀ {c x : ℝ}, 0 < c → ∀ (u : ℝ), 0 < x → rexp (-x) * x ^ (u - 1) = f c u x ^ (1 / c)
c u : ℝ
hc : 0 < c
hu : 0 < u
A : ENNReal.ofReal (1 / c) ≠ 0
B : ENNReal.ofReal (1 / c) ≠ ∞
⊢ AEStronglyMeasurable (f c u) (volume.restrict (Ioi 0))
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: n : ℕ
z : ℂ
hz : ‖z‖ < 1
⊢ ‖log (1 + -z) - logTaylor (n + 1) (-z)‖ ≤ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / (↑n + 1)

Tactic:
]

Goal state after:
n : ℕ
z : ℂ
hz : ‖z‖ < 1
⊢ ‖log (1 + -z) - logTaylor (n + 1) (-z)‖ ≤ ‖z‖ ^ (n + 1) * (1 - ‖z‖)⁻¹ / (↑n + 1)
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: case e'_5
n : ℕ
z : ℂ
hz : ‖z‖ < 1
⊢ ‖z‖ = ‖z‖

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Complex.LogBounds

Goal state before:
pp: case e'_6
n : ℕ
z : ℂ
hz : ‖z‖ < 1
⊢ 1 - ‖z‖ = 1 - ‖z‖

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.MellinTransform

Goal state before:
pp: a b : ℝ
f : ℝ → ℝ
s : ℝ
hfc : LocallyIntegrableOn f (Ioi 0) volume
hf_top : f =O[atTop] fun x ↦ x ^ (-a)
hs_top : s < a
hf_bot : f =O[𝓝[>] 0] fun x ↦ x ^ (-b)
hs_bot : b < s
c1 : ℝ
hc1 : 0 < c1
hc1' : IntegrableOn (fun t ↦ t ^ (s - 1) * f t) (Ioi c1) volume
c2 : ℝ
hc2 : 0 < c2
hc2' : IntegrableOn (fun t ↦ t ^ (s - 1) * f t) (Ioc 0 c2) volume
this : Ioi 0 = Ioc 0 c2 ∪ Ioc c2 c1 ∪ Ioi c1
⊢ (IntegrableOn (fun t ↦ t ^ (s - 1) * f t) (Ioc 0 c2) volume ∧
      IntegrableOn (fun t ↦ t ^ (s - 1) * f t) (Ioc c2 c1) volume) ∧
    IntegrableOn (fun t ↦ t ^ (s - 1) * f t) (Ioi c1) volume

Tactic:
]

Goal state after:
a b : ℝ
f : ℝ → ℝ
s : ℝ
hfc : LocallyIntegrableOn f (Ioi 0) volume
hf_top : f =O[atTop] fun x ↦ x ^ (-a)
hs_top : s < a
hf_bot : f =O[𝓝[>] 0] fun x ↦ x ^ (-b)
hs_bot : b < s
c1 : ℝ
hc1 : 0 < c1
hc1' : IntegrableOn (fun t ↦ t ^ (s - 1) * f t) (Ioi c1) volume
c2 : ℝ
hc2 : 0 < c2
hc2' : IntegrableOn (fun t ↦ t ^ (s - 1) * f t) (Ioc 0 c2) volume
this : Ioi 0 = Ioc 0 c2 ∪ Ioc c2 c1 ∪ Ioi c1
⊢ (IntegrableOn (fun t ↦ t ^ (s - 1) * f t) (Ioc 0 c2) volume ∧
      IntegrableOn (fun t ↦ t ^ (s - 1) * f t) (Ioc c2 c1) volume) ∧
    IntegrableOn (fun t ↦ t ^ (s - 1) * f t) (Ioi c1) volume
Module: Mathlib.Analysis.SpecialFunctions.Trigonometric.EulerSineProd

Goal state before:
pp: case e'_9
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
a✝ : x ∈ uIcc 0 (π / 2)
c : HasDerivAt ((fun x ↦ x ^ (n - 1)) ∘ Complex.cos) (↑(n - 1) * Complex.cos ↑x ^ (n - 1 - 1) * -Complex.sin ↑x) ↑x
⊢ Complex.cos ↑x ^ n - (↑n - 1) * Complex.sin ↑x ^ 2 * Complex.cos ↑x ^ (n - 2) =
    Complex.cos ↑x * Complex.cos ↑x ^ (n - 1) -
      Complex.sin ↑x * (↑(n - 1) * Complex.cos ↑x ^ (n - 1 - 1) * Complex.sin ↑x)

Tactic:
]

Goal state after:
case e'_9
z : ℂ
n : ℕ
hn : 2 ≤ n
hz : z ≠ 0
x : ℝ
a✝ : x ∈ uIcc 0 (π / 2)
c : HasDerivAt ((fun x ↦ x ^ (n - 1)) ∘ Complex.cos) (↑(n - 1) * Complex.cos ↑x ^ (n - 1 - 1) * -Complex.sin ↑x) ↑x
⊢ Complex.cos ↑x ^ n - (↑n - 1) * Complex.sin ↑x ^ 2 * Complex.cos ↑x ^ (n - 2) =
    Complex.cos ↑x * Complex.cos ↑x ^ (n - 1) -
      Complex.sin ↑x * (↑(n - 1) * Complex.cos ↑x ^ (n - 1 - 1) * Complex.sin ↑x)