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

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ℂ → E
c : ℂ
r : ENNReal
hf : DifferentiableOn ℂ f (Metric.eball c r)
z : ℂ
hz : z ∈ Metric.eball c r
⊢ HasSum (fun n ↦ (↑n !)⁻¹ • (z - c) ^ n • iteratedDeriv n f c) (f z)

Tactic:
by

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

Goal state before:
pp: a b : ℝ
m n : ℕ
hc : Continuous fun u ↦ u ^ n * (1 - u ^ 2) ^ m
⊢ ∫ (x : ℝ) in a..b, sin x ^ (2 * m + 1) * cos x ^ n = -∫ (x : ℝ) in b..a, sin x ^ (2 * m + 1) * cos x ^ n

Tactic:
by

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

Goal state before:
pp: f : ℂ → ℂ
hf : Differentiable ℂ f
c : ℂ
h : ∀ (n : ℕ), 0 ≤ iteratedDeriv n f c
z : ℂ
hz : c ≤ z
⊢ 0 ≤ f z

Tactic:
by

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

Goal state before:
pp: a b : ℝ
m n : ℕ
hc : Continuous fun u ↦ u ^ n * (1 - u ^ 2) ^ m
⊢ -∫ (x : ℝ) in b..a, sin x ^ (2 * m + 1) * cos x ^ n = ∫ (x : ℝ) in b..a, (1 - cos x ^ 2) ^ m * -sin x * cos x ^ n

Tactic:
by

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

Goal state before:
pp: ρ w : ℂ
R : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
r : ℕ → ℝ
hr_lt : ∀ (n : ℕ), r n < R
hr_tendsto : Tendsto r atTop (𝓝 R)
bound : ℝ → ℝ :=
  fun θ ↦ (R + ‖w‖) / ((R + ‖w‖) / 2 - ‖w‖) * (|log (2 * R)| + |log √((R + ‖w‖) / 2 / R)| + |log ‖circleMap 0 R θ - ρ‖|)
⊢ MeromorphicOn (fun z ↦ z - ρ) (sphere 0 |R|)

Tactic:
by

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

Goal state before:
pp: c : ℂ
r : ENNReal
z : ℂ
hz : z ∈ Metric.eball c r
f : ℂ → ℂ
hf : DifferentiableOn ℂ f (Metric.eball c r)
⊢ ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = f z

Tactic:
by

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

Goal state before:
pp: f : ℂ → ℂ
c : ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ iteratedDeriv n f c
z : ℂ
hz : c ≤ z
n : ℕ
⊢ 0 ≤ iteratedDeriv n (fun x ↦ f x - f c) c

Tactic:
by

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

Goal state before:
pp: f : ℂ → ℂ
c : ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ iteratedDeriv n f c
z : ℂ
hz : c ≤ z
⊢ f c ≤ f z

Tactic:
by

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

Goal state before:
pp: c z : ℂ
f : ℂ → ℂ
hf : Differentiable ℂ f
⊢ ∑' (n : ℕ), (↑n !)⁻¹ * iteratedDeriv n f c * (z - c) ^ n = f z

Tactic:
by

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

Goal state before:
pp: a b : ℝ
m n : ℕ
hc : Continuous fun u ↦ u ^ n * (1 - u ^ 2) ^ m
⊢ ∫ (x : ℝ) in b..a, (1 - cos x ^ 2) ^ m * -sin x * cos x ^ n =
    ∫ (x : ℝ) in b..a, cos x ^ n * (1 - cos x ^ 2) ^ m * -sin x

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: ρ w : ℂ
R : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
r : ℕ → ℝ
hr_lt : ∀ (n : ℕ), r n < R
hr_tendsto : Tendsto r atTop (𝓝 R)
bound : ℝ → ℝ :=
  fun θ ↦ (R + ‖w‖) / ((R + ‖w‖) / 2 - ‖w‖) * (|log (2 * R)| + |log √((R + ‖w‖) / 2 / R)| + |log ‖circleMap 0 R θ - ρ‖|)
