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

Goal state before:
pp: w ρ : ℂ
R r₀ r : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hw : ‖w‖ < r₀
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
hdR : 0 < ‖circleMap 0 R θ - ρ‖
hrw : 0 < r₀ - ‖w‖
hr : 0 < r
h_norm_sub₁ : √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
h_norm_sub₂ : 0 < ‖circleMap 0 r θ - ρ‖
⊢ -(|log (2 * R)| + |log √(r₀ / R)| + |log ‖circleMap 0 R θ - ρ‖|) ≤ log ‖circleMap 0 r θ - ρ‖

pp: w ρ : ℂ
R r₀ r : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hw : ‖w‖ < r₀
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
hdR : 0 < ‖circleMap 0 R θ - ρ‖
hrw : 0 < r₀ - ‖w‖
hr : 0 < r
h_norm_sub₁ : √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
h_norm_sub₂ : 0 < ‖circleMap 0 r θ - ρ‖
⊢ log ‖circleMap 0 r θ - ρ‖ ≤ |log (2 * R)| + |log √(r₀ / R)| + |log ‖circleMap 0 R θ - ρ‖|

Tactic:
·

Goal state after:
w ρ : ℂ
R r₀ r : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hw : ‖w‖ < r₀
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
hdR : 0 < ‖circleMap 0 R θ - ρ‖
hrw : 0 < r₀ - ‖w‖
hr : 0 < r
h_norm_sub₁ : √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
h_norm_sub₂ : 0 < ‖circleMap 0 r θ - ρ‖
⊢ -(|log (2 * R)| + |log √(r₀ / R)| + |log ‖circleMap 0 R θ - ρ‖|) ≤ log ‖circleMap 0 r θ - ρ‖
Module: Mathlib.Analysis.Complex.OpenMapping

Goal state before:
pp: case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
U : Set E
g : E → ℂ
hg : AnalyticOnNhd ℂ g U
hU : IsPreconnected U
h : ∃ z₀ ∈ U, ∀ᶠ (z : E) in 𝓝 z₀, g z = g z₀
⊢ (∃ w, ∀ z ∈ U, g z = w) ∨ ∀ s ⊆ U, IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s → IsOpen (g '' s)

pp: case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
U : Set E
g : E → ℂ
hg : AnalyticOnNhd ℂ g U
hU : IsPreconnected U
h : ¬∃ z₀ ∈ U, ∀ᶠ (z : E) in 𝓝 z₀, g z = g z₀
⊢ (∃ w, ∀ z ∈ U, g z = w) ∨ ∀ s ⊆ U, IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s → IsOpen (g '' s)

Tactic:
·

Goal state after:
case pos
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
U : Set E
g : E → ℂ
hg : AnalyticOnNhd ℂ g U
hU : IsPreconnected U
h : ∃ z₀ ∈ U, ∀ᶠ (z : E) in 𝓝 z₀, g z = g z₀
⊢ (∃ w, ∀ z ∈ U, g z = w) ∨ ∀ s ⊆ U, IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s → IsOpen (g '' s)
Module: Mathlib.Analysis.Complex.OpenMapping

Goal state before:
pp: case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
U : Set E
g : E → ℂ
hg : AnalyticOnNhd ℂ g U
hU : IsPreconnected U
h : ¬∃ z₀ ∈ U, ∀ᶠ (z : E) in 𝓝 z₀, g z = g z₀
⊢ (∃ w, ∀ z ∈ U, g z = w) ∨ ∀ s ⊆ U, IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s → IsOpen (g '' s)

Tactic:
·

Goal state after:
case neg
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
U : Set E
g : E → ℂ
hg : AnalyticOnNhd ℂ g U
hU : IsPreconnected U
h : ¬∃ z₀ ∈ U, ∀ᶠ (z : E) in 𝓝 z₀, g z = g z₀
⊢ (∃ w, ∀ z ∈ U, g z = w) ∨ ∀ s ⊆ U, IsOpen[PseudoMetricSpace.toUniformSpace.toTopologicalSpace] s → IsOpen (g '' s)
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: w ρ : ℂ
R r₀ r : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hw : ‖w‖ < r₀
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
hdR : 0 < ‖circleMap 0 R θ - ρ‖
hrw : 0 < r₀ - ‖w‖
hr : 0 < r
h_norm_sub₁ : √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
h_norm_sub₂ : 0 < ‖circleMap 0 r θ - ρ‖
⊢ log ‖circleMap 0 r θ - ρ‖ ≤ |log (2 * R)| + |log √(r₀ / R)| + |log ‖circleMap 0 R θ - ρ‖|

Tactic:
·

Goal state after:
w ρ : ℂ
R r₀ r : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hw : ‖w‖ < r₀
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
hdR : 0 < ‖circleMap 0 R θ - ρ‖
hrw : 0 < r₀ - ‖w‖
hr : 0 < r
h_norm_sub₁ : √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
h_norm_sub₂ : 0 < ‖circleMap 0 r θ - ρ‖
⊢ log ‖circleMap 0 r θ - ρ‖ ≤ |log (2 * R)| + |log √(r₀ / R)| + |log ‖circleMap 0 R θ - ρ‖|
Module: Mathlib.Analysis.Complex.OpenMapping

Goal state before:
pp: case inl
p : ℂ[X]
h : ¬∃ x, C x = p
x : ℂ
eq : ∀ (z : ℂ), eval z p = x
⊢ IsOpenQuotientMap fun x ↦ eval x p

pp: case inr
p : ℂ[X]
h : ¬∃ x, C x = p
hp : IsOpenMap fun x ↦ eval x p
⊢ IsOpenQuotientMap fun x ↦ eval x p

Tactic:
·

Goal state after:
case inl
p : ℂ[X]
h : ¬∃ x, C x = p
x : ℂ
eq : ∀ (z : ℂ), eval z p = x
⊢ IsOpenQuotientMap fun x ↦ eval x p
Module: Mathlib.Analysis.Complex.OpenMapping

Goal state before:
pp: case inr
p : ℂ[X]
h : ¬∃ x, C x = p
hp : IsOpenMap fun x ↦ eval x p
⊢ IsOpenQuotientMap fun x ↦ eval x p

Tactic:
·

Goal state after:
case inr
p : ℂ[X]
h : ¬∃ x, C x = p
hp : IsOpenMap fun x ↦ eval x p
⊢ IsOpenQuotientMap fun x ↦ eval x p
Module: Mathlib.Analysis.Complex.OpenMapping

Goal state before:
pp: p : ℂ[X]
⊢ (∃ x, C x = p) ∨ IsOpenQuotientMap fun x ↦ eval x p

Tactic:
refine or_iff_not_imp_left.mpr fun h ↦ ?_
  obtain ⟨x, eq⟩ | hp := (AnalyticOnNhd.eval_polynomial p).is_constant_or_isOpenMap
  · exact (h ⟨x, funext <| by simpa [eq_comm (a := x)]⟩).elim
  · exact ⟨IsAlgClosed.eval_surjective <| natDegree_eq_zero.not.mpr h, p.continuous_aeval, hp⟩

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

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
x✝ : ℂ
⊢ x✝ ^ n = Polynomial.eval x✝ (Polynomial.X ^ n)

pp: n : ℕ
inst✝ : NeZero n
⊢ (Polynomial.X ^ n).natDegree ≠ 0

Tactic:
·

Goal state after:
n : ℕ
inst✝ : NeZero n
x✝ : ℂ
⊢ x✝ ^ n = Polynomial.eval x✝ (Polynomial.X ^ n)
Module: Mathlib.Analysis.Complex.OpenMapping

Goal state before:
pp: n : ℕ
inst✝ : NeZero n
⊢ (Polynomial.X ^ n).natDegree ≠ 0

Tactic:
·

Goal state after:
n : ℕ
inst✝ : NeZero n
⊢ (Polynomial.X ^ n).natDegree ≠ 0
Module: Mathlib.Analysis.Complex.OpenMapping

Goal state before:
pp: case inl
n : ℕ
inst✝ : NeZero ↑n
⊢ IsOpenQuotientMap fun z ↦ ⟨↑z ^ ↑n, ⋯⟩

pp: case inr
n : ℕ
inst✝ : NeZero (-↑n)
⊢ IsOpenQuotientMap fun z ↦ ⟨↑z ^ (-↑n), ⋯⟩

Tactic:
·

Goal state after:
case inl
n : ℕ
inst✝ : NeZero ↑n
⊢ IsOpenQuotientMap fun z ↦ ⟨↑z ^ ↑n, ⋯⟩
Module: Mathlib.Analysis.Complex.OpenMapping

Goal state before:
pp: case inr
n : ℕ
inst✝ : NeZero (-↑n)
⊢ IsOpenQuotientMap fun z ↦ ⟨↑z ^ (-↑n), ⋯⟩

Tactic:
·

Goal state after:
case inr
n : ℕ
inst✝ : NeZero (-↑n)
⊢ IsOpenQuotientMap fun z ↦ ⟨↑z ^ (-↑n), ⋯⟩
Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas

Goal state before:
pp: case pos
P : ℂ[X]
hP : 0 < P.degree
z : ℂ
hP₀ : P ≠ 0
hPz : eval z P = 0
⊢ 0 < ∑ w ∈ P.roots.toFinset, P.derivRootWeight z w

pp: case neg
P : ℂ[X]
hP : 0 < P.degree
z : ℂ
hP₀ : P ≠ 0
hPz : ¬eval z P = 0
⊢ 0 < ∑ w ∈ P.roots.toFinset, P.derivRootWeight z w

Tactic:
·

Goal state after:
case pos
P : ℂ[X]
hP : 0 < P.degree
z : ℂ
hP₀ : P ≠ 0
hPz : eval z P = 0
⊢ 0 < ∑ w ∈ P.roots.toFinset, P.derivRootWeight z w
Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas

Goal state before:
pp: case neg
P : ℂ[X]
hP : 0 < P.degree
z : ℂ
hP₀ : P ≠ 0
hPz : ¬eval z P = 0
⊢ 0 < ∑ w ∈ P.roots.toFinset, P.derivRootWeight z w

Tactic:
·

Goal state after:
case neg
P : ℂ[X]
hP : 0 < P.degree
z : ℂ
hP₀ : P ≠ 0
hPz : ¬eval z P = 0
⊢ 0 < ∑ w ∈ P.roots.toFinset, P.derivRootWeight z w
Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas

Goal state before:
pp: case neg.h
P : ℂ[X]
hP : 0 < P.degree
z : ℂ
hP₀ : P ≠ 0
hPz : ¬eval z P = 0
⊢ ∀ i ∈ P.roots.toFinset, 0 < ↑(rootMultiplicity i P) / ‖z - i‖ ^ 2

pp: case neg.hs
P : ℂ[X]
hP : 0 < P.degree
z : ℂ
hP₀ : P ≠ 0
hPz : ¬eval z P = 0
⊢ P.roots.toFinset.Nonempty

Tactic:
·

Goal state after:
case neg.h
P : ℂ[X]
hP : 0 < P.degree
z : ℂ
hP₀ : P ≠ 0
hPz : ¬eval z P = 0
⊢ ∀ i ∈ P.roots.toFinset, 0 < ↑(rootMultiplicity i P) / ‖z - i‖ ^ 2
Module: Mathlib.Analysis.SpecialFunctions.Integrals.Basic

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

pp: case refine_1
a b : ℝ
n : ℕ
C : ℝ := cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ x ∈ [[a, b]], HasDerivAt (fun y ↦ cos y ^ (n + 1)) (-↑(n + 1) * sin x * cos x ^ n) x
hv : ∀ x ∈ [[a, b]], HasDerivAt sin (cos x) x
⊢ IntervalIntegrable (fun x ↦ -↑(n + 1) * sin x * cos x ^ n) MeasureTheory.volume a b

pp: case refine_2
a b : ℝ
n : ℕ
C : ℝ := cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ x ∈ [[a, b]], HasDerivAt (fun y ↦ cos y ^ (n + 1)) (-↑(n + 1) * sin x * cos x ^ n) x
hv : ∀ x ∈ [[a, b]], HasDerivAt sin (cos x) x
⊢ IntervalIntegrable cos MeasureTheory.volume a b

Tactic:
·

Goal state after:
case refine_3
a b : ℝ
n : ℕ
C : ℝ := cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a
h : ∀ (α β γ : ℝ), β * α * γ * α = β * (α * α * γ)
hu : ∀ x ∈ [[a, b]], HasDerivAt (fun y ↦ cos y ^ (n + 1)) (-↑(n + 1) * sin x * cos x ^ n) x
hv : ∀ x ∈ [[a, b]], HasDerivAt sin (cos x) x
H :
  ∫ (x : ℝ) in a..b, cos x ^ (n + 1) * cos x =
    cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a - ∫ (x : ℝ) in a..b, -↑(n + 1) * sin x * cos x ^ n * sin x
⊢ ∫ (x : ℝ) in a..b, cos x ^ (n + 2) =
    (cos b ^ (n + 1) * sin b - cos a ^ (n + 1) * sin a + (↑n + 1) * ∫ (x : ℝ) in a..b, cos x ^ n) -
      (↑n + 1) * ∫ (x : ℝ) in a..b, cos x ^ (n + 2)
Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas

Goal state before:
pp: case neg.hs
P : ℂ[X]
hP : 0 < P.degree
z : ℂ
hP₀ : P ≠ 0
hPz : ¬eval z P = 0
⊢ P.roots.toFinset.Nonempty

Tactic:
·

Goal state after:
case neg.hs
P : ℂ[X]
hP : 0 < P.degree
z : ℂ
hP₀ : P ≠ 0
hPz : ¬eval z P = 0
⊢ P.roots.toFinset.Nonempty
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: case hF_meas
ρ w : ℂ
R : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
r : ℕ → ℝ
hr_lt : ∀ (n : ℕ), r n < R
hr_tendsto : Tendsto r atTop (𝓝 R)
bound : ℝ → ℝ := ⋯
⊢ ∀ᶠ (n : ℕ) in atTop,
    AEStronglyMeasurable (fun x ↦ herglotzLogIntegrand w ρ (circleMap 0 (r n) x)) (volume.restrict (uIoc 0 (2 * π)))

pp: case h_bound
ρ w : ℂ
R : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
r : ℕ → ℝ
hr_lt : ∀ (n : ℕ), r n < R
hr_tendsto : Tendsto r atTop (𝓝 R)
bound : ℝ → ℝ := ⋯
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ᵐ (x : ℝ), x ∈ uIoc 0 (2 * π) → ‖herglotzLogIntegrand w ρ (circleMap 0 (r n) x)‖ ≤ bound x

pp: case bound_integrable
ρ w : ℂ
R : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
r : ℕ → ℝ
hr_lt : ∀ (n : ℕ), r n < R
hr_tendsto : Tendsto r atTop (𝓝 R)
bound : ℝ → ℝ := ⋯
⊢ IntervalIntegrable bound volume 0 (2 * π)

pp: case h_lim
ρ w : ℂ
R : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
r : ℕ → ℝ
hr_lt : ∀ (n : ℕ), r n < R
hr_tendsto : Tendsto r atTop (𝓝 R)
bound : ℝ → ℝ := ⋯
⊢ ∀ᵐ (x : ℝ),
    x ∈ uIoc 0 (2 * π) →
      Tendsto (fun n ↦ herglotzLogIntegrand w ρ (circleMap 0 (r n) x)) atTop
        (𝓝 (herglotzLogIntegrand w ρ (circleMap 0 R x)))

Tactic:
·

Goal state after:
case hF_meas
ρ w : ℂ
R : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
r : ℕ → ℝ
hr_lt : ∀ (n : ℕ), r n < R
hr_tendsto : Tendsto r atTop (𝓝 R)
bound : ℝ → ℝ := ⋯
⊢ ∀ᶠ (n : ℕ) in atTop,
    AEStronglyMeasurable (fun x ↦ herglotzLogIntegrand w ρ (circleMap 0 (r n) x)) (volume.restrict (uIoc 0 (2 * π)))
Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas

Goal state before:
pp: case pos
P : ℂ[X]
z : ℂ
hP : 0 < P.degree
hz : eval z (derivative P) = 0
weight : ℂ → ℝ := P.derivRootWeight z
s : Finset ℂ := P.roots.toFinset
hzP : eval z P = 0
⊢ ∑ x ∈ s, weight x • (z - x) = 0

pp: case neg
P : ℂ[X]
z : ℂ
hP : 0 < P.degree
hz : eval z (derivative P) = 0
weight : ℂ → ℝ := P.derivRootWeight z
s : Finset ℂ := P.roots.toFinset
hzP : ¬eval z P = 0
⊢ ∑ x ∈ s, weight x • (z - x) = 0

Tactic:
·

Goal state after:
case pos
P : ℂ[X]
z : ℂ
hP : 0 < P.degree
hz : eval z (derivative P) = 0
weight : ℂ → ℝ := P.derivRootWeight z
s : Finset ℂ := P.roots.toFinset
hzP : eval z P = 0
⊢ ∑ x ∈ s, weight x • (z - x) = 0
Module: Mathlib.Analysis.Complex.Periodic

