awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
hf : MeromorphicOn f (sphere c |R|)
t₀ : ∀ (u : (↑(sphere c |R|) : Type)), meromorphicOrderAt f (↑u : ℂ) ≠ ⊤
⊢ CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log ‖f x‖) c R
have pos : ∀ (g : ℂ → E) (h₁g : AnalyticOnNhd ℂ g (sphere c |R|)) (h₂g : ∀ (u : (↑(sphere c |R|) : Type)), g (↑u : ℂ) ≠ 0)
  (h₃g :
    f =ᶠ[codiscreteWithin (sphere c |R|)]
      HSMul.hSMul (α := ℂ → ℂ)
        (∏ᶠ (u : ℂ),
          HPow.hPow (α := ℂ → ℂ) (β := ℤ) (fun (x : ℂ) ↦ x - u) ((divisor f (sphere c |R|) : (a : ℂ) → ℤ) u : ℤ))
        g),
  CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log ‖f x‖) c R
Tactic: obtain ⟨g, h₁g, h₂g, h₃g⟩ := hf.extract_zeros_poles t₀
      ((divisor f (sphere c |R|)).finiteSupport (isCompact_sphere c |R|))
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
hf : MeromorphicOn f (sphere c |R|)
t₀ : ∀ (u : (↑(sphere c |R|) : Type)), meromorphicOrderAt f (↑u : ℂ) ≠ ⊤
g : ℂ → E
h₁g : AnalyticOnNhd ℂ g (sphere c |R|)
h₂g : ∀ (u : (↑(sphere c |R|) : Type)), g (↑u : ℂ) ≠ 0
h₃g :
  f =ᶠ[codiscreteWithin (sphere c |R|)]
    HSMul.hSMul (α := ℂ → ℂ)
      (∏ᶠ (u : ℂ),
        HPow.hPow (α := ℂ → ℂ) (β := ℤ) (fun (x : ℂ) ↦ x - u) ((divisor f (sphere c |R|) : (a : ℂ) → ℤ) u : ℤ))
      g
⊢ CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log ‖f x‖) c R
have h₄g : (fun (x : ℂ) ↦ log ‖f x‖) =ᶠ[codiscreteWithin (sphere c |R|)]
  HAdd.hAdd (α := ℂ → ℝ) (∑ᶠ (u : ℂ), fun (x : ℂ) ↦ (↑((divisor f (sphere c |R|) : (a : ℂ) → ℤ) u) : ℝ) * log ‖x - u‖)
    fun (x : ℂ) ↦ log ‖g x‖
Tactic: have h₄g := MeromorphicOn.extract_zeros_poles_log h₂g h₃g
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
hf : MeromorphicOn f (sphere c |R|)
t₀ : ∀ (u : (↑(sphere c |R|) : Type)), meromorphicOrderAt f (↑u : ℂ) ≠ ⊤
g : ℂ → E
h₁g : AnalyticOnNhd ℂ g (sphere c |R|)
h₂g : ∀ (u : (↑(sphere c |R|) : Type)), g (↑u : ℂ) ≠ 0
h₃g :
  f =ᶠ[codiscreteWithin (sphere c |R|)]
    HSMul.hSMul (α := ℂ → ℂ)
      (∏ᶠ (u : ℂ),
        HPow.hPow (α := ℂ → ℂ) (β := ℤ) (fun (x : ℂ) ↦ x - u) ((divisor f (sphere c |R|) : (a : ℂ) → ℤ) u : ℤ))
      g
h₄g :
  (fun (x : ℂ) ↦ log ‖f x‖) =ᶠ[codiscreteWithin (sphere c |R|)]
    HAdd.hAdd (α := ℂ → ℝ) (∑ᶠ (u : ℂ), fun (x : ℂ) ↦ (↑((divisor f (sphere c |R|) : (a : ℂ) → ℤ) u) : ℝ) * log ‖x - u‖)
      fun (x : ℂ) ↦ log ‖g x‖
⊢ CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log ‖f x‖) c R
have pos : CircleIntegrable
  (HAdd.hAdd (α := ℂ → ℝ) (∑ᶠ (u : ℂ), fun (x : ℂ) ↦ (↑((divisor f (sphere c |R|) : (a : ℂ) → ℤ) u) : ℝ) * log ‖x - u‖)
    fun (x : ℂ) ↦ log ‖g x‖)
  c R
Tactic: apply CircleIntegrable.congr_codiscreteWithin h₄g.symm
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
hf : MeromorphicOn f (sphere c |R|)
t₀ : ∀ (u : (↑(sphere c |R|) : Type)), meromorphicOrderAt f (↑u : ℂ) ≠ ⊤
g : ℂ → E
h₁g : AnalyticOnNhd ℂ g (sphere c |R|)
h₂g : ∀ (u : (↑(sphere c |R|) : Type)), g (↑u : ℂ) ≠ 0
h₃g :
  f =ᶠ[codiscreteWithin (sphere c |R|)]
    HSMul.hSMul (α := ℂ → ℂ)
      (∏ᶠ (u : ℂ),
        HPow.hPow (α := ℂ → ℂ) (β := ℤ) (fun (x : ℂ) ↦ x - u) ((divisor f (sphere c |R|) : (a : ℂ) → ℤ) u : ℤ))
      g
h₄g :
  (fun (x : ℂ) ↦ log ‖f x‖) =ᶠ[codiscreteWithin (sphere c |R|)]
    HAdd.hAdd (α := ℂ → ℝ) (∑ᶠ (u : ℂ), fun (x : ℂ) ↦ (↑((divisor f (sphere c |R|) : (a : ℂ) → ℤ) u) : ℝ) * log ‖x - u‖)
      fun (x : ℂ) ↦ log ‖g x‖
⊢ CircleIntegrable
    (HAdd.hAdd (α := ℂ → ℝ)
      (∑ᶠ (u : ℂ), fun (x : ℂ) ↦ (↑((divisor f (sphere c |R|) : (a : ℂ) → ℤ) u) : ℝ) * log ‖x - u‖) fun (x : ℂ) ↦
      log ‖g x‖)
    c R
have pos : CircleIntegrable (E := ℝ) (∑ᶠ (u : ℂ), fun (x : ℂ) ↦ (↑((divisor f (sphere c |R|) : (a : ℂ) → ℤ) u) : ℝ) * log ‖x - u‖)
  c R
Tactic: apply CircleIntegrable.add
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
hf : MeromorphicOn f (sphere c |R|)
t₀ : ∀ (u : (↑(sphere c |R|) : Type)), meromorphicOrderAt f (↑u : ℂ) ≠ ⊤
g : ℂ → E
h₁g : AnalyticOnNhd ℂ g (sphere c |R|)
h₂g : ∀ (u : (↑(sphere c |R|) : Type)), g (↑u : ℂ) ≠ 0
h₃g :
  f =ᶠ[codiscreteWithin (sphere c |R|)]
    HSMul.hSMul (α := ℂ → ℂ)
      (∏ᶠ (u : ℂ),
        HPow.hPow (α := ℂ → ℂ) (β := ℤ) (fun (x : ℂ) ↦ x - u) ((divisor f (sphere c |R|) : (a : ℂ) → ℤ) u : ℤ))
      g
h₄g :
  (fun (x : ℂ) ↦ log ‖f x‖) =ᶠ[codiscreteWithin (sphere c |R|)]
    HAdd.hAdd (α := ℂ → ℝ) (∑ᶠ (u : ℂ), fun (x : ℂ) ↦ (↑((divisor f (sphere c |R|) : (a : ℂ) → ℤ) u) : ℝ) * log ‖x - u‖)
      fun (x : ℂ) ↦ log ‖g x‖
pos :
  CircleIntegrable (E := ℝ)
    (∑ᶠ (u : ℂ), fun (x : ℂ) ↦ (↑((divisor f (sphere c |R|) : (a : ℂ) → ℤ) u) : ℝ) * log ‖x - u‖) c R
⊢ CircleIntegrable
    (HAdd.hAdd (α := ℂ → ℝ)
      (∑ᶠ (u : ℂ), fun (x : ℂ) ↦ (↑((divisor f (sphere c |R|) : (a : ℂ) → ℤ) u) : ℝ) * log ‖x - u‖) fun (x : ℂ) ↦
      log ‖g x‖)
    c R
have pos₁ : CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log ‖g x‖) c R
Tactic: apply CircleIntegrable.add
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
hf : MeromorphicOn f (sphere c |R|)
t₀ : ∀ (u : (↑(sphere c |R|) : Type)), meromorphicOrderAt f (↑u : ℂ) ≠ ⊤
g : ℂ → E
h₁g : AnalyticOnNhd ℂ g (sphere c |R|)
h₂g : ∀ (u : (↑(sphere c |R|) : Type)), g (↑u : ℂ) ≠ 0
h₃g :
  f =ᶠ[codiscreteWithin (sphere c |R|)]
    HSMul.hSMul (α := ℂ → ℂ)
      (∏ᶠ (u : ℂ),
        HPow.hPow (α := ℂ → ℂ) (β := ℤ) (fun (x : ℂ) ↦ x - u) ((divisor f (sphere c |R|) : (a : ℂ) → ℤ) u : ℤ))
      g
h₄g :
  (fun (x : ℂ) ↦ log ‖f x‖) =ᶠ[codiscreteWithin (sphere c |R|)]
    HAdd.hAdd (α := ℂ → ℝ) (∑ᶠ (u : ℂ), fun (x : ℂ) ↦ (↑((divisor f (sphere c |R|) : (a : ℂ) → ℤ) u) : ℝ) * log ‖x - u‖)
      fun (x : ℂ) ↦ log ‖g x‖
⊢ CircleIntegrable (E := ℝ)
    (∑ᶠ (u : ℂ), fun (x : ℂ) ↦ (↑((divisor f (sphere c |R|) : (a : ℂ) → ℤ) u) : ℝ) * log ‖x - u‖) c R
have pos : ∀ (i : ℂ),
  CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ (↑((divisor f (sphere c |R|) : (a : ℂ) → ℤ) i) : ℝ) * log ‖x - i‖) c R
Tactic: apply CircleIntegrable.finsum
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
hf : MeromorphicOn f (sphere c |R|)
t₀ : ∀ (u : (↑(sphere c |R|) : Type)), meromorphicOrderAt f (↑u : ℂ) ≠ ⊤
g : ℂ → E
h₁g : AnalyticOnNhd ℂ g (sphere c |R|)
h₂g : ∀ (u : (↑(sphere c |R|) : Type)), g (↑u : ℂ) ≠ 0
h₃g :
  f =ᶠ[codiscreteWithin (sphere c |R|)]
    HSMul.hSMul (α := ℂ → ℂ)
      (∏ᶠ (u : ℂ),
        HPow.hPow (α := ℂ → ℂ) (β := ℤ) (fun (x : ℂ) ↦ x - u) ((divisor f (sphere c |R|) : (a : ℂ) → ℤ) u : ℤ))
      g
h₄g :
  (fun (x : ℂ) ↦ log ‖f x‖) =ᶠ[codiscreteWithin (sphere c |R|)]
    HAdd.hAdd (α := ℂ → ℝ) (∑ᶠ (u : ℂ), fun (x : ℂ) ↦ (↑((divisor f (sphere c |R|) : (a : ℂ) → ℤ) u) : ℝ) * log ‖x - u‖)
      fun (x : ℂ) ↦ log ‖g x‖
i : ℂ
⊢ CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ (↑((divisor f (sphere c |R|) : (a : ℂ) → ℤ) i) : ℝ) * log ‖x - i‖) c R
have pos : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log ‖circleMap c R x - i‖) volume 0 (2 * π)
Tactic: apply IntervalIntegrable.const_mul
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
hf : MeromorphicOn f (sphere c |R|)
t₀ : ∀ (u : (↑(sphere c |R|) : Type)), meromorphicOrderAt f (↑u : ℂ) ≠ ⊤
g : ℂ → E
h₁g : AnalyticOnNhd ℂ g (sphere c |R|)
h₂g : ∀ (u : (↑(sphere c |R|) : Type)), g (↑u : ℂ) ≠ 0
h₃g :
  f =ᶠ[codiscreteWithin (sphere c |R|)]
    HSMul.hSMul (α := ℂ → ℂ)
      (∏ᶠ (u : ℂ),
        HPow.hPow (α := ℂ → ℂ) (β := ℤ) (fun (x : ℂ) ↦ x - u) ((divisor f (sphere c |R|) : (a : ℂ) → ℤ) u : ℤ))
      g
h₄g :
  (fun (x : ℂ) ↦ log ‖f x‖) =ᶠ[codiscreteWithin (sphere c |R|)]
    HAdd.hAdd (α := ℂ → ℝ) (∑ᶠ (u : ℂ), fun (x : ℂ) ↦ (↑((divisor f (sphere c |R|) : (a : ℂ) → ℤ) u) : ℝ) * log ‖x - u‖)
      fun (x : ℂ) ↦ log ‖g x‖
i : ℂ
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log ‖circleMap c R x - i‖) volume 0 (2 * π)
have pos : MeromorphicOn (E := ℂ) (fun (x : ℝ) ↦ circleMap c R x - i) [[0, 2 * π]]
Tactic: apply MeromorphicOn.intervalIntegrable_log_norm
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
hf : MeromorphicOn f (sphere c |R|)
t₀ : ∀ (u : (↑(sphere c |R|) : Type)), meromorphicOrderAt f (↑u : ℂ) ≠ ⊤
g : ℂ → E
h₁g : AnalyticOnNhd ℂ g (sphere c |R|)
h₂g : ∀ (u : (↑(sphere c |R|) : Type)), g (↑u : ℂ) ≠ 0
h₃g :
  f =ᶠ[codiscreteWithin (sphere c |R|)]
    HSMul.hSMul (α := ℂ → ℂ)
      (∏ᶠ (u : ℂ),
        HPow.hPow (α := ℂ → ℂ) (β := ℤ) (fun (x : ℂ) ↦ x - u) ((divisor f (sphere c |R|) : (a : ℂ) → ℤ) u : ℤ))
      g
h₄g :
  (fun (x : ℂ) ↦ log ‖f x‖) =ᶠ[codiscreteWithin (sphere c |R|)]
    HAdd.hAdd (α := ℂ → ℝ) (∑ᶠ (u : ℂ), fun (x : ℂ) ↦ (↑((divisor f (sphere c |R|) : (a : ℂ) → ℤ) u) : ℝ) * log ‖x - u‖)
      fun (x : ℂ) ↦ log ‖g x‖
i : ℂ
⊢ MeromorphicOn (E := ℂ) (fun (x : ℝ) ↦ circleMap c R x - i) [[0, 2 * π]]
have pos : AnalyticOnNhd ℝ (F := ℂ) (fun (x : ℝ) ↦ circleMap c R x - i) [[0, 2 * π]]
Tactic: apply AnalyticOnNhd.meromorphicOn
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
hf : MeromorphicOn f (sphere c |R|)
t₀ : ∀ (u : (↑(sphere c |R|) : Type)), meromorphicOrderAt f (↑u : ℂ) ≠ ⊤
g : ℂ → E
h₁g : AnalyticOnNhd ℂ g (sphere c |R|)
h₂g : ∀ (u : (↑(sphere c |R|) : Type)), g (↑u : ℂ) ≠ 0
h₃g :
  f =ᶠ[codiscreteWithin (sphere c |R|)]
    HSMul.hSMul (α := ℂ → ℂ)
      (∏ᶠ (u : ℂ),
        HPow.hPow (α := ℂ → ℂ) (β := ℤ) (fun (x : ℂ) ↦ x - u) ((divisor f (sphere c |R|) : (a : ℂ) → ℤ) u : ℤ))
      g
h₄g :
  (fun (x : ℂ) ↦ log ‖f x‖) =ᶠ[codiscreteWithin (sphere c |R|)]
    HAdd.hAdd (α := ℂ → ℝ) (∑ᶠ (u : ℂ), fun (x : ℂ) ↦ (↑((divisor f (sphere c |R|) : (a : ℂ) → ℤ) u) : ℝ) * log ‖x - u‖)
      fun (x : ℂ) ↦ log ‖g x‖
i : ℂ
⊢ AnalyticOnNhd ℝ (F := ℂ) (fun (x : ℝ) ↦ circleMap c R x - i) [[0, 2 * π]]
have apply : AnalyticOnNhd ℝ (circleMap c R) [[0, 2 * π]]
Tactic: apply AnalyticOnNhd.sub _ analyticOnNhd_const
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
hf : MeromorphicOn f (sphere c |R|)
t₀ : ∀ (u : (↑(sphere c |R|) : Type)), meromorphicOrderAt f (↑u : ℂ) ≠ ⊤
g : ℂ → E
h₁g : AnalyticOnNhd ℂ g (sphere c |R|)
h₂g : ∀ (u : (↑(sphere c |R|) : Type)), g (↑u : ℂ) ≠ 0
h₃g :
  f =ᶠ[codiscreteWithin (sphere c |R|)]
    HSMul.hSMul (α := ℂ → ℂ)
      (∏ᶠ (u : ℂ),
        HPow.hPow (α := ℂ → ℂ) (β := ℤ) (fun (x : ℂ) ↦ x - u) ((divisor f (sphere c |R|) : (a : ℂ) → ℤ) u : ℤ))
      g
h₄g :
  (fun (x : ℂ) ↦ log ‖f x‖) =ᶠ[codiscreteWithin (sphere c |R|)]
    HAdd.hAdd (α := ℂ → ℝ) (∑ᶠ (u : ℂ), fun (x : ℂ) ↦ (↑((divisor f (sphere c |R|) : (a : ℂ) → ℤ) u) : ℝ) * log ‖x - u‖)
      fun (x : ℂ) ↦ log ‖g x‖
i : ℂ
⊢ [[0, 2 * π]] ⊆ Set.univ
have tauto : ∀ ⦃a : ℝ⦄, a ∈ [[0, 2 * π]] → Membership.mem (γ := Set ℝ) Set.univ a
Tactic: tauto
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
hf : MeromorphicOn f (sphere c |R|)
t₀ : ∀ (u : (↑(sphere c |R|) : Type)), meromorphicOrderAt f (↑u : ℂ) ≠ ⊤
g : ℂ → E
h₁g : AnalyticOnNhd ℂ g (sphere c |R|)
h₂g : ∀ (u : (↑(sphere c |R|) : Type)), g (↑u : ℂ) ≠ 0
h₃g :
  f =ᶠ[codiscreteWithin (sphere c |R|)]
    HSMul.hSMul (α := ℂ → ℂ)
      (∏ᶠ (u : ℂ),
        HPow.hPow (α := ℂ → ℂ) (β := ℤ) (fun (x : ℂ) ↦ x - u) ((divisor f (sphere c |R|) : (a : ℂ) → ℤ) u : ℤ))
      g
h₄g :
  (fun (x : ℂ) ↦ log ‖f x‖) =ᶠ[codiscreteWithin (sphere c |R|)]
    HAdd.hAdd (α := ℂ → ℝ) (∑ᶠ (u : ℂ), fun (x : ℂ) ↦ (↑((divisor f (sphere c |R|) : (a : ℂ) → ℤ) u) : ℝ) * log ‖x - u‖)
      fun (x : ℂ) ↦ log ‖g x‖
⊢ CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log ‖g x‖) c R
have pos : ContinuousOn (Y := ℝ) (fun (θ : ℝ) ↦ (fun (x : ℂ) ↦ log ‖g x‖) (circleMap c R θ)) [[0, 2 * π]]
Tactic: apply ContinuousOn.intervalIntegrable
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
hf : MeromorphicOn f (sphere c |R|)
t₀ : ∀ (u : (↑(sphere c |R|) : Type)), meromorphicOrderAt f (↑u : ℂ) ≠ ⊤
g : ℂ → E
h₁g : AnalyticOnNhd ℂ g (sphere c |R|)
h₂g : ∀ (u : (↑(sphere c |R|) : Type)), g (↑u : ℂ) ≠ 0
h₃g :
  f =ᶠ[codiscreteWithin (sphere c |R|)]
    HSMul.hSMul (α := ℂ → ℂ)
      (∏ᶠ (u : ℂ),
        HPow.hPow (α := ℂ → ℂ) (β := ℤ) (fun (x : ℂ) ↦ x - u) ((divisor f (sphere c |R|) : (a : ℂ) → ℤ) u : ℤ))
      g
h₄g :
  (fun (x : ℂ) ↦ log ‖f x‖) =ᶠ[codiscreteWithin (sphere c |R|)]
    HAdd.hAdd (α := ℂ → ℝ) (∑ᶠ (u : ℂ), fun (x : ℂ) ↦ (↑((divisor f (sphere c |R|) : (a : ℂ) → ℤ) u) : ℝ) * log ‖x - u‖)
      fun (x : ℂ) ↦ log ‖g x‖
⊢ ContinuousOn (Y := ℝ) (fun (θ : ℝ) ↦ (fun (x : ℂ) ↦ log ‖g x‖) (circleMap c R θ)) [[0, 2 * π]]
have pos : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ ‖g (circleMap c R x)‖) [[0, 2 * π]]
Tactic: apply ContinuousOn.log
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
hf : MeromorphicOn f (sphere c |R|)
t₀ : ∀ (u : (↑(sphere c |R|) : Type)), meromorphicOrderAt f (↑u : ℂ) ≠ ⊤
g : ℂ → E
h₁g : AnalyticOnNhd ℂ g (sphere c |R|)
h₂g : ∀ (u : (↑(sphere c |R|) : Type)), g (↑u : ℂ) ≠ 0
h₃g :
  f =ᶠ[codiscreteWithin (sphere c |R|)]
    HSMul.hSMul (α := ℂ → ℂ)
      (∏ᶠ (u : ℂ),
        HPow.hPow (α := ℂ → ℂ) (β := ℤ) (fun (x : ℂ) ↦ x - u) ((divisor f (sphere c |R|) : (a : ℂ) → ℤ) u : ℤ))
      g
h₄g :
  (fun (x : ℂ) ↦ log ‖f x‖) =ᶠ[codiscreteWithin (sphere c |R|)]
    HAdd.hAdd (α := ℂ → ℝ) (∑ᶠ (u : ℂ), fun (x : ℂ) ↦ (↑((divisor f (sphere c |R|) : (a : ℂ) → ℤ) u) : ℝ) * log ‖x - u‖)
      fun (x : ℂ) ↦ log ‖g x‖
pos : ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ ‖g (circleMap c R x)‖) [[0, 2 * π]]
⊢ ContinuousOn (Y := ℝ) (fun (θ : ℝ) ↦ (fun (x : ℂ) ↦ log ‖g x‖) (circleMap c R θ)) [[0, 2 * π]]
have pos₁ : ∀ x ∈ [[0, 2 * π]], ‖g (circleMap c R x)‖ ≠ 0
Tactic: apply ContinuousOn.log
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
hf : MeromorphicOn f (sphere c |R|)
t₀ : ∀ (u : (↑(sphere c |R|) : Type)), meromorphicOrderAt f (↑u : ℂ) ≠ ⊤
g : ℂ → E
h₁g : AnalyticOnNhd ℂ g (sphere c |R|)
h₂g : ∀ (u : (↑(sphere c |R|) : Type)), g (↑u : ℂ) ≠ 0
h₃g :
  f =ᶠ[codiscreteWithin (sphere c |R|)]
    HSMul.hSMul (α := ℂ → ℂ)
      (∏ᶠ (u : ℂ),
        HPow.hPow (α := ℂ → ℂ) (β := ℤ) (fun (x : ℂ) ↦ x - u) ((divisor f (sphere c |R|) : (a : ℂ) → ℤ) u : ℤ))
      g
h₄g :
  (fun (x : ℂ) ↦ log ‖f x‖) =ᶠ[codiscreteWithin (sphere c |R|)]
    HAdd.hAdd (α := ℂ → ℝ) (∑ᶠ (u : ℂ), fun (x : ℂ) ↦ (↑((divisor f (sphere c |R|) : (a : ℂ) → ℤ) u) : ℝ) * log ‖x - u‖)
      fun (x : ℂ) ↦ log ‖g x‖
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ ‖g (circleMap c R x)‖) [[0, 2 * π]]
have pos : ContinuousOn.{0, u_1} (Y := E) (fun (x : ℝ) ↦ g (circleMap c R x)) [[0, 2 * π]]
Tactic: apply ContinuousOn.norm
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
hf : MeromorphicOn f (sphere c |R|)
t₀ : ∀ (u : (↑(sphere c |R|) : Type)), meromorphicOrderAt f (↑u : ℂ) ≠ ⊤
g : ℂ → E
h₁g : AnalyticOnNhd ℂ g (sphere c |R|)
h₂g : ∀ (u : (↑(sphere c |R|) : Type)), g (↑u : ℂ) ≠ 0
h₃g :
  f =ᶠ[codiscreteWithin (sphere c |R|)]
    HSMul.hSMul (α := ℂ → ℂ)
      (∏ᶠ (u : ℂ),
        HPow.hPow (α := ℂ → ℂ) (β := ℤ) (fun (x : ℂ) ↦ x - u) ((divisor f (sphere c |R|) : (a : ℂ) → ℤ) u : ℤ))
      g
h₄g :
  (fun (x : ℂ) ↦ log ‖f x‖) =ᶠ[codiscreteWithin (sphere c |R|)]
    HAdd.hAdd (α := ℂ → ℝ) (∑ᶠ (u : ℂ), fun (x : ℂ) ↦ (↑((divisor f (sphere c |R|) : (a : ℂ) → ℤ) u) : ℝ) * log ‖x - u‖)
      fun (x : ℂ) ↦ log ‖g x‖
⊢ ContinuousOn.{0, u_1} (Y := E) (fun (x : ℝ) ↦ g (circleMap c R x)) [[0, 2 * π]]
have pos : Set.MapsTo (circleMap c R) [[0, 2 * π]] (sphere c |R|)
Tactic: apply h₁g.continuousOn.comp (t := sphere c |R|) (continuous_circleMap c R).continuousOn
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
hf : MeromorphicOn f (sphere c |R|)
t₀ : ∀ (u : (↑(sphere c |R|) : Type)), meromorphicOrderAt f (↑u : ℂ) ≠ ⊤
g : ℂ → E
h₁g : AnalyticOnNhd ℂ g (sphere c |R|)
h₂g : ∀ (u : (↑(sphere c |R|) : Type)), g (↑u : ℂ) ≠ 0
h₃g :
  f =ᶠ[codiscreteWithin (sphere c |R|)]
    HSMul.hSMul (α := ℂ → ℂ)
      (∏ᶠ (u : ℂ),
        HPow.hPow (α := ℂ → ℂ) (β := ℤ) (fun (x : ℂ) ↦ x - u) ((divisor f (sphere c |R|) : (a : ℂ) → ℤ) u : ℤ))
      g
h₄g :
  (fun (x : ℂ) ↦ log ‖f x‖) =ᶠ[codiscreteWithin (sphere c |R|)]
    HAdd.hAdd (α := ℂ → ℝ) (∑ᶠ (u : ℂ), fun (x : ℂ) ↦ (↑((divisor f (sphere c |R|) : (a : ℂ) → ℤ) u) : ℝ) * log ‖x - u‖)
      fun (x : ℂ) ↦ log ‖g x‖
x : ℝ
hx : x ∈ [[0, 2 * π]]
⊢ ‖g (circleMap c R x)‖ ≠ 0
have pos : ¬g (circleMap c R x) = 0
Tactic: rw [ne_eq, norm_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
hf : MeromorphicOn f (sphere c |R|)
t₀ : ¬∀ (u : (↑(sphere c |R|) : Type)), meromorphicOrderAt f (↑u : ℂ) ≠ ⊤
⊢ CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log ‖f x‖) c R
have t₁ : ¬∃ (u : (↑(sphere c |R|) : Type)), meromorphicOrderAt f (↑u : ℂ) ≠ ⊤
Tactic: rw [← hf.exists_meromorphicOrderAt_ne_top_iff_forall (isConnected_sphere (by simp) c
      (abs_nonneg R))] at t₀
Cleared hypotheses: t₀
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
hf : MeromorphicOn f (sphere c |R|)
t₀ : ¬∃ (u : (↑(sphere c |R|) : Type)), meromorphicOrderAt f (↑u : ℂ) ≠ ⊤
⊢ CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log ‖f x‖) c R
have t₁ : ∀ (u : (↑(sphere c |R|) : Type)), meromorphicOrderAt f (↑u : ℂ) = ⊤
Tactic: push Not at t₀
Cleared hypotheses: t₀
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
hf : MeromorphicOn f (sphere c |R|)
t₀ : ∀ (u : (↑(sphere c |R|) : Type)), meromorphicOrderAt f (↑u : ℂ) = ⊤
⊢ (codiscreteWithin (sphere c |R|)).EventuallyEq (β := ℝ) (fun (x : ℂ) ↦ log ‖f x‖) 0
have h : ∀ (x : ℂ) (h₁x : MeromorphicNFAt f x) (h₂x : x ∈ sphere c |R|), log ‖f x‖ = 0 x
Tactic: filter_upwards [hf.meromorphicNFAt_mem_codiscreteWithin,
        self_mem_codiscreteWithin (sphere c |R|)] with x h₁x h₂x
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
hf : MeromorphicOn f (sphere c |R|)
t₀ : ∀ (u : (↑(sphere c |R|) : Type)), meromorphicOrderAt f (↑u : ℂ) = ⊤
x : ℂ
h₁x : MeromorphicNFAt f x
h₂x : x ∈ sphere c |R|
⊢ log ‖f x‖ = 0 x
have h : f x = 0 ∨ ‖f x‖ = 1 ∨ ‖f x‖ = -1
Tactic: simp only [Pi.zero_apply, log_eq_zero, norm_eq_zero]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
hf : MeromorphicOn f (sphere c |R|)
t₀ : ∀ (u : (↑(sphere c |R|) : Type)), meromorphicOrderAt f (↑u : ℂ) = ⊤
x : ℂ
h₁x : MeromorphicNFAt f x
h₂x : x ∈ sphere c |R|
⊢ f x = 0 ∨ ‖f x‖ = 1 ∨ ‖f x‖ = -1
have h : f x = 0
Tactic: left
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
hf : MeromorphicOn f (sphere c |R|)
t₀ : ∀ (u : (↑(sphere c |R|) : Type)), meromorphicOrderAt f (↑u : ℂ) = ⊤
x : ℂ
h₁x : MeromorphicNFAt f x
h₂x : x ∈ sphere c |R|
⊢ f x = 0
have h : ∀ (hCon : ¬f x = 0), False
Tactic: by_contra hCon
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
hf : MeromorphicOn f (sphere c |R|)
t₀ : ∀ (u : (↑(sphere c |R|) : Type)), meromorphicOrderAt f (↑u : ℂ) = ⊤
⊢ CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log ‖f x‖) c R
have this : (codiscreteWithin (sphere c |R|)).EventuallyEq (β := ℝ) (fun (x : ℂ) ↦ log ‖f x‖) 0
Tactic: have : (log ‖f ·‖) =ᶠ[codiscreteWithin (sphere c |R|)] 0 := by
      filter_upwards [hf.meromorphicNFAt_mem_codiscreteWithin,
        self_mem_codiscreteWithin (sphere c |R|)] with x h₁x h₂x
      simp only [Pi.zero_apply, log_eq_zero, norm_eq_zero]
      left
      by_contra hCon
      simp_all [← h₁x.meromorphicOrderAt_eq_zero_iff, t₀ ⟨x, h₂x⟩]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
hf : MeromorphicOn f (sphere c R)
hR : 0 ≤ R
⊢ CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log ‖f x‖) c R
have hf₁ : MeromorphicOn f (sphere c |R|)
Tactic: rw [← abs_of_nonneg hR] at hf
Cleared hypotheses: hf, hR
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
hf : MeromorphicOn f (sphere c |R|)
⊢ CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f x‖) c R
have simp_rw : CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ 2⁻¹ * log ‖f x‖ + 2⁻¹ * |log ‖f x‖|) c R
Tactic: simp_rw [← half_mul_log_add_log_abs, mul_add]
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
hf : MeromorphicOn f (sphere c |R|)
⊢ CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ 2⁻¹ * log ‖f x‖ + 2⁻¹ * |log ‖f x‖|) c R
have hf₁ : CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ 2⁻¹ * log ‖f x‖) c R
Tactic: apply CircleIntegrable.add
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic (goal)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
hf : MeromorphicOn f (sphere c |R|)
hf₁ : CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ 2⁻¹ * log ‖f x‖) c R
⊢ CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ 2⁻¹ * log ‖f x‖ + 2⁻¹ * |log ‖f x‖|) c R
have hg : CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ 2⁻¹ * |log ‖f x‖|) c R
Tactic: apply CircleIntegrable.add
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic (hypothesis)
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
hf : MeromorphicOn f (sphere c R)
hR : 0 ≤ R
⊢ CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f x‖) c R
have hf₁ : MeromorphicOn f (sphere c |R|)
Tactic: rw [← abs_of_nonneg hR] at hf
Cleared hypotheses: hf, hR
-- Lean 4 proof step from Mathlib.Analysis.SpecialFunctions.Integrals.Basic (goal)
Goal:
a b : ℝ
r : ℂ
h : -1 < r.re ∨ r ≠ -1 ∧ 0 ∉ [[a, b]]
⊢ ∫ (x : ℝ) in a..b, (↑x : ℂ) ^ r = ((↑b : ℂ) ^ (r + 1) - (↑a : ℂ) ^ (r + 1)) / (r + 1)
have rw : ∫ (x : ℝ) in a..b, (↑x : ℂ) ^ r = (↑b : ℂ) ^ (r + 1) / (r + 1) - (↑a : ℂ) ^ (r + 1) / (r + 1)
Tactic: rw [sub_div]