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

Goal state before:
pp: case pos
c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall c |R|)
CB : Set ℂ := closedBall c |R|
h₂f : ∀ u ∈ CB, meromorphicOrderAt f u ≠ ⊤
⊢ circleAverage (fun x ↦ log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * log (R * ‖c - u‖⁻¹) +
        ↑((divisor f (closedBall c |R|)) c) * log R +
      log ‖meromorphicTrailingCoeffAt f c‖

pp: case neg
c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall c |R|)
CB : Set ℂ := closedBall c |R|
h₂f : ¬∀ u ∈ CB, meromorphicOrderAt f u ≠ ⊤
⊢ circleAverage (fun x ↦ log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * log (R * ‖c - u‖⁻¹) +
        ↑((divisor f (closedBall c |R|)) c) * log R +
      log ‖meromorphicTrailingCoeffAt f c‖

Tactic:
·

Goal state after:
case pos
c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall c |R|)
CB : Set ℂ := closedBall c |R|
h₂f : ∀ u ∈ CB, meromorphicOrderAt f u ≠ ⊤
⊢ circleAverage (fun x ↦ log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * log (R * ‖c - u‖⁻¹) +
        ↑((divisor f (closedBall c |R|)) c) * log R +
      log ‖meromorphicTrailingCoeffAt f c‖
Module: Mathlib.Order.Monotone.Union

Goal state before:
pp: case inr
α : 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
B : ∀ x ∈ s ∪ t, c ≤ x → x ∈ t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
hxy : x < y
hcx : c ≤ x
⊢ f x < f y

Tactic:
·

Goal state after:
case inr
α : 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
B : ∀ x ∈ s ∪ t, c ≤ x → x ∈ t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
hxy : x < y
hcx : c ≤ x
⊢ f x < f y
Module: Mathlib.Order.Monotone.Union

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

pp: case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
x : α
hxc : x ≤ c
h✝ : x ∈ t
⊢ x ∈ s

Tactic:
·

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
x : α
hxc : x ≤ c
h✝ : x ∈ s
⊢ x ∈ s
Module: Mathlib.Order.Monotone.Union

Goal state before:
pp: case inr.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s t : Set α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
x : α
h✝ : x ∈ t
hs : IsGreatest s x
ht : IsLeast t x
hxc : x ≤ x
⊢ x ∈ s

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

Tactic:
·

Goal state after:
case inr.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s t : Set α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
x : α
h✝ : x ∈ t
hs : IsGreatest s x
ht : IsLeast t x
hxc : x ≤ x
⊢ x ∈ s
Module: Mathlib.Order.Monotone.Union

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

pp: case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s
x : α
hx✝ : x ∈ s ∪ t
hxc : c ≤ x
hx : x ∈ s
h'x : c < x
⊢ x ∈ t

Tactic:
·

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s
hx✝ : c ∈ s ∪ t
hxc : c ≤ c
hx : c ∈ s
⊢ c ∈ t
Module: Mathlib.Order.Monotone.Union

Goal state before:
pp: case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s
B : ∀ x ∈ s ∪ t, c ≤ x → x ∈ t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
hxy : x ≤ y
hxc : x < c
⊢ f x ≤ f y

pp: case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s
B : ∀ x ∈ s ∪ t, c ≤ x → x ∈ t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
hxy : x ≤ y
hcx : c ≤ x
⊢ f x ≤ f y

Tactic:
·

Goal state after:
case inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s
B : ∀ x ∈ s ∪ t, c ≤ x → x ∈ t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
hxy : x ≤ y
hxc : x < c
⊢ f x ≤ f y
Module: Mathlib.Order.Monotone.Union

Goal state before:
pp: case inl.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s
B : ∀ x ∈ s ∪ t, c ≤ x → x ∈ t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
hxy : x ≤ y
hxc : x < c
xs : x ∈ s
hyc : y < c
⊢ f x ≤ f y

pp: case inl.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s
B : ∀ x ∈ s ∪ t, c ≤ x → x ∈ t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
hxy : x ≤ y
hxc : x < c
xs : x ∈ s
hcy : c ≤ y
⊢ f x ≤ f y

Tactic:
·

Goal state after:
case inl.inl
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s
B : ∀ x ∈ s ∪ t, c ≤ x → x ∈ t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
hxy : x ≤ y
hxc : x < c
xs : x ∈ s
hyc : y < c
⊢ f x ≤ f y
Module: Mathlib.Order.Monotone.Union

Goal state before:
pp: case inl.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s
B : ∀ x ∈ s ∪ t, c ≤ x → x ∈ t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
hxy : x ≤ y
hxc : x < c
xs : x ∈ s
hcy : c ≤ y
⊢ f x ≤ f y

Tactic:
·

Goal state after:
case inl.inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s
B : ∀ x ∈ s ∪ t, c ≤ x → x ∈ t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
hxy : x ≤ y
hxc : x < c
xs : x ∈ s
hcy : c ≤ y
⊢ f x ≤ f y
Module: Mathlib.Order.Monotone.Union

Goal state before:
pp: case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s
B : ∀ x ∈ s ∪ t, c ≤ x → x ∈ t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
hxy : x ≤ y
hcx : c ≤ x
⊢ f x ≤ f y

Tactic:
·

Goal state after:
case inr
α : Type u_1
β : Type u_2
inst✝¹ : LinearOrder α
inst✝ : Preorder β
f : α → β
s t : Set α
c : α
h₁ : MonotoneOn f s
h₂ : MonotoneOn f t
hs : IsGreatest s c
ht : IsLeast t c
A : ∀ x ∈ s ∪ t, x ≤ c → x ∈ s
B : ∀ x ∈ s ∪ t, c ≤ x → x ∈ t
x : α
hx : x ∈ s ∪ t
y : α
hy : y ∈ s ∪ t
hxy : x ≤ y
hcx : c ≤ x
⊢ f x ≤ f y
Module: Mathlib.Order.Interval.Set.IsoIoo

Goal state before:
pp: case refine_1
k : Type u_1
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : IsStrictOrderedRing k
⊢ k → ↑(Ioo (-1) 1)

pp: case refine_2
k : Type u_1
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : IsStrictOrderedRing k
⊢ StrictMono ?refine_1

pp: case refine_3
k : Type u_1
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : IsStrictOrderedRing k
⊢ Function.RightInverse (fun x ↦ ↑x / (1 - |↑x|)) ?refine_1

Tactic:
·

Goal state after:
case refine_1
k : Type u_1
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : IsStrictOrderedRing k
⊢ k → ↑(Ioo (-1) 1)
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall c |R|)
CB : Set ℂ := closedBall c |R|
h₂f : ∀ u ∈ CB, meromorphicOrderAt f u ≠ ⊤
h₃f : (divisor f CB).support.Finite
g : ℂ → ℂ
h₁g : AnalyticOnNhd ℂ g (closedBall c |R|)
h₂g : ∀ (u : ↑(closedBall c |R|)), g ↑u ≠ 0
h₃g : f =ᶠ[codiscreteWithin (closedBall c |R|)] (∏ᶠ (u : ℂ), (fun x ↦ x - u) ^ (divisor f (closedBall c |R|)) u) • g
⊢ ∑ᶠ (i : ℂ), (↑((divisor f CB) i) * log R - ↑((divisor f CB) i) * log ‖c - i‖) + log ‖meromorphicTrailingCoeffAt f c‖ =
    ∑ᶠ (u : ℂ), ↑((divisor f CB) u) * (log R - log ‖c - u‖) + log ‖meromorphicTrailingCoeffAt f c‖

pp: case hf
c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall c |R|)
CB : Set ℂ := closedBall c |R|
h₂f : ∀ u ∈ CB, meromorphicOrderAt f u ≠ ⊤
h₃f : (divisor f CB).support.Finite
g : ℂ → ℂ
h₁g : AnalyticOnNhd ℂ g (closedBall c |R|)
h₂g : ∀ (u : ↑(closedBall c |R|)), g ↑u ≠ 0
h₃g : f =ᶠ[codiscreteWithin (closedBall c |R|)] (∏ᶠ (u : ℂ), (fun x ↦ x - u) ^ (divisor f (closedBall c |R|)) u) • g
⊢ Function.HasFiniteSupport fun u ↦ ↑((divisor f CB) u) * log R

pp: case hg
c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall c |R|)
CB : Set ℂ := closedBall c |R|
h₂f : ∀ u ∈ CB, meromorphicOrderAt f u ≠ ⊤
h₃f : (divisor f CB).support.Finite
g : ℂ → ℂ
h₁g : AnalyticOnNhd ℂ g (closedBall c |R|)
h₂g : ∀ (u : ↑(closedBall c |R|)), g ↑u ≠ 0
h₃g : f =ᶠ[codiscreteWithin (closedBall c |R|)] (∏ᶠ (u : ℂ), (fun x ↦ x - u) ^ (divisor f (closedBall c |R|)) u) • g
⊢ Function.HasFiniteSupport fun u ↦ ↑((divisor f CB) u) * log ‖c - u‖

Tactic:
·

Goal state after:
c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall c |R|)
CB : Set ℂ := closedBall c |R|
h₂f : ∀ u ∈ CB, meromorphicOrderAt f u ≠ ⊤
h₃f : (divisor f CB).support.Finite
g : ℂ → ℂ
h₁g : AnalyticOnNhd ℂ g (closedBall c |R|)
h₂g : ∀ (u : ↑(closedBall c |R|)), g ↑u ≠ 0
h₃g : f =ᶠ[codiscreteWithin (closedBall c |R|)] (∏ᶠ (u : ℂ), (fun x ↦ x - u) ^ (divisor f (closedBall c |R|)) u) • g
⊢ ∑ᶠ (i : ℂ), (↑((divisor f CB) i) * log R - ↑((divisor f CB) i) * log ‖c - i‖) + log ‖meromorphicTrailingCoeffAt f c‖ =
    ∑ᶠ (u : ℂ), ↑((divisor f CB) u) * (log R - log ‖c - u‖) + log ‖meromorphicTrailingCoeffAt f c‖
Module: Mathlib.Order.Interval.Set.IsoIoo

Goal state before:
pp: case refine_2
k : Type u_1
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : IsStrictOrderedRing k
⊢ StrictMono (codRestrict (fun x ↦ x / (1 + |x|)) (Ioo (-1) 1) ⋯)

pp: case refine_3
k : Type u_1
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : IsStrictOrderedRing k
⊢ Function.RightInverse (fun x ↦ ↑x / (1 - |↑x|)) (codRestrict (fun x ↦ x / (1 + |x|)) (Ioo (-1) 1) ⋯)

Tactic:
·

Goal state after:
case refine_2
k : Type u_1
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : IsStrictOrderedRing k
⊢ StrictMono (codRestrict (fun x ↦ x / (1 + |x|)) (Ioo (-1) 1) ⋯)
Module: Mathlib.Order.Interval.Set.IsoIoo

Goal state before:
pp: case refine_2.refine_1
k : Type u_1
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : IsStrictOrderedRing k
⊢ ∀ (x : k), -x / (1 + |(-x)|) = -(x / (1 + |x|))

pp: case refine_2.refine_2
k : Type u_1
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : IsStrictOrderedRing k
⊢ StrictMonoOn (fun x ↦ x / (1 + |x|)) (Ici 0)

Tactic:
·

Goal state after:
case refine_2.refine_1
k : Type u_1
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : IsStrictOrderedRing k
⊢ ∀ (x : k), -x / (1 + |(-x)|) = -(x / (1 + |x|))
Module: Mathlib.Order.Interval.Set.IsoIoo

Goal state before:
pp: case refine_2.refine_2
k : Type u_1
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : IsStrictOrderedRing k
⊢ StrictMonoOn (fun x ↦ x / (1 + |x|)) (Ici 0)

Tactic:
·

Goal state after:
case refine_2.refine_2
k : Type u_1
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : IsStrictOrderedRing k
⊢ StrictMonoOn (fun x ↦ x / (1 + |x|)) (Ici 0)
Module: Mathlib.Order.Interval.Set.IsoIoo

Goal state before:
pp: case refine_3
k : Type u_1
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : IsStrictOrderedRing k
⊢ Function.RightInverse (fun x ↦ ↑x / (1 - |↑x|)) (codRestrict (fun x ↦ x / (1 + |x|)) (Ioo (-1) 1) ⋯)

Tactic:
·

Goal state after:
case refine_3
k : Type u_1
inst✝² : Field k
inst✝¹ : LinearOrder k
inst✝ : IsStrictOrderedRing k
⊢ Function.RightInverse (fun x ↦ ↑x / (1 - |↑x|)) (codRestrict (fun x ↦ x / (1 + |x|)) (Ioo (-1) 1) ⋯)
Module: Mathlib.Analysis.RCLike.Sqrt

Goal state before:
pp: case pos
a : ℂ
h : 0 ≤ a.im
⊢ a ^ 2⁻¹ = ↑(a ^ 2⁻¹).re + (if 0 ≤ a.im then 1 else -1) * ↑√((‖a‖ - a.re) / 2) * I

pp: case neg
a : ℂ
h : a.im < 0
⊢ a ^ 2⁻¹ = ↑(a ^ 2⁻¹).re + (if 0 ≤ a.im then 1 else -1) * ↑√((‖a‖ - a.re) / 2) * I

Tactic:
·

Goal state after:
case pos
a : ℂ
h : 0 ≤ a.im
⊢ a ^ 2⁻¹ = ↑(a ^ 2⁻¹).re + (if 0 ≤ a.im then 1 else -1) * ↑√((‖a‖ - a.re) / 2) * I
Module: Mathlib.Analysis.RCLike.Sqrt

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a : 𝕜
h : im I = 1
⊢ (complexRingEquiv h).symm ((complexRingEquiv h) a).sqrt = (map ℂ 𝕜) ((map 𝕜 ℂ) a).sqrt

pp: case neg
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a : 𝕜
h : ¬im I = 1
⊢ ↑√(re a) = (map ℂ 𝕜) ((map 𝕜 ℂ) a).sqrt

Tactic:
·

Goal state after:
case pos
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a : 𝕜
h : im I = 1
⊢ (complexRingEquiv h).symm ((complexRingEquiv h) a).sqrt = (map ℂ 𝕜) ((map 𝕜 ℂ) a).sqrt
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: case neg
c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall c |R|)
CB : Set ℂ := closedBall c |R|
h₂f : ¬∀ u ∈ CB, meromorphicOrderAt f u ≠ ⊤
⊢ circleAverage (fun x ↦ log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * log (R * ‖c - u‖⁻¹) +
        ↑((divisor f (closedBall c |R|)) c) * log R +
      log ‖meromorphicTrailingCoeffAt f c‖

Tactic:
·

Goal state after:
case neg
c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall c |R|)
CB : Set ℂ := closedBall c |R|
h₂f : ¬∀ u ∈ CB, meromorphicOrderAt f u ≠ ⊤
⊢ circleAverage (fun x ↦ log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * log (R * ‖c - u‖⁻¹) +
        ↑((divisor f (closedBall c |R|)) c) * log R +
      log ‖meromorphicTrailingCoeffAt f c‖
Module: Mathlib.Analysis.RCLike.Sqrt

Goal state before:
pp: case neg
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a : 𝕜
h : ¬0 = 1
this : I = 0
⊢ √(re a) = √((‖↑(re a) + ↑0 * I‖ + (↑(re a) + ↑0 * I).re) / 2)

Tactic:
by_cases! ha' : 0 ≤ re a

Goal state after:
case pos
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a : 𝕜
h : ¬0 = 1
this : I = 0
ha' : 0 ≤ re a
⊢ √(re a) = √((‖↑(re a) + ↑0 * I‖ + (↑(re a) + ↑0 * I).re) / 2)

case neg
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a : 𝕜
h : ¬0 = 1
this : I = 0
ha' : re a < 0
⊢ √(re a) = √((‖↑(re a) + ↑0 * I‖ + (↑(re a) + ↑0 * I).re) / 2)
Module: Mathlib.Analysis.RCLike.Sqrt

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a : 𝕜
h : ¬0 = 1
this : I = 0
ha' : 0 ≤ re a
⊢ √(re a) = √((‖↑(re a) + ↑0 * I‖ + (↑(re a) + ↑0 * I).re) / 2)

pp: case neg
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a : 𝕜
h : ¬0 = 1
this : I = 0
ha' : re a < 0
⊢ √(re a) = √((‖↑(re a) + ↑0 * I‖ + (↑(re a) + ↑0 * I).re) / 2)

Tactic:
·

Goal state after:
case pos
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a : 𝕜
h : ¬0 = 1
this : I = 0
ha' : 0 ≤ re a
⊢ √(re a) = √((‖↑(re a) + ↑0 * I‖ + (↑(re a) + ↑0 * I).re) / 2)
Module: Mathlib.Analysis.RCLike.Sqrt

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a : 𝕜
h : I = 0
⊢ (map ℂ 𝕜)
      (↑√((‖(map 𝕜 ℂ) a‖ + ((map 𝕜 ℂ) a).re) / 2) +
        (if 0 ≤ ((map 𝕜 ℂ) a).im then 1 else -1) * ↑√((‖(map 𝕜 ℂ) a‖ - ((map 𝕜 ℂ) a).re) / 2) * Complex.I) =
    ↑√((‖a‖ + re a) / 2) + (if 0 ≤ im a then 1 else -1) * ↑√((‖a‖ - re a) / 2) * I

pp: case inr
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a : 𝕜
h : im I = 1
⊢ (map ℂ 𝕜)
      (↑√((‖(map 𝕜 ℂ) a‖ + ((map 𝕜 ℂ) a).re) / 2) +
        (if 0 ≤ ((map 𝕜 ℂ) a).im then 1 else -1) * ↑√((‖(map 𝕜 ℂ) a‖ - ((map 𝕜 ℂ) a).re) / 2) * Complex.I) =
    ↑√((‖a‖ + re a) / 2) + (if 0 ≤ im a then 1 else -1) * ↑√((‖a‖ - re a) / 2) * I

Tactic:
·

Goal state after:
case inl
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a : 𝕜
h : I = 0
⊢ (map ℂ 𝕜)
      (↑√((‖(map 𝕜 ℂ) a‖ + ((map 𝕜 ℂ) a).re) / 2) +
        (if 0 ≤ ((map 𝕜 ℂ) a).im then 1 else -1) * ↑√((‖(map 𝕜 ℂ) a‖ - ((map 𝕜 ℂ) a).re) / 2) * Complex.I) =
    ↑√((‖a‖ + re a) / 2) + (if 0 ≤ im a then 1 else -1) * ↑√((‖a‖ - re a) / 2) * I
Module: Mathlib.Analysis.RCLike.Sqrt

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a : 𝕜
ha : 0 ≤ a
h : I = 0
⊢ sqrt a = ↑√(re a)

pp: case inr
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a : 𝕜
ha : 0 ≤ a
h : im I = 1
⊢ sqrt a = ↑√(re a)

Tactic:
·

Goal state after:
case inl
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a : 𝕜
ha : 0 ≤ a
h : I = 0
⊢ sqrt a = ↑√(re a)
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: case neg
c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall c |R|)
CB : Set ℂ := closedBall c |R|
h₂f✝ : ¬∀ u ∈ CB, meromorphicOrderAt f u ≠ ⊤
h₂f : ∀ (u : ↑(closedBall c |R|)), meromorphicOrderAt f ↑u = ⊤
this✝ : divisor f CB = 0
this : f =ᶠ[codiscreteWithin CB] 0
⊢ circleAverage 0 c R = 0

pp: c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall c |R|)
CB : Set ℂ := closedBall c |R|
h₂f✝ : ¬∀ u ∈ CB, meromorphicOrderAt f u ≠ ⊤
h₂f : ∀ (u : ↑(closedBall c |R|)), meromorphicOrderAt f ↑u = ⊤
this✝ : divisor f CB = 0
this : f =ᶠ[codiscreteWithin CB] 0
⊢ (fun x ↦ log ‖f x‖) =ᶠ[codiscreteWithin (sphere c |R|)] 0

Tactic:
·

Goal state after:
case neg
c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall c |R|)
CB : Set ℂ := closedBall c |R|
h₂f✝ : ¬∀ u ∈ CB, meromorphicOrderAt f u ≠ ⊤
h₂f : ∀ (u : ↑(closedBall c |R|)), meromorphicOrderAt f ↑u = ⊤
this✝ : divisor f CB = 0
this : f =ᶠ[codiscreteWithin CB] 0
⊢ circleAverage 0 c R = 0
Module: Mathlib.Analysis.RCLike.Sqrt

Goal state before:
pp: case inl
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a : 𝕜
ha : 0 ≤ a
h : I = 0
⊢ sqrt (-a) = I * sqrt a

pp: case inr
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a : 𝕜
ha : 0 ≤ a
h : im I = 1
⊢ sqrt (-a) = I * sqrt a

Tactic:
·

Goal state after:
case inl
𝕜 : Type u_1
inst✝ : RCLike 𝕜
a : 𝕜
ha : 0 ≤ a
h : I = 0
⊢ sqrt (-a) = I * sqrt a
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
⊢ ↑(∑ᶠ (u : ℂ), (divisor f (closedBall c |r|)) u) ≤ ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |r|)) u)

pp: c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
⊢ ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |r|)) u) ≤ Real.log (M / ‖f c‖) / Real.log (R / r)

Tactic:
·

Goal state after:
c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
⊢ ↑(∑ᶠ (u : ℂ), (divisor f (closedBall c |r|)) u) ≤ ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |r|)) u)
Module: Mathlib.Analysis.RCLike.Sqrt

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝ : RCLike 𝕜
h : im I = 1
⊢ (complexRingEquiv h).symm ((complexRingEquiv h) I).sqrt = ↑√2⁻¹ * (1 - I) * I

pp: case neg
𝕜 : Type u_1
inst✝ : RCLike 𝕜
h : ¬im I = 1
⊢ ↑√(re I) = ↑√2⁻¹ * (1 - I) * I

Tactic:
·

Goal state after:
case pos
𝕜 : Type u_1
inst✝ : RCLike 𝕜
h : im I = 1
⊢ (complexRingEquiv h).symm ((complexRingEquiv h) I).sqrt = ↑√2⁻¹ * (1 - I) * I
Module: Mathlib.Analysis.RCLike.Sqrt

Goal state before:
pp: case pos
𝕜 : Type u_1
inst✝ : RCLike 𝕜
h : im I = 1
⊢ (complexRingEquiv h).symm ((complexRingEquiv h) (-I)).sqrt = ↑√2⁻¹ * (1 + I) * -I

pp: case neg
𝕜 : Type u_1
inst✝ : RCLike 𝕜
h : ¬im I = 1
⊢ ↑√(re (-I)) = ↑√2⁻¹ * (1 + I) * -I

Tactic:
·

Goal state after:
case pos
𝕜 : Type u_1
inst✝ : RCLike 𝕜
h : im I = 1
⊢ (complexRingEquiv h).symm ((complexRingEquiv h) (-I)).sqrt = ↑√2⁻¹ * (1 + I) * -I
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: case hf
c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun x ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
⊢ CircleIntegrable (fun x ↦ Real.log ‖f x‖) c R

pp: case h₂f
c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun x ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
⊢ ∀ x ∈ sphere c |R|, Real.log ‖f x‖ ≤ Real.log M

Tactic:
·

Goal state after:
case hf
c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun x ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
⊢ CircleIntegrable (fun x ↦ Real.log ‖f x‖) c R
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: case h₂f
c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun x ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
⊢ ∀ x ∈ sphere c |R|, Real.log ‖f x‖ ≤ Real.log M

Tactic:
·

Goal state after:
case h₂f
c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun x ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
⊢ ∀ x ∈ sphere c |R|, Real.log ‖f x‖ ≤ Real.log M
Module: Mathlib.Analysis.Complex.JensenFormula

Goal state before:
pp: case h₂f.h.h.inl
c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun x ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
z : ℂ
hz : z ∈ sphere c |R|
this : ‖f z‖ ≤ M
h : f z = 0
⊢ Real.log ‖f z‖ ≤ Real.log M

pp: case h₂f.h.h.inr
c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun x ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
z : ℂ
hz : z ∈ sphere c |R|
this : ‖f z‖ ≤ M
h : 0 < ‖f z‖
⊢ Real.log ‖f z‖ ≤ Real.log M

Tactic:
·

Goal state after:
case h₂f.h.h.inl
c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun x ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), ↑((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
z : ℂ
hz : z ∈ sphere c |R|
this : ‖f z‖ ≤ M
h : f z = 0
⊢ Real.log ‖f z‖ ≤ Real.log M