Goal state before:
pp: case inl
h : ℝ
f : ℂ → ℂ
hfcts : ContinuousAt (update (f ∘ invQParam h) 0 ((𝓝[≠] 0).limUnder (f ∘ invQParam h))) 0
a : ℂ
⊢ update ((a • f) ∘ invQParam h) 0 ((𝓝[≠] 0).limUnder ((a • f) ∘ invQParam h)) 0 =
    (a • update (f ∘ invQParam h) 0 ((𝓝[≠] 0).limUnder (f ∘ invQParam h))) 0

pp: case inr
h : ℝ
f : ℂ → ℂ
hfcts : ContinuousAt (update (f ∘ invQParam h) 0 ((𝓝[≠] 0).limUnder (f ∘ invQParam h))) 0
a y : ℂ
hy : y ≠ 0
⊢ update ((a • f) ∘ invQParam h) 0 ((𝓝[≠] 0).limUnder ((a • f) ∘ invQParam h)) y =
    (a • update (f ∘ invQParam h) 0 ((𝓝[≠] 0).limUnder (f ∘ invQParam h))) y

Tactic:
·

Goal state after:
case inl
h : ℝ
f : ℂ → ℂ
hfcts : ContinuousAt (update (f ∘ invQParam h) 0 ((𝓝[≠] 0).limUnder (f ∘ invQParam h))) 0
a : ℂ
⊢ update ((a • f) ∘ invQParam h) 0 ((𝓝[≠] 0).limUnder ((a • f) ∘ invQParam h)) 0 =
    (a • update (f ∘ invQParam h) 0 ((𝓝[≠] 0).limUnder (f ∘ invQParam h))) 0
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: case h_bound
ρ w : ℂ
R : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
r : ℕ → ℝ
hr_lt : ∀ (n : ℕ), r n < R
hr_tendsto : Tendsto r atTop (𝓝 R)
bound : ℝ → ℝ := ⋯
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ᵐ (x : ℝ), x ∈ uIoc 0 (2 * π) → ‖herglotzLogIntegrand w ρ (circleMap 0 (r n) x)‖ ≤ bound x

pp: case bound_integrable
ρ w : ℂ
R : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
r : ℕ → ℝ
hr_lt : ∀ (n : ℕ), r n < R
hr_tendsto : Tendsto r atTop (𝓝 R)
bound : ℝ → ℝ := ⋯
⊢ IntervalIntegrable bound volume 0 (2 * π)

pp: case h_lim
ρ w : ℂ
R : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
r : ℕ → ℝ
hr_lt : ∀ (n : ℕ), r n < R
hr_tendsto : Tendsto r atTop (𝓝 R)
bound : ℝ → ℝ := ⋯
⊢ ∀ᵐ (x : ℝ),
    x ∈ uIoc 0 (2 * π) →
      Tendsto (fun n ↦ herglotzLogIntegrand w ρ (circleMap 0 (r n) x)) atTop
        (𝓝 (herglotzLogIntegrand w ρ (circleMap 0 R x)))

Tactic:
·

Goal state after:
case h_bound
ρ w : ℂ
R : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
r : ℕ → ℝ
hr_lt : ∀ (n : ℕ), r n < R
hr_tendsto : Tendsto r atTop (𝓝 R)
bound : ℝ → ℝ := ⋯
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ᵐ (x : ℝ), x ∈ uIoc 0 (2 * π) → ‖herglotzLogIntegrand w ρ (circleMap 0 (r n) x)‖ ≤ bound x
Module: Mathlib.Analysis.Complex.Periodic

Goal state before:
pp: case inr
h : ℝ
f : ℂ → ℂ
hfcts : ContinuousAt (update (f ∘ invQParam h) 0 ((𝓝[≠] 0).limUnder (f ∘ invQParam h))) 0
a y : ℂ
hy : y ≠ 0
⊢ update ((a • f) ∘ invQParam h) 0 ((𝓝[≠] 0).limUnder ((a • f) ∘ invQParam h)) y =
    (a • update (f ∘ invQParam h) 0 ((𝓝[≠] 0).limUnder (f ∘ invQParam h))) y

Tactic:
·

Goal state after:
case inr
h : ℝ
f : ℂ → ℂ
hfcts : ContinuousAt (update (f ∘ invQParam h) 0 ((𝓝[≠] 0).limUnder (f ∘ invQParam h))) 0
a y : ℂ
hy : y ≠ 0
⊢ update ((a • f) ∘ invQParam h) 0 ((𝓝[≠] 0).limUnder ((a • f) ∘ invQParam h)) y =
    (a • update (f ∘ invQParam h) 0 ((𝓝[≠] 0).limUnder (f ∘ invQParam h))) y
Module: Mathlib.Analysis.Complex.Periodic

Goal state before:
pp: case inl
h : ℝ
f g : ℂ → ℂ
hfcts : ContinuousAt (cuspFunction h f) 0
hgcts : ContinuousAt (cuspFunction h g) 0
y : ℂ
hy : y ≠ 0
⊢ update ((f + g) ∘ invQParam h) 0 ((𝓝[≠] 0).limUnder ((f + g) ∘ invQParam h)) y =
    (update (f ∘ invQParam h) 0 ((𝓝[≠] 0).limUnder (f ∘ invQParam h)) +
        update (g ∘ invQParam h) 0 ((𝓝[≠] 0).limUnder (g ∘ invQParam h)))
      y

pp: case inr
h : ℝ
f g : ℂ → ℂ
hfcts : ContinuousAt (cuspFunction h f) 0
hgcts : ContinuousAt (cuspFunction h g) 0
⊢ update ((f + g) ∘ invQParam h) 0 ((𝓝[≠] 0).limUnder ((f + g) ∘ invQParam h)) 0 =
    (update (f ∘ invQParam h) 0 ((𝓝[≠] 0).limUnder (f ∘ invQParam h)) +
        update (g ∘ invQParam h) 0 ((𝓝[≠] 0).limUnder (g ∘ invQParam h)))
      0

Tactic:
·

Goal state after:
case inl
h : ℝ
f g : ℂ → ℂ
hfcts : ContinuousAt (cuspFunction h f) 0
hgcts : ContinuousAt (cuspFunction h g) 0
y : ℂ
hy : y ≠ 0
⊢ update ((f + g) ∘ invQParam h) 0 ((𝓝[≠] 0).limUnder ((f + g) ∘ invQParam h)) y =
    (update (f ∘ invQParam h) 0 ((𝓝[≠] 0).limUnder (f ∘ invQParam h)) +
        update (g ∘ invQParam h) 0 ((𝓝[≠] 0).limUnder (g ∘ invQParam h)))
      y
Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas

Goal state before:
pp: case hw₀
P : ℂ[X]
h₀ : 0 < P.degree
z : ℂ
hz : derivative P ≠ 0 ∧ eval z (derivative P) = 0
⊢ ∀ i ∈ P.roots.toFinset, 0 ≤ P.derivRootWeight z i

pp: case hws
P : ℂ[X]
h₀ : 0 < P.degree
z : ℂ
hz : derivative P ≠ 0 ∧ eval z (derivative P) = 0
⊢ 0 < ∑ i ∈ P.roots.toFinset, P.derivRootWeight z i

pp: case hz
P : ℂ[X]
h₀ : 0 < P.degree
z : ℂ
hz : derivative P ≠ 0 ∧ eval z (derivative P) = 0
⊢ ∀ i ∈ P.roots.toFinset, id i ∈ P.rootSet ℂ

Tactic:
·

Goal state after:
case hw₀
P : ℂ[X]
h₀ : 0 < P.degree
z : ℂ
hz : derivative P ≠ 0 ∧ eval z (derivative P) = 0
⊢ ∀ i ∈ P.roots.toFinset, 0 ≤ P.derivRootWeight z i
Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas

Goal state before:
pp: case hws
P : ℂ[X]
h₀ : 0 < P.degree
z : ℂ
hz : derivative P ≠ 0 ∧ eval z (derivative P) = 0
⊢ 0 < ∑ i ∈ P.roots.toFinset, P.derivRootWeight z i

pp: case hz
P : ℂ[X]
h₀ : 0 < P.degree
z : ℂ
hz : derivative P ≠ 0 ∧ eval z (derivative P) = 0
⊢ ∀ i ∈ P.roots.toFinset, id i ∈ P.rootSet ℂ

Tactic:
·

Goal state after:
case hws
P : ℂ[X]
h₀ : 0 < P.degree
z : ℂ
hz : derivative P ≠ 0 ∧ eval z (derivative P) = 0
⊢ 0 < ∑ i ∈ P.roots.toFinset, P.derivRootWeight z i
Module: Mathlib.Analysis.Complex.Periodic

