mathlib-initiative/mathlib-tactics huggingface dataset:
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: E✝ : Type u_1
inst✝² : NormedAddCommGroup E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D₁ D₂ : locallyFinsupp E ℤ
r : ℝ
this : ∀ {A B C D : ℝ}, A + B + (C + D) = A + C + (B + D)
⊢ ∑ᶠ (z : E), (↑(((toClosedBall r) D₁) z) + ↑(((toClosedBall r) D₂) z)) * log (r * ‖z‖⁻¹) +
      (↑(D₁ 0) + ↑(D₂ 0)) * log r =
    ∑ᶠ (z : E), ↑(((toClosedBall r) D₁) z) * log (r * ‖z‖⁻¹) +
        ∑ᶠ (z : E), ↑(((toClosedBall r) D₂) z) * log (r * ‖z‖⁻¹) +
      (↑(D₁ 0) * log r + ↑(D₂ 0) * log r)

Tactic:
]

Goal state after:
E✝ : Type u_1
inst✝² : NormedAddCommGroup E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D₁ D₂ : locallyFinsupp E ℤ
r : ℝ
this : ∀ {A B C D : ℝ}, A + B + (C + D) = A + C + (B + D)
⊢ ∑ᶠ (z : E), (↑(((toClosedBall r) D₁) z) + ↑(((toClosedBall r) D₂) z)) * log (r * ‖z‖⁻¹) +
      (↑(D₁ 0) + ↑(D₂ 0)) * log r =
    ∑ᶠ (z : E), ↑(((toClosedBall r) D₁) z) * log (r * ‖z‖⁻¹) +
        ∑ᶠ (z : E), ↑(((toClosedBall r) D₂) z) * log (r * ‖z‖⁻¹) +
      (↑(D₁ 0) * log r + ↑(D₂ 0) * log r)
Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a₀ : E
f : ℂ → E
r : ℝ
h : Meromorphic f
h₁f : CircleIntegrable (fun x ↦ log⁺ ‖f x‖) 0 r
h₂f : CircleIntegrable (fun x ↦ log⁺ ‖f x - a₀‖) 0 r
⊢ |(proximity f ⊤ - proximity (fun x ↦ f x - a₀) ⊤) r| ≤ log⁺ ‖a₀‖ + log 2

Tactic:
]

Goal state after:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a₀ : E
f : ℂ → E
r : ℝ
h : Meromorphic f
h₁f : CircleIntegrable (fun x ↦ log⁺ ‖f x‖) 0 r
h₂f : CircleIntegrable (fun x ↦ log⁺ ‖f x - a₀‖) 0 r
⊢ |(proximity f ⊤ - proximity (fun x ↦ f x - a₀) ⊤) r| ≤ log⁺ ‖a₀‖ + log 2
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: case e_a
E✝ : Type u_1
inst✝² : NormedAddCommGroup E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D₁ D₂ : locallyFinsupp E ℤ
r : ℝ
this : ∀ {A B C D : ℝ}, A + B + (C + D) = A + C + (B + D)
h₁s : (((toClosedBall r) D₁).support ∪ ((toClosedBall r) D₂).support).Finite
⊢ ∑ i ∈ h₁s.toFinset, (↑(((toClosedBall r) D₁) i) + ↑(((toClosedBall r) D₂) i)) * log (r * ‖i‖⁻¹) =
    ∑ᶠ (z : E), ↑(((toClosedBall r) D₁) z) * log (r * ‖z‖⁻¹) + ∑ᶠ (z : E), ↑(((toClosedBall r) D₂) z) * log (r * ‖z‖⁻¹)

pp: case e_a.h
E✝ : Type u_1
inst✝² : NormedAddCommGroup E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D₁ D₂ : locallyFinsupp E ℤ
r : ℝ
this : ∀ {A B C D : ℝ}, A + B + (C + D) = A + C + (B + D)
h₁s : (((toClosedBall r) D₁).support ∪ ((toClosedBall r) D₂).support).Finite
⊢ (Function.support fun z ↦ (↑(((toClosedBall r) D₁) z) + ↑(((toClosedBall r) D₂) z)) * log (r * ‖z‖⁻¹)) ⊆ ↑h₁s.toFinset

Tactic:
]

Goal state after:
case e_a
E✝ : Type u_1
inst✝² : NormedAddCommGroup E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D₁ D₂ : locallyFinsupp E ℤ
r : ℝ
this : ∀ {A B C D : ℝ}, A + B + (C + D) = A + C + (B + D)
h₁s : (((toClosedBall r) D₁).support ∪ ((toClosedBall r) D₂).support).Finite
⊢ ∑ i ∈ h₁s.toFinset, (↑(((toClosedBall r) D₁) i) + ↑(((toClosedBall r) D₂) i)) * log (r * ‖i‖⁻¹) =
    ∑ᶠ (z : E), ↑(((toClosedBall r) D₁) z) * log (r * ‖z‖⁻¹) + ∑ᶠ (z : E), ↑(((toClosedBall r) D₂) z) * log (r * ‖z‖⁻¹)

case e_a.h
E✝ : Type u_1
inst✝² : NormedAddCommGroup E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D₁ D₂ : locallyFinsupp E ℤ
r : ℝ
this : ∀ {A B C D : ℝ}, A + B + (C + D) = A + C + (B + D)
h₁s : (((toClosedBall r) D₁).support ∪ ((toClosedBall r) D₂).support).Finite
⊢ (Function.support fun z ↦ (↑(((toClosedBall r) D₁) z) + ↑(((toClosedBall r) D₂) z)) * log (r * ‖z‖⁻¹)) ⊆ ↑h₁s.toFinset
Module: Mathlib.Analysis.Complex.UpperHalfPlane.ProperAction

Goal state before:
pp: 𝒢 : Subgroup SL(2, ℝ)
inst✝ : DiscreteTopology ↥𝒢
this : IsClosed ↑𝒢
⊢ ProperSMul ↥𝒢 ℍ

Tactic:
]

Goal state after:
𝒢 : Subgroup SL(2, ℝ)
inst✝ : DiscreteTopology ↥𝒢
this : IsClosed ↑𝒢
⊢ ProperSMul ↥𝒢 ℍ
Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan

Goal state before:
pp: f : ℂ → ℂ
a : ℂ
h : 0 < meromorphicOrderAt f 0
ha : a ∈ sphere 0 |1|
⊢ log ‖meromorphicTrailingCoeffAt (fun x ↦ -a) 0‖ = 0

pp: f : ℂ → ℂ
a : ℂ
h : 0 < meromorphicOrderAt f 0
ha : a ∈ sphere 0 |1|
⊢ meromorphicOrderAt (fun x ↦ -a) 0 < meromorphicOrderAt f 0

Tactic:
]

Goal state after:
f : ℂ → ℂ
a : ℂ
h : 0 < meromorphicOrderAt f 0
ha : a ∈ sphere 0 |1|
⊢ log ‖meromorphicTrailingCoeffAt (fun x ↦ -a) 0‖ = 0

f : ℂ → ℂ
a : ℂ
h : 0 < meromorphicOrderAt f 0
ha : a ∈ sphere 0 |1|
⊢ meromorphicOrderAt (fun x ↦ -a) 0 < meromorphicOrderAt f 0
Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem

Goal state before:
pp: case e'_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a₀ : E
f : ℂ → E
r : ℝ
h✝ : Meromorphic f
h₁f : CircleIntegrable (fun x ↦ log⁺ ‖f x‖) 0 r
h₂f : CircleIntegrable (fun x ↦ log⁺ ‖f x - a₀‖) 0 r
θ : ℂ
hθ : θ ∈ sphere 0 |r|
h : ¬0 ≤ log⁺ ‖f θ‖ - log⁺ ‖f θ - a₀‖
⊢ ‖-(f θ - a₀)‖ = ‖-f θ + a₀‖

Tactic:
]

Goal state after:
case e'_3
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a₀ : E
f : ℂ → E
r : ℝ
h✝ : Meromorphic f
h₁f : CircleIntegrable (fun x ↦ log⁺ ‖f x‖) 0 r
h₂f : CircleIntegrable (fun x ↦ log⁺ ‖f x - a₀‖) 0 r
θ : ℂ
hθ : θ ∈ sphere 0 |r|
h : ¬0 ≤ log⁺ ‖f θ‖ - log⁺ ‖f θ - a₀‖
⊢ ‖-(f θ - a₀)‖ = ‖-f θ + a₀‖
Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan

Goal state before:
pp: f : ℂ → ℂ
a : ℂ
h : 0 < meromorphicOrderAt f 0
ha : a ∈ sphere 0 |1|
⊢ (if -a = 0 then ⊤ else 0) < meromorphicOrderAt f 0

Tactic:
]

