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

Goal state before:
pp: case h₂f
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|
⊢ |log⁺ ‖f θ‖ - log⁺ ‖f θ - a₀‖| ≤ log⁺ ‖a₀‖ + log 2

Tactic:
by_cases h : 0 ≤ log⁺ ‖f θ‖ - log⁺ ‖f θ - a₀‖

Goal state after:
case pos
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₀‖
⊢ |log⁺ ‖f θ‖ - log⁺ ‖f θ - a₀‖| ≤ log⁺ ‖a₀‖ + log 2

case neg
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₀‖
⊢ |log⁺ ‖f θ‖ - log⁺ ‖f θ - a₀‖| ≤ log⁺ ‖a₀‖ + log 2
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 ↦ f x - a) 0‖ = 0

Tactic:
by

Goal state after:
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}ᶜ
⊢ MeromorphicAt (fun x ↦ a) 0

Tactic:
by

Goal state after:
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
⊢ |characteristic f ⊤ r - characteristic (fun x ↦ f x - a₀) ⊤ r| ≤ log⁺ ‖a₀‖ + log 2

Tactic:
by

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

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
a₀ : E
f : ℂ → E
h : Meromorphic f
R : ℝ
⊢ ‖(characteristic f ⊤ - characteristic (fun x ↦ f x - a₀) ⊤) R‖ ≤ (log⁺ ‖a₀‖ + log 2) * ‖1 R‖

Tactic:
by

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

Goal state before:
pp: f : ℂ → ℂ
h₁ : MeromorphicAt f 0
h₂ : meromorphicOrderAt f 0 = 0
⊢ (fun x ↦ log ‖meromorphicTrailingCoeffAt f 0 - x‖) =ᶠ[codiscreteWithin (sphere 0 |1|)] fun a ↦
    log ‖meromorphicTrailingCoeffAt (fun x ↦ f x - a) 0‖

Tactic:
by

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

Goal state before:
pp: f : ℂ → ℂ
h : ¬MeromorphicAt f 0
a : ℂ
⊢ MeromorphicAt (fun x ↦ a) 0

Tactic:
by

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

Goal state before:
pp: f : ℂ → ℂ
h : ¬MeromorphicAt f 0
a : ℂ
⊢ ¬MeromorphicAt (fun x ↦ f x - a) 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

Goal state before:
pp: f : ℂ → ℂ
R β : ℝ
⊢ IntegrableOn (fun x ↦ cartanKernel f R x β) (Ioc 0 (2 * π)) volume

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
hf : Measurable f
⊢ Measurable fun p ↦ cartanKernel f R p.1 p.2

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

Goal state before:
pp: f : ℂ → ℂ
R β : ℝ
μ : Measure ℝ := volume.restrict (Ioc 0 (2 * π))
z : ℂ := f (circleMap 0 R β)
h_avg : circleAverage (fun x ↦ log ‖z - x‖) 0 1 = log⁺ ‖z‖
⊢ ∫ (α : ℝ), cartanKernel f R α β ∂μ = 2 * π * log⁺ ‖z‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

Goal state before:
pp: f : ℂ → ℂ
R β : ℝ
μ : Measure ℝ := volume.restrict (Ioc 0 (2 * π))
⊢ 2 * ∫ (α : ℝ), (cartanKernel f R α β)⁺ ∂μ - ∫ (α : ℝ), cartanKernel f R α β ∂μ =
    2 * ∫ (α : ℝ), (cartanKernel f R α β)⁺ ∂μ - 2 * π * log⁺ ‖f (circleMap 0 R β)‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

Goal state before:
pp: f : ℂ → ℂ
R β : ℝ
⊢ ∫ (α : ℝ) in Ioc 0 (2 * π), ‖cartanKernel f R α β‖ =
    (2 * ∫ (α : ℝ) in Ioc 0 (2 * π), (cartanKernel f R α β)⁺) - 2 * π * log⁺ ‖f (circleMap 0 R β)‖

Tactic:
by

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

Goal state before:
pp: f : ℂ → ℂ
⊢ CircleIntegrable (fun a ↦ log ‖meromorphicTrailingCoeffAt (fun x ↦ f x - a) 0‖) 0 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
h : Meromorphic f
μ : Measure ℝ := volume.restrict (Ioc 0 (2 * π))
⊢ Measurable fun a ↦ (cartanKernel f R a.1 a.2)⁺

Tactic:
by

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 (fun x ↦ a) 0

Tactic:
by

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 (fun x ↦ f x - a) 0

Tactic:
by

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

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

Tactic:
by

Goal state after:
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)⁺
⊢ Integrable (fun β ↦ log⁺ ‖f (circleMap 0 R β)‖) μ

Tactic:
by

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

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

Tactic:
simp only

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

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

Tactic:
by

Goal state after:
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) μ
β : ℝ
⊢ 0 ≤ ∫ (α : ℝ), (cartanKernel f R α β)⁺ ∂μ

Tactic:
by

Goal state after:
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 α β)⁺ ∂μ
⊢ 0 ≤ 2 * π * (log⁺ ‖f (circleMap 0 R β)‖ + log 2)

Tactic:
by

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

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
h : Meromorphic f
hR : R ≠ 0
a : ℂ
⊢ Meromorphic (f - fun x ↦ a)

Tactic:
by

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

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

Tactic:
by

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

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

Tactic:
by

Goal state after:
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)
⊢ ∀ (x : ℝ), 0 x ≤ (fun α ↦ (cartanKernel f R α β)⁺) x

Tactic:
by

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

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
h : Meromorphic f
⊢ CircleIntegrable (fun x ↦ logCounting f (↑x) R) 0 1

Tactic:
by

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

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

Tactic:
by

Goal state after:
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 α β)⁺ = log⁺ ‖f (circleMap 0 R β) + -circleMap 0 1 α‖

Tactic:
by

Goal state after:
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)
α : ℝ
⊢ log⁺ ‖f (circleMap 0 R β)‖ + log⁺ ‖-circleMap 0 1 α‖ + log 2 = log⁺ ‖f (circleMap 0 R β)‖ + log 2

Tactic:
by

Goal state after:
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)
⊢ ∫ (α : ℝ) in Ioc 0 (2 * π), (cartanKernel f R α β)⁺ ≤ ∫ (x : ℝ) in Ioc 0 (2 * π), log⁺ ‖f (circleMap 0 R β)‖ + log 2

Tactic:
by

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

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

Tactic:
by

Goal state after:
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
⊢ characteristic f ⊤ R = circleAverage (fun x ↦ logCounting f (↑x) R) 0 1

Tactic:
by

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

Goal state before:
pp: f : ℂ → ℂ
h : Meromorphic f
⊢ MonotoneOn (characteristic f ⊤) (Ioi 0)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
h : HasConstantSpeedOnWith f s l
x y : ℝ
hx : x ∈ s
hy : y ∈ s
⊢ BoundedVariationOn f (s ∩ Icc x y)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
hs : s.Subsingleton
l : ℝ≥0
⊢ HasConstantSpeedOnWith f s l

Tactic:
by

Goal state after:
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) μ
⊢ Integrable (fun β ↦ ∫ (α : ℝ), (cartanKernel f R α β)⁺ ∂μ) μ

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

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

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

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

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

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

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.ConstantSpeed

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

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

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

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

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

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

Goal state before:
pp: f : ℂ → ℂ
h : Meromorphic f
R : ℝ
F : ℝ → ℝ → ℝ := Cartan.cartanKernel f R
⊢ circleAverage (fun a ↦ circleAverage (fun x ↦ log ‖f x - a‖) 0 R) 0 1 =
    (2 * π)⁻¹ * (2 * π)⁻¹ * ∫ (α : ℝ) (β : ℝ) in 0..2 * π, F α β

Tactic:
by

Goal state after:
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 ℤ
⊢ (fun r ↦ ∑ᶠ (z : E), ↑(((toClosedBall r) (D₁ + D₂)) z) * log (r * ‖z‖⁻¹) + ↑((D₁ + D₂) 0) * log r) =
    (fun r ↦ ∑ᶠ (z : E), ↑(((toClosedBall r) D₁) z) * log (r * ‖z‖⁻¹) + ↑(D₁ 0) * log r) + fun r ↦
      ∑ᶠ (z : E), ↑(((toClosedBall r) D₂) z) * log (r * ‖z‖⁻¹) + ↑(D₂ 0) * log r

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsupp E ℤ
⊢ logCounting D 0 = 0

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

Goal state before:
pp: f : ℂ → ℂ
h : Meromorphic f
R : ℝ
F : ℝ → ℝ → ℝ := Cartan.cartanKernel f R
⊢ (2 * π)⁻¹ * (2 * π)⁻¹ * ∫ (α : ℝ) (β : ℝ) in 0..2 * π, F α β =
    (2 * π)⁻¹ * (2 * π)⁻¹ * ∫ (β : ℝ) (α : ℝ) in 0..2 * π, F α β

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

Goal state before:
pp: f : ℂ → ℂ
h : Meromorphic f
R : ℝ
F : ℝ → ℝ → ℝ := Cartan.cartanKernel f R
⊢ (2 * π)⁻¹ * (2 * π)⁻¹ * ∫ (β : ℝ) (α : ℝ) in 0..2 * π, F α β =
    (2 * π)⁻¹ * ∫ (β : ℝ) in 0..2 * π, (2 * π)⁻¹ * ∫ (α : ℝ) in 0..2 * π, F α β

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : DecidableEq E
inst✝ : ProperSpace E
e : E
r : ℝ
n : ℤ
hr : ‖e‖ ≤ r
⊢ (Function.support fun z ↦ ↑(((toClosedBall r) (single e n)) z) * log (r * ‖z‖⁻¹)) ⊆ ↑⋯.toFinset

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

Goal state before:
pp: f : ℂ → ℂ
h : Meromorphic f
R : ℝ
F : ℝ → ℝ → ℝ := Cartan.cartanKernel f R
β : ℝ
hβ : β ∈ uIcc 0 (2 * π)
⊢ (2 * π)⁻¹ * ∫ (α : ℝ) in 0..2 * π, F α β = circleAverage (fun x ↦ log ‖f (circleMap 0 R β) - x‖) 0 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

Goal state before:
pp: f : ℂ → ℂ
h : Meromorphic f
R : ℝ
F : ℝ → ℝ → ℝ := Cartan.cartanKernel f R
β : ℝ
hβ : β ∈ uIcc 0 (2 * π)
⊢ circleAverage (fun x ↦ log ‖f (circleMap 0 R β) - x‖) 0 1 = log⁺ ‖f (circleMap 0 R β)‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

Goal state before:
pp: f : ℂ → ℂ
h : Meromorphic f
R : ℝ
F : ℝ → ℝ → ℝ := Cartan.cartanKernel f R
⊢ (2 * π)⁻¹ * ∫ (β : ℝ) in 0..2 * π, (2 * π)⁻¹ * ∫ (α : ℝ) in 0..2 * π, F α β =
    (2 * π)⁻¹ * ∫ (β : ℝ) in 0..2 * π, log⁺ ‖f (circleMap 0 R β)‖

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : DecidableEq E
inst✝ : ProperSpace E
e : E
r : ℝ
n : ℤ
hr : ‖e‖ ≤ r
⊢ e ∈ closedBall 0 |r|

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

Goal state before:
pp: f : ℂ → ℂ
h : Meromorphic f
R : ℝ
F : ℝ → ℝ → ℝ := Cartan.cartanKernel f R
⊢ (2 * π)⁻¹ * ∫ (β : ℝ) in 0..2 * π, log⁺ ‖f (circleMap 0 R β)‖ = circleAverage (fun x ↦ log⁺ ‖f x‖) 0 R

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

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

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
h : Meromorphic f
hR : ¬R = 0
x✝¹ : ℝ
x✝ : x✝¹ ∈ Ioc 0 (2 * π)
⊢ (2 * π)⁻¹ * ∫ (β : ℝ) in 0..2 * π, Cartan.cartanKernel f R x✝¹ β =
    circleAverage (fun x ↦ log ‖f x - circleMap 0 1 x✝¹‖) 0 R

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation

Goal state before:
pp: f : ℂ → ℂ
R : ℝ
h : Meromorphic f
⊢ CircleIntegrable (fun a ↦ circleAverage (fun x ↦ log ‖f x - a‖) 0 R) 0 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : DecidableEq E
inst✝ : ProperSpace E
e : E
r : ℝ
n : ℤ
hr : ‖e‖ ≤ r
⊢ logCounting (single e n) r = ↑n * (log r - log ‖e‖)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsupp E ℤ
r : ℝ
⊢ logCounting D (-r) = logCounting D r

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.AmpleSet

Goal state before:
pp: F : Type u_2
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace ℝ F
⊢ AmpleSet univ

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.AmpleSet

Goal state before:
pp: F : Type u_1
inst✝² : AddCommGroup F
inst✝¹ : Module ℝ F
inst✝ : TopologicalSpace F
s t : Set F
hs : AmpleSet s
ht : AmpleSet t
⊢ AmpleSet (s ∪ t)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.AmpleSet

Goal state before:
pp: F : Type u_1
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module ℝ F
inst✝³ : TopologicalSpace F
E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : Module ℝ E
inst✝ : TopologicalSpace E
s : Set E
h : AmpleSet s
L : E ≃ᴬ[ℝ] F
x : E
hx : x ∈ s
⊢ ⇑L '' (convexHull ℝ) (connectedComponentIn s x) = univ

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.AmpleSet

Goal state before:
pp: F : Type u_1
inst✝⁵ : AddCommGroup F
inst✝⁴ : Module ℝ F
inst✝³ : TopologicalSpace F
E : Type u_2
inst✝² : AddCommGroup E
inst✝¹ : Module ℝ E
inst✝ : TopologicalSpace E
s : Set F
h : AmpleSet s
L : E ≃ᴬ[ℝ] F
⊢ AmpleSet (⇑L ⁻¹' s)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
⊢ HasConstantSpeedOnWith f s l ↔
    LocallyBoundedVariationOn f s ∧ ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → variationOnFromTo f s x y = ↑l * (y - x)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.ConstantSpeed

Goal state before:
pp: E : Type u_2
inst✝ : PseudoEMetricSpace E
f : ℝ → E
s : Set ℝ
l : ℝ≥0
⊢ HasConstantSpeedOnWith f s l ↔
    LocallyBoundedVariationOn f s ∧ ∀ ⦃x : ℝ⦄, x ∈ s → ∀ ⦃y : ℝ⦄, y ∈ s → variationOnFromTo f s x y = ↑l * (y - x)

Tactic:
by
  constructor
  · rintro h; refine ⟨h.hasLocallyBoundedVariationOn, fun x xs y ys => ?_⟩
    rw [hasConstantSpeedOnWith_iff_ordered] at h
    rcases le_total x y with (xy | yx)
    · rw [variationOnFromTo.eq_of_le f s xy, h xs ys xy]
      exact ENNReal.toReal_ofReal (mul_nonneg l.prop (sub_nonneg.mpr xy))
    · rw [variationOnFromTo.eq_of_ge f s yx, h ys xs yx]
      have := ENNReal.toReal_ofReal (mul_nonneg l.prop (sub_nonneg.mpr yx))
      simp_all only [NNReal.val_eq_coe]; ring
  · rw [hasConstantSpeedOnWith_iff_ordered]
    rintro h x xs y ys xy
    rw [← h.2 xs ys, variationOnFromTo.eq_of_le f s xy, ENNReal.ofReal_toReal (h.1 x y xs ys)]

Goal state after:
Module: Mathlib.Analysis.Convex.AmpleSet

Goal state before:
pp: F : Type u_1
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℝ F
inst✝² : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
E : Submodule ℝ F
hcodim : 1 < Module.rank ℝ (F ⧸ E)
x : F
hx : x ∈ (↑E)ᶜ
y : F
h : y ∈ E
⊢ ∃ z, z ∉ E

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic

Goal state before:
pp: E : Type u_1
inst✝² : NormedAddCommGroup E
inst✝¹ : DecidableEq E
inst✝ : ProperSpace E
e : E
⊢ 1 =o[atTop] logCounting (single e 1)

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsuppWithin univ ℤ
h : 0 ≤ D
h₂ : D = 0
⊢ logCounting D =O[atTop] 1

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Convex.AmpleSet

Goal state before:
pp: F : Type u_1
inst✝⁴ : AddCommGroup F
inst✝³ : Module ℝ F
inst✝² : TopologicalSpace F
inst✝¹ : IsTopologicalAddGroup F
inst✝ : ContinuousSMul ℝ F
E : Submodule ℝ F
hcodim : 1 < Module.rank ℝ (F ⧸ E)
x : F
hx : x ∈ (↑E)ᶜ
⊢ (convexHull ℝ) (connectedComponentIn (↑E)ᶜ x) = univ

Tactic:
by

Goal state after:
Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic

Goal state before:
pp: E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : ProperSpace E
D : locallyFinsuppWithin univ ℤ
h : 0 ≤ D
h₁ : ¬D = 0
e : E
he : single e 1 ≤ D
a : ℝ
ha : a > 0
b c : ℝ
hc : ∀ (b : ℝ), c ≤ b → ‖1 b‖ ≤ a * ‖logCounting (single e 1) b‖
ℓ : ℝ := 1 + max ‖e‖ (max |b| |c|)
⊢ c ≤ ℓ

Tactic:
by

Goal state after: