mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: p t x : ℝ
hp : p ∈ Ioo 0 1
ht : 0 < t
hx : 0 ≤ x
⊢ t ^ (p - 1) / t * x = t ^ (p - 2) * x

Tactic:
by

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

Goal state before:
pp: ⊢ ∀ (x : ℂ), 2 * (2 * ↑π) ^ (-x) ≠ 0

Tactic:
by

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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
L R : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hL : Tendsto f (𝓝[>] 0) (𝓝 L)
hR : Tendsto f atTop (𝓝 R)
g : ℝ → E := fun x ↦ x⁻¹ • (f (a * x) - f (b * x))
hint : IntegrableOn g (Ioi 0) volume
hg : g = fun x ↦ x⁻¹ • (f (a * x) - f (b * x))
ε : ℝ
hε : ε > 0
δ : ℝ
hδ_pos : δ > 0
x : ℝ
hδ : ∀ᶠ (y : ℝ) in atTop, dist (intervalIntegral g x y volume) (log (b / a) • (L - R)) < ε / 2
hx : x ∈ Ioi 0
hdist : dist x 0 < δ
⊢ volume ≤ volume

Tactic:
by

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

Goal state before:
pp: ⊢ 2 * ↑π ≠ 0 ∨ ∀ (x : ℂ), -x ≠ 0

Tactic:
by

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

Goal state before:
pp: p t x : ℝ
hp : p ∈ Ioo 0 1
ht : 0 ≤ t
hx : 0 ≤ x
hx_zero : ¬x = 0
⊢ p.rpowIntegrand₀₁ t x = t ^ (p - 1) * x / (t + x)

Tactic:
by

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

Goal state before:
pp: ⊢ Differentiable ℂ fun s ↦ s.Gammaℂ⁻¹

Tactic:
by

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

Goal state before:
pp: p t x : ℝ
hp : p ∈ Ioo 0 1
ht : 0 ≤ t
hx : 0 ≤ x
hx_zero : ¬x = 0
⊢ t ^ (p - 1) * x / (t + x) ≤ t ^ (p - 1) * x / x

Tactic:
by

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

Goal state before:
pp: p t x : ℝ
hp : p ∈ Ioo 0 1
ht : 0 ≤ t
hx : 0 ≤ x
hx_zero : ¬x = 0
⊢ t ^ (p - 1) * x / x = t ^ (p - 1) * (x / x)

Tactic:
by

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

Goal state before:
pp: ⊢ 𝓝 0 = 𝓝 (0 / 2)

Tactic:
by

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

Goal state before:
pp: p t x : ℝ
hp : p ∈ Ioo 0 1
ht : 0 ≤ t
hx : 0 ≤ x
hx_zero : ¬x = 0
⊢ t ^ (p - 1) * (x / x) = t ^ (p - 1) * 1

Tactic:
by

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

Goal state before:
pp: p t x : ℝ
hp : p ∈ Ioo 0 1
ht : 0 ≤ t
hx : 0 ≤ x
hx_zero : ¬x = 0
⊢ t ^ (p - 1) * 1 = t ^ (p - 1)

Tactic:
by

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

Goal state before:
pp: p t x : ℝ
hp : p ∈ Ioo 0 1
ht : 0 ≤ t
hx : 0 ≤ x
⊢ p.rpowIntegrand₀₁ t x ≤ t ^ (p - 1)

Tactic:
by

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

Goal state before:
pp: p t : ℝ
hp : p ∈ Ioo 0 1
ht : 1 ≤ t
⊢ p - 2 = p - 1 - 1

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: p t : ℝ
hp : p ∈ Ioo 0 1
ht : 1 ≤ t
this : p - 2 = p - 1 - 1
⊢ 0 < t

Tactic:
by

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

Goal state before:
pp: h : Tendsto (fun z ↦ z / 2 * Gamma (z / 2)) (𝓝[≠] 0) (𝓝 1)
⊢ 𝓝 2 = 𝓝 (2 * ↑π ^ (-0 / 2))

Tactic:
by

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

Goal state before:
pp: p t : ℝ
hp : p ∈ Ioo 0 1
ht : 1 ≤ t
⊢ 1 / 2 * t ^ (p - 2) = t ^ (p - 1) * (1 / 2 * 1 / t)

Tactic:
by

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

Goal state before:
pp: p t : ℝ
hp : p ∈ Ioo 0 1
ht : 1 ≤ t
⊢ 0 < 2 * t

Tactic:
by

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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
L R : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hL : Tendsto f (𝓝[>] 0) (𝓝 L)
hR : Tendsto f atTop (𝓝 R)
hint : IntegrableOn (fun x ↦ x⁻¹ • (f (a * x) - f (b * x))) (Ioi 0) volume
⊢ ∫ (x : ℝ) in Ioi 0, x⁻¹ • (f (a * x) - f (b * x)) = log (b / a) • (L - R)

Tactic:
by

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

Goal state before:
pp: p t : ℝ
hp : p ∈ Ioo 0 1
ht : 1 ≤ t
⊢ 0 < t + 1

Tactic:
by

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

Goal state before:
pp: p t : ℝ
hp : p ∈ Ioo 0 1
ht : 1 ≤ t
⊢ t ^ (p - 1) * (1 / 2 * 1 / t) ≤ t ^ (p - 1) * (1 / (t + 1))

Tactic:
by

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

Goal state before:
pp: h : Tendsto (fun z ↦ z / 2 * Gamma (z / 2)) (𝓝[≠] 0) (𝓝 1)
⊢ ContinuousAt (fun s ↦ -s / 2) 0

Tactic:
by

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

Goal state before:
pp: p t : ℝ
hp : p ∈ Ioo 0 1
ht : 1 ≤ t
⊢ 0 ≤ t

Tactic:
by

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

Goal state before:
pp: h : Tendsto (fun z ↦ z / 2 * Gamma (z / 2)) (𝓝[≠] 0) (𝓝 1)
⊢ Tendsto (fun s ↦ 2 * ↑π ^ (-s / 2)) (𝓝[≠] 0) (𝓝 2)

Tactic:
by

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

Goal state before:
pp: p t : ℝ
hp : p ∈ Ioo 0 1
ht : 1 ≤ t
⊢ t ^ (p - 1) * (1 / (t + 1)) = p.rpowIntegrand₀₁ t 1

Tactic:
by

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

Goal state before:
pp: p t : ℝ
ht : 0 < t
x : ℝ
hx : x ∈ Ici 0
⊢ p.rpowIntegrand₀₁ t x = t ^ p * (t⁻¹ - t⁻¹ * (1 + x * t⁻¹)⁻¹)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: ⊢ eulerMascheroniSeq 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

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

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: n : ℕ
⊢ ↑n + 1 ≠ 0

Tactic:
by

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

Goal state before:
pp: p t : ℝ
ht : 0 < t
x : ℝ
hx : x ∈ Ici 0
⊢ t ^ p * (t⁻¹ - t⁻¹ * (1 + x * t⁻¹)⁻¹) = t ^ (p - 1) * (1 - (1 + x * t⁻¹)⁻¹)

Tactic:
by

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

Goal state before:
pp: p t : ℝ
ht : 0 < t
x : ℝ
hx : x ∈ Ici 0
⊢ t ^ (p - 1) * (1 - (1 + x * t⁻¹)⁻¹) = (fun x ↦ t ^ (p - 1) * p.rpowIntegrand₀₁ 1 (t⁻¹ • x)) x

Tactic:
by

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

Goal state before:
pp: ⊢ Tendsto (fun s ↦ s * s.Gammaℝ) (𝓝[≠] 0) (𝓝 2)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: ⊢ StrictMono eulerMascheroniSeq

Tactic:
by

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

Goal state before:
pp: p t : ℝ
ht : 0 < t
⊢ EqOn (p.rpowIntegrand₀₁ t) (fun x ↦ t ^ (p - 1) * p.rpowIntegrand₀₁ 1 (t⁻¹ • x)) (Ici 0)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: ⊢ eulerMascheroniSeq 6 = 49 / 20 - log 7

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: this : eulerMascheroniSeq 6 = 49 / 20 - log 7
⊢ 0 < 7

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: this : eulerMascheroniSeq 6 = 49 / 20 - log 7
⊢ 0 ≤ 49 / 20 - 1 / 2

Tactic:
by

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