Goal state after:
f : ℂ → ℂ
a : ℂ
h : 0 < meromorphicOrderAt f 0
ha : a ∈ sphere 0 |1|
⊢ (if -a = 0 then ⊤ else 0) < meromorphicOrderAt f 0
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: case e_a
E✝ : Type u_1
inst✝² : NormedAddCommGroup E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D₁ D₂ : locallyFinsupp E ℤ
r : ℝ
this : ∀ {A B C D : ℝ}, A + B + (C + D) = A + C + (B + D)
h₁s : (((toClosedBall r) D₁).support ∪ ((toClosedBall r) D₂).support).Finite
⊢ ∑ i ∈ h₁s.toFinset, (↑(((toClosedBall r) D₁) i) + ↑(((toClosedBall r) D₂) i)) * log (r * ‖i‖⁻¹) =
    ∑ i ∈ h₁s.toFinset, ↑(((toClosedBall r) D₁) i) * log (r * ‖i‖⁻¹) +
      ∑ᶠ (z : E), ↑(((toClosedBall r) D₂) z) * log (r * ‖z‖⁻¹)

pp: case e_a.h
E✝ : Type u_1
inst✝² : NormedAddCommGroup E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D₁ D₂ : locallyFinsupp E ℤ
r : ℝ
this : ∀ {A B C D : ℝ}, A + B + (C + D) = A + C + (B + D)
h₁s : (((toClosedBall r) D₁).support ∪ ((toClosedBall r) D₂).support).Finite
⊢ (Function.support fun z ↦ ↑(((toClosedBall r) D₁) z) * log (r * ‖z‖⁻¹)) ⊆ ↑h₁s.toFinset

pp: case e_a.h
E✝ : Type u_1
inst✝² : NormedAddCommGroup E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D₁ D₂ : locallyFinsupp E ℤ
r : ℝ
this : ∀ {A B C D : ℝ}, A + B + (C + D) = A + C + (B + D)
h₁s : (((toClosedBall r) D₁).support ∪ ((toClosedBall r) D₂).support).Finite
⊢ (Function.support fun z ↦ (↑(((toClosedBall r) D₁) z) + ↑(((toClosedBall r) D₂) z)) * log (r * ‖z‖⁻¹)) ⊆ ↑h₁s.toFinset

Tactic:
]

Goal state after:
case e_a
E✝ : Type u_1
inst✝² : NormedAddCommGroup E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D₁ D₂ : locallyFinsupp E ℤ
r : ℝ
this : ∀ {A B C D : ℝ}, A + B + (C + D) = A + C + (B + D)
h₁s : (((toClosedBall r) D₁).support ∪ ((toClosedBall r) D₂).support).Finite
⊢ ∑ i ∈ h₁s.toFinset, (↑(((toClosedBall r) D₁) i) + ↑(((toClosedBall r) D₂) i)) * log (r * ‖i‖⁻¹) =
    ∑ i ∈ h₁s.toFinset, ↑(((toClosedBall r) D₁) i) * log (r * ‖i‖⁻¹) +
      ∑ᶠ (z : E), ↑(((toClosedBall r) D₂) z) * log (r * ‖z‖⁻¹)

case e_a.h
E✝ : Type u_1
inst✝² : NormedAddCommGroup E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D₁ D₂ : locallyFinsupp E ℤ
r : ℝ
this : ∀ {A B C D : ℝ}, A + B + (C + D) = A + C + (B + D)
h₁s : (((toClosedBall r) D₁).support ∪ ((toClosedBall r) D₂).support).Finite
⊢ (Function.support fun z ↦ ↑(((toClosedBall r) D₁) z) * log (r * ‖z‖⁻¹)) ⊆ ↑h₁s.toFinset

case e_a.h
E✝ : Type u_1
inst✝² : NormedAddCommGroup E✝
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D₁ D₂ : locallyFinsupp E ℤ
r : ℝ
this : ∀ {A B C D : ℝ}, A + B + (C + D) = A + C + (B + D)
h₁s : (((toClosedBall r) D₁).support ∪ ((toClosedBall r) D₂).support).Finite
⊢ (Function.support fun z ↦ (↑(((toClosedBall r) D₁) z) + ↑(((toClosedBall r) D₂) z)) * log (r * ‖z‖⁻¹)) ⊆ ↑h₁s.toFinset
Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan

Goal state before:
pp: f : ℂ → ℂ
h₁ : MeromorphicAt f 0
h₂ : meromorphicOrderAt f 0 = 0
a : ℂ
ha_sphere : a ∈ sphere 0 |1|
ha_ne : a ∈ {meromorphicTrailingCoeffAt f 0}ᶜ
⊢ meromorphicTrailingCoeffAt f 0 + -a = meromorphicTrailingCoeffAt f 0 + -a

pp: case h₁
f : ℂ → ℂ
h₁ : MeromorphicAt f 0
h₂ : meromorphicOrderAt f 0 = 0
a : ℂ
ha_sphere : a ∈ sphere 0 |1|
ha_ne : a ∈ {meromorphicTrailingCoeffAt f 0}ᶜ
⊢ meromorphicOrderAt f 0 = meromorphicOrderAt (fun x ↦ a) 0

pp: case h₂
f : ℂ → ℂ
h₁ : MeromorphicAt f 0
h₂ : meromorphicOrderAt f 0 = 0
a : ℂ
ha_sphere : a ∈ sphere 0 |1|
ha_ne : a ∈ {meromorphicTrailingCoeffAt f 0}ᶜ
⊢ meromorphicTrailingCoeffAt f 0 - meromorphicTrailingCoeffAt (fun x ↦ a) 0 ≠ 0

Tactic:
]

Goal state after:
case h₁
f : ℂ → ℂ
h₁ : MeromorphicAt f 0
h₂ : meromorphicOrderAt f 0 = 0
a : ℂ
ha_sphere : a ∈ sphere 0 |1|
ha_ne : a ∈ {meromorphicTrailingCoeffAt f 0}ᶜ
⊢ meromorphicOrderAt f 0 = meromorphicOrderAt (fun x ↦ a) 0

case h₂
f : ℂ → ℂ
h₁ : MeromorphicAt f 0
h₂ : meromorphicOrderAt f 0 = 0
a : ℂ
ha_sphere : a ∈ sphere 0 |1|
ha_ne : a ∈ {meromorphicTrailingCoeffAt f 0}ᶜ
⊢ meromorphicTrailingCoeffAt f 0 - meromorphicTrailingCoeffAt (fun x ↦ a) 0 ≠ 0
Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan

Goal state before:
pp: f : ℂ → ℂ
h : ¬MeromorphicAt f 0
a : ℂ
⊢ ¬MeromorphicAt f 0

Tactic:
]

Goal state after:
f : ℂ → ℂ
h : ¬MeromorphicAt f 0
a : ℂ
⊢ ¬MeromorphicAt f 0
Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan

Goal state before:
pp: case neg.inl
f : ℂ → ℂ
h : ¬¬MeromorphicAt f 0
hneg : meromorphicOrderAt f 0 < 0
a : ℂ
ha : a ∈ sphere 0 |1|
⊢ log ‖meromorphicTrailingCoeffAt f 0‖ = log ‖meromorphicTrailingCoeffAt f 0‖

pp: case neg.inl
f : ℂ → ℂ
h : ¬¬MeromorphicAt f 0
hneg : meromorphicOrderAt f 0 < 0
a : ℂ
ha : a ∈ sphere 0 |1|
⊢ meromorphicOrderAt f 0 < meromorphicOrderAt (fun x ↦ a) 0

Tactic:
]

Goal state after:
case neg.inl
f : ℂ → ℂ
h : ¬¬MeromorphicAt f 0
hneg : meromorphicOrderAt f 0 < 0
a : ℂ
ha : a ∈ sphere 0 |1|
⊢ meromorphicOrderAt f 0 < meromorphicOrderAt (fun x ↦ a) 0
Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan

Goal state before:
pp: case neg.inl
f : ℂ → ℂ
h : ¬¬MeromorphicAt f 0
hneg : meromorphicOrderAt f 0 < 0
a : ℂ
ha : a ∈ sphere 0 |1|
⊢ meromorphicOrderAt f 0 < if a = 0 then ⊤ else 0

Tactic:
]

Goal state after:
case neg.inl
f : ℂ → ℂ
h : ¬¬MeromorphicAt f 0
hneg : meromorphicOrderAt f 0 < 0
a : ℂ
ha : a ∈ sphere 0 |1|
⊢ meromorphicOrderAt f 0 < if a = 0 then ⊤ else 0
Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan

Goal state before:
pp: case pos
f : ℂ → ℂ
h : meromorphicOrderAt f 0 = 0
hf : MeromorphicAt f 0
⊢ circleAverage (fun x ↦ log ‖meromorphicTrailingCoeffAt f 0 - x‖) 0 1 = log⁺ ‖meromorphicTrailingCoeffAt f 0‖

Tactic:
]

Goal state after:
case pos
f : ℂ → ℂ
h : meromorphicOrderAt f 0 = 0
hf : MeromorphicAt f 0
⊢ circleAverage (fun x ↦ log ‖meromorphicTrailingCoeffAt f 0 - x‖) 0 1 = log⁺ ‖meromorphicTrailingCoeffAt f 0‖
Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan

Goal state before:
pp: case pos
f : ℂ → ℂ
h : meromorphicOrderAt f 0 = 0
hf : MeromorphicAt f 0
⊢ log⁺ ‖meromorphicTrailingCoeffAt f 0‖ = log⁺ ‖meromorphicTrailingCoeffAt f 0‖

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan

Goal state before:
pp: f : ℂ → ℂ
h : meromorphicOrderAt f 0 = 0
hf : ¬MeromorphicAt f 0
a : ℂ
⊢ ¬MeromorphicAt f 0

Tactic:
]

Goal state after:
f : ℂ → ℂ
h : meromorphicOrderAt f 0 = 0
hf : ¬MeromorphicAt f 0
a : ℂ
⊢ ¬MeromorphicAt f 0
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
h : Meromorphic f
μ : Measure ℝ := volume.restrict (Ioc 0 (2 * π))
h_meas_K : Measurable fun a ↦ (cartanKernel f R a.1 a.2)⁺
this : IntegrableOn (fun θ ↦ log⁺ ‖f (circleMap 0 R θ)‖) (Ioc 0 (2 * π)) volume
⊢ Integrable (fun β ↦ log⁺ ‖f (circleMap 0 R β)‖) μ

Tactic:
]

Goal state after:
f : ℂ → ℂ
R : ℝ
h : Meromorphic f
μ : Measure ℝ := volume.restrict (Ioc 0 (2 * π))
h_meas_K : Measurable fun a ↦ (cartanKernel f R a.1 a.2)⁺
this : IntegrableOn (fun θ ↦ log⁺ ‖f (circleMap 0 R θ)‖) (Ioc 0 (2 * π)) volume
⊢ Integrable (fun β ↦ log⁺ ‖f (circleMap 0 R β)‖) μ
Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan

Goal state before:
pp: f : ℂ → ℂ
h : meromorphicOrderAt f 0 < 0
⊢ log ‖meromorphicTrailingCoeffAt f 0‖ = log ‖meromorphicTrailingCoeffAt f 0‖

pp: f : ℂ → ℂ
h : meromorphicOrderAt f 0 < 0
⊢ EqOn (fun a ↦ log ‖meromorphicTrailingCoeffAt (fun x ↦ f x - a) 0‖) (fun x ↦ log ‖meromorphicTrailingCoeffAt f 0‖)
    (sphere 0 |1|)

Tactic:
]

Goal state after:
f : ℂ → ℂ
h : meromorphicOrderAt f 0 < 0
⊢ EqOn (fun a ↦ log ‖meromorphicTrailingCoeffAt (fun x ↦ f x - a) 0‖) (fun x ↦ log ‖meromorphicTrailingCoeffAt f 0‖)
    (sphere 0 |1|)
Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan

Goal state before:
pp: f : ℂ → ℂ
h : meromorphicOrderAt f 0 < 0
a : ℂ
ha : a ∈ sphere 0 |1|
⊢ meromorphicTrailingCoeffAt f 0 = meromorphicTrailingCoeffAt f 0

pp: f : ℂ → ℂ
h : meromorphicOrderAt f 0 < 0
a : ℂ
ha : a ∈ sphere 0 |1|
⊢ meromorphicOrderAt f 0 < meromorphicOrderAt (fun x ↦ a) 0

Tactic:
]

Goal state after:
f : ℂ → ℂ
h : meromorphicOrderAt f 0 < 0
a : ℂ
ha : a ∈ sphere 0 |1|
⊢ meromorphicOrderAt f 0 < meromorphicOrderAt (fun x ↦ a) 0
Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan

Goal state before:
pp: f : ℂ → ℂ
h : meromorphicOrderAt f 0 < 0
a : ℂ
ha : a ∈ sphere 0 |1|
⊢ meromorphicOrderAt f 0 < if a = 0 then ⊤ else 0

Tactic:
]

Goal state after:
f : ℂ → ℂ
h : meromorphicOrderAt f 0 < 0
a : ℂ
ha : a ∈ sphere 0 |1|
⊢ meromorphicOrderAt f 0 < if a = 0 then ⊤ else 0
Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
h : Meromorphic f
hR : R ≠ 0
a : ℂ
⊢ logCounting (f - fun x ↦ a) 0 R - logCounting (f - fun x ↦ ?m.127) ⊤ R =
    circleAverage (fun x ↦ log ‖f x - a‖) 0 R - log ‖meromorphicTrailingCoeffAt (fun x ↦ f x - a) 0‖

pp: f : ℂ → ℂ
R : ℝ
h : Meromorphic f
hR : R ≠ 0
a : ℂ
⊢ ℂ

Tactic:
]

Goal state after:
f : ℂ → ℂ
R : ℝ
h : Meromorphic f
hR : R ≠ 0
a : ℂ
⊢ logCounting (f - fun x ↦ a) 0 R - logCounting (f - fun x ↦ ?m.127) ⊤ R =
    circleAverage (fun x ↦ log ‖f x - a‖) 0 R - log ‖meromorphicTrailingCoeffAt (fun x ↦ f x - a) 0‖

f : ℂ → ℂ
R : ℝ
h : Meromorphic f
hR : R ≠ 0
a : ℂ
⊢ ℂ
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
h : Meromorphic f
μ : Measure ℝ := volume.restrict (Ioc 0 (2 * π))
h_meas_K : Measurable fun a ↦ (cartanKernel f R a.1 a.2)⁺
h_int_posLog : Integrable (fun β ↦ log⁺ ‖f (circleMap 0 R β)‖) μ
h_int_Bound : Integrable (fun β ↦ log⁺ ‖f (circleMap 0 R β)‖ + log 2) μ
β : ℝ
h_int_nonneg : 0 ≤ ∫ (α : ℝ), (cartanKernel f R α β)⁺ ∂μ
h_bound_nonneg : 0 ≤ 2 * π * (log⁺ ‖f (circleMap 0 R β)‖ + log 2)
⊢ ∫ (α : ℝ), (cartanKernel f R α β)⁺ ∂μ ≤ 2 * π * (log⁺ ‖f (circleMap 0 R β)‖ + log 2)

Tactic:
]

Goal state after:
f : ℂ → ℂ
R : ℝ
h : Meromorphic f
μ : Measure ℝ := volume.restrict (Ioc 0 (2 * π))
h_meas_K : Measurable fun a ↦ (cartanKernel f R a.1 a.2)⁺
h_int_posLog : Integrable (fun β ↦ log⁺ ‖f (circleMap 0 R β)‖) μ
h_int_Bound : Integrable (fun β ↦ log⁺ ‖f (circleMap 0 R β)‖ + log 2) μ
β : ℝ
h_int_nonneg : 0 ≤ ∫ (α : ℝ), (cartanKernel f R α β)⁺ ∂μ
h_bound_nonneg : 0 ≤ 2 * π * (log⁺ ‖f (circleMap 0 R β)‖ + log 2)
⊢ ∫ (α : ℝ), (cartanKernel f R α β)⁺ ∂μ ≤ 2 * π * (log⁺ ‖f (circleMap 0 R β)‖ + log 2)
Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
h : Meromorphic f
hR : R ≠ 0
⊢ (fun R ↦ circleAverage (fun a ↦ circleAverage (fun x ↦ log ‖f x - a‖) 0 R) 0 1) R + logCounting f ⊤ R =
    circleAverage (fun a ↦ circleAverage (fun x ↦ log ‖f x - a‖) 0 R) 0 1 + logCounting f ⊤ R

Tactic:
]

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
h : Meromorphic f
hR : R ≠ 0
⊢ circleAverage ?m.195 0 1 =
    circleAverage ((fun x ↦ logCounting f (↑x) R) + fun a ↦ log ‖meromorphicTrailingCoeffAt (fun x ↦ f x - a) 0‖) 0 1

pp: f : ℂ → ℂ
R : ℝ
h : Meromorphic f
hR : R ≠ 0
⊢ EqOn (fun a ↦ circleAverage (fun x ↦ log ‖f x - a‖) 0 R + logCounting f ⊤ R) ?m.195 (sphere 0 |1|)

pp: f : ℂ → ℂ
R : ℝ
h : Meromorphic f
hR : R ≠ 0
⊢ ℂ → ℝ

Tactic:
]

Goal state after:
f : ℂ → ℂ
R : ℝ
h : Meromorphic f
hR : R ≠ 0
⊢ EqOn (fun a ↦ circleAverage (fun x ↦ log ‖f x - a‖) 0 R + logCounting f ⊤ R)
    ((fun x ↦ logCounting f (↑x) R) + fun a ↦ log ‖meromorphicTrailingCoeffAt (fun x ↦ f x - a) 0‖) (sphere 0 |1|)
Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
h₁f : Meromorphic f
h₂f : 0 < meromorphicOrderAt f 0
hR : R ≠ 0
⊢ circleAverage (fun x ↦ logCounting f (↑x) R) 0 1 +
      circleAverage (fun a ↦ log ‖meromorphicTrailingCoeffAt (fun x ↦ f x - a) 0‖) 0 1 =
    circleAverage (fun x ↦ logCounting f (↑x) R) 0 1

Tactic:
]

Goal state after:
f : ℂ → ℂ
R : ℝ
h₁f : Meromorphic f
h₂f : 0 < meromorphicOrderAt f 0
hR : R ≠ 0
⊢ circleAverage (fun x ↦ logCounting f (↑x) R) 0 1 +
      circleAverage (fun a ↦ log ‖meromorphicTrailingCoeffAt (fun x ↦ f x - a) 0‖) 0 1 =
    circleAverage (fun x ↦ logCounting f (↑x) R) 0 1
Module: Mathlib.Analysis.Complex.ValueDistribution.Cartan

Goal state before:
pp: f : ℂ → ℂ
h : Meromorphic f
a : ℝ
ha : a ∈ Ioi 0
b : ℝ
hb : b ∈ Ioi 0
hab : a ≤ b
⊢ circleAverage (fun x ↦ logCounting f (↑x) a) 0 1 +
      circleAverage (fun a ↦ log ‖meromorphicTrailingCoeffAt (fun x ↦ f x - a) 0‖) 0 1 ≤
    circleAverage (fun x ↦ logCounting f (↑x) b) 0 1 +
      circleAverage (fun a ↦ log ‖meromorphicTrailingCoeffAt (fun x ↦ f x - a) 0‖) 0 1

Tactic:
]

Goal state after:
f : ℂ → ℂ
h : Meromorphic f
a : ℝ
ha : a ∈ Ioi 0
b : ℝ
hb : b ∈ Ioi 0
hab : a ≤ b
⊢ circleAverage (fun x ↦ logCounting f (↑x) a) 0 1 +
      circleAverage (fun a ↦ log ‖meromorphicTrailingCoeffAt (fun x ↦ f x - a) 0‖) 0 1 ≤
    circleAverage (fun x ↦ logCounting f (↑x) b) 0 1 +
      circleAverage (fun a ↦ log ‖meromorphicTrailingCoeffAt (fun x ↦ f x - a) 0‖) 0 1
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: case refl
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
hs : s.Subsingleton
l : ℝ≥0
x : ℝ
hx hy : x ∈ s
⊢ 0 = ENNReal.ofReal (↑l * (x - x))

Tactic:
]

Goal state after:
case refl
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
hs : s.Subsingleton
l : ℝ≥0
x : ℝ
hx hy : x ∈ s
⊢ 0 = ENNReal.ofReal (↑l * (x - x))
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: case inr
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
yx : y ≤ x
⊢ 0 = 0

pp: case inr
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
yx : y ≤ x
⊢ ↑l * (y - x) ≤ 0

pp: case inr.hs
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
yx : y ≤ x
⊢ (s ∩ Icc x y).Subsingleton

Tactic:
]

Goal state after:
case inr
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
yx : y ≤ x
⊢ ↑l * (y - x) ≤ 0

case inr.hs
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
yx : y ≤ x
⊢ (s ∩ Icc x y).Subsingleton
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
h : Meromorphic f
μ : Measure ℝ := volume.restrict (Ioc 0 (2 * π))
h_meas_K : Measurable fun a ↦ (cartanKernel f R a.1 a.2)⁺
h_int_posLog : Integrable (fun β ↦ log⁺ ‖f (circleMap 0 R β)‖) μ
h_int_Bound : Integrable (fun β ↦ log⁺ ‖f (circleMap 0 R β)‖ + log 2) μ
β : ℝ
h_int_nonneg : 0 ≤ ∫ (α : ℝ), (cartanKernel f R α β)⁺ ∂μ
h_bound_nonneg : 0 ≤ 2 * π * (log⁺ ‖f (circleMap 0 R β)‖ + log 2)
this : ∫ (α : ℝ) in Ioc 0 (2 * π), (cartanKernel f R α β)⁺ ≤ 2 * π * (log⁺ ‖f (circleMap 0 R β)‖ + log 2)
⊢ ∫ (α : ℝ), (cartanKernel f R α β)⁺ ∂μ ≤ 2 * π * (log⁺ ‖f (circleMap 0 R β)‖ + log 2)

Tactic:
]

Goal state after:
f : ℂ → ℂ
R : ℝ
h : Meromorphic f
μ : Measure ℝ := volume.restrict (Ioc 0 (2 * π))
h_meas_K : Measurable fun a ↦ (cartanKernel f R a.1 a.2)⁺
h_int_posLog : Integrable (fun β ↦ log⁺ ‖f (circleMap 0 R β)‖) μ
h_int_Bound : Integrable (fun β ↦ log⁺ ‖f (circleMap 0 R β)‖ + log 2) μ
β : ℝ
h_int_nonneg : 0 ≤ ∫ (α : ℝ), (cartanKernel f R α β)⁺ ∂μ
h_bound_nonneg : 0 ≤ 2 * π * (log⁺ ‖f (circleMap 0 R β)‖ + log 2)
this : ∫ (α : ℝ) in Ioc 0 (2 * π), (cartanKernel f R α β)⁺ ≤ 2 * π * (log⁺ ‖f (circleMap 0 R β)‖ + log 2)
⊢ ∫ (α : ℝ), (cartanKernel f R α β)⁺ ∂μ ≤ 2 * π * (log⁺ ‖f (circleMap 0 R β)‖ + log 2)
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
h : Meromorphic f
⊢ Integrable (fun p ↦ cartanKernel f R p.1 p.2)
    ((volume.restrict (uIoc 0 (2 * π))).prod (volume.restrict (uIoc 0 (2 * π))))

Tactic:
]

Goal state after:
f : ℂ → ℂ
R : ℝ
h : Meromorphic f
⊢ Integrable (fun p ↦ cartanKernel f R p.1 p.2)
    ((volume.restrict (uIoc 0 (2 * π))).prod (volume.restrict (uIoc 0 (2 * π))))
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
h : Meromorphic f
h_int :
  Integrable (fun p ↦ cartanKernel f R p.1 p.2)
    ((volume.restrict (Ioc 0 (2 * π))).prod (volume.restrict (Ioc 0 (2 * π))))
⊢ IntegrableOn (fun x ↦ ∫ (α : ℝ) in 0..2 * π, cartanKernel f R α x) (Ioc 0 (2 * π)) volume

Tactic:
]

Goal state after:
f : ℂ → ℂ
R : ℝ
h : Meromorphic f
h_int :
  Integrable (fun p ↦ cartanKernel f R p.1 p.2)
    ((volume.restrict (Ioc 0 (2 * π))).prod (volume.restrict (Ioc 0 (2 * π))))
⊢ IntegrableOn (fun x ↦ ∫ (α : ℝ) in 0..2 * π, cartanKernel f R α x) (Ioc 0 (2 * π)) volume
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: case mp
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
⊢ variationOnFromTo f s x y = ↑l * (y - x)

Tactic:
]

Goal state after:
case mp
E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → x ≤ y → eVariationOn f (s ∩ Icc x y) = ENNReal.ofReal (↑l * (y - x))
x : ℝ
xs : x ∈ s
y : ℝ
ys : y ∈ s
⊢ variationOnFromTo f s x y = ↑l * (y - x)
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
h : Meromorphic f
h_int :
  Integrable (fun p ↦ cartanKernel f R p.1 p.2)
    ((volume.restrict (Ioc 0 (2 * π))).prod (volume.restrict (Ioc 0 (2 * π))))
⊢ IntegrableOn (fun x ↦ ∫ (β : ℝ) in 0..2 * π, cartanKernel f R x β) (Ioc 0 (2 * π)) volume

Tactic:
]

Goal state after:
f : ℂ → ℂ
R : ℝ
h : Meromorphic f
h_int :
  Integrable (fun p ↦ cartanKernel f R p.1 p.2)
    ((volume.restrict (Ioc 0 (2 * π))).prod (volume.restrict (Ioc 0 (2 * π))))
⊢ IntegrableOn (fun x ↦ ∫ (β : ℝ) in 0..2 * π, cartanKernel f R x β) (Ioc 0 (2 * π)) volume