awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
R : ℝ
f : ℂ → ℂ
h : Meromorphic f
hR : R ≠ 0
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ :
  ∀ (x : ℂ), Membership.mem (γ := Set ℂ) (closedBall 0 |R|) x → MeromorphicAt f x
⊢ MeromorphicOn f (closedBall 0 |R|)

Tactic:
tauto
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
R : ℝ
f : ℂ → ℂ
h : Meromorphic f
hR : R ≠ 0
⊢ MeromorphicOn f (closedBall 0 |R|)

Tactic:
have h₁f : MeromorphicOn f (closedBall 0 |R|) := by tauto
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
R : ℝ
f : ℂ → ℂ
h : Meromorphic f
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall 0 |R|)
simp :
  ∑ᶠ (z : ℂ),
        (↑((((toClosedBall R : (a : locallyFinsupp ℂ ℤ) → locallyFinsuppWithin (closedBall 0 |R|) ℤ) (divisor f univ) :
                    locallyFinsuppWithin (X := ℂ) (closedBall 0 |R|) ℤ) :
                  (a : ℂ) → ℤ)
                z) :
            ℝ) *
          log (R * ‖z‖⁻¹) +
      (↑((divisor f univ : (a : ℂ) → ℤ) 0) : ℝ) * log R =
    ∑ᶠ (u : ℂ), (↑((divisor f (closedBall 0 |R|) : (a : ℂ) → ℤ) u) : ℝ) * log (R * ‖u‖⁻¹) +
      (↑((divisor f (closedBall 0 |R|) : (a : ℂ) → ℤ) 0) : ℝ) * log R
⊢ (logCounting : (a : locallyFinsupp ℂ ℤ) → ℝ → ℝ) (divisor f univ) R =
    circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 R - log ‖meromorphicTrailingCoeffAt f 0‖

Tactic:
simp only [MeromorphicOn.circleAverage_log_norm hR h₁f, logCounting, AddMonoidHom.coe_mk,
    ZeroHom.coe_mk, zero_sub, norm_neg, add_sub_cancel_right]

Premises used: AddMonoidHom.coe_mk, Function.locallyFinsuppWithin.logCounting, ZeroHom.coe_mk, MeromorphicOn.circleAverage_log_norm, norm_neg, add_sub_cancel_right, zero_sub
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
R : ℝ
f : ℂ → ℂ
h : Meromorphic f
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall 0 |R|)
e_a :
  Eq (α := ℝ)
    (∑ᶠ (z : ℂ),
      (↑((((toClosedBall R : (a : locallyFinsupp ℂ ℤ) → locallyFinsuppWithin (closedBall 0 |R|) ℤ) (divisor f univ) :
                  locallyFinsuppWithin (X := ℂ) (closedBall 0 |R|) ℤ) :
                (a : ℂ) → ℤ)
              z) :
          ℝ) *
        log (R * ‖z‖⁻¹))
    (∑ᶠ (u : ℂ), (↑((divisor f (closedBall 0 |R|) : (a : ℂ) → ℤ) u) : ℝ) * log (R * ‖u‖⁻¹))
e_a₁ :
  (↑((divisor f univ : (a : ℂ) → ℤ) 0) : ℝ) * log R = (↑((divisor f (closedBall 0 |R|) : (a : ℂ) → ℤ) 0) : ℝ) * log R
⊢ ∑ᶠ (z : ℂ),
        (↑((((toClosedBall R : (a : locallyFinsupp ℂ ℤ) → locallyFinsuppWithin (closedBall 0 |R|) ℤ) (divisor f univ) :
                    locallyFinsuppWithin (X := ℂ) (closedBall 0 |R|) ℤ) :
                  (a : ℂ) → ℤ)
                z) :
            ℝ) *
          log (R * ‖z‖⁻¹) +
      (↑((divisor f univ : (a : ℂ) → ℤ) 0) : ℝ) * log R =
    ∑ᶠ (u : ℂ), (↑((divisor f (closedBall 0 |R|) : (a : ℂ) → ℤ) u) : ℝ) * log (R * ‖u‖⁻¹) +
      (↑((divisor f (closedBall 0 |R|) : (a : ℂ) → ℤ) 0) : ℝ) * log R

Tactic:
congr 1
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
R : ℝ
f : ℂ → ℂ
h : Meromorphic f
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall 0 |R|)
⊢ Eq (α := ℝ)
    (∑ᶠ (z : ℂ),
      (↑((((toClosedBall R : (a : locallyFinsupp ℂ ℤ) → locallyFinsuppWithin (closedBall 0 |R|) ℤ) (divisor f univ) :
                  locallyFinsuppWithin (X := ℂ) (closedBall 0 |R|) ℤ) :
                (a : ℂ) → ℤ)
              z) :
          ℝ) *
        log (R * ‖z‖⁻¹))
    (∑ᶠ (u : ℂ), (↑((divisor f (closedBall 0 |R|) : (a : ℂ) → ℤ) u) : ℝ) * log (R * ‖u‖⁻¹))

Tactic:
simp_all
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
R : ℝ
f : ℂ → ℂ
h : Meromorphic f
hR : R ≠ 0
h₁f e_a : MeromorphicOn f (closedBall 0 |R|)
e_a₁ : Membership.mem (γ := Set ℂ) (closedBall 0 |R|) 0
e_a₂ : MeromorphicOn f univ
e_a₃ : Membership.mem (γ := Set ℂ) univ 0
⊢ (↑((divisor f univ : (a : ℂ) → ℤ) 0) : ℝ) * log R = (↑((divisor f (closedBall 0 |R|) : (a : ℂ) → ℤ) 0) : ℝ) * log R

Tactic:
rw [divisor_apply, divisor_apply]

Premises used: MeromorphicOn.divisor_apply
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
R : ℝ
f : ℂ → ℂ
h : Meromorphic f
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall 0 |R|)
⊢ MeromorphicOn f (closedBall 0 |R|)

Tactic:
aesop
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
R : ℝ
f : ℂ → ℂ
h : Meromorphic f
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall 0 |R|)
⊢ Membership.mem (γ := Set ℂ) (closedBall 0 |R|) 0

Tactic:
aesop
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
R : ℝ
f : ℂ → ℂ
h : Meromorphic f
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall 0 |R|)
⊢ MeromorphicOn f univ

Tactic:
aesop
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
R : ℝ
f : ℂ → ℂ
h : Meromorphic f
hR : R ≠ 0
h₁f : MeromorphicOn f (closedBall 0 |R|)
⊢ Membership.mem (γ := Set ℂ) univ 0

Tactic:
aesop
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
R : ℝ
f : ℂ → ℂ
h : Meromorphic f
hR : R ≠ 0
rw :
  (locallyFinsuppWithin.logCounting : (a : locallyFinsupp ℂ ℤ) → ℝ → ℝ) (divisor f univ) R =
    circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 R - log ‖meromorphicTrailingCoeffAt f 0‖
⊢ (logCounting f 0 - logCounting f ⊤) R =
    circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 R - log ‖meromorphicTrailingCoeffAt f 0‖

Tactic:
rw [← locallyFinsuppWithin.logCounting_divisor]

Premises used: locallyFinsuppWithin.logCounting_divisor
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
R : ℝ
f : ℂ → ℂ
h : Meromorphic f
hR : R ≠ 0
⊢ (locallyFinsuppWithin.logCounting : (a : locallyFinsupp ℂ ℤ) → ℝ → ℝ) (divisor f univ) R =
    circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 R - log ‖meromorphicTrailingCoeffAt f 0‖

Tactic:
locallyFinsuppWithin.logCounting_divisor_eq_circleAverage_sub_const h hR

Premises used: Function.locallyFinsuppWithin.logCounting_divisor_eq_circleAverage_sub_const
-- Module: Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
Goal:
R : ℝ
f : ℂ → ℂ
h : Meromorphic f
hR : R ≠ 0
⊢ (locallyFinsuppWithin.logCounting : (a : locallyFinsupp ℂ ℤ) → ℝ → ℝ) (divisor f univ) R =
    circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 R - log ‖meromorphicTrailingCoeffAt f 0‖

Tactic:
exact locallyFinsuppWithin.logCounting_divisor_eq_circleAverage_sub_const h hR

Premises used: Function.locallyFinsuppWithin.logCounting_divisor_eq_circleAverage_sub_const
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f g : ℂ → E
a : WithTop E
a₀ : E
pos : (h : a = ⊤) → ℝ → ℝ
neg : (h : ¬a = ⊤) → ℝ → ℝ
⊢ ℝ → ℝ

Tactic:
by_cases h : a = ⊤
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f g : ℂ → E
a : WithTop E
a₀ : E
h : a = ⊤
⊢ ℝ → ℝ

Tactic:
exact circleAverage (log⁺ ‖f ·‖) 0

Premises used: Norm.norm, Real.posLog, OfNat.ofNat, Real.circleAverage
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f g : ℂ → E
a : WithTop E
a₀ : E
h : ¬a = ⊤
⊢ ℝ → ℝ

Tactic:
exact circleAverage (log⁺ ‖f · - a.untop₀‖⁻¹) 0

Premises used: Norm.norm, WithTop.untop₀, Real.posLog, HSub.hSub, Inv.inv, OfNat.ofNat, Real.circleAverage
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
a₀ : E
⊢ proximity f (↑a₀ : WithTop E) = circleAverage (fun (x : ℂ) ↦ log⁺ ‖f x - a₀‖⁻¹) 0

Tactic:
simp [proximity]

Premises used: ValueDistribution.proximity
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
⊢ proximity f 0 = circleAverage (fun (x : ℂ) ↦ log⁺ ‖f x‖⁻¹) 0

Tactic:
simp [proximity]

Premises used: ValueDistribution.proximity
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
f : ℂ → ℂ
⊢ proximity f 0 = circleAverage (fun (x : ℂ) ↦ log⁺ ‖f⁻¹ x‖) 0

Tactic:
simp [proximity]

Premises used: ValueDistribution.proximity
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
⊢ proximity f ⊤ = circleAverage (fun (x : ℂ) ↦ log⁺ ‖f x‖) 0

Tactic:
simp [proximity]

Premises used: ValueDistribution.proximity
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f g : ℂ → E
a : WithTop E
r : ℝ
hfg : f =ᶠ[codiscreteWithin (sphere 0 |r|)] g
hr : r ≠ 0
pos : ∀ (h : a = ⊤), proximity f a r = proximity g a r
neg : ∀ (h : ¬a = ⊤), proximity f a r = proximity g a r
⊢ proximity f a r = proximity g a r

Tactic:
by_cases h : a = ⊤
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f g : ℂ → E
a : WithTop E
r : ℝ
hfg : f =ᶠ[codiscreteWithin (sphere 0 |r|)] g
hr : r ≠ 0
h : a = ⊤
pos : Eq (α := ℝ) (circleAverage (fun (x : ℂ) ↦ log⁺ ‖f x‖) 0 r) (circleAverage (fun (x : ℂ) ↦ log⁺ ‖g x‖) 0 r)
⊢ proximity f a r = proximity g a r

Tactic:
simp only [proximity, h, ↓reduceDIte]

Premises used: reduceDIte, ValueDistribution.proximity
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f g : ℂ → E
a : WithTop E
r : ℝ
hfg : f =ᶠ[codiscreteWithin (sphere 0 |r|)] g
hr : r ≠ 0
h : a = ⊤
apply : EventuallyEq (β := ℝ) (codiscreteWithin (sphere 0 |r|)) (fun (x : ℂ) ↦ log⁺ ‖f x‖) fun (x : ℂ) ↦ log⁺ ‖g x‖
⊢ Eq (α := ℝ) (circleAverage (fun (x : ℂ) ↦ log⁺ ‖f x‖) 0 r) (circleAverage (fun (x : ℂ) ↦ log⁺ ‖g x‖) 0 r)

Tactic:
apply circleAverage_congr_codiscreteWithin _ hr

Premises used: Real.circleAverage_congr_codiscreteWithin
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f g : ℂ → E
a : WithTop E
r : ℝ
hfg : f =ᶠ[codiscreteWithin (sphere 0 |r|)] g
hr : r ≠ 0
h : a = ⊤
⊢ ∀ (a : ℂ), f a = g a → log⁺ ‖f a‖ = log⁺ ‖g a‖

Tactic:
aesop
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f g : ℂ → E
a : WithTop E
r : ℝ
hfg : f =ᶠ[codiscreteWithin (sphere 0 |r|)] g
hr : r ≠ 0
h : a = ⊤
h₁ :
  ∀ (a : ℂ),
    Membership.mem (γ := Set ℂ)
      {x : ℂ |
        Membership.mem (γ := Set ℂ) {x : ℂ | (fun (x : ℂ) ↦ f x = g x) x} x →
          Membership.mem (γ := Set ℂ)
            {x : ℂ | (fun (x : ℂ) ↦ Eq (α := ℝ) ((fun (x : ℂ) ↦ log⁺ ‖f x‖) x) ((fun (x : ℂ) ↦ log⁺ ‖g x‖) x)) x} x}
      a
h₂ : ∀ (a : ℂ), f a = g a → log⁺ ‖f a‖ = log⁺ ‖g a‖
⊢ EventuallyEq (β := ℝ) (codiscreteWithin (sphere 0 |r|)) (fun (x : ℂ) ↦ log⁺ ‖f x‖) fun (x : ℂ) ↦ log⁺ ‖g x‖

Tactic:
filter_upwards [hfg] using by aesop
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f g : ℂ → E
a : WithTop E
r : ℝ
hfg : f =ᶠ[codiscreteWithin (sphere 0 |r|)] g
hr : r ≠ 0
h : ¬a = ⊤
neg :
  Eq (α := ℝ) (circleAverage (fun (x : ℂ) ↦ log⁺ ‖f x - a.untop₀‖⁻¹) 0 r)
    (circleAverage (fun (x : ℂ) ↦ log⁺ ‖g x - a.untop₀‖⁻¹) 0 r)
⊢ proximity f a r = proximity g a r

Tactic:
simp only [proximity, h, ↓reduceDIte]

Premises used: reduceDIte, ValueDistribution.proximity
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f g : ℂ → E
a : WithTop E
r : ℝ
hfg : f =ᶠ[codiscreteWithin (sphere 0 |r|)] g
hr : r ≠ 0
h : ¬a = ⊤
apply :
  EventuallyEq (β := ℝ) (codiscreteWithin (sphere 0 |r|)) (fun (x : ℂ) ↦ log⁺ ‖f x - a.untop₀‖⁻¹) fun (x : ℂ) ↦
    log⁺ ‖g x - a.untop₀‖⁻¹
⊢ Eq (α := ℝ) (circleAverage (fun (x : ℂ) ↦ log⁺ ‖f x - a.untop₀‖⁻¹) 0 r)
    (circleAverage (fun (x : ℂ) ↦ log⁺ ‖g x - a.untop₀‖⁻¹) 0 r)

Tactic:
apply circleAverage_congr_codiscreteWithin _ hr

Premises used: Real.circleAverage_congr_codiscreteWithin
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f g : ℂ → E
a : WithTop E
r : ℝ
hfg : f =ᶠ[codiscreteWithin (sphere 0 |r|)] g
hr : r ≠ 0
h : ¬a = ⊤
⊢ ∀ (a_1 : ℂ), f a_1 = g a_1 → log⁺ ‖f a_1 - a.untop₀‖⁻¹ = log⁺ ‖g a_1 - a.untop₀‖⁻¹

Tactic:
aesop
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f g : ℂ → E
a : WithTop E
r : ℝ
hfg : f =ᶠ[codiscreteWithin (sphere 0 |r|)] g
hr : r ≠ 0
h : ¬a = ⊤
h₁ :
  ∀ (a_1 : ℂ),
    Membership.mem (γ := Set ℂ)
      {x : ℂ |
        Membership.mem (γ := Set ℂ) {x : ℂ | (fun (x : ℂ) ↦ f x = g x) x} x →
          Membership.mem (γ := Set ℂ)
            {x : ℂ |
              (fun (x : ℂ) ↦
                  Eq (α := ℝ) ((fun (x : ℂ) ↦ log⁺ ‖f x - a.untop₀‖⁻¹) x) ((fun (x : ℂ) ↦ log⁺ ‖g x - a.untop₀‖⁻¹) x))
                x}
            x}
      a_1
h₂ : ∀ (a_1 : ℂ), f a_1 = g a_1 → log⁺ ‖f a_1 - a.untop₀‖⁻¹ = log⁺ ‖g a_1 - a.untop₀‖⁻¹
⊢ EventuallyEq (β := ℝ) (codiscreteWithin (sphere 0 |r|)) (fun (x : ℂ) ↦ log⁺ ‖f x - a.untop₀‖⁻¹) fun (x : ℂ) ↦
    log⁺ ‖g x - a.untop₀‖⁻¹

Tactic:
filter_upwards [hfg] using by aesop
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f g : ℂ → E
a : WithTop E
r : ℝ
hfg : f =ᶠ[codiscrete ℂ] g
hr : r ≠ 0
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ :
  ∀ ⦃a : ℂ⦄, Membership.mem (γ := Set ℂ) (sphere 0 |r|) a → Membership.mem (γ := Set ℂ) univ a
⊢ Subset (α := Set ℂ) (sphere 0 |r|) univ

Tactic:
tauto
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
a₀ : E
⊢ proximity f (↑a₀ : WithTop E) = proximity (f - fun (x : ℂ) ↦ a₀) 0

Tactic:
simp [proximity]

Premises used: ValueDistribution.proximity
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
f : ℂ → ℂ
⊢ proximity f⁻¹ ⊤ = proximity f 0

Tactic:
simp [proximity_zero, proximity_top]

Premises used: ValueDistribution.proximity_zero, ValueDistribution.proximity_top
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
f : ℂ → ℂ
h₁f : Meromorphic f
h : ∀ (R : ℝ), (proximity f ⊤ - proximity f⁻¹ ⊤) R = circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 R
⊢ proximity f ⊤ - proximity f⁻¹ ⊤ = circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0

Tactic:
ext R
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
f : ℂ → ℂ
h₁f : Meromorphic f
R : ℝ
h :
  HSub.hSub (α := ℝ) (circleAverage (fun (x : ℂ) ↦ log⁺ ‖f x‖) 0 R) (circleAverage (fun (x : ℂ) ↦ log⁺ ‖f x‖⁻¹) 0 R) =
    circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 R
⊢ (proximity f ⊤ - proximity f⁻¹ ⊤) R = circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 R

Tactic:
simp only [proximity, ↓reduceDIte, Pi.inv_apply, norm_inv, Pi.sub_apply]

Premises used: reduceDIte, norm_inv, ValueDistribution.proximity, Pi.inv_apply, Pi.sub_apply
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
f : ℂ → ℂ
h₁f : Meromorphic f
R : ℝ
h :
  circleAverage (HSub.hSub (α := ℂ → ℝ) (fun (x : ℂ) ↦ log⁺ ‖f x‖) fun (x : ℂ) ↦ log⁺ ‖f x‖⁻¹) 0 R =
    circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 R
h₁ : CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f x‖) 0 R
h₂ : CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f x‖⁻¹) 0 R
⊢ HSub.hSub (α := ℝ) (circleAverage (fun (x : ℂ) ↦ log⁺ ‖f x‖) 0 R) (circleAverage (fun (x : ℂ) ↦ log⁺ ‖f x‖⁻¹) 0 R) =
    circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 R

Tactic:
rw [← circleAverage_sub]

Premises used: Real.circleAverage_sub
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
f : ℂ → ℂ
h₁f : Meromorphic f
R : ℝ
h :
  circleAverage (HSub.hSub (α := ℂ → ℝ) (fun (x : ℂ) ↦ log⁺ ‖f x‖) fun (x : ℂ) ↦ log⁺ ‖f x‖⁻¹) 0 R =
    circleAverage (fun (x : ℂ) ↦ log⁺ ‖f x‖ - log⁺ ‖f x‖⁻¹) 0 R
⊢ circleAverage (HSub.hSub (α := ℂ → ℝ) (fun (x : ℂ) ↦ log⁺ ‖f x‖) fun (x : ℂ) ↦ log⁺ ‖f x‖⁻¹) 0 R =
    circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 R

Tactic:
simp_rw [← posLog_sub_posLog_inv, Pi.sub_def]

Premises used: Real.posLog_sub_posLog_inv, Pi.sub_def
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
f : ℂ → ℂ
h₁f : Meromorphic f
R : ℝ
⊢ CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f x‖) 0 R

Tactic:
apply h₁f.meromorphicOn.circleIntegrable_posLog_norm

Premises used: Meromorphic.meromorphicOn, MeromorphicOn.circleIntegrable_posLog_norm
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
f : ℂ → ℂ
h₁f : Meromorphic f
R : ℝ
h : CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖(f x)⁻¹‖) 0 R
⊢ CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f x‖⁻¹) 0 R

Tactic:
simp_rw [← norm_inv]

Premises used: norm_inv
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
f : ℂ → ℂ
h₁f : Meromorphic f
R : ℝ
⊢ CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖(f x)⁻¹‖) 0 R

Tactic:
apply h₁f.inv.meromorphicOn.circleIntegrable_posLog_norm

Premises used: Meromorphic.meromorphicOn, MeromorphicOn.circleIntegrable_posLog_norm, Meromorphic.inv
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
a : WithTop E
r : ℝ
pos : ∀ (h : a = ⊤), proximity f a (-r) = proximity f a r
neg : ∀ (h : ¬a = ⊤), proximity f a (-r) = proximity f a r
⊢ proximity f a (-r) = proximity f a r

Tactic:
by_cases h : a = ⊤
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
a : WithTop E
r : ℝ
h : a = ⊤
⊢ proximity f a (-r) = proximity f a r

Tactic:
simp [proximity, h]

Premises used: ValueDistribution.proximity
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
a : WithTop E
r : ℝ
h : ¬a = ⊤
⊢ proximity f a (-r) = proximity f a r

Tactic:
simp [proximity, h]

Premises used: ValueDistribution.proximity
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
a : WithTop E
pos : ∀ (h : a = ⊤), 0 ≤ proximity f a
neg : ∀ (h : ¬a = ⊤), 0 ≤ proximity f a
⊢ 0 ≤ proximity f a

Tactic:
by_cases h : a = ⊤
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
a : WithTop E
h : a = ⊤
r : ℝ
⊢ 0 r ≤ proximity f a r

Tactic:
simpa [proximity, h] using circleAverage_nonneg_of_nonneg (fun x _ ↦ posLog_nonneg)

Premises used: ValueDistribution.proximity, Real.posLog_nonneg, Real.circleAverage_nonneg_of_nonneg
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
f : ℂ → E
a : WithTop E
h : ¬a = ⊤
r : ℝ
⊢ 0 r ≤ proximity f a r

Tactic:
simpa [proximity, h] using circleAverage_nonneg_of_nonneg (fun x _ ↦ posLog_nonneg)

Premises used: ValueDistribution.proximity, Real.posLog_nonneg, Real.circleAverage_nonneg_of_nonneg
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
c : E
r : ℝ
⊢ proximity.{u_1} (E := E) (fun (x : ℂ) ↦ c) ⊤ r = log⁺ ‖c‖

Tactic:
simp [proximity, circleAverage_const]

Premises used: ValueDistribution.proximity, Real.circleAverage_const
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
hf : ∀ a ∈ s, Meromorphic (f a)
simp :
  circleAverage (fun (x : ℂ) ↦ log⁺ (Norm.norm.{u_1} (E := E) (∑ c ∈ s, f c x))) 0 ≤
    HAdd.hAdd (α := ℝ → ℝ) (∑ x ∈ s, circleAverage (fun (x_1 : ℂ) ↦ log⁺ ‖f x x_1‖) 0) fun (x : ℝ) ↦ log (↑s.card : ℝ)
⊢ proximity.{u_1} (E := E) (∑ a ∈ s, f a) ⊤ ≤
    HAdd.hAdd (α := ℝ → ℝ) (∑ a ∈ s, proximity (f a) ⊤) fun (x : ℝ) ↦ log (↑s.card : ℝ)

Tactic:
simp only [proximity_top, Finset.sum_apply]

Premises used: Finset.sum_apply, ValueDistribution.proximity_top
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
hf : ∀ a ∈ s, Meromorphic (f a)
r : ℝ
⊢ ∀ i ∈ s, CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f i x‖) 0 r

Tactic:
have h₂f : ∀ i ∈ s, CircleIntegrable (log⁺ ‖f i ·‖) 0 r :=
    fun i hi ↦ MeromorphicOn.circleIntegrable_posLog_norm (fun x hx ↦ hf i hi x)
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
hf : ∀ a ∈ s, Meromorphic (f a)
r : ℝ
h₂f : ∀ i ∈ s, CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f i x‖) 0 r
simp :
  circleAverage (fun (x : ℂ) ↦ log⁺ (Norm.norm.{u_1} (E := E) (∑ c ∈ s, f c x))) 0 r ≤
    ∑ c ∈ s, circleAverage (fun (x : ℂ) ↦ log⁺ ‖f c x‖) 0 r + log (↑s.card : ℝ)
⊢ circleAverage (fun (x : ℂ) ↦ log⁺ (Norm.norm.{u_1} (E := E) (∑ c ∈ s, f c x))) 0 r ≤
    HAdd.hAdd (α := ℝ → ℝ) (β := ℝ → ℝ) (∑ x ∈ s, circleAverage (fun (x_1 : ℂ) ↦ log⁺ ‖f x x_1‖) 0)
      (fun (x : ℝ) ↦ log (↑s.card : ℝ)) r

Tactic:
simp only [Pi.add_apply, Finset.sum_apply]

Premises used: Finset.sum_apply, Pi.add_apply
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
hf : ∀ a ∈ s, Meromorphic (f a)
r : ℝ
h₂f : ∀ i ∈ s, CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f i x‖) 0 r
hf₁ : CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ (Norm.norm.{u_1} (E := E) (∑ c ∈ s, f c x))) 0 r
hf₂ : CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ ∑ c ∈ s, log⁺ ‖f c x‖ + log (↑s.card : ℝ)) 0 r
h :
  ∀ (x : ℂ),
    Membership.mem (γ := Set ℂ) (sphere 0 |r|) x →
      log⁺ (Norm.norm.{u_1} (E := E) (∑ c ∈ s, f c x)) ≤ ∑ c ∈ s, log⁺ ‖f c x‖ + log (↑s.card : ℝ)
⊢ LE.le (α := ℝ) (circleAverage (fun (x : ℂ) ↦ log⁺ (Norm.norm.{u_1} (E := E) (∑ c ∈ s, f c x))) 0 r)
    (circleAverage (fun (x : ℂ) ↦ ∑ c ∈ s, log⁺ ‖f c x‖ + log (↑s.card : ℝ)) 0 r)

Tactic:
apply circleAverage_mono

Premises used: Real.circleAverage_mono
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
hf : ∀ a ∈ s, Meromorphic (f a)
r : ℝ
h₂f : ∀ i ∈ s, CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f i x‖) 0 r
⊢ CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ (Norm.norm.{u_1} (E := E) (∑ c ∈ s, f c x))) 0 r

Tactic:
apply (Meromorphic.fun_sum hf).meromorphicOn.circleIntegrable_posLog_norm

Premises used: Meromorphic.fun_sum, Meromorphic.meromorphicOn, MeromorphicOn.circleIntegrable_posLog_norm
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
hf : ∀ a ∈ s, Meromorphic (f a)
r : ℝ
h₂f : ∀ i ∈ s, CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f i x‖) 0 r
⊢ CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ ∑ c ∈ s, log⁺ ‖f c x‖ + log (↑s.card : ℝ)) 0 r

Tactic:
apply (CircleIntegrable.fun_sum s h₂f).add (circleIntegrable_const _ _ _)

Premises used: circleIntegrable_const, CircleIntegrable.add, CircleIntegrable.fun_sum
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
hf : ∀ a ∈ s, Meromorphic (f a)
r : ℝ
h₂f : ∀ i ∈ s, CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f i x‖) 0 r
x : ℂ
hx : Membership.mem (γ := Set ℂ) (sphere 0 |r|) x
h : log⁺ (Norm.norm.{u_1} (E := E) (∑ c ∈ s, f c x)) ≤ log (↑s.card : ℝ) + ∑ c ∈ s, log⁺ ‖f c x‖
⊢ log⁺ (Norm.norm.{u_1} (E := E) (∑ c ∈ s, f c x)) ≤ ∑ c ∈ s, log⁺ ‖f c x‖ + log (↑s.card : ℝ)

Tactic:
rw [add_comm]

Premises used: add_comm
-- Module: Mathlib.Analysis.Complex.ValueDistribution.Proximity.Basic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
hf : ∀ a ∈ s, Meromorphic (f a)
r : ℝ
h₂f : ∀ i ∈ s, CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f i x‖) 0 r
x : ℂ
hx : Membership.mem (γ := Set ℂ) (sphere 0 |r|) x
⊢ log⁺ (Norm.norm.{u_1} (E := E) (∑ c ∈ s, f c x)) ≤ log (↑s.card : ℝ) + ∑ c ∈ s, log⁺ ‖f c x‖

Tactic:
apply posLog_norm_sum_le

Premises used: Real.posLog_norm_sum_le