mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
hf : MeromorphicOn f (sphere c |R|)
t₀ : ∀ (u : ↑(sphere c |R|)), meromorphicOrderAt f ↑u ≠ ⊤
g : ℂ → E
h₁g : AnalyticOnNhd ℂ g (sphere c |R|)
h₂g : ∀ (u : ↑(sphere c |R|)), g ↑u ≠ 0
h₃g : f =ᶠ[codiscreteWithin (sphere c |R|)] (∏ᶠ (u : ℂ), (fun x ↦ x - u) ^ (divisor f (sphere c |R|)) u) • g
h₄g :
  (fun x ↦ log ‖f x‖) =ᶠ[codiscreteWithin (sphere c |R|)]
    (∑ᶠ (u : ℂ), fun x ↦ ↑((divisor f (sphere c |R|)) u) * log ‖x - u‖) + fun x ↦ log ‖g x‖
i : ℂ
⊢ [[0, 2 * π]] ⊆ Set.univ

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
hre : SuperpolynomialDecay atTop expR fun x ↦ ‖f ↑x‖
C : ℝ
hC : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
g : ℕ → ℂ → E := fun n z ↦ cexp z ^ n • f z
n : ℕ
z : ℂ
⊢ ‖g n z‖ = expR z.re ^ n * ‖f z‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: b : ℝ
⊢ ∫ (s : ℝ) in 0..b, log s = b * log b - b

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: ⊢ ∫ (x : ℝ) in 0..π, log 4 + 2 * log (sin x) = (∫ (x : ℝ) in 0..π, log 4) + 2 * ∫ (x : ℝ) in 0..π, log (sin x)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: ⊢ 4 = 2 * 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: ⊢ (∫ (x : ℝ) in 0..π, log 4) + 2 * ∫ (x : ℝ) in 0..π, log (sin x) = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
⊢ ∫ (s : ℝ) in a..b, log s = b * log b - a * log a - b + a

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: ⊢ ∫ (x : ℝ) in 0..2 * π, log (4 * sin (x / 2) ^ 2) / 2 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a : ℂ
h : ‖a‖ = 1
⊢ ∃ ζ, a⁻¹ = circleMap 0 1 ζ

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
⊢ ∫ (x : ℝ) in a..b, sin x = cos a - cos b

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a : ℂ
h : ‖a‖ = 1
ζ : ℝ
hζ : a⁻¹ = circleMap 0 1 ζ
⊢ ∫ (x : ℝ) in 0..2 * π, log ‖circleMap 0 1 x - a‖ =
    ∫ (x : ℝ) in 0..2 * π, log ‖circleMap 0 1 ζ * (circleMap 0 1 x - a)‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a : ℂ
h : ‖a‖ = 1
ζ : ℝ
hζ : a⁻¹ = circleMap 0 1 ζ
⊢ ∫ (x : ℝ) in 0..2 * π, log ‖circleMap 0 1 ζ * (circleMap 0 1 x - a)‖ =
    ∫ (x : ℝ) in 0..2 * π, log ‖circleMap 0 1 (ζ + x) - circleMap 0 1 ζ * a‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a : ℂ
h : ‖a‖ = 1
ζ : ℝ
hζ : a⁻¹ = circleMap 0 1 ζ
⊢ a ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a : ℂ
h : ‖a‖ = 1
ζ : ℝ
hζ : a⁻¹ = circleMap 0 1 ζ
⊢ ∫ (x : ℝ) in 0..2 * π, log ‖circleMap 0 1 (ζ + x) - circleMap 0 1 ζ * a‖ =
    ∫ (x : ℝ) in 0..2 * π, log ‖circleMap 0 1 (ζ + x) - 1‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
⊢ ∫ (x : ℝ) in a..b, cos x = sin b - sin a

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a : ℂ
h : ‖a‖ = 1
ζ : ℝ
hζ : a⁻¹ = circleMap 0 1 ζ
x : ℝ
⊢ (fun x ↦ log ‖circleMap 0 1 x - 1‖) (x + 2 * π) = (fun x ↦ log ‖circleMap 0 1 x - 1‖) x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: z : ℂ
hz : z ≠ 0
a b : ℝ
⊢ Continuous fun y ↦ Complex.cos (z * ↑y)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a : ℂ
h : ‖a‖ = 1
ζ : ℝ
hζ : a⁻¹ = circleMap 0 1 ζ
⊢ ∫ (x : ℝ) in 0..2 * π, log ‖circleMap 0 1 (ζ + x) - 1‖ = ∫ (x : ℝ) in 0..2 * π, log ‖circleMap 0 1 x - 1‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a : ℂ
h : ‖a‖ = 1
ζ : ℝ
hζ : a⁻¹ = circleMap 0 1 ζ
x : ℝ
hx : x ∈ [[0, 2 * π]]
⊢ (fun x ↦ log ‖circleMap 0 1 x - 1‖) x = (fun x ↦ log (4 * sin (x / 2) ^ 2) / 2) x

Tactic:
simp only

Goal state after:
a : ℂ
h : ‖a‖ = 1
ζ : ℝ
hζ : a⁻¹ = circleMap 0 1 ζ
x : ℝ
hx : x ∈ [[0, 2 * π]]
⊢ log ‖circleMap 0 1 x - 1‖ = log (4 * sin (x / 2) ^ 2) / 2
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
hre : SuperpolynomialDecay atTop expR fun x ↦ ‖f ↑x‖
C : ℝ
hC : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
g : ℕ → ℂ → E := fun n z ↦ cexp z ^ n • f z
hg : ∀ (n : ℕ) (z : ℂ), ‖g n z‖ = expR z.re ^ n * ‖f z‖
z : ℂ
hz : 0 < z.re
H : ∀ (n : ℕ), ‖g n z‖ ≤ C
⊢ f z = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a : ℂ
h : ‖a‖ = 1
ζ : ℝ
hζ : a⁻¹ = circleMap 0 1 ζ
x : ℝ
hx : x ∈ [[0, 2 * π]]
⊢ Complex.normSq (circleMap 0 1 x - 1) = (cos x - 1) * (cos x - 1) + sin x * sin x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a : ℂ
h : ‖a‖ = 1
ζ : ℝ
hζ : a⁻¹ = circleMap 0 1 ζ
x : ℝ
hx : x ∈ [[0, 2 * π]]
⊢ (cos x - 1) * (cos x - 1) + sin x * sin x = sin x ^ 2 + cos x ^ 2 + 1 - 2 * cos x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: z : ℂ
hz : z ≠ 0
a b : ℝ
⊢ ∫ (x : ℝ) in a..b, Complex.cos (z * ↑x) = Complex.sin (z * ↑b) / z - Complex.sin (z * ↑a) / z

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a : ℂ
h : ‖a‖ = 1
ζ : ℝ
hζ : a⁻¹ = circleMap 0 1 ζ
x : ℝ
hx : x ∈ [[0, 2 * π]]
⊢ sin x ^ 2 + cos x ^ 2 + 1 - 2 * cos x = 2 - 2 * cos x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
⊢ ∫ (x : ℝ) in a..b, cos x ^ 2 - sin x ^ 2 = sin b * cos b - sin a * cos a

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a : ℂ
h : ‖a‖ = 1
ζ : ℝ
hζ : a⁻¹ = circleMap 0 1 ζ
x : ℝ
hx : x ∈ [[0, 2 * π]]
⊢ 2 - 2 * cos x = 2 - 2 * cos (2 * (x / 2))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
⊢ ∫ (x : ℝ) in a..b, 1 / (1 + x ^ 2) = arctan b - arctan a

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
⊢ ∫ (x : ℝ) in a..b, (1 + x ^ 2)⁻¹ = arctan b - arctan a

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a : ℂ
h : ‖a‖ = 1
ζ : ℝ
hζ : a⁻¹ = circleMap 0 1 ζ
x : ℝ
hx : x ∈ [[0, 2 * π]]
⊢ 2 - 2 * cos (2 * (x / 2)) = 4 - 4 * cos (x / 2) ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b c : ℝ
hc : c ≠ 0
⊢ ∫ (x : ℝ) in a..b, (c ^ 2 + x ^ 2)⁻¹ = ∫ (x : ℝ) in a..b, (c ^ 2)⁻¹ * (1 + (x / c) ^ 2)⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b c : ℝ
hc : c ≠ 0
⊢ ∫ (x : ℝ) in a..b, (c ^ 2)⁻¹ * (1 + (x / c) ^ 2)⁻¹ = c⁻¹ * (arctan (b / c) - arctan (a / c))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a : ℂ
h : ‖a‖ = 1
ζ : ℝ
hζ : a⁻¹ = circleMap 0 1 ζ
x : ℝ
hx : x ∈ [[0, 2 * π]]
⊢ 4 - 4 * cos (x / 2) ^ 2 = 4 * sin (x / 2) ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:

Tactic:
Complex.normSq (circleMap 0 1 x - 1)
    _ = (cos x - 1) * (cos x - 1) + sin x * sin x := by
      simp [circleMap, Complex.normSq_apply]
    _ = sin x ^ 2 + cos x ^ 2 + 1 - 2 * cos x := by
      ring
    _ = 2 - 2 * cos x := by
      rw [sin_sq_add_cos_sq]
      norm_num
    _ = 2 - 2 * cos (2 * (x / 2)) := by
      rw [← mul_div_assoc]
      simp
    _ = 4 - 4 * cos (x / 2) ^ 2 := by
      rw [cos_two_mul]
      ring
    _ = 4 * sin (x / 2) ^ 2 := by
      nth_rw 1 [← mul_one 4, ← sin_sq_add_cos_sq (x / 2)]
      ring

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b c : ℝ
⊢ ∫ (x : ℝ) in a..b, c / (c ^ 2 + x ^ 2) = ∫ (x : ℝ) in a..b, c * (c ^ 2 + x ^ 2)⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a : ℂ
h : ‖a‖ = 1
ζ : ℝ
hζ : a⁻¹ = circleMap 0 1 ζ
⊢ ∫ (x : ℝ) in 0..2 * π, log ‖circleMap 0 1 x - 1‖ = ∫ (x : ℝ) in 0..2 * π, log (4 * sin (x / 2) ^ 2) / 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a : ℂ
h : ‖a‖ = 1
⊢ circleAverage (fun x ↦ log ‖x - a‖) 0 1 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a : ℂ
h : 1 < ‖a‖
x : ℂ
hx : x ∈ closedBall 0 |1|
⊢ AnalyticAt ℂ (fun x ↦ x - a) x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b c : ℝ
⊢ ∫ (x : ℝ) in a..b, c * (c ^ 2 + x ^ 2)⁻¹ = arctan (b / c) - arctan (a / c)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a : ℂ
h : 1 < ‖a‖
⊢ circleAverage (fun x ↦ log ‖x - a‖) 0 1 = log ‖a‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
ha : 1 < a
hb : 1 < b
x✝¹ : ℝ
x✝ : x✝¹ ∈ [[a, b]]
⊢ 1 < x✝¹

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
ha : 1 < a
hb : 1 < b
⊢ ∫ (t : ℝ) in a..b, t⁻¹ / log t = log (log b) - log (log a)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
ha : 1 < a
hb : 1 < b
this : ∫ (t : ℝ) in a..b, deriv (fun t ↦ (log t)⁻¹) t = (log b)⁻¹ - (log a)⁻¹
⊢ ∫ (t : ℝ) in a..b, t⁻¹ / log t ^ 2 = (log a)⁻¹ - (log b)⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
ha : 1 < a
hb : 1 < b
this : ContinuousOn (fun x ↦ -x⁻¹ * (log x)⁻¹ ^ 2) [[a, b]]
⊢ ContinuousOn (deriv fun t ↦ (log t)⁻¹) [[a, b]]

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
hf : MeromorphicOn f (sphere c |R|)
t₀ : ¬∀ (u : ↑(sphere c |R|)), meromorphicOrderAt f ↑u ≠ ⊤
⊢ 1 < Module.rank ℝ ℂ

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
ha : 1 < a
hb : 1 < b
⊢ ∫ (t : ℝ) in a..b, t⁻¹ / log t ^ 2 = (log a)⁻¹ - (log b)⁻¹

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
t : ℂ
ht : t ≠ -1
⊢ t + 1 ≠ 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
hf : MeromorphicOn f (sphere c |R|)
t₀ : ∀ (u : ↑(sphere c |R|)), meromorphicOrderAt f ↑u = ⊤
⊢ (fun x ↦ log ‖f x‖) =ᶠ[codiscreteWithin (sphere c |R|)] 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
hf : MeromorphicOn f (sphere c |R|)
⊢ CircleIntegrable (fun x ↦ log ‖f x‖) c R

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a : ℂ
⊢ circleAverage (fun x ↦ log ‖x - a‖) 0 1 = log⁺ ‖a‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
a✝ : x ∈ [[a, b]]
⊢ HasDerivAt (fun y ↦ 1 + y ^ 2) (2 * ↑x) ↑x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
hf : MeromorphicOn f (sphere c R)
hR : 0 ≤ R
⊢ CircleIntegrable (fun x ↦ log ‖f x‖) c R

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a : ℂ
⊢ (fun x ↦ log ‖x + a‖) = fun x ↦ log ‖x - -a‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a : ℂ
⊢ circleAverage (fun x ↦ log ‖x + a‖) 0 1 = log⁺ ‖a‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
x : ℝ
a✝ : x ∈ [[a, b]]
f : HasDerivAt (fun y ↦ 1 + y ^ 2) (2 * ↑x) ↑x
⊢ ∀ {z : ℂ}, 0 < z.re → HasDerivAt (fun z ↦ z ^ (t + 1) / (2 * (t + 1))) (z ^ t / 2) z

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
hf : MeromorphicOn f (sphere c |R|)
⊢ CircleIntegrable (fun x ↦ log⁺ ‖f x‖) c R

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a c : ℂ
R : ℝ
hR : R ≠ 0
⊢ circleAverage (fun x ↦ log ‖x - a‖) c R = circleAverage (fun z ↦ log ‖↑R * (z + ↑R⁻¹ * (c - a))‖) 0 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
hf : MeromorphicOn f (sphere c R)
hR : 0 ≤ R
⊢ CircleIntegrable (fun x ↦ log⁺ ‖f x‖) c R

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
t : ℂ
ht : t ≠ -1
this : t + 1 ≠ 0
⊢ Continuous fun x ↦ 1 + ↑x ^ 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
t : ℂ
ht : t ≠ -1
⊢ ∫ (x : ℝ) in a..b, ↑x * (1 + ↑x ^ 2) ^ t =
    (1 + ↑b ^ 2) ^ (t + 1) / (2 * (t + 1)) - (1 + ↑a ^ 2) ^ (t + 1) / (2 * (t + 1))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b t : ℝ
ht : t ≠ -1
⊢ ∀ (x s : ℝ), ↑((1 + x ^ 2) ^ s) = (1 + ↑x ^ 2) ^ ↑s

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a c : ℂ
R : ℝ
hR : R ≠ 0
⊢ {z | ‖z + ↑R⁻¹ * (c - a)‖ ≠ 0} ∈ codiscreteWithin (sphere 0 |1|)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a c : ℂ
R : ℝ
hR : R ≠ 0
⊢ circleAverage (fun z ↦ log ‖↑R * (z + ↑R⁻¹ * (c - a))‖) 0 1 =
    circleAverage (fun z ↦ log ‖R‖ + log ‖z + ↑R⁻¹ * (c - a)‖) 0 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.PhragmenLindelof

Goal state before:
pp: case refine_1
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
hre : SuperpolynomialDecay atTop expR fun x ↦ ‖f ↑x‖
C : ℝ
hC : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
g : ℕ → ℂ → E := fun n z ↦ cexp z ^ n • f z
hg : ∀ (n : ℕ) (z : ℂ), ‖g n z‖ = expR z.re ^ n * ‖f z‖
z : ℂ
hz : 0 < z.re
n : ℕ
⊢ ∃ c < 2, ∃ B, g n =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)

pp: case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
hre : SuperpolynomialDecay atTop expR fun x ↦ ‖f ↑x‖
C : ℝ
hC : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
g : ℕ → ℂ → E := fun n z ↦ cexp z ^ n • f z
hg : ∀ (n : ℕ) (z : ℂ), ‖g n z‖ = expR z.re ^ n * ‖f z‖
z : ℂ
hz : 0 < z.re
n : ℕ
⊢ Tendsto (fun x ↦ g n ↑x) atTop (𝓝 0)

pp: case refine_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
hre : SuperpolynomialDecay atTop expR fun x ↦ ‖f ↑x‖
C : ℝ
hC : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
g : ℕ → ℂ → E := fun n z ↦ cexp z ^ n • f z
hg : ∀ (n : ℕ) (z : ℂ), ‖g n z‖ = expR z.re ^ n * ‖f z‖
z : ℂ
hz : 0 < z.re
n : ℕ
y : ℝ
⊢ ‖g n (↑y * I)‖ ≤ C

Tactic:
· rcases hexp with ⟨c, hc, B, hO⟩
    refine ⟨max c 1, max_lt hc one_lt_two, n + max B 0, .of_norm_left ?_⟩
    simp only [hg]
    refine ((isBigO_refl (fun z : ℂ => expR z.re ^ n) _).mul hO.norm_left).trans (.of_bound' ?_)
    filter_upwards [(eventually_cobounded_le_norm 1).filter_mono inf_le_left] with z hz
    simp only [← Real.exp_nat_mul, ← Real.exp_add, Real.norm_eq_abs, Real.abs_exp, add_mul]
    gcongr
    · calc
        z.re ≤ ‖z‖ := re_le_norm _
        _ = ‖z‖ ^ (1 : ℝ) := (Real.rpow_one _).symm
        _ ≤ ‖z‖ ^ max c 1 := Real.rpow_le_rpow_of_exponent_le hz (le_max_right _ _)
    exacts [le_max_left _ _, le_max_left _ _]

Goal state after:
case refine_2
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
hre : SuperpolynomialDecay atTop expR fun x ↦ ‖f ↑x‖
C : ℝ
hC : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
g : ℕ → ℂ → E := fun n z ↦ cexp z ^ n • f z
hg : ∀ (n : ℕ) (z : ℂ), ‖g n z‖ = expR z.re ^ n * ‖f z‖
z : ℂ
hz : 0 < z.re
n : ℕ
⊢ Tendsto (fun x ↦ g n ↑x) atTop (𝓝 0)

case refine_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
hd : DiffContOnCl ℂ f {z | 0 < z.re}
hexp : ∃ c < 2, ∃ B, f =O[cobounded ℂ ⊓ 𝓟 {z | 0 < z.re}] fun z ↦ expR (B * ‖z‖ ^ c)
hre : SuperpolynomialDecay atTop expR fun x ↦ ‖f ↑x‖
C : ℝ
hC : ∀ (x : ℝ), ‖f (↑x * I)‖ ≤ C
g : ℕ → ℂ → E := fun n z ↦ cexp z ^ n • f z
hg : ∀ (n : ℕ) (z : ℂ), ‖g n z‖ = expR z.re ^ n * ‖f z‖
z : ℂ
hz : 0 < z.re
n : ℕ
y : ℝ
⊢ ‖g n (↑y * I)‖ ≤ C
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a c : ℂ
R : ℝ
hR : R ≠ 0
x✝¹ : ℂ
x✝ : x✝¹ ∈ sphere 0 |1|
⊢ MeromorphicAt (fun z ↦ z + ↑R⁻¹ * (c - a)) x✝¹

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a c : ℂ
R : ℝ
hR : R ≠ 0
⊢ circleAverage (fun z ↦ log ‖R‖ + log ‖z + ↑R⁻¹ * (c - a)‖) 0 1 = log R + log⁺ (|R|⁻¹ * ‖c - a‖)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a c : ℂ
R : ℝ
hR : R ≠ 0
⊢ log R + log⁺ (|R|⁻¹ * ‖c - a‖) = log R + log⁺ (R⁻¹ * ‖c - a‖)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b t : ℝ
ht : t ≠ -1
⊢ ∫ (x : ℝ) in a..b, x * (1 + x ^ 2) ^ t = (1 + b ^ 2) ^ (t + 1) / (2 * (t + 1)) - (1 + a ^ 2) ^ (t + 1) / (2 * (t + 1))

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a c : ℂ
R : ℝ
hR : R ≠ 0
⊢ circleAverage (fun x ↦ log ‖x - a‖) c R = log R + log⁺ (R⁻¹ * ‖c - a‖)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
n : ℕ
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
α β γ : ℝ
⊢ β * α * γ * α = β * (α * α * γ)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
n : ℕ
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
x : ℝ
x✝ : x ∈ [[a, b]]
⊢ HasDerivAt (fun y ↦ sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
n : ℕ
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ x ∈ [[a, b]], HasDerivAt (fun y ↦ sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
x : ℝ
x✝ : x ∈ [[a, b]]
⊢ HasDerivAt (-cos) (sin x) x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.PosLogEqCircleAverage

Goal state before:
pp: a c : ℂ
R : ℝ
hu : a ∈ closedBall c |R|
⊢ circleAverage (fun x ↦ log ‖x - a‖) c R = log R

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.OpenMapping

Goal state before:
pp: f : ℂ → ℂ
z₀ : ℂ
ε r : ℝ
h : DiffContOnCl ℂ f (ball z₀ r)
hr : 0 < r
hf : ∀ z ∈ sphere z₀ r, ε ≤ ‖f z - f z₀‖
hz₀ : ∃ᶠ (z : ℂ) in 𝓝 z₀, f z ≠ f z₀
v : ℂ
hv : v ∈ ball (f z₀) (ε / 2)
h1 : DiffContOnCl ℂ (fun z ↦ f z - v) (ball z₀ r)
h2 : ContinuousOn (fun z ↦ ‖f z - v‖) (closedBall z₀ r)
h3 : AnalyticOnNhd ℂ f (ball z₀ r)
z : ℂ
hz : z ∈ sphere z₀ r
⊢ ε / 2 ≤ ‖f z - v‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.OpenMapping

Goal state before:
pp: f : ℂ → ℂ
z₀ : ℂ
ε r : ℝ
h : DiffContOnCl ℂ f (ball z₀ r)
hr : 0 < r
hf : ∀ z ∈ sphere z₀ r, ε ≤ ‖f z - f z₀‖
hz₀ : ∃ᶠ (z : ℂ) in 𝓝 z₀, f z ≠ f z₀
v : ℂ
hv : v ∈ ball (f z₀) (ε / 2)
h1 : DiffContOnCl ℂ (fun z ↦ f z - v) (ball z₀ r)
h2 : ContinuousOn (fun z ↦ ‖f z - v‖) (closedBall z₀ r)
h3 : AnalyticOnNhd ℂ f (ball z₀ r)
h4 : ∀ z ∈ sphere z₀ r, ε / 2 ≤ ‖f z - v‖
⊢ ‖f z₀ - v‖ < ε / 2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

Goal state before:
pp: a b : ℝ
n : ℕ
C : ℝ := sin a ^ (n + 1) * cos a - sin b ^ (n + 1) * cos b
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ x ∈ [[a, b]], HasDerivAt (fun y ↦ sin y ^ (n + 1)) (↑(n + 1) * cos x * sin x ^ n) x
hv : ∀ x ∈ [[a, b]], HasDerivAt (-cos) (sin x) x
H :
  ∫ (x : ℝ) in a..b, sin x ^ (n + 1) * sin x =
    sin b ^ (n + 1) * (-cos) b - sin a ^ (n + 1) * (-cos) a - ∫ (x : ℝ) in a..b, ↑(n + 1) * cos x * sin x ^ n * (-cos) x
⊢ ∫ (x : ℝ) in a..b, sin x ^ (n + 2) = ∫ (x : ℝ) in a..b, sin x ^ (n + 1) * sin x

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.OpenMapping

Goal state before:
pp: f : ℂ → ℂ
z₀ : ℂ
ε r : ℝ
h : DiffContOnCl ℂ f (ball z₀ r)
hr : 0 < r
hf : ∀ z ∈ sphere z₀ r, ε ≤ ‖f z - f z₀‖
hz₀ : ∃ᶠ (z : ℂ) in 𝓝 z₀, f z ≠ f z₀
v : ℂ
hv : v ∈ ball (f z₀) (ε / 2)
h1 : DiffContOnCl ℂ (fun z ↦ f z - v) (ball z₀ r)
h2 : ContinuousOn (fun z ↦ ‖f z - v‖) (closedBall z₀ r)
h3 : AnalyticOnNhd ℂ f (ball z₀ r)
h4 : ∀ z ∈ sphere z₀ r, ε / 2 ≤ ‖f z - v‖
h5 : ‖f z₀ - v‖ < ε / 2
z : ℂ
hz1 : z ∈ ball z₀ r
hz2 : IsLocalMin (fun z ↦ ‖f z - v‖) z
⊢ f z - v = 0

Tactic:
have h6 := h1.differentiableOn.eventually_differentiableAt (isOpen_ball.mem_nhds hz1)

Goal state after:
f : ℂ → ℂ
z₀ : ℂ
ε r : ℝ
h : DiffContOnCl ℂ f (ball z₀ r)
hr : 0 < r
hf : ∀ z ∈ sphere z₀ r, ε ≤ ‖f z - f z₀‖
hz₀ : ∃ᶠ (z : ℂ) in 𝓝 z₀, f z ≠ f z₀
v : ℂ
hv : v ∈ ball (f z₀) (ε / 2)
h1 : DiffContOnCl ℂ (fun z ↦ f z - v) (ball z₀ r)
h2 : ContinuousOn (fun z ↦ ‖f z - v‖) (closedBall z₀ r)
h3 : AnalyticOnNhd ℂ f (ball z₀ r)
h4 : ∀ z ∈ sphere z₀ r, ε / 2 ≤ ‖f z - v‖
h5 : ‖f z₀ - v‖ < ε / 2
z : ℂ
hz1 : z ∈ ball z₀ r
hz2 : IsLocalMin (fun z ↦ ‖f z - v‖) z
h6 : ∀ᶠ (y : ℂ) in 𝓝 z, DifferentiableAt ℂ (fun z ↦ f z - v) y
⊢ f z - v = 0