Goal state before:
pp: case inr
h : ℝ
f g : ℂ → ℂ
hfcts : ContinuousAt (cuspFunction h f) 0
hgcts : ContinuousAt (cuspFunction h g) 0
⊢ update ((f + g) ∘ invQParam h) 0 ((𝓝[≠] 0).limUnder ((f + g) ∘ invQParam h)) 0 =
    (update (f ∘ invQParam h) 0 ((𝓝[≠] 0).limUnder (f ∘ invQParam h)) +
        update (g ∘ invQParam h) 0 ((𝓝[≠] 0).limUnder (g ∘ invQParam h)))
      0

Tactic:
·

Goal state after:
case inr
h : ℝ
f g : ℂ → ℂ
hfcts : ContinuousAt (cuspFunction h f) 0
hgcts : ContinuousAt (cuspFunction h g) 0
⊢ update ((f + g) ∘ invQParam h) 0 ((𝓝[≠] 0).limUnder ((f + g) ∘ invQParam h)) 0 =
    (update (f ∘ invQParam h) 0 ((𝓝[≠] 0).limUnder (f ∘ invQParam h)) +
        update (g ∘ invQParam h) 0 ((𝓝[≠] 0).limUnder (g ∘ invQParam h)))
      0
Module: Mathlib.Analysis.Complex.Polynomial.GaussLucas

Goal state before:
pp: case hz
P : ℂ[X]
h₀ : 0 < P.degree
z : ℂ
hz : derivative P ≠ 0 ∧ eval z (derivative P) = 0
⊢ ∀ i ∈ P.roots.toFinset, id i ∈ P.rootSet ℂ

Tactic:
·

Goal state after:
case hz
P : ℂ[X]
h₀ : 0 < P.degree
z : ℂ
hz : derivative P ≠ 0 ∧ eval z (derivative P) = 0
⊢ ∀ i ∈ P.roots.toFinset, id i ∈ P.rootSet ℂ
Module: Mathlib.Analysis.Complex.Polynomial.UnitTrinomial

Goal state before:
pp: case refine_1
p : ℤ[X]
hp : p.IsUnitTrinomial
h : ∀ (z : ℂ), ¬((aeval z) p = 0 ∧ (aeval z) p.mirror = 0)
q : ℤ[X]
hq : q ∣ p
hq' : q ∣ p.mirror
hq'' : 0 < (map (algebraMap ℤ ℂ) q).degree
z : ℂ
hz : (aeval z) q = 0
⊢ (aeval z) p = 0

pp: case refine_2
p : ℤ[X]
hp : p.IsUnitTrinomial
h : ∀ (z : ℂ), ¬((aeval z) p = 0 ∧ (aeval z) p.mirror = 0)
q : ℤ[X]
hq : q ∣ p
hq' : q ∣ p.mirror
hq'' : 0 < (map (algebraMap ℤ ℂ) q).degree
z : ℂ
hz : (aeval z) q = 0
⊢ (aeval z) p.mirror = 0

Tactic:
·

Goal state after:
case refine_1
p : ℤ[X]
hp : p.IsUnitTrinomial
h : ∀ (z : ℂ), ¬((aeval z) p = 0 ∧ (aeval z) p.mirror = 0)
q : ℤ[X]
hq : q ∣ p
hq' : q ∣ p.mirror
hq'' : 0 < (map (algebraMap ℤ ℂ) q).degree
z : ℂ
hz : (aeval z) q = 0
⊢ (aeval z) p = 0
Module: Mathlib.Analysis.Complex.Polynomial.UnitTrinomial

Goal state before:
pp: case refine_2
p : ℤ[X]
hp : p.IsUnitTrinomial
h : ∀ (z : ℂ), ¬((aeval z) p = 0 ∧ (aeval z) p.mirror = 0)
q : ℤ[X]
hq : q ∣ p
hq' : q ∣ p.mirror
hq'' : 0 < (map (algebraMap ℤ ℂ) q).degree
z : ℂ
hz : (aeval z) q = 0
⊢ (aeval z) p.mirror = 0

Tactic:
·

Goal state after:
case refine_2
p : ℤ[X]
hp : p.IsUnitTrinomial
h : ∀ (z : ℂ), ¬((aeval z) p = 0 ∧ (aeval z) p.mirror = 0)
q : ℤ[X]
hq : q ∣ p
hq' : q ∣ p.mirror
hq'' : 0 < (map (algebraMap ℤ ℂ) q).degree
z : ℂ
hz : (aeval z) q = 0
⊢ (aeval z) p.mirror = 0
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: case bound_integrable
ρ w : ℂ
R : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
r : ℕ → ℝ
hr_lt : ∀ (n : ℕ), r n < R
hr_tendsto : Tendsto r atTop (𝓝 R)
bound : ℝ → ℝ := ⋯
⊢ IntervalIntegrable bound volume 0 (2 * π)

pp: case h_lim
ρ w : ℂ
R : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
r : ℕ → ℝ
hr_lt : ∀ (n : ℕ), r n < R
hr_tendsto : Tendsto r atTop (𝓝 R)
bound : ℝ → ℝ := ⋯
⊢ ∀ᵐ (x : ℝ),
    x ∈ uIoc 0 (2 * π) →
      Tendsto (fun n ↦ herglotzLogIntegrand w ρ (circleMap 0 (r n) x)) atTop
        (𝓝 (herglotzLogIntegrand w ρ (circleMap 0 R x)))

Tactic:
·

Goal state after:
case bound_integrable
ρ w : ℂ
R : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
r : ℕ → ℝ
hr_lt : ∀ (n : ℕ), r n < R
hr_tendsto : Tendsto r atTop (𝓝 R)
bound : ℝ → ℝ := ⋯
⊢ IntervalIntegrable bound volume 0 (2 * π)
Module: Mathlib.Analysis.Complex.Positivity

Goal state before:
pp: case succ
f : ℂ → ℂ
c : ℂ
hf : Differentiable ℂ f
z : ℂ
hz : c ≤ z
n : ℕ
h : 0 ≤ iteratedDeriv (n + 1) f c
⊢ 0 ≤ iteratedDeriv (n + 1) (fun x ↦ f x - f c) c

Tactic:
rw [iteratedDeriv_succ'] at h ⊢

Goal state after:
case succ
f : ℂ → ℂ
c : ℂ
hf : Differentiable ℂ f
z : ℂ
hz : c ≤ z
n : ℕ
h : 0 ≤ iteratedDeriv n (_root_.deriv f) c
⊢ 0 ≤ iteratedDeriv n (_root_.deriv fun x ↦ f x - f c) c
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: case h_lim
ρ w : ℂ
R : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
r : ℕ → ℝ
hr_lt : ∀ (n : ℕ), r n < R
hr_tendsto : Tendsto r atTop (𝓝 R)
bound : ℝ → ℝ := ⋯
⊢ ∀ᵐ (x : ℝ),
    x ∈ uIoc 0 (2 * π) →
      Tendsto (fun n ↦ herglotzLogIntegrand w ρ (circleMap 0 (r n) x)) atTop
        (𝓝 (herglotzLogIntegrand w ρ (circleMap 0 R x)))

Tactic:
·

Goal state after:
case h_lim
ρ w : ℂ
R : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
r : ℕ → ℝ
hr_lt : ∀ (n : ℕ), r n < R
hr_tendsto : Tendsto r atTop (𝓝 R)
bound : ℝ → ℝ := ⋯
⊢ ∀ᵐ (x : ℝ),
    x ∈ uIoc 0 (2 * π) →
      Tendsto (fun n ↦ herglotzLogIntegrand w ρ (circleMap 0 (r n) x)) atTop
        (𝓝 (herglotzLogIntegrand w ρ (circleMap 0 R x)))
Module: Mathlib.Analysis.Complex.Positivity

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

pp: case e'_4
f : ℂ → ℂ
c : ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ (-1) ^ n * iteratedDeriv n f c
z : ℂ
hz : z ≤ c
⊢ f z = f (- -z)

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

Tactic:
·

Goal state after:
case e'_3
f : ℂ → ℂ
c : ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ (-1) ^ n * iteratedDeriv n f c
z : ℂ
hz : z ≤ c
⊢ f c = f (- -c)
Module: Mathlib.Analysis.Complex.Positivity

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

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

Tactic:
·

Goal state after:
case e'_4
f : ℂ → ℂ
c : ℂ
hf : Differentiable ℂ f
h : ∀ (n : ℕ), n ≠ 0 → 0 ≤ (-1) ^ n * iteratedDeriv n f c
z : ℂ
hz : z ≤ c
⊢ f z = f (- -z)
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
n : ℕ
hn : n ≠ 0
⊢ 0 ≤ iteratedDeriv n (fun z ↦ f (-z)) (-c)

Tactic:
·

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