Goal state before:
pp: s : ℂ
⊢ ↑π ^ (-s / 2) * Gamma (s / 2) * (↑π ^ (-(s + 1) / 2) * Gamma ((s + 1) / 2)) =
    ↑π ^ (-s / 2) * ↑π ^ (-(s + 1) / 2) * (Gamma (s / 2) * Gamma (s / 2 + 1 / 2))

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: ⊢ 1 / 2 < eulerMascheroniSeq 6

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: ⊢ eulerMascheroniSeq' 1 = 1

Tactic:
by

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

Goal state before:
pp: p x : ℝ
hp : p ∈ Ioo 0 1
hx : 0 ≤ x
⊢ IntegrableOn (fun x_1 ↦ p.rpowIntegrand₀₁ x_1 x) (Ioc 0 1) volume

Tactic:
by

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

Goal state before:
pp: s : ℂ
⊢ ↑π ^ (-s / 2) * ↑π ^ (-(s + 1) / 2) * (Gamma (s / 2) * Gamma (s / 2 + 1 / 2)) =
    2 ^ (1 - s) * (↑π ^ (-1 / 2 - s) * ↑π ^ (1 / 2)) * Gamma s

Tactic:
by

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

Goal state before:
pp: p x : ℝ
hp : p ∈ Ioo 0 1
hx : 0 ≤ x
t : ℝ
ht : 1 < t
⊢ 0 ≤ t

Tactic:
by

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

Goal state before:
pp: p x : ℝ
hp : p ∈ Ioo 0 1
hx : 0 ≤ x
t : ℝ
ht : 1 < t
⊢ 0 < t

Tactic:
by

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

Goal state before:
pp: p x : ℝ
hp : p ∈ Ioo 0 1
hx : 0 ≤ x
⊢ IntegrableOn (fun x_1 ↦ p.rpowIntegrand₀₁ x_1 x) (Ioi 1) volume

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

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

Tactic:
by

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

Goal state before:
pp: p x : ℝ
hp : p ∈ Ioo 0 1
hx : 0 ≤ x
⊢ IntegrableOn (fun x_1 ↦ p.rpowIntegrand₀₁ x_1 x) (Ioi 0) volume

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

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

Tactic:
by

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

Goal state before:
pp: s : ℂ
⊢ 2 ^ (1 - s) * (↑π ^ (-1 / 2 - s) * ↑π ^ (1 / 2)) * Gamma s = 2 * (↑2 ^ (-s) * ↑π ^ (-s)) * Gamma s

Tactic:
by

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

Goal state before:
pp: p x : ℝ
hp : p ∈ Ioo 0 1
hx✝ : 0 ≤ x
hx : 0 < x
this :
  ∫ (t : ℝ) in Ioi 0, ((fun x_1 ↦ p.rpowIntegrand₀₁ x_1 x) ∘ fun x_1 ↦ x * x_1) t * x =
    x ^ p * ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 1
⊢ ContinuousOn (fun x_1 ↦ x * x_1) (Ici 0)

Tactic:
by

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

Goal state before:
pp: s : ℂ
⊢ 2 * (↑2 ^ (-s) * ↑π ^ (-s)) * Gamma s = 2 * (2 * ↑π) ^ (-s) * Gamma s

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: ⊢ StrictAnti eulerMascheroniSeq'

Tactic:
by

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

Goal state before:
pp: s : ℂ
⊢ s.Gammaℝ * (s + 1).Gammaℝ = s.Gammaℂ

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: ⊢ eulerMascheroniSeq' 6 = 49 / 20 - log 6

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
⊢ 0 < 6

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: h1 : eulerMascheroniSeq' 6 = 49 / 20 - log 6
⊢ 0 < 107 / 60

Tactic:
by

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

Goal state before:
pp: s : ℂ
⊢ (1 - s).Gammaℝ * (1 + s).Gammaℝ =
    ↑π ^ ((s - 1) / 2) * ↑π ^ ((-1 - s) / 2) * (Gamma ((1 - s) / 2) * Gamma (1 - (1 - s) / 2))

Tactic:
by

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

Goal state before:
pp: s : ℂ
⊢ ↑π ^ ((s - 1) / 2) * ↑π ^ ((-1 - s) / 2) * (Gamma ((1 - s) / 2) * Gamma (1 - (1 - s) / 2)) =
    ↑π ^ ((s - 1) / 2) * ↑π ^ ((-1 - s) / 2) * ↑π ^ 1 / sin (↑π / 2 - ↑π * s / 2)

Tactic:
by

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

Goal state before:
pp: s : ℂ
⊢ ↑π ^ ((s - 1) / 2) * ↑π ^ ((-1 - s) / 2) * ↑π ^ 1 / sin (↑π / 2 - ↑π * s / 2) = (cos (↑π * s / 2))⁻¹

Tactic:
by

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

Goal state before:
pp: s : ℂ
hs : ∀ (n : ℕ), s ≠ -(2 * ↑n + 1)
⊢ (s + 1).Gammaℝ ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: ⊢ eulerMascheroniSeq' 6 < 2 / 3

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: m n r : ℕ
⊢ eulerMascheroniSeq r < eulerMascheroniSeq' r

Tactic:
by

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

Goal state before:
pp: s : ℂ
hs : ∀ (n : ℕ), s ≠ -(2 * ↑n + 1)
this : (s + 1).Gammaℝ ≠ 0
⊢ s.Gammaℝ / (1 - s).Gammaℝ = s.Gammaℝ * (s + 1).Gammaℝ / ((1 - s).Gammaℝ * (1 + s).Gammaℝ)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: m n : ℕ
⊢ eulerMascheroniSeq m < eulerMascheroniSeq' n

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: ⊢ Tendsto eulerMascheroniSeq atTop (𝓝 eulerMascheroniConstant)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: this : Tendsto (fun n ↦ eulerMascheroniSeq' n - eulerMascheroniSeq n) atTop (𝓝 0)
⊢ Tendsto eulerMascheroniSeq' atTop (𝓝 eulerMascheroniConstant)

Tactic:
by

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

Goal state before:
pp: s : ℂ
hs : ∀ (n : ℕ), s ≠ -(2 * ↑n + 1)
this : (s + 1).Gammaℝ ≠ 0
⊢ s.Gammaℝ * (s + 1).Gammaℝ / ((1 - s).Gammaℝ * (1 + s).Gammaℝ) = 2 * (2 * ↑π) ^ (-s) * Gamma s / (cos (↑π * s / 2))⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: this : Tendsto (fun x ↦ log (x + 1) - log x) atTop (𝓝 0)
⊢ Tendsto (fun n ↦ eulerMascheroniSeq' n - eulerMascheroniSeq n) atTop (𝓝 0)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: ⊢ Tendsto eulerMascheroniSeq' atTop (𝓝 eulerMascheroniConstant)

Tactic:
by

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

Goal state before:
pp: s : ℂ
hs : ∀ (n : ℕ), s ≠ -(2 * ↑n + 1)
this : (s + 1).Gammaℝ ≠ 0
⊢ 2 * (2 * ↑π) ^ (-s) * Gamma s / (cos (↑π * s / 2))⁻¹ = s.Gammaℂ * cos (↑π * s / 2)

Tactic:
by

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

Goal state before:
pp: s : ℂ
hs : ∀ (n : ℕ), s ≠ -(2 * ↑n + 1)
⊢ s.Gammaℝ / (1 - s).Gammaℝ = s.Gammaℂ * cos (↑π * s / 2)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: ⊢ Tendsto (fun n ↦ ↑(harmonic n) - log ↑n) atTop (𝓝 eulerMascheroniConstant)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: n : ℕ
⊢ eulerMascheroniSeq n < eulerMascheroniConstant

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.EulerMascheroni

Goal state before:
pp: n : ℕ
⊢ eulerMascheroniConstant < eulerMascheroniSeq' n

Tactic:
by

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

Goal state before:
pp: s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
⊢ s.Gammaℝ ≠ 0

Tactic:
by

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

Goal state before:
pp: s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h1 : s.Gammaℝ ≠ 0
⊢ ∀ (n : ℕ), s ≠ -(2 * ↑n + 1)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: n : ℕ
f : ℝ → ℝ := log ∘ Gamma
this : deriv (fun x ↦ log (Gamma x)) (↑n + 1) = -γ + ↑(harmonic n)
m : ℕ
⊢ ↑n + 1 ≠ -↑m

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: n : ℕ
f : ℝ → ℝ := log ∘ Gamma
this : deriv (fun x ↦ log (Gamma x)) (↑n + 1) = -γ + ↑(harmonic n)
⊢ Gamma (↑n + 1) ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: n : ℕ
f : ℝ → ℝ := log ∘ Gamma
this : deriv Gamma (↑n + 1) / ↑n ! = -γ + ↑(harmonic n)
⊢ ↑n ! ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: n : ℕ
f : ℝ → ℝ := log ∘ Gamma
this : deriv (log ∘ Gamma) (↑n + 1) = -γ + ↑(harmonic n)
⊢ deriv Gamma (↑n + 1) = ↑n ! * (-γ + ↑(harmonic n))

Tactic:
by

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

Goal state before:
pp: s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
⊢ (1 - s).Gammaℝ⁻¹ = s.Gammaℂ * cos (↑π * s / 2) * s.Gammaℝ⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: n : ℕ
f : ℝ → ℝ := log ∘ Gamma
hc : ConvexOn ℝ (Ioi 0) f
x : ℝ
hx : 0 < x
⊢ f (x + 1) = f x + log x

Tactic:
by

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

Goal state before:
pp: p x : ℝ
hp : p ∈ Ioo 0 1
hx✝ : 0 ≤ x
hx : 0 < x
this :
  ∫ (t : ℝ) in Ioi 0, ((fun x_1 ↦ p.rpowIntegrand₀₁ x_1 x) ∘ fun x_1 ↦ x * x_1) t * x =
    x ^ p * ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 1
⊢ ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t x = x ^ p * ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 1

Tactic:
by

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

Goal state before:
pp: s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s = 1
⊢ 2 - 1 = 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: n : ℕ
f : ℝ → ℝ := log ∘ Gamma
hc : ConvexOn ℝ (Ioi 0) f
h_rec : ∀ (x : ℝ), 0 < x → f (x + 1) = f x + log x
x : ℝ
hx : 0 < x
m : ℕ
⊢ -↑m < x

Tactic:
by

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

Goal state before:
pp: s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s = 1
⊢ (1 + 1) / 2 = 1

Tactic:
by

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

Goal state before:
pp: p x : ℝ
hp : p ∈ Ioo 0 1
hx : 0 ≤ x
⊢ ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t x = x ^ p * ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: n : ℕ
f : ℝ → ℝ := log ∘ Gamma
hc : ConvexOn ℝ (Ioi 0) f
h_rec : ∀ (x : ℝ), 0 < x → f (x + 1) = f x + log x
x : ℝ
hx : 0 < x
⊢ DifferentiableAt ℝ f x

Tactic:
by

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

Goal state before:
pp: p : ℝ
hp : p ∈ Ioo 0 1
⊢ -1 / (2 * (p - 1)) = 1 / 2 * -1 ^ (p - 1) / (p - 1)

Tactic:
by

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

Goal state before:
pp: p : ℝ
hp : 0 < p ∧ p < 1
⊢ p - 2 < -1

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: n : ℕ
f : ℝ → ℝ := log ∘ Gamma
hc : ConvexOn ℝ (Ioi 0) f
h_rec : ∀ (x : ℝ), 0 < x → f (x + 1) = f x + log x
hder : ∀ {x : ℝ}, 0 < x → DifferentiableAt ℝ f x
x : ℝ
hx : 0 < x
⊢ 0 < x

Tactic:
by

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

Goal state before:
pp: p : ℝ
hp : p ∈ Ioo 0 1
⊢ 1 / 2 * -1 ^ (p - 1) / (p - 1) = ∫ (t : ℝ) in Ioi 1, 1 / 2 * t ^ (p - 2)

Tactic:
by

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

Goal state before:
pp: case refine_1
p : ℝ
hp : p ∈ Ioo 0 1
⊢ IntegrableOn (fun t ↦ 1 / 2 * t ^ (p - 2)) (Ioi 1) volume

pp: case refine_2
p : ℝ
hp : p ∈ Ioo 0 1
⊢ IntegrableOn (fun t ↦ p.rpowIntegrand₀₁ t 1) (Ioi 1) volume

pp: case refine_3
p : ℝ
hp : p ∈ Ioo 0 1
⊢ ∀ x ∈ Ioi 1, 1 / 2 * x ^ (p - 2) ≤ p.rpowIntegrand₀₁ x 1

Tactic:
· refine Integrable.const_mul ?_ _
          push _ ∈ _ at hp
          exact integrableOn_Ioi_rpow_of_lt (by linarith) zero_lt_one

Goal state after:
case refine_2
p : ℝ
hp : p ∈ Ioo 0 1
⊢ IntegrableOn (fun t ↦ p.rpowIntegrand₀₁ t 1) (Ioi 1) volume

case refine_3
p : ℝ
hp : p ∈ Ioo 0 1
⊢ ∀ x ∈ Ioi 1, 1 / 2 * x ^ (p - 2) ≤ p.rpowIntegrand₀₁ x 1
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: n : ℕ
f : ℝ → ℝ := log ∘ Gamma
hc : ConvexOn ℝ (Ioi 0) f
h_rec : ∀ (x : ℝ), 0 < x → f (x + 1) = f x + log x
hder : ∀ {x : ℝ}, 0 < x → DifferentiableAt ℝ f x
x : ℝ
hx : 0 < x
⊢ deriv f (x + 1) = deriv f x + 1 / x

Tactic:
by

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

Goal state before:
pp: p : ℝ
hp : p ∈ Ioo 0 1
⊢ ∫ (t : ℝ) in Ioi 1, 1 / 2 * t ^ (p - 2) ≤ ∫ (t : ℝ) in Ioi 1, p.rpowIntegrand₀₁ t 1

Tactic:
by

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

Goal state before:
pp: p : ℝ
hp : p ∈ Ioo 0 1
⊢ ∫ (t : ℝ) in Ioi 1, p.rpowIntegrand₀₁ t 1 ≤ ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 1

Tactic:
by

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

Goal state before:
pp: p : ℝ
hp : p ∈ Ioo 0 1
⊢ 0 < -1 / (2 * (p - 1))

Tactic:
by

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

Goal state before:
pp: p x : ℝ
hx : 0 ≤ x
hx_zero : x = 0
hp : 0 < p ∧ p < 1
⊢ ?m.78 ≠ 0

Tactic:
by

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

Goal state before:
pp: s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s - 1 ≠ 0
n : ℕ
⊢ s - 1 ≠ -↑n

Tactic:
by

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

Goal state before:
pp: s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s - 1 ≠ 0
h' : ∀ (n : ℕ), s - 1 ≠ -↑n
⊢ 2 - s = 1 - (s - 1)

Tactic:
by

Goal state after:
Module: Mathlib.NumberTheory.Harmonic.GammaDeriv

Goal state before:
pp: n✝ : ℕ
f : ℝ → ℝ := log ∘ Gamma
hc : ConvexOn ℝ (Ioi 0) f
h_rec : ∀ (x : ℝ), 0 < x → f (x + 1) = f x + log x
hder : ∀ {x : ℝ}, 0 < x → DifferentiableAt ℝ f x
hder_rec : ∀ (x : ℝ), 0 < x → deriv f (x + 1) = deriv f x + 1 / x
n : ℕ
hn : deriv f (↑n + 1) = deriv f 1 + ↑(harmonic n)
⊢ 0 < ↑n + 1

Tactic:
by

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

Goal state before:
pp: p x : ℝ
hp : p ∈ Ioo 0 1
hx : 0 ≤ x
⊢ x ^ p = (∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 1)⁻¹ * ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t x

Tactic:
by

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

Goal state before:
pp: p : ℝ
hp : p ∈ Ioo 0 1
⊢ 0 ≤ (∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t 1)⁻¹

Tactic:
by

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

Goal state before:
pp: s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s - 1 ≠ 0
h' : ∀ (n : ℕ), s - 1 ≠ -↑n
⊢ s.Gammaℂ = (s - 1 + 1).Gammaℂ

Tactic:
by

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

Goal state before:
pp: s : ℂ
hs : ∀ (n : ℕ), s ≠ -↑n
h : s - 1 ≠ 0
h' : ∀ (n : ℕ), s - 1 ≠ -↑n
⊢ s + 1 = s - 1 + 2

Tactic:
by

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

Goal state before:
pp: p : ℝ
hp : p ∈ Ioo 0 1
⊢ ∃ μ,
    ∀ x ∈ Ici 0,
      IntegrableOn (fun t ↦ p.rpowIntegrand₀₁ t x) (Ioi 0) μ ∧ x ^ p = ∫ (t : ℝ) in Ioi 0, p.rpowIntegrand₀₁ t x ∂μ

Tactic:
by

Goal state after: