awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
r : ℝ
hf : ∀ a ∈ s, Meromorphic (f a)
hr : 1 ≤ r
⊢ proximity.{u_1} (E := E) (∑ a ∈ s, f a) ⊤ r ≤ (∑ a ∈ s, proximity (f a) ⊤) r + log (↑s.card : ℝ)

Tactic:
apply proximity_sum_top_le s f hf r

Premises used: ValueDistribution.proximity_sum_top_le
-- Module: Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
r : ℝ
hf : ∀ a ∈ s, Meromorphic (f a)
hr : 1 ≤ r
⊢ logCounting.{0, u_1} (𝕜 := ℂ) (E := E) (∑ a ∈ s, f a) ⊤ r ≤ (∑ a ∈ s, logCounting (f a) ⊤) r

Tactic:
apply logCounting_sum_top_le s f hf hr

Premises used: ValueDistribution.logCounting_sum_top_le
-- Module: Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
r : ℝ
hf : ∀ a ∈ s, Meromorphic (f a)
hr : 1 ≤ r
⊢ (∑ a ∈ s, proximity (f a) ⊤) r + log (↑s.card : ℝ) + (∑ a ∈ s, logCounting (f a) ⊤) r =
    HAdd.hAdd (α := ℝ) ((∑ a ∈ s, proximity (f a) ⊤) r) ((∑ a ∈ s, logCounting (f a) ⊤) r) + log (↑s.card : ℝ)

Tactic:
ring
-- Module: Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
r : ℝ
hf : ∀ a ∈ s, Meromorphic (f a)
hr : 1 ≤ r
⊢ HAdd.hAdd (α := ℝ) ((∑ a ∈ s, proximity (f a) ⊤) r) ((∑ a ∈ s, logCounting (f a) ⊤) r) + log (↑s.card : ℝ) =
    ∑ x ∈ s, (proximity (f x) ⊤ r + logCounting (f x) ⊤ r) + log (↑s.card : ℝ)

Tactic:
simp [Finset.sum_add_distrib]

Premises used: Finset.sum_add_distrib
-- Module: Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
α : Type u_2
s : Finset α
f : α → ℂ → E
r : ℝ
hf : ∀ a ∈ s, Meromorphic (f a)
hr : 1 ≤ r
calc :
  proximity.{u_1} (E := E) (∑ a ∈ s, f a) ⊤ r + logCounting.{0, u_1} (𝕜 := ℂ) (E := E) (∑ a ∈ s, f a) ⊤ r ≤
    (∑ a ∈ s, proximity (f a) ⊤) r + log (↑s.card : ℝ) + (∑ a ∈ s, logCounting (f a) ⊤) r
calc₁ :
  (∑ a ∈ s, proximity (f a) ⊤) r + log (↑s.card : ℝ) + (∑ a ∈ s, logCounting (f a) ⊤) r =
    HAdd.hAdd (α := ℝ) ((∑ a ∈ s, proximity (f a) ⊤) r) ((∑ a ∈ s, logCounting (f a) ⊤) r) + log (↑s.card : ℝ)
calc₂ :
  HAdd.hAdd (α := ℝ) ((∑ a ∈ s, proximity (f a) ⊤) r) ((∑ a ∈ s, logCounting (f a) ⊤) r) + log (↑s.card : ℝ) =
    ∑ x ∈ s, (proximity (f x) ⊤ r + logCounting (f x) ⊤ r) + log (↑s.card : ℝ)
⊢ proximity.{u_1} (E := E) (∑ a ∈ s, f a) ⊤ r + logCounting.{0, u_1} (𝕜 := ℂ) (E := E) (∑ a ∈ s, f a) ⊤ r ≤
    ∑ x ∈ s, (proximity (f x) ⊤ r + logCounting (f x) ⊤ r) + log (↑s.card : ℝ)

Tactic:
calc proximity (∑ a ∈ s, f a) ⊤ r + logCounting (∑ a ∈ s, f a) ⊤ r
  _ ≤ ((∑ a ∈ s, proximity (f a) ⊤) r) + log s.card + (∑ a ∈ s, (logCounting (f a) ⊤)) r := by
      gcongr
      · apply proximity_sum_top_le s f hf r
      · apply logCounting_sum_top_le s f hf hr
    _ = ((∑ a ∈ s, proximity (f a) ⊤) r) + (∑ a ∈ s, (logCounting (f a) ⊤)) r + log s.card := by
      ring
    _ = ∑ x ∈ s, (proximity (f x) ⊤ r + logCounting (f x) ⊤ r) + log s.card := by
      simp [Finset.sum_add_distrib]

Premises used: ValueDistribution.logCounting, Nat.cast, Real.log, Finset.card, ValueDistribution.proximity, Top.top, Finset.sum
-- Module: Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction
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)
⊢ ∀ (a : ℝ),
    1 ≤ a →
      characteristic.{u_1} (E := E) (∑ a ∈ s, f a) ⊤ a ≤
        HAdd.hAdd (α := ℝ → ℝ) (β := ℝ → ℝ) (∑ a ∈ s, characteristic (f a) ⊤) (fun (x : ℝ) ↦ log (↑s.card : ℝ)) a

Tactic:
fun _ hr ↦ characteristic_sum_top_le s f hf hr

Premises used: ValueDistribution.characteristic_sum_top_le
-- Module: Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction
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)
h :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ |
        Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ 1 ≤ x) x} x →
          Membership.mem (γ := Set ℝ)
            {x : ℝ |
              (fun (x : ℝ) ↦
                  characteristic.{u_1} (E := E) (∑ a ∈ s, f a) ⊤ x ≤
                    HAdd.hAdd (α := ℝ → ℝ) (β := ℝ → ℝ) (∑ a ∈ s, characteristic (f a) ⊤)
                      (fun (x : ℝ) ↦ log (↑s.card : ℝ)) x)
                x}
            x}
      a
h₁ :
  ∀ (a : ℝ),
    1 ≤ a →
      characteristic.{u_1} (E := E) (∑ a ∈ s, f a) ⊤ a ≤
        HAdd.hAdd (α := ℝ → ℝ) (β := ℝ → ℝ) (∑ a ∈ s, characteristic (f a) ⊤) (fun (x : ℝ) ↦ log (↑s.card : ℝ)) a
⊢ characteristic.{u_1} (E := E) (∑ a ∈ s, f a) ⊤ ≤ᶠ[atTop]
    HAdd.hAdd (α := ℝ → ℝ) (∑ a ∈ s, characteristic (f a) ⊤) fun (x : ℝ) ↦ log (↑s.card : ℝ)

Tactic:
filter_upwards [Filter.eventually_ge_atTop 1]
    using fun _ hr ↦ characteristic_sum_top_le s f hf hr

Premises used: ValueDistribution.characteristic_sum_top_le, Filter.eventually_ge_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f₁ f₂ : ℂ → E
r : ℝ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
hr : 1 ≤ r
⊢ ∀ (a : Fin (Nat.succ 0).succ),
    Membership.mem (γ := Finset (Fin (Nat.succ 0).succ)) Finset.univ a → Meromorphic (![f₁, f₂] a)

Tactic:
simpa using ⟨h₁f₁, h₁f₂⟩
-- Module: Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f₁ f₂ : ℂ → E
r : ℝ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
hr : 1 ≤ r
⊢ ∀ (a : Fin (Nat.succ 0).succ),
    Membership.mem (γ := Finset (Fin (Nat.succ 0).succ)) Finset.univ a → Meromorphic (![f₁, f₂] a)

Tactic:
have h_meromorphic : ∀ a ∈ Finset.univ, Meromorphic (![f₁, f₂] a) := by
    simpa using ⟨h₁f₁, h₁f₂⟩
-- Module: Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f₁ f₂ : ℂ → E
r : ℝ
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
hr : 1 ≤ r
h_meromorphic :
  ∀ (a : Fin (Nat.succ 0).succ),
    Membership.mem (γ := Finset (Fin (Nat.succ 0).succ)) Finset.univ a → Meromorphic (![f₁, f₂] a)
⊢ characteristic (f₁ + f₂) ⊤ r ≤ characteristic f₁ ⊤ r + characteristic f₂ ⊤ r + log 2

Tactic:
simpa using characteristic_sum_top_le Finset.univ ![f₁, f₂] h_meromorphic hr

Premises used: Finset.univ, ValueDistribution.characteristic_sum_top_le, Matrix.vecEmpty, Matrix.vecCons
-- Module: Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f₁ f₂ : ℂ → E
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
r : ℝ
hr : 1 ≤ r
⊢ characteristic (f₁ + f₂) ⊤ r ≤
    HAdd.hAdd (β := ℝ → ℝ) (characteristic f₁ ⊤ + characteristic f₂ ⊤) (fun (x : ℝ) ↦ log 2) r

Tactic:
characteristic_add_top_le h₁f₁ h₁f₂ hr

Premises used: ValueDistribution.characteristic_add_top_le
-- Module: Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
f₁ f₂ : ℂ → E
h₁f₁ : Meromorphic f₁
h₁f₂ : Meromorphic f₂
h :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ |
        Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ 1 ≤ x) x} x →
          Membership.mem (γ := Set ℝ)
            {x : ℝ |
              (fun (x : ℝ) ↦
                  characteristic (f₁ + f₂) ⊤ x ≤
                    HAdd.hAdd (β := ℝ → ℝ) (characteristic f₁ ⊤ + characteristic f₂ ⊤) (fun (x : ℝ) ↦ log 2) x)
                x}
            x}
      a
h₁ h₂ :
  ∀ (r : ℝ) (hr : 1 ≤ r),
    characteristic (f₁ + f₂) ⊤ r ≤
      HAdd.hAdd (β := ℝ → ℝ) (characteristic f₁ ⊤ + characteristic f₂ ⊤) (fun (x : ℝ) ↦ log 2) r
⊢ characteristic (f₁ + f₂) ⊤ ≤ᶠ[atTop] characteristic f₁ ⊤ + characteristic f₂ ⊤ + fun (x : ℝ) ↦ log 2

Tactic:
filter_upwards [Filter.eventually_ge_atTop 1] with r hr
    using characteristic_add_top_le h₁f₁ h₁f₂ hr

Premises used: Filter.eventually_ge_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction
Goal:
f₁ f₂ : ℂ → ℂ
r : ℝ
hr : 1 ≤ r
h₁f₁ : Meromorphic f₁
h₂f₁ : ∀ (z : ℂ), meromorphicOrderAt f₁ z ≠ ⊤
h₁f₂ : Meromorphic f₂
h₂f₂ : ∀ (z : ℂ), meromorphicOrderAt f₂ z ≠ ⊤
rw :
  proximity (f₁ * f₂) 0 r + logCounting (f₁ * f₂) 0 r ≤
    proximity f₁ 0 r + proximity f₂ 0 r + (logCounting f₁ 0 r + logCounting f₂ 0 r)
⊢ proximity (f₁ * f₂) 0 r + logCounting (f₁ * f₂) 0 r ≤
    proximity f₁ 0 r + logCounting f₁ 0 r + (proximity f₂ 0 r + logCounting f₂ 0 r)

Tactic:
rw [add_add_add_comm]

Premises used: add_add_add_comm
-- Module: Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction
Goal:
f₁ f₂ : ℂ → ℂ
r : ℝ
hr : 1 ≤ r
h₁f₁ : Meromorphic f₁
h₂f₁ : ∀ (z : ℂ), meromorphicOrderAt f₁ z ≠ ⊤
h₁f₂ : Meromorphic f₂
h₂f₂ : ∀ (z : ℂ), meromorphicOrderAt f₂ z ≠ ⊤
⊢ proximity (f₁ * f₂) 0 r + logCounting (f₁ * f₂) 0 r ≤
    proximity f₁ 0 r + proximity f₂ 0 r + (logCounting f₁ 0 r + logCounting f₂ 0 r)

Tactic:
apply add_le_add (proximity_mul_zero_le h₁f₁ h₁f₂ r)
    (logCounting_mul_zero_le hr h₁f₁ h₂f₁ h₁f₂ h₂f₂)

Premises used: add_le_add, ValueDistribution.proximity_mul_zero_le, ValueDistribution.logCounting_mul_zero_le
-- Module: Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction
Goal:
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₂f₁ : ∀ (z : ℂ), meromorphicOrderAt f₁ z ≠ ⊤
h₁f₂ : Meromorphic f₂
h₂f₂ : ∀ (z : ℂ), meromorphicOrderAt f₂ z ≠ ⊤
⊢ ∀ (a : ℝ), 1 ≤ a → characteristic (f₁ * f₂) 0 a ≤ (characteristic f₁ 0 + characteristic f₂ 0) a

Tactic:
fun _ hr ↦ characteristic_mul_zero_le hr h₁f₁ h₂f₁ h₁f₂ h₂f₂

Premises used: ValueDistribution.characteristic_mul_zero_le
-- Module: Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction
Goal:
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₂f₁ : ∀ (z : ℂ), meromorphicOrderAt f₁ z ≠ ⊤
h₁f₂ : Meromorphic f₂
h₂f₂ : ∀ (z : ℂ), meromorphicOrderAt f₂ z ≠ ⊤
h :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ |
        Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ 1 ≤ x) x} x →
          Membership.mem (γ := Set ℝ)
            {x : ℝ | (fun (x : ℝ) ↦ characteristic (f₁ * f₂) 0 x ≤ (characteristic f₁ 0 + characteristic f₂ 0) x) x} x}
      a
h₁ : ∀ (a : ℝ), 1 ≤ a → characteristic (f₁ * f₂) 0 a ≤ (characteristic f₁ 0 + characteristic f₂ 0) a
⊢ characteristic (f₁ * f₂) 0 ≤ᶠ[atTop] characteristic f₁ 0 + characteristic f₂ 0

Tactic:
filter_upwards [Filter.eventually_ge_atTop 1]
    using fun _ hr ↦ characteristic_mul_zero_le hr h₁f₁ h₂f₁ h₁f₂ h₂f₂

Premises used: ValueDistribution.characteristic_mul_zero_le, Filter.eventually_ge_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction
Goal:
f₁ f₂ : ℂ → ℂ
r : ℝ
hr : 1 ≤ r
h₁f₁ : Meromorphic f₁
h₂f₁ : ∀ (z : ℂ), meromorphicOrderAt f₁ z ≠ ⊤
h₁f₂ : Meromorphic f₂
h₂f₂ : ∀ (z : ℂ), meromorphicOrderAt f₂ z ≠ ⊤
rw :
  proximity (f₁ * f₂) ⊤ r + logCounting (f₁ * f₂) ⊤ r ≤
    proximity f₁ ⊤ r + proximity f₂ ⊤ r + (logCounting f₁ ⊤ r + logCounting f₂ ⊤ r)
⊢ proximity (f₁ * f₂) ⊤ r + logCounting (f₁ * f₂) ⊤ r ≤
    proximity f₁ ⊤ r + logCounting f₁ ⊤ r + (proximity f₂ ⊤ r + logCounting f₂ ⊤ r)

Tactic:
rw [add_add_add_comm]

Premises used: add_add_add_comm
-- Module: Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction
Goal:
f₁ f₂ : ℂ → ℂ
r : ℝ
hr : 1 ≤ r
h₁f₁ : Meromorphic f₁
h₂f₁ : ∀ (z : ℂ), meromorphicOrderAt f₁ z ≠ ⊤
h₁f₂ : Meromorphic f₂
h₂f₂ : ∀ (z : ℂ), meromorphicOrderAt f₂ z ≠ ⊤
⊢ proximity (f₁ * f₂) ⊤ r + logCounting (f₁ * f₂) ⊤ r ≤
    proximity f₁ ⊤ r + proximity f₂ ⊤ r + (logCounting f₁ ⊤ r + logCounting f₂ ⊤ r)

Tactic:
apply add_le_add (proximity_mul_top_le h₁f₁ h₁f₂ r)
    (logCounting_mul_top_le hr h₁f₁ h₂f₁ h₁f₂ h₂f₂)

Premises used: add_le_add, ValueDistribution.logCounting_mul_top_le, ValueDistribution.proximity_mul_top_le
-- Module: Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction
Goal:
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₂f₁ : ∀ (z : ℂ), meromorphicOrderAt f₁ z ≠ ⊤
h₁f₂ : Meromorphic f₂
h₂f₂ : ∀ (z : ℂ), meromorphicOrderAt f₂ z ≠ ⊤
⊢ ∀ (a : ℝ), 1 ≤ a → characteristic (f₁ * f₂) ⊤ a ≤ (characteristic f₁ ⊤ + characteristic f₂ ⊤) a

Tactic:
fun _ hr ↦ characteristic_mul_top_le hr h₁f₁ h₂f₁ h₁f₂ h₂f₂

Premises used: ValueDistribution.characteristic_mul_top_le
-- Module: Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction
Goal:
f₁ f₂ : ℂ → ℂ
h₁f₁ : Meromorphic f₁
h₂f₁ : ∀ (z : ℂ), meromorphicOrderAt f₁ z ≠ ⊤
h₁f₂ : Meromorphic f₂
h₂f₂ : ∀ (z : ℂ), meromorphicOrderAt f₂ z ≠ ⊤
h :
  ∀ (a : ℝ),
    Membership.mem (γ := Set ℝ)
      {x : ℝ |
        Membership.mem (γ := Set ℝ) {x : ℝ | (fun (x : ℝ) ↦ 1 ≤ x) x} x →
          Membership.mem (γ := Set ℝ)
            {x : ℝ | (fun (x : ℝ) ↦ characteristic (f₁ * f₂) ⊤ x ≤ (characteristic f₁ ⊤ + characteristic f₂ ⊤) x) x} x}
      a
h₁ : ∀ (a : ℝ), 1 ≤ a → characteristic (f₁ * f₂) ⊤ a ≤ (characteristic f₁ ⊤ + characteristic f₂ ⊤) a
⊢ characteristic (f₁ * f₂) ⊤ ≤ᶠ[atTop] characteristic f₁ ⊤ + characteristic f₂ ⊤

Tactic:
filter_upwards [Filter.eventually_ge_atTop 1]
    using fun _ hr ↦ characteristic_mul_top_le hr h₁f₁ h₂f₁ h₁f₂ h₂f₂

Premises used: ValueDistribution.characteristic_mul_top_le, Filter.eventually_ge_atTop, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction
Goal:
f : ℂ → ℂ
n : ℕ
hf : Meromorphic f
⊢ characteristic (f ^ n) 0 = n • characteristic f 0

Tactic:
simp_all [characteristic]

Premises used: ValueDistribution.characteristic
-- Module: Mathlib.Analysis.Complex.ValueDistribution.CharacteristicFunction
Goal:
f : ℂ → ℂ
n : ℕ
hf : Meromorphic f
⊢ characteristic (f ^ n) ⊤ = n • characteristic f ⊤

Tactic:
simp_all [characteristic]

Premises used: ValueDistribution.characteristic
-- Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem
Goal:
f : ℂ → ℂ
h : Meromorphic f
⊢ proximity f ⊤ + logCounting f ⊤ - (proximity f⁻¹ ⊤ + logCounting f⁻¹ ⊤) =
    proximity f ⊤ - proximity f⁻¹ ⊤ - (logCounting f⁻¹ ⊤ - logCounting f ⊤)

Tactic:
ring
-- Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem
Goal:
f : ℂ → ℂ
h : Meromorphic f
rw rw₁ :
  circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 - (logCounting f⁻¹ ⊤ - logCounting f ⊤) =
    circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 - (logCounting f⁻¹ ⊤ - logCounting f ⊤)
⊢ proximity f ⊤ - proximity f⁻¹ ⊤ - (logCounting f⁻¹ ⊤ - logCounting f ⊤) =
    circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 - (logCounting f⁻¹ ⊤ - logCounting f ⊤)

Tactic:
rw [proximity_sub_proximity_inv_eq_circleAverage h]

Premises used: ValueDistribution.proximity_sub_proximity_inv_eq_circleAverage
-- Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem
Goal:
f : ℂ → ℂ
h : Meromorphic f
rw rw₁ :
  circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 - (logCounting f 0 - logCounting f ⊤) =
    circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 - (logCounting f 0 - logCounting f ⊤)
⊢ circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 - (logCounting f⁻¹ ⊤ - logCounting f ⊤) =
    circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 - (logCounting f 0 - logCounting f ⊤)

Tactic:
rw [logCounting_inv]

Premises used: ValueDistribution.logCounting_inv
-- Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem
Goal:
f : ℂ → ℂ
h : Meromorphic f
rw rw₁ :
  HSub.hSub (α := (R : ℝ) → ℝ) (β := ℝ → ℝ) (circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0)
      ((Function.locallyFinsuppWithin.logCounting : (a : Function.locallyFinsupp ℂ ℤ) → ℝ → ℝ) (divisor f Set.univ) :
        ℝ → ℝ) =
    HSub.hSub (α := (R : ℝ) → ℝ) (β := ℝ → ℝ) (circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0)
      ((Function.locallyFinsuppWithin.logCounting : (a : Function.locallyFinsupp ℂ ℤ) → ℝ → ℝ) (divisor f Set.univ) :
        ℝ → ℝ)
⊢ circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 - (logCounting f 0 - logCounting f ⊤) =
    HSub.hSub (α := (R : ℝ) → ℝ) (β := ℝ → ℝ) (circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0)
      ((Function.locallyFinsuppWithin.logCounting : (a : Function.locallyFinsupp ℂ ℤ) → ℝ → ℝ) (divisor f Set.univ) :
        ℝ → ℝ)

Tactic:
rw [← ValueDistribution.log_counting_zero_sub_logCounting_top]

Premises used: ValueDistribution.log_counting_zero_sub_logCounting_top
-- Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem
Goal:
f : ℂ → ℂ
h : Meromorphic f
calc :
  characteristic f ⊤ - characteristic f⁻¹ ⊤ = proximity f ⊤ - proximity f⁻¹ ⊤ - (logCounting f⁻¹ ⊤ - logCounting f ⊤)
calc₁ :
  proximity f ⊤ - proximity f⁻¹ ⊤ - (logCounting f⁻¹ ⊤ - logCounting f ⊤) =
    circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 - (logCounting f⁻¹ ⊤ - logCounting f ⊤)
calc₂ :
  circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 - (logCounting f⁻¹ ⊤ - logCounting f ⊤) =
    circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 - (logCounting f 0 - logCounting f ⊤)
calc₃ :
  circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 - (logCounting f 0 - logCounting f ⊤) =
    HSub.hSub (α := (R : ℝ) → ℝ) (β := ℝ → ℝ) (circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0)
      ((Function.locallyFinsuppWithin.logCounting : (a : Function.locallyFinsupp ℂ ℤ) → ℝ → ℝ) (divisor f Set.univ) :
        ℝ → ℝ)
⊢ characteristic f ⊤ - characteristic f⁻¹ ⊤ =
    HSub.hSub (α := (R : ℝ) → ℝ) (β := ℝ → ℝ) (circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0)
      ((Function.locallyFinsuppWithin.logCounting : (a : Function.locallyFinsupp ℂ ℤ) → ℝ → ℝ) (divisor f Set.univ) :
        ℝ → ℝ)

Tactic:
calc characteristic f ⊤ - characteristic f⁻¹ ⊤
  _ = proximity f ⊤ - proximity f⁻¹ ⊤ - (logCounting f⁻¹ ⊤ - logCounting f ⊤) := by
    unfold characteristic
    ring
  _ = circleAverage (log ‖f ·‖) 0 - (logCounting f⁻¹ ⊤ - logCounting f ⊤) := by
    rw [proximity_sub_proximity_inv_eq_circleAverage h]
  _ = circleAverage (log ‖f ·‖) 0 - (logCounting f 0 - logCounting f ⊤) := by
    rw [logCounting_inv]
  _ = circleAverage (log ‖f ·‖) 0 - (divisor f Set.univ).logCounting := by
    rw [← ValueDistribution.log_counting_zero_sub_logCounting_top]

Premises used: Norm.norm, ValueDistribution.logCounting, Set.univ, HSub.hSub, Function.locallyFinsuppWithin.logCounting, ValueDistribution.characteristic, MeromorphicOn.divisor, Real.log, Inv.inv, ValueDistribution.proximity, Top.top, OfNat.ofNat, DFunLike.coe, Real.circleAverage
-- Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem
Goal:
f : ℂ → ℂ
R : ℝ
hf : Meromorphic f
hR : R ≠ 0
⊢ characteristic f ⊤ R - characteristic f⁻¹ ⊤ R = (characteristic f ⊤ - characteristic f⁻¹ ⊤) R

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem
Goal:
f : ℂ → ℂ
R : ℝ
hf : Meromorphic f
hR : R ≠ 0
rw :
  HSub.hSub (α := (R : ℝ) → ℝ) (β := ℝ → ℝ) (circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0)
      ((Function.locallyFinsuppWithin.logCounting : (a : Function.locallyFinsupp ℂ ℤ) → ℝ → ℝ) (divisor f Set.univ) :
        ℝ → ℝ)
      R =
    HSub.hSub (α := ℝ) (β := ℝ) (circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 R : ℝ)
      ((Function.locallyFinsuppWithin.logCounting : (a : Function.locallyFinsupp ℂ ℤ) → ℝ → ℝ) (divisor f Set.univ) R :
        ℝ)
rw₁ rw₂ :
  HSub.hSub (α := ℝ) (β := ℝ) (circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 R : ℝ)
      ((Function.locallyFinsuppWithin.logCounting : (a : Function.locallyFinsupp ℂ ℤ) → ℝ → ℝ) (divisor f Set.univ) R :
        ℝ) =
    HSub.hSub (α := ℝ) (β := ℝ) (circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 R : ℝ)
      ((Function.locallyFinsuppWithin.logCounting : (a : Function.locallyFinsupp ℂ ℤ) → ℝ → ℝ) (divisor f Set.univ) R :
        ℝ)
⊢ (characteristic f ⊤ - characteristic f⁻¹ ⊤) R =
    HSub.hSub (α := ℝ) (β := ℝ) (circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 R : ℝ)
      ((Function.locallyFinsuppWithin.logCounting : (a : Function.locallyFinsupp ℂ ℤ) → ℝ → ℝ) (divisor f Set.univ) R :
        ℝ)

Tactic:
rw [characteristic_sub_characteristic_inv hf, Pi.sub_apply]

Premises used: ValueDistribution.characteristic_sub_characteristic_inv, Pi.sub_apply
-- Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem
Goal:
f : ℂ → ℂ
R : ℝ
hf : Meromorphic f
hR : R ≠ 0
rw :
  HSub.hSub (β := ℝ)
      (∑ᶠ (u : ℂ), (↑((divisor f (closedBall 0 |R|) : (a : ℂ) → ℤ) u) : ℝ) * log (R * ‖0 - u‖⁻¹) +
          (↑((divisor f (closedBall 0 |R|) : (a : ℂ) → ℤ) 0) : ℝ) * log R +
        log ‖meromorphicTrailingCoeffAt f 0‖)
      ((Function.locallyFinsuppWithin.logCounting : (a : Function.locallyFinsupp ℂ ℤ) → ℝ → ℝ) (divisor f Set.univ) R :
        ℝ) =
    log ‖meromorphicTrailingCoeffAt f 0‖
⊢ HSub.hSub (α := ℝ) (β := ℝ) (circleAverage (fun (x : ℂ) ↦ log ‖f x‖) 0 R : ℝ)
      ((Function.locallyFinsuppWithin.logCounting : (a : Function.locallyFinsupp ℂ ℤ) → ℝ → ℝ) (divisor f Set.univ) R :
        ℝ) =
    log ‖meromorphicTrailingCoeffAt f 0‖

Tactic:
rw [MeromorphicOn.circleAverage_log_norm hR hf.meromorphicOn]

Premises used: Meromorphic.meromorphicOn, MeromorphicOn.circleAverage_log_norm
-- Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem
Goal:
f : ℂ → ℂ
R : ℝ
hf : Meromorphic f
hR : R ≠ 0
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ :
  ∀ ⦃a : ℂ⦄, Membership.mem (γ := Set ℂ) (closedBall 0 |R|) a → Membership.mem (γ := Set ℂ) Set.univ a
⊢ Subset (α := Set ℂ) (closedBall 0 |R|) Set.univ

Tactic:
tauto
-- Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem
Goal:
f : ℂ → ℂ
R : ℝ
hf : Meromorphic f
hR : R ≠ 0
⊢ Eq (α := Function.locallyFinsuppWithin (X := ℂ) (closedBall 0 |R|) ℤ) (divisor f (closedBall 0 |R|))
    ((toClosedBall R : (a : Function.locallyFinsupp ℂ ℤ) → Function.locallyFinsuppWithin (closedBall 0 |R|) ℤ)
      (divisor f Set.univ))

Tactic:
have : (divisor f (closedBall 0 |R|)) = (divisor f Set.univ).toClosedBall R :=
      (divisor_restrict hf.meromorphicOn (by tauto)).symm
-- Module: Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem
Goal:
f : ℂ → ℂ
R : ℝ
hf : Meromorphic f
hR : R ≠ 0
this :
  Eq (α := Function.locallyFinsuppWithin (X := ℂ) (closedBall 0 |R|) ℤ) (divisor f (closedBall 0 |R|))
    ((toClosedBall R : (a : Function.locallyFinsupp ℂ ℤ) → Function.locallyFinsuppWithin (closedBall 0 |R|) ℤ)
      (divisor f Set.univ))
⊢ HSub.hSub (β := ℝ)
      (∑ᶠ (u : ℂ), (↑((divisor f (closedBall 0 |R|) : (a : ℂ) → ℤ) u) : ℝ) * log (R * ‖0 - u‖⁻¹) +
          (↑((divisor f (closedBall 0 |R|) : (a : ℂ) → ℤ) 0) : ℝ) * log R +
        log ‖meromorphicTrailingCoeffAt f 0‖)
      (({
              toFun := fun (D : Function.locallyFinsupp ℂ ℤ) (r : ℝ) ↦
                ∑ᶠ (z : ℂ),
                    (↑((((toClosedBall r :
                                    (a : Function.locallyFinsupp ℂ ℤ) →
                                      Function.locallyFinsuppWithin (closedBall 0 |r|) ℤ)
                                  D :
                                Function.locallyFinsuppWithin (X := ℂ) (closedBall 0 |r|) ℤ) :
                              (a : ℂ) → ℤ)
                            z) :
                        ℝ) *
                      log (r * ‖z‖⁻¹) +
                  (↑((D : (a : ℂ) → ℤ) 0) : ℝ) * log r,
              map_zero' := ⋯, map_add' := ⋯ : Function.locallyFinsupp ℂ ℤ →+ ℝ → ℝ } :
            (a : Function.locallyFinsupp ℂ ℤ) → ℝ → ℝ)
          (divisor f Set.univ) R :
        ℝ) =
    log ‖meromorphicTrailingCoeffAt f 0‖

Tactic:
simp [this, toClosedBall, restrictMonoidHom, restrict_apply]

Premises used: Function.locallyFinsuppWithin.restrict_apply, Function.locallyFinsuppWithin.restrictMonoidHom, Function.locallyFinsuppWithin.toClosedBall