h_measure_zero : volume {θ | circleMap 0 R θ = w ∨ circleMap 0 R θ = ρ} = 0
θ : ℝ
hθ : ¬(circleMap 0 R θ = w ∨ circleMap 0 R θ = ρ)
a✝ : θ ∈ uIoc 0 (2 * π)
⊢ circleMap 0 R θ ≠ w

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: ρ w : ℂ
R : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
r : ℕ → ℝ
hr_lt : ∀ (n : ℕ), r n < R
hr_tendsto : Tendsto r atTop (𝓝 R)
bound : ℝ → ℝ :=
  fun θ ↦ (R + ‖w‖) / ((R + ‖w‖) / 2 - ‖w‖) * (|log (2 * R)| + |log √((R + ‖w‖) / 2 / R)| + |log ‖circleMap 0 R θ - ρ‖|)
h_measure_zero : volume {θ | circleMap 0 R θ = w ∨ circleMap 0 R θ = ρ} = 0
θ : ℝ
hθ : ¬(circleMap 0 R θ = w ∨ circleMap 0 R θ = ρ)
a✝ : θ ∈ uIoc 0 (2 * π)
⊢ circleMap 0 R θ ≠ ρ

Tactic:
by

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

Goal state before:
pp: f : ℂ → ℂ
c : ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ (-1) ^ n * iteratedDeriv n f c
z : ℂ
hz : z ≤ c
⊢ f c ≤ f z

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: ρ w : ℂ
R : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
r : ℕ → ℝ
hr_lt : ∀ (n : ℕ), r n < R
hr_tendsto : Tendsto r atTop (𝓝 R)
⊢ Tendsto (fun n ↦ circleAverage (herglotzLogIntegrand w ρ) 0 (r n)) atTop
    (𝓝 (circleAverage (herglotzLogIntegrand w ρ) 0 R))

Tactic:
by

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

Goal state before:
pp: a b : ℝ
m n : ℕ
⊢ ∫ (x : ℝ) in a..b, sin x ^ (2 * m) * cos x ^ (2 * n) =
    ∫ (x : ℝ) in a..b, ((1 - cos (2 * x)) / 2) ^ m * ((1 + cos (2 * x)) / 2) ^ n

Tactic:
by

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

Goal state before:
pp: a b c : ℝ
⊢ (1 - c) / 2 * ((1 + c) / 2) = (1 - c ^ 2) / 4

Tactic:
by

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

Goal state before:
pp: a b : ℝ
h1 : ∀ (c : ℝ), (1 - c) / 2 * ((1 + c) / 2) = (1 - c ^ 2) / 4
⊢ Continuous fun x ↦ cos (2 * x) ^ 2

Tactic:
by

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

Goal state before:
pp: a b : ℝ
h1 : ∀ (c : ℝ), (1 - c) / 2 * ((1 + c) / 2) = (1 - c ^ 2) / 4
h2 : Continuous fun x ↦ cos (2 * x) ^ 2
⊢ ∀ (x : ℝ), cos x * sin x = sin (2 * x) / 2

Tactic:
by

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

Goal state before:
pp: a b : ℝ
h1 : ∀ (c : ℝ), (1 - c) / 2 * ((1 + c) / 2) = (1 - c ^ 2) / 4
h2 : Continuous fun x ↦ cos (2 * x) ^ 2
h3 : ∀ (x : ℝ), cos x * sin x = sin (2 * x) / 2
d : ℝ
⊢ 2 * (2 * d) = 4 * d

Tactic:
by

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

Goal state before:
pp: w ρ : ℂ
R : ℝ
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
hR : 0 < R
r : ℕ → ℝ := fun n ↦ R - (R - ‖w‖) / (↑n + 2)
n : ℕ
⊢ r n < R

Tactic:
by

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

Goal state before:
pp: w ρ : ℂ
R : ℝ
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
hR : 0 < R
r : ℕ → ℝ := fun n ↦ R - (R - ‖w‖) / (↑n + 2)
n : ℕ
hr_lt : ∀ (n : ℕ), 0 < ↑n + 2
⊢ 0 < ↑n + 2

Tactic:
by

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

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

Tactic:
by

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

Goal state before:
pp: w ρ : ℂ
R : ℝ
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
hR : 0 < R
r : ℕ → ℝ := fun n ↦ R - (R - ‖w‖) / (↑n + 2)
n : ℕ
hr_lt : ∀ (n : ℕ), 0 < ↑n + 2
⊢ R - ‖w‖ ≤ R * 1

Tactic:
by

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

Goal state before:
pp: w ρ : ℂ
R : ℝ
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
hR : 0 < R
r : ℕ → ℝ := fun n ↦ R - (R - ‖w‖) / (↑n + 2)
n : ℕ
hr_lt : ∀ (n : ℕ), 0 < ↑n + 2
⊢ R * 1 < R * (↑n + 2)

Tactic:
by

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

Goal state before:
pp: w ρ : ℂ
R : ℝ
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
hR : 0 < R
r : ℕ → ℝ := fun n ↦ R - (R - ‖w‖) / (↑n + 2)
hr_lt : ∀ (n : ℕ), r n < R
n : ℕ
⊢ 0 < r n

Tactic:
by

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

Goal state before:
pp: ⊢ ∫ (x : ℝ) in -1..1, √(1 - x ^ 2) = ∫ (x : ℝ) in sin (-(π / 2))..sin (π / 2), √(1 - x ^ 2)

Tactic:
by

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

Goal state before:
pp: ⊢ Continuous fun x ↦ √(1 - x ^ 2)

Tactic:
by

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

Goal state before:
pp: ⊢ ∫ (x : ℝ) in -(π / 2)..π / 2, √(1 - sin x ^ 2) * cos x = ∫ (x : ℝ) in -(π / 2)..π / 2, cos x ^ 2

Tactic:
by

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

Goal state before:
pp: ⊢ ∫ (x : ℝ) in -(π / 2)..π / 2, cos x ^ 2 = π / 2

Tactic:
by

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

Goal state before:
pp: w ρ : ℂ
R : ℝ
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
hR : 0 < R
r : ℕ → ℝ := fun n ↦ R - (R - ‖w‖) / (↑n + 2)
hr_lt : ∀ (n : ℕ), r n < R
hr_pos : ∀ (n : ℕ), 0 < r n
hr_tendsto : Tendsto r atTop (𝓝 R)
DCT :
  Tendsto (fun n ↦ circleAverage (herglotzLogIntegrand w ρ) 0 (r n)) atTop
    (𝓝 (circleAverage (herglotzLogIntegrand w ρ) 0 R))
n : ℕ
z : ℂ
hz : z ∈ ball 0 (r n)
⊢ AnalyticAt ℂ (fun x ↦ x - ρ) z

Tactic:
by

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

Goal state before:
pp: w ρ : ℂ
R : ℝ
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
hR : 0 < R
r : ℕ → ℝ := fun n ↦ R - (R - ‖w‖) / (↑n + 2)
hr_lt : ∀ (n : ℕ), r n < R
hr_pos : ∀ (n : ℕ), 0 < r n
hr_tendsto : Tendsto r atTop (𝓝 R)
DCT :
  Tendsto (fun n ↦ circleAverage (herglotzLogIntegrand w ρ) 0 (r n)) atTop
    (𝓝 (circleAverage (herglotzLogIntegrand w ρ) 0 R))
n : ℕ
z : ℂ
hz : z ∈ ball 0 (r n)
⊢ z - ρ ≠ 0

Tactic:
by

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

Goal state before:
pp: w ρ : ℂ
R : ℝ
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
hR : 0 < R
r : ℕ → ℝ := fun n ↦ R - (R - ‖w‖) / (↑n + 2)
hr_lt : ∀ (n : ℕ), r n < R
hr_pos : ∀ (n : ℕ), 0 < r n
hr_tendsto : Tendsto r atTop (𝓝 R)
DCT :
  Tendsto (fun n ↦ circleAverage (herglotzLogIntegrand w ρ) 0 (r n)) atTop
    (𝓝 (circleAverage (herglotzLogIntegrand w ρ) 0 R))
n : ℕ
x : ℂ
hx : x ∈ closure (ball 0 (r n))
this : ‖x - ρ‖ ≠ 0
⊢ ContinuousWithinAt (fun x ↦ log ‖x - ρ‖) (closure (ball 0 (r n))) x

Tactic:
by

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

Goal state before:
pp: U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
this :
  ∀ {U : Set ℂ},
    IsOpen U → IsSimplyConnected U → U ≠ univ → 0 ∉ U → ∃ f, Injective f ∧ ¬Dense (f '' U) ∧ ∀ z ∈ U, deriv f z ≠ 0
hU₀ : ¬0 ∉ U
a : ℂ
ha : a ∉ U
⊢ IsSimplyConnected (-a +ᵥ U)

Tactic:
by

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

Goal state before:
pp: w ρ : ℂ
R : ℝ
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
hR : 0 < R
r : ℕ → ℝ := fun n ↦ R - (R - ‖w‖) / (↑n + 2)
hr_lt : ∀ (n : ℕ), r n < R
hr_pos : ∀ (n : ℕ), 0 < r n
hr_tendsto : Tendsto r atTop (𝓝 R)
DCT :
  Tendsto (fun n ↦ circleAverage (herglotzLogIntegrand w ρ) 0 (r n)) atTop
    (𝓝 (circleAverage (herglotzLogIntegrand w ρ) 0 R))
n : ℕ
x : ℂ
hx : x ∈ closure (ball 0 (r n))
this : x ≠ ρ
⊢ ‖x - ρ‖ ≠ 0

Tactic:
by

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

Goal state before:
pp: U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
this :
  ∀ {U : Set ℂ},
    IsOpen U → IsSimplyConnected U → U ≠ univ → 0 ∉ U → ∃ f, Injective f ∧ ¬Dense (f '' U) ∧ ∀ z ∈ U, deriv f z ≠ 0
hU₀ : ¬0 ∉ U
a : ℂ
ha : a ∉ U
⊢ -a +ᵥ U ≠ univ

Tactic:
by

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

Goal state before:
pp: U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
this :
  ∀ {U : Set ℂ},
    IsOpen U → IsSimplyConnected U → U ≠ univ → 0 ∉ U → ∃ f, Injective f ∧ ¬Dense (f '' U) ∧ ∀ z ∈ U, deriv f z ≠ 0
hU₀ : ¬0 ∉ U
a : ℂ
ha : a ∉ U
⊢ 0 ∉ -a +ᵥ U

Tactic:
by

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

Goal state before:
pp: w ρ : ℂ
R : ℝ
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
hR : 0 < R
r : ℕ → ℝ := fun n ↦ R - (R - ‖w‖) / (↑n + 2)
hr_lt : ∀ (n : ℕ), r n < R
hr_pos : ∀ (n : ℕ), 0 < r n
hr_tendsto : Tendsto r atTop (𝓝 R)
DCT :
  Tendsto (fun n ↦ circleAverage (herglotzLogIntegrand w ρ) 0 (r n)) atTop
    (𝓝 (circleAverage (herglotzLogIntegrand w ρ) 0 R))
n : ℕ
x : ℂ
hx : x ∈ closure (ball 0 (r n))
⊢ ?m.450

Tactic:
by

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

Goal state before:
pp: U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
hU₀ : 0 ∉ U
⊢ 0 ∉ id '' U

Tactic:
by

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

Goal state before:
pp: w ρ : ℂ
R : ℝ
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
hR : 0 < R
r : ℕ → ℝ := fun n ↦ R - (R - ‖w‖) / (↑n + 2)
hr_lt : ∀ (n : ℕ), r n < R
hr_pos : ∀ (n : ℕ), 0 < r n
hr_tendsto : Tendsto r atTop (𝓝 R)
DCT :
  Tendsto (fun n ↦ circleAverage (herglotzLogIntegrand w ρ) 0 (r n)) atTop
    (𝓝 (circleAverage (herglotzLogIntegrand w ρ) 0 R))
n : ℕ
⊢ ‖w‖ * (↑n + 2) + (R - ‖w‖) = ‖w‖ * (↑n + 1) + R

Tactic:
by

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

Goal state before:
pp: w ρ : ℂ
R : ℝ
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
hR : 0 < R
r : ℕ → ℝ := fun n ↦ R - (R - ‖w‖) / (↑n + 2)
hr_lt : ∀ (n : ℕ), r n < R
hr_pos : ∀ (n : ℕ), 0 < r n
hr_tendsto : Tendsto r atTop (𝓝 R)
DCT :
  Tendsto (fun n ↦ circleAverage (herglotzLogIntegrand w ρ) 0 (r n)) atTop
    (𝓝 (circleAverage (herglotzLogIntegrand w ρ) 0 R))
n : ℕ
⊢ ‖w‖ * (↑n + 1) + R < R * (↑n + 1) + R

Tactic:
by

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

Goal state before:
pp: U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
hU₀ : 0 ∉ U
f : ℂ → ℂ
hfc : ContinuousOn f U
hf_inv : LeftInverse (fun x ↦ x ^ 2) f
⊢ ∀ z ∈ U, f z ≠ 0

Tactic:
by

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

Goal state before:
pp: w ρ : ℂ
R : ℝ
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
hR : 0 < R
r : ℕ → ℝ := fun n ↦ R - (R - ‖w‖) / (↑n + 2)
hr_lt : ∀ (n : ℕ), r n < R
hr_pos : ∀ (n : ℕ), 0 < r n
hr_tendsto : Tendsto r atTop (𝓝 R)
DCT :
  Tendsto (fun n ↦ circleAverage (herglotzLogIntegrand w ρ) 0 (r n)) atTop
    (𝓝 (circleAverage (herglotzLogIntegrand w ρ) 0 R))
n : ℕ
⊢ R * (↑n + 1) + R = R * (↑n + 2)

Tactic:
by

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

Goal state before:
pp: w ρ : ℂ
R : ℝ
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
hR : 0 < R
r : ℕ → ℝ := fun n ↦ R - (R - ‖w‖) / (↑n + 2)
hr_lt : ∀ (n : ℕ), r n < R
hr_pos : ∀ (n : ℕ), 0 < r n
hr_tendsto : Tendsto r atTop (𝓝 R)
DCT :
  Tendsto (fun n ↦ circleAverage (herglotzLogIntegrand w ρ) 0 (r n)) atTop
    (𝓝 (circleAverage (herglotzLogIntegrand w ρ) 0 R))
n : ℕ
⊢ circleAverage (herglotzLogIntegrand w ρ) 0 (r n) = log ‖w - ρ‖

Tactic:
by

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

Goal state before:
pp: w ρ : ℂ
R : ℝ
hρ : ρ ∈ sphere 0 R
hw : w ∈ ball 0 R
⊢ circleAverage (Complex.re ∘ herglotzRieszKernel 0 w • fun x ↦ log ‖x - ρ‖) 0 R = log ‖w - ρ‖

Tactic:
by

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

Goal state before:
pp: w ρ c : ℂ
R : ℝ
hρ : ρ ∈ sphere c R
hw : w ∈ ball c R
z : ℂ
⊢ z + 0 + c - ρ = z - (ρ - c)

Tactic:
by

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

Goal state before:
pp: U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
hU₀ : 0 ∉ U
f : ℂ → ℂ
hfc : ContinuousOn f U
hf_inv : LeftInverse (fun x ↦ x ^ 2) f
hf₀ : ∀ z ∈ U, f z ≠ 0
⊢ ∀ z ∈ U, HasStrictDerivAt f (2 * f z)⁻¹ z

Tactic:
by

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

Goal state before:
pp: U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
hU₀ : 0 ∉ U
f : ℂ → ℂ
hfc : ContinuousOn f U
hf_inv : LeftInverse (fun x ↦ x ^ 2) f
hf₀ : ∀ z ∈ U, f z ≠ 0
⊢ ∃ f, Injective f ∧ ¬Dense (f '' U) ∧ ∀ z ∈ U, deriv f z ≠ 0

Tactic:
have hdf : ∀ z ∈ U, HasStrictDerivAt f (2 * f z)⁻¹ z := by
    intro z hz
    apply HasStrictDerivAt.of_local_left_inverse
    · exact hfc.continuousAt <| hUo.mem_nhds hz
    · simpa using hasStrictDerivAt_pow 2 (f z)
    · simpa using hf₀ z hz
    · exact .of_forall hf_inv

Goal state after:
U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
hU₀ : 0 ∉ U
f : ℂ → ℂ
hfc : ContinuousOn f U
hf_inv : LeftInverse (fun x ↦ x ^ 2) f
hf₀ : ∀ z ∈ U, f z ≠ 0
hdf : ∀ z ∈ U, HasStrictDerivAt f (2 * f z)⁻¹ z
⊢ ∃ f, Injective f ∧ ¬Dense (f '' U) ∧ ∀ z ∈ U, deriv f z ≠ 0
Module: Mathlib.Analysis.Complex.RiemannMapping

Goal state before:
pp: U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
hU₀ : 0 ∉ U
f : ℂ → ℂ
hfc : ContinuousOn f U
hf_inv : LeftInverse (fun x ↦ x ^ 2) f
hf₀ : ∀ z ∈ U, f z ≠ 0
hdf : ∀ z ∈ U, HasStrictDerivAt f (2 * f z)⁻¹ z
x : ℂ
hx : x ∈ U
⊢ (2 * f x)⁻¹ ≠ 0

Tactic:
by

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

Goal state before:
pp: w ρ c : ℂ
R : ℝ
hρ : ρ ∈ sphere c R
hw : w ∈ ball c R
⊢ (fun z ↦ (herglotzRieszKernel 0 (w - c) z).re * log ‖z - (ρ - c)‖) =
    Complex.re ∘ herglotzRieszKernel 0 (w - c) • fun x ↦ log ‖x - (ρ - c)‖

Tactic:
by

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

Goal state before:
pp: w ρ c : ℂ
R : ℝ
hρ : ρ ∈ sphere c R
hw : w ∈ ball c R
⊢ circleAverage (fun z ↦ (herglotzRieszKernel 0 (w - c) z).re * log ‖z - (ρ - c)‖) 0 R = log ‖w - ρ‖

Tactic:
have : (fun z ↦ (herglotzRieszKernel 0 (w - c) z).re * log ‖z - (ρ - c)‖) =
    (Complex.re ∘ herglotzRieszKernel 0 (w - c)) • (log ‖· - (ρ - c)‖) := by rfl

Goal state after:
w ρ c : ℂ
R : ℝ
hρ : ρ ∈ sphere c R
hw : w ∈ ball c R
this :
  (fun z ↦ (herglotzRieszKernel 0 (w - c) z).re * log ‖z - (ρ - c)‖) =
    Complex.re ∘ herglotzRieszKernel 0 (w - c) • fun x ↦ log ‖x - (ρ - c)‖
⊢ circleAverage (fun z ↦ (herglotzRieszKernel 0 (w - c) z).re * log ‖z - (ρ - c)‖) 0 R = log ‖w - ρ‖
Module: Mathlib.Analysis.Complex.RiemannMapping

Goal state before:
pp: U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
hU₀ : 0 ∉ U
f : ℂ → ℂ
hfc : ContinuousOn f U
hf_inv : LeftInverse (fun x ↦ x ^ 2) f
hf₀ : ∀ z ∈ U, f z ≠ 0
hdf : ∀ z ∈ U, HasStrictDerivAt f (2 * f z)⁻¹ z
x : ℂ
hx : x ∈ U
⊢ f '' U ∈ 𝓝 (f x)

Tactic:
by

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

Goal state before:
pp: w ρ c : ℂ
R : ℝ
hρ : ρ ∈ sphere c R
hw : w ∈ ball c R
this :
  (fun z ↦ (herglotzRieszKernel 0 (w - c) z).re * log ‖z - (ρ - c)‖) =
    Complex.re ∘ herglotzRieszKernel 0 (w - c) • fun x ↦ log ‖x - (ρ - c)‖
⊢ ρ - c ∈ sphere 0 R

Tactic:
by

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

Goal state before:
pp: w ρ c : ℂ
R : ℝ
hρ : ρ ∈ sphere c R
hw : w ∈ ball c R
this :
  (fun z ↦ (herglotzRieszKernel 0 (w - c) z).re * log ‖z - (ρ - c)‖) =
    Complex.re ∘ herglotzRieszKernel 0 (w - c) • fun x ↦ log ‖x - (ρ - c)‖
⊢ w - c ∈ ball 0 R

Tactic:
by

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

Goal state before:
pp: U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
hU₀ : 0 ∉ U
f : ℂ → ℂ
hfc : ContinuousOn f U
hf_inv : LeftInverse (fun x ↦ x ^ 2) f
hf₀ : ∀ z ∈ U, f z ≠ 0
hdf : ∀ z ∈ U, HasStrictDerivAt f (2 * f z)⁻¹ z
x : ℂ
hx : x ∈ U
this : f '' U ∈ 𝓝 (f x)
a : ℂ
ha : a ∈ U
b : ℂ
hb : b ∈ U
hab : f b = -f a
⊢ a = b

Tactic:
by

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

Goal state before:
pp: w ρ c : ℂ
R : ℝ
hρ : ρ ∈ sphere c R
hw : w ∈ ball c R
⊢ circleAverage (Complex.re ∘ herglotzRieszKernel c w * fun x ↦ log ‖x - ρ‖) c R = log ‖w - ρ‖

Tactic:
by

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

Goal state before:
pp: U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
⊢ ∃ f, Injective f ∧ ¬Dense (f '' U) ∧ ∀ z ∈ U, deriv f z ≠ 0

Tactic:
by

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

Goal state before:
pp: U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
f : ℂ → ℂ
hf_inj : Injective f
hfd : ¬Dense (f '' U)
hdf : ∀ z ∈ U, deriv f z ≠ 0
⊢ ∃ x ε, 0 < ε ∧ ∀ a ∈ U, ε < dist (f a) x

Tactic:
by

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

Goal state before:
pp: U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
f : ℂ → ℂ
hf_inj : Injective f
hfd : ¬Dense (f '' U)
hdf : ∀ z ∈ U, deriv f z ≠ 0
x : ℂ
ε : ℝ
hε₀ : 0 < ε
hε : ∀ a ∈ U, ε < dist (f a) x
z : ℂ
hz : z ∈ U
⊢ f z ≠ x

Tactic:
by

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

Goal state before:
pp: R : ℝ
c : ℂ
D : Function.locallyFinsuppWithin (closedBall c |R|) ℤ
h : D.support.Finite
⊢ circleAverage (∑ᶠ (u : ℂ), fun x ↦ ↑(D u) * log ‖x - u‖) c R =
    circleAverage (∑ u ∈ h.toFinset, fun x ↦ ↑(D u) * log ‖x - u‖) c R

Tactic:
by

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

Goal state before:
pp: R : ℝ
c : ℂ
D : Function.locallyFinsuppWithin (closedBall c |R|) ℤ
h : D.support.Finite
⊢ circleAverage (∑ u ∈ h.toFinset, fun x ↦ ↑(D u) * log ‖x - u‖) c R =
    ∑ i ∈ h.toFinset, circleAverage (fun x ↦ ↑(D i) * log ‖x - i‖) c R

Tactic:
by

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

Goal state before:
pp: z : ℂ
hz : z ∈ slitPlane
⊢ 2⁻¹ * z ^ (2⁻¹ - 1) = z ^ (-1 / 2) / 2

Tactic:
by

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

Goal state before:
pp: R : ℝ
c : ℂ
D : Function.locallyFinsuppWithin (closedBall c |R|) ℤ
h : D.support.Finite
⊢ ∑ i ∈ h.toFinset, circleAverage (fun x ↦ ↑(D i) * log ‖x - i‖) c R = ∑ u ∈ h.toFinset, ↑(D u) * log R

Tactic:
by

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

Goal state before:
pp: z : ℂ
hz : z ∈ slitPlane
⊢ HasStrictDerivAt sqrt (z ^ (-1 / 2) / 2) z

Tactic:
by

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

Goal state before:
pp: z : ℂ
hz : 0 ≤ z.re ∨ z.im ≠ 0
⊢ 0 < 2⁻¹.re

Tactic:
by

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

Goal state before:
pp: R : ℝ
c : ℂ
D : Function.locallyFinsuppWithin (closedBall c |R|) ℤ
h : D.support.Finite
⊢ ∑ u ∈ h.toFinset, ↑(D u) * log R = ∑ᶠ (u : ℂ), ↑(D u) * log R

Tactic:
by

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

Goal state before:
pp: R : ℝ
c : ℂ
D : Function.locallyFinsuppWithin (closedBall c |R|) ℤ
⊢ circleAverage (∑ᶠ (u : ℂ), fun x ↦ ↑(D u) * log ‖x - u‖) c R = ∑ᶠ (u : ℂ), ↑(D u) * log R

Tactic:
by

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

Goal state before:
pp: c : ℂ
R : ℝ
D : ℂ → ℤ
hR : R ≠ 0
hD : Function.HasFiniteSupport D
h : c ∈ Function.support D
g : ℂ → ℝ
x : ℂ
⊢ (x ∈ Function.support fun u ↦ ↑(D u) * g u) → x ∈ ↑(Finite.toFinset hD)

Tactic:
by

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

Goal state before:
pp: U : Set ℂ
hUo : IsOpen U
hUc : IsSimplyConnected U
hU : U ≠ univ
⊢ ∃ f, MapsTo f U (ball 0 1) ∧ InjOn f U ∧ ∀ z ∈ U, deriv f z ≠ 0

Tactic:
by

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

Goal state before:
pp: ι : Type u_1
E : Type u_2
inst✝² : NormedAddCommGroup E
inst✝¹ : NormedSpace ℂ E
inst✝ : CompleteSpace E
f : ι → ℂ → E
s : Set ℂ
hs : IsOpen s
h : SummableLocallyUniformlyOn f s
hf2 : ∀ (n : ι), ∀ r ∈ s, DifferentiableAt ℂ (f n) r
⊢ DifferentiableOn ℂ (fun z ↦ ∑' (n : ι), f n z) s

Tactic:
by

Goal state after:
Module: Mathlib.Order.Monotone.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
x : α
hxc : x ≤ c
h✝ : x ∈ t
h'x : x < c
⊢ x ∈ t

Tactic:
by

Goal state after:
Module: Mathlib.Order.Monotone.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
⊢ ∀ x ∈ s ∪ t, x ≤ c → x ∈ s

Tactic:
by

Goal state after:
Module: Mathlib.Order.Monotone.Union

Goal state before:
pp: α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s t : Set α
c : α
h₁ : StrictMonoOn f s
h₂ : StrictMonoOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s
⊢ ∀ x ∈ s ∪ t, c ≤ x → x ∈ t

Tactic:
by

Goal state after:
Module: Mathlib.Order.Monotone.Odd

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝⁵ : AddCommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedAddMonoid G
inst✝² : AddCommGroup H
inst✝¹ : PartialOrder H
inst✝ : IsOrderedAddMonoid H
f : G → H
h₁ : ∀ (x : G), f (-x) = -f x
h₂ : StrictMonoOn f (Ici 0)
⊢ StrictMono f

Tactic:
by

Goal state after:
Module: Mathlib.Order.Monotone.Odd

Goal state before:
pp: G : Type u_1
H : Type u_2
inst✝⁵ : AddCommGroup G
inst✝⁴ : LinearOrder G
inst✝³ : IsOrderedAddMonoid G
inst✝² : AddCommGroup H
inst✝¹ : PartialOrder H
inst✝ : IsOrderedAddMonoid H
f : G → H
h₁ : ∀ (x : G), f (-x) = -f x
h₂ : MonotoneOn f (Ici 0)
⊢ Monotone f

Tactic:
by

Goal state after: