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

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
z : A := (conjSqrt x⁻¹ʳ) y
zpos : IsStrictlyPositive z
xinvpos : IsStrictlyPositive x⁻¹ʳ
hsp : IsStrictlyPositive (a • 1 + b • z)
h₁ : (a • 1 + b • z) ^ (-1) = cfc (fun r ↦ (a + b * r) ^ (-1)) z
h₂ : a • 1 + b • z ^ (-1) = cfc (fun r ↦ a + b * r ^ (-1)) z
⊢ (a • x + b • y)⁻¹ʳ = (a • x + b • y)⁻¹ʳ

Tactic:
]

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 : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hL : Tendsto f (𝓝[>] 0) (𝓝 L)
δ : ℝ
hδ : δ > 0
η : ℝ
hη : η > 0
hη_sub : ball 0 η ∩ Ioi 0 ⊆ {x | dist (f x) L < δ}
M : ℝ := max a b
hM_def : M = max a b
hM : 0 < M
t : ℝ
ht_pos : 0 < t
ht_bound : t ∈ Iio (η / M)
x : ℝ
hx : x ∈ uIoc (a * t) (b * t)
hx_pos : 0 < x
hx_lt_η : dist x 0 < η
this : ‖f x - L‖ < δ
⊢ ‖f x - L‖ ≤ δ

Tactic:
]

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
L : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hL : Tendsto f (𝓝[>] 0) (𝓝 L)
δ : ℝ
hδ : δ > 0
η : ℝ
hη : η > 0
hη_sub : ball 0 η ∩ Ioi 0 ⊆ {x | dist (f x) L < δ}
M : ℝ := max a b
hM_def : M = max a b
hM : 0 < M
t : ℝ
ht_pos : 0 < t
ht_bound : t ∈ Iio (η / M)
x : ℝ
hx : x ∈ uIoc (a * t) (b * t)
hx_pos : 0 < x
hx_lt_η : dist x 0 < η
this : ‖f x - L‖ < δ
⊢ ‖f x - L‖ ≤ δ
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
z : A := (conjSqrt x⁻¹ʳ) y
zpos : IsStrictlyPositive z
xinvpos : IsStrictlyPositive x⁻¹ʳ
hsp : IsStrictlyPositive (a • 1 + b • z)
h₁ : (a • 1 + b • z) ^ (-1) = cfc (fun r ↦ (a + b * r) ^ (-1)) z
h₂ : a • 1 + b • z ^ (-1) = cfc (fun r ↦ a + b * r ^ (-1)) z
⊢ (conjSqrt x⁻¹ʳ) (a • 1 + b • z)⁻¹ʳ = (conjSqrt x⁻¹ʳ) (a • 1 + b • z)⁻¹ʳ

Tactic:
]

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 : ℝ
R : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hR : Tendsto f atTop (𝓝 R)
δ : ℝ
hδ : δ > 0
hev : ∃ a, ∀ (b : ℝ), a ≤ b → dist (f b) R < δ
⊢ ∀ᶠ (t : ℝ) in atTop, ∀ x ∈ uIoc (a * t) (b * t), ‖f x - R‖ ≤ δ

Tactic:
]

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
R : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hR : Tendsto f atTop (𝓝 R)
δ : ℝ
hδ : δ > 0
hev : ∃ a, ∀ (b : ℝ), a ≤ b → dist (f b) R < δ
⊢ ∀ᶠ (t : ℝ) in atTop, ∀ x ∈ uIoc (a * t) (b * t), ‖f x - R‖ ≤ δ
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder

Goal state before:
pp: case h
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
z : A := (conjSqrt x⁻¹ʳ) y
zpos : IsStrictlyPositive z
xinvpos : IsStrictlyPositive x⁻¹ʳ
hsp : IsStrictlyPositive (a • 1 + b • z)
h₁ : (a • 1 + b • z) ^ (-1) = cfc (fun r ↦ (a + b * r) ^ (-1)) z
h₂ : a • 1 + b • z ^ (-1) = cfc (fun r ↦ a + b * r ^ (-1)) z
⊢ cfc (fun r ↦ (a + b * r) ^ (-1)) z ≤ cfc (fun r ↦ a + b * r ^ (-1)) z

Tactic:
]

Goal state after:
case h
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
z : A := (conjSqrt x⁻¹ʳ) y
zpos : IsStrictlyPositive z
xinvpos : IsStrictlyPositive x⁻¹ʳ
hsp : IsStrictlyPositive (a • 1 + b • z)
h₁ : (a • 1 + b • z) ^ (-1) = cfc (fun r ↦ (a + b * r) ^ (-1)) z
h₂ : a • 1 + b • z ^ (-1) = cfc (fun r ↦ a + b * r ^ (-1)) z
⊢ cfc (fun r ↦ (a + b * r) ^ (-1)) z ≤ cfc (fun r ↦ a + b * r ^ (-1)) z
Module: Mathlib.Analysis.SpecialFunctions.FrullaniIntegral

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
R : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hR : Tendsto f atTop (𝓝 R)
δ : ℝ
hδ : δ > 0
N : ℝ
hN : ∀ (b : ℝ), N ≤ b → dist (f b) R < δ
hm : 0 < min a b
t : ℝ
ht : max 1 (N / min a b) ≤ t
x : ℝ
hx : x ∈ uIoc (a * t) (b * t)
ht_pos : 0 < t
⊢ min (a * t) (b * t) = min (a * t) (b * t)

Tactic:
]

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 : ℝ
R : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hR : Tendsto f atTop (𝓝 R)
δ : ℝ
hδ : δ > 0
N : ℝ
hN : ∀ (b : ℝ), N ≤ b → dist (f b) R < δ
hm : 0 < min a b
t : ℝ
ht : max 1 (N / min a b) ≤ t
x : ℝ
hx : x ∈ uIoc (a * t) (b * t)
ht_pos : 0 < t
hNx : N ≤ x
hdist : ‖f x - R‖ < δ
⊢ ‖f x - R‖ ≤ δ

Tactic:
]

Goal state after:
E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℝ E
f : ℝ → E
a b : ℝ
R : E
inst✝ : CompleteSpace E
hf : LocallyIntegrableOn f (Ioi 0) volume
ha : 0 < a
hb : 0 < b
hR : Tendsto f atTop (𝓝 R)
δ : ℝ
hδ : δ > 0
N : ℝ
hN : ∀ (b : ℝ), N ≤ b → dist (f b) R < δ
hm : 0 < min a b
t : ℝ
ht : max 1 (N / min a b) ≤ t
x : ℝ
hx : x ∈ uIoc (a * t) (b * t)
ht_pos : 0 < t
hNx : N ≤ x
hdist : ‖f x - R‖ < δ
⊢ ‖f x - R‖ ≤ δ
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)
u : ℝ → E := fun x ↦ x⁻¹ • f x
hint : ∀ {p q : ℝ}, 0 < p → 0 < q → IntervalIntegrable u volume p q
ε r : ℝ
hε : 0 < ε
hr : 0 < r
⊢ (∫ (x : ℝ) in a * ε..a * r, x⁻¹ • f x) - ∫ (x : ℝ) in b * ε..b * r, x⁻¹ • f x =
    (∫ (y : ℝ) in a * ε..a * r, u y) - ∫ (y : ℝ) in b * ε..b * r, u y

Tactic:
]

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)
u : ℝ → E := fun x ↦ x⁻¹ • f x
hint : ∀ {p q : ℝ}, 0 < p → 0 < q → IntervalIntegrable u volume p q
hsplit :
  ∀ {ε r : ℝ},
    0 < ε →
      0 < r →
        ∫ (x : ℝ) in ε..r, x⁻¹ • (f (a * x) - f (b * x)) =
          (∫ (x : ℝ) in a * ε..b * ε, u x) - ∫ (x : ℝ) in a * r..b * r, u x
h_ev :
  (fun p ↦ ∫ (x : ℝ) in p.1..p.2, x⁻¹ • (f (a * x) - f (b * x))) =ᶠ[𝓝[>] 0 ×ˢ atTop] fun p ↦
    (∫ (x : ℝ) in a * p.1..b * p.1, u x) - ∫ (x : ℝ) in a * p.2..b * p.2, u x
⊢ Tendsto (fun p ↦ (∫ (x : ℝ) in a * p.1..b * p.1, u x) - ∫ (x : ℝ) in a * p.2..b * p.2, u x) (𝓝[>] 0 ×ˢ atTop)
    (𝓝 (log (b / a) • L - log (b / a) • R))

Tactic:
]

Goal state after:
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)
u : ℝ → E := fun x ↦ x⁻¹ • f x
hint : ∀ {p q : ℝ}, 0 < p → 0 < q → IntervalIntegrable u volume p q
hsplit :
  ∀ {ε r : ℝ},
    0 < ε →
      0 < r →
        ∫ (x : ℝ) in ε..r, x⁻¹ • (f (a * x) - f (b * x)) =
          (∫ (x : ℝ) in a * ε..b * ε, u x) - ∫ (x : ℝ) in a * r..b * r, u x
h_ev :
  (fun p ↦ ∫ (x : ℝ) in p.1..p.2, x⁻¹ • (f (a * x) - f (b * x))) =ᶠ[𝓝[>] 0 ×ˢ atTop] fun p ↦
    (∫ (x : ℝ) in a * p.1..b * p.1, u x) - ∫ (x : ℝ) in a * p.2..b * p.2, u x
⊢ Tendsto (fun p ↦ (∫ (x : ℝ) in a * p.1..b * p.1, u x) - ∫ (x : ℝ) in a * p.2..b * p.2, u x) (𝓝[>] 0 ×ˢ atTop)
    (𝓝 (log (b / a) • L - log (b / a) • R))
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
h_lim : Tendsto (fun p ↦ intervalIntegral g p.1 p.2 volume) ((𝓝[>] 0).curry atTop) (𝓝 (log (b / a) • (L - R)))
hg : g = fun x ↦ x⁻¹ • (f (a * x) - f (b * x))
⊢ ∀ ε > 0,
    ∃ δ > 0, ∀ ⦃x : ℝ⦄, x ∈ Ioi 0 → dist x 0 < δ → dist (∫ (x : ℝ) in Ioi x, g x ∂volume) (log (b / a) • (L - R)) < ε

Tactic:
]

Goal state after:
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
h_lim : Tendsto (fun p ↦ intervalIntegral g p.1 p.2 volume) ((𝓝[>] 0).curry atTop) (𝓝 (log (b / a) • (L - R)))
hg : g = fun x ↦ x⁻¹ • (f (a * x) - f (b * x))
⊢ ∀ ε > 0,
    ∃ δ > 0, ∀ ⦃x : ℝ⦄, x ∈ Ioi 0 → dist x 0 < δ → dist (∫ (x : ℝ) in Ioi x, g x ∂volume) (log (b / a) • (L - R)) < ε
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

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

Tactic:
]

Goal state after:
p t : ℝ
hp : p ≠ 1
ht : 0 < t
x : ℝ
⊢ t ^ (p + -1) - t ^ p * (t + x)⁻¹ = t ^ (p - 1) - t ^ p * (t + x)⁻¹
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

Goal state before:
pp: case inr
p t x : ℝ
hp : 0 < p
ht : 0 ≤ t
hx : 0 ≤ x
ht_pos : 0 < t
⊢ (t + x)⁻¹ ≤ t⁻¹

Tactic:
]

Goal state after:
case inr
p t x : ℝ
hp : 0 < p
ht : 0 ≤ t
hx : 0 ≤ x
ht_pos : 0 < t
⊢ (t + x)⁻¹ ≤ t⁻¹
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
z : A := (conjSqrt x⁻¹ʳ) y
zpos : IsStrictlyPositive z
xinvpos : IsStrictlyPositive x⁻¹ʳ
hsp : IsStrictlyPositive (a • 1 + b • z)
h₁ : (a • 1 + b • z) ^ (-1) = cfc (fun r ↦ (a + b * r) ^ (-1)) z
h₂ : a • 1 + b • z ^ (-1) = cfc (fun r ↦ a + b * r ^ (-1)) z
⊢ (conjSqrt x⁻¹ʳ) (a • 1 + b • z⁻¹ʳ) = (conjSqrt x⁻¹ʳ) (a • 1 + b • z⁻¹ʳ)

Tactic:
]

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
ht' : ¬t = 0
hxt : t + x ≠ 0
⊢ t ^ p * ((1 * (t + x) - t * 1) / (t * (t + x))) = t ^ p * ((t + x - t) / (t * (t + x)))

Tactic:
]

Goal state after:
p t x : ℝ
hp : p ∈ Ioo 0 1
ht : 0 ≤ t
hx : 0 ≤ x
ht' : ¬t = 0
hxt : t + x ≠ 0
⊢ t ^ p * ((1 * (t + x) - t * 1) / (t * (t + x))) = t ^ p * ((t + x - t) / (t * (t + x)))
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
h_lim :
  ∀ ε > 0, ∀ᶠ (x : ℝ × ℝ) in (𝓝[>] 0).curry atTop, dist (intervalIntegral g x.1 x.2 volume) (log (b / a) • (L - R)) < ε
hg : g = fun x ↦ x⁻¹ • (f (a * x) - f (b * x))
ε : ℝ
hε : ε > 0
⊢ ∃ δ > 0, ∀ ⦃x : ℝ⦄, x ∈ Ioi 0 → dist x 0 < δ → dist (∫ (x : ℝ) in Ioi x, g x ∂volume) (log (b / a) • (L - R)) < ε

Tactic:
]

Goal state after:
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
h_lim :
  ∀ ε > 0, ∀ᶠ (x : ℝ × ℝ) in (𝓝[>] 0).curry atTop, dist (intervalIntegral g x.1 x.2 volume) (log (b / a) • (L - R)) < ε
hg : g = fun x ↦ x⁻¹ • (f (a * x) - f (b * x))
ε : ℝ
hε : ε > 0
⊢ ∃ δ > 0, ∀ ⦃x : ℝ⦄, x ∈ Ioi 0 → dist x 0 < δ → dist (∫ (x : ℝ) in Ioi x, g x ∂volume) (log (b / a) • (L - R)) < ε
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
hxt : 0 ≤ x * t
⊢ (x * t) ^ (p - 1) * x / (x * t + x) = t ^ (p - 1) * 1 / (t + 1) * x ^ (p - 1)

Tactic:
]

Goal state after:
p t x : ℝ
hp : p ∈ Ioo 0 1
ht : 0 ≤ t
hx : 0 ≤ x
hxt : 0 ≤ x * t
⊢ (x * t) ^ (p - 1) * x / (x * t + x) = t ^ (p - 1) * 1 / (t + 1) * x ^ (p - 1)
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
hxt : 0 ≤ x * t
hx_zero : ¬x = 0
⊢ x ^ (p - 1) * t ^ (p - 1) * (x / (x * t + x)) = x ^ (p - 1) * t ^ (p - 1) * (x / (x * t + x))

Tactic:
]

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

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
xpos : IsStrictlyPositive x
y : A
ypos : IsStrictlyPositive y
a b : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
z : A := (conjSqrt x⁻¹ʳ) y
zpos : IsStrictlyPositive z
xinvpos : IsStrictlyPositive x⁻¹ʳ
hsp : IsStrictlyPositive (a • 1 + b • z)
h₁ : (a • 1 + b • z) ^ (-1) = cfc (fun r ↦ (a + b * r) ^ (-1)) z
h₂ : a • 1 + b • z ^ (-1) = cfc (fun r ↦ a + b * r ^ (-1)) z
⊢ a • x⁻¹ʳ + b • y⁻¹ʳ = a • x⁻¹ʳ + b • y⁻¹ʳ

Tactic:
]

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
hxt : 0 ≤ x * t
hx_zero : ¬x = 0
this : x * t + x = x * (t + 1)
⊢ x ^ (p - 1) * (t ^ (p - 1) * (1 / (t + 1))) = x ^ (p - 1) * (t ^ (p - 1) * (1 / (t + 1)))

Tactic:
]

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_lim :
  ∃ ε_1 > 0,
    ball 0 ε_1 ∩ Ioi 0 ⊆
      {x | ∀ᶠ (y : ℝ) in atTop, dist (intervalIntegral g (x, y).1 (x, y).2 volume) (log (b / a) • (L - R)) < ε / 2}
hε : ε > 0
⊢ ∃ δ > 0, ∀ ⦃x : ℝ⦄, x ∈ Ioi 0 → dist x 0 < δ → dist (∫ (x : ℝ) in Ioi x, g x ∂volume) (log (b / a) • (L - R)) < ε

Tactic:
]

Goal state after:
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_lim :
  ∃ ε_1 > 0,
    ball 0 ε_1 ∩ Ioi 0 ⊆
      {x | ∀ᶠ (y : ℝ) in atTop, dist (intervalIntegral g (x, y).1 (x, y).2 volume) (log (b / a) • (L - R)) < ε / 2}
hε : ε > 0
⊢ ∃ δ > 0, ∀ ⦃x : ℝ⦄, x ∈ Ioi 0 → dist x 0 < δ → dist (∫ (x : ℝ) in Ioi x, g x ∂volume) (log (b / a) • (L - R)) < ε
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
hxt : 0 ≤ x * t
hx_zero : ¬x = 0
⊢ t ^ (p - 1) * 1 / (t + 1) * x ^ (p - 1) = t ^ (p - 1) * 1 / (t + 1) * x ^ (p - 1)

Tactic:
]

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

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
t : ℝ
ht : 0 < t
this : ∀ x ∈ Ici 0, IsStrictlyPositive ((algebraMap ℝ A) t + x)
addl : A →ᵃ[ℝ] A := (AffineMap.toConstProdLinearMap ℝ).symm ((algebraMap ℝ A) t, LinearMap.id)
haddl : Function.Injective ⇑addl
⊢ Ici 0 = Ici 0

Tactic:
]

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

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

Tactic:
]

Goal state after:
p t x : ℝ
hp : 0 < p ∧ p < 1
ht : 0 ≤ t
hx : 0 ≤ x
hxt : 0 ≤ x * t
hx_zero : x = 0
⊢ (x * t) ^ (p - 1) * x / (x * t + x) = t ^ (p - 1) * 1 / (t + 1) * x ^ (p - 1)
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.RingInverseOrder

Goal state before:
pp: A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
t : ℝ
ht : 0 < t
this : ∀ x ∈ Ici 0, IsStrictlyPositive ((algebraMap ℝ A) t + x)
addl : A →ᵃ[ℝ] A := (AffineMap.toConstProdLinearMap ℝ).symm ((algebraMap ℝ A) t, LinearMap.id)
haddl : Function.Injective ⇑addl
hici : Ici 0 = ⇑addl ⁻¹' ⇑addl '' Ici 0
⊢ ConvexOn ℝ (⇑addl ⁻¹' ⇑addl '' Ici 0) (Ring.inverse ∘ ⇑addl)

Tactic:
]

Goal state after:
A : Type u_1
inst✝² : CStarAlgebra A
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
t : ℝ
ht : 0 < t
this : ∀ x ∈ Ici 0, IsStrictlyPositive ((algebraMap ℝ A) t + x)
addl : A →ᵃ[ℝ] A := (AffineMap.toConstProdLinearMap ℝ).symm ((algebraMap ℝ A) t, LinearMap.id)
haddl : Function.Injective ⇑addl
hici : Ici 0 = ⇑addl ⁻¹' ⇑addl '' Ici 0
⊢ ConvexOn ℝ (⇑addl ⁻¹' ⇑addl '' Ici 0) (Ring.inverse ∘ ⇑addl)
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: s : ℂ
hs : s ≠ 0
⊢ ↑π ^ (-(s / 2)) * (↑π)⁻¹ * (s / 2 * Gamma (s / 2)) = ↑π ^ (-s / 2) * Gamma (s / 2) * s / 2 / ↑π

Tactic:
]

Goal state after:
s : ℂ
hs : s ≠ 0
⊢ ↑π ^ (-(s / 2)) * (↑π)⁻¹ * (s / 2 * Gamma (s / 2)) = ↑π ^ (-s / 2) * Gamma (s / 2) * s / 2 / ↑π
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: s : ℂ
hs : s ≠ 0
⊢ 2 * ((2 * ↑π) ^ (-s) * (2 * ↑π)⁻¹) * (s * Gamma s) = 2 * (2 * ↑π) ^ (-s) * Gamma s * s / 2 / ↑π

Tactic:
]

Goal state after:
s : ℂ
hs : s ≠ 0
⊢ 2 * ((2 * ↑π) ^ (-s) * (2 * ↑π)⁻¹) * (s * Gamma s) = 2 * (2 * ↑π) ^ (-s) * Gamma s * s / 2 / ↑π
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: case hb
s : ℂ
hs : 0 < s.re
⊢ 0 < s.re / 2

Tactic:
]

Goal state after:
case hb
s : ℂ
hs : 0 < s.re
⊢ 0 < s.re / 2
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

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

Tactic:
]

Goal state after:
⊢ ↑π ^ (-1 / 2) * ↑π ^ (1 / 2) = 1
Module: Mathlib.Analysis.SpecialFunctions.Gamma.Deligne

Goal state before:
pp: ⊢ 2 * (2 * ↑π)⁻¹ * 1 = 1 / ↑π

Tactic:
]

Goal state after:
⊢ 2 * (2 * ↑π)⁻¹ * 1 = 1 / ↑π
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 < δ
⊢ dist (∫ (x : ℝ) in Ioi x, g x ∂volume) (log (b / a) • (L - R)) < ε

Tactic:
]

Goal state after:
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 < δ
⊢ dist (∫ (x : ℝ) in Ioi x, g x ∂volume) (log (b / a) • (L - R)) < ε
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) * x / (t + x) = t ^ (p - 1) * x / (t + x)

Tactic:
]

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
⊢ t ^ (p - 1) * x / t = t ^ (p - 1) / t * x

Tactic:
by ring

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

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

Tactic:
]

Goal state after:
case e_a
p t x : ℝ
hp : p ∈ Ioo 0 1
ht : 0 < t
hx : 0 ≤ x
⊢ t ^ (p - 1 - 1) = t ^ (p - 2)
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 / (t + x)

Tactic:
]

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 ring

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

Goal state before:
pp: ⊢ Tendsto (fun z ↦ z / 2) (𝓝[≠] 0) (𝓝 (0 / 2)) ∧ ∀ᶠ (n : ℂ) in 𝓝[≠] 0, n / 2 ∈ {0}ᶜ

Tactic:
]

Goal state after:
⊢ Tendsto (fun z ↦ z / 2) (𝓝[≠] 0) (𝓝 (0 / 2)) ∧ ∀ᶠ (n : ℂ) in 𝓝[≠] 0, n / 2 ∈ {0}ᶜ
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
⊢ 1 / 2 * (t ^ (p - 1) / t) = t ^ (p - 1) * (1 / 2 * 1 / t)

Tactic:
]

Goal state after:
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 1 ≤ t
this : p - 2 = p - 1 - 1
⊢ 1 / 2 * (t ^ (p - 1) / t) = t ^ (p - 1) * (1 / 2 * 1 / t)
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 * ↑π ^ (-0 / 2)))

Tactic:
]

Goal state after:
h : Tendsto (fun z ↦ z / 2 * Gamma (z / 2)) (𝓝[≠] 0) (𝓝 1)
⊢ Tendsto (fun s ↦ 2 * ↑π ^ (-s / 2)) (𝓝[≠] 0) (𝓝 (2 * ↑π ^ (-0 / 2)))
Module: Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation

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

Tactic:
]

Goal state after:
case hbc
p t : ℝ
hp : p ∈ Ioo 0 1
ht : 1 ≤ t
⊢ t + 1 ≤ 2 * t
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)) = t ^ (p - 1) * (1 / (t + 1))

Tactic:
]

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

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

Tactic:
]

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