awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
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 :
  ∀ (i : ℂ),
    CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ (↑((divisor f (sphere c |R|) : (a : ℂ) → ℤ) i) : ℝ) * log ‖x - i‖) c R
⊢ CircleIntegrable (E := ℝ)
    (∑ᶠ (u : ℂ), fun (x : ℂ) ↦ (↑((divisor f (sphere c |R|) : (a : ℂ) → ℤ) u) : ℝ) * log ‖x - u‖) c R

Tactic:
apply CircleIntegrable.finsum

Premises used: CircleIntegrable.finsum
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
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 : ℂ
pos : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log ‖circleMap c R x - i‖) volume 0 (2 * π)
⊢ CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ (↑((divisor f (sphere c |R|) : (a : ℂ) → ℤ) i) : ℝ) * log ‖x - i‖) c R

Tactic:
apply IntervalIntegrable.const_mul

Premises used: IntervalIntegrable.const_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
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 : ℂ
pos : MeromorphicOn (E := ℂ) (fun (x : ℝ) ↦ circleMap c R x - i) [[0, 2 * π]]
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log ‖circleMap c R x - i‖) volume 0 (2 * π)

Tactic:
apply MeromorphicOn.intervalIntegrable_log_norm

Premises used: MeromorphicOn.intervalIntegrable_log_norm
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
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 : ℂ
pos : AnalyticOnNhd ℝ (F := ℂ) (fun (x : ℝ) ↦ circleMap c R x - i) [[0, 2 * π]]
⊢ MeromorphicOn (E := ℂ) (fun (x : ℝ) ↦ circleMap c R x - i) [[0, 2 * π]]

Tactic:
apply AnalyticOnNhd.meromorphicOn

Premises used: AnalyticOnNhd.meromorphicOn
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
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 : ℂ
apply : AnalyticOnNhd ℝ (circleMap c R) [[0, 2 * π]]
⊢ AnalyticOnNhd ℝ (F := ℂ) (fun (x : ℝ) ↦ circleMap c R x - i) [[0, 2 * π]]

Tactic:
apply AnalyticOnNhd.sub _ analyticOnNhd_const

Premises used: analyticOnNhd_const, AnalyticOnNhd.sub
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
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 : ℂ
tauto tauto₁ tauto₂ tauto₃ tauto₄ tauto₅ tauto₆ tauto₇ :
  ∀ ⦃a : ℝ⦄, a ∈ [[0, 2 * π]] → Membership.mem (γ := Set ℝ) Set.univ a
⊢ [[0, 2 * π]] ⊆ Set.univ

Tactic:
tauto
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
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 ℝ (circleMap c R) [[0, 2 * π]]

Tactic:
apply (analyticOnNhd_circleMap c R).mono (by tauto)

Premises used: analyticOnNhd_circleMap, AnalyticOnNhd.mono
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
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 (θ : ℝ) ↦ (fun (x : ℂ) ↦ log ‖g x‖) (circleMap c R θ)) [[0, 2 * π]]
⊢ CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log ‖g x‖) c R

Tactic:
apply ContinuousOn.intervalIntegrable

Premises used: ContinuousOn.intervalIntegrable
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
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 * π]]
pos₁ : ∀ x ∈ [[0, 2 * π]], ‖g (circleMap c R x)‖ ≠ 0
⊢ ContinuousOn (Y := ℝ) (fun (θ : ℝ) ↦ (fun (x : ℂ) ↦ log ‖g x‖) (circleMap c R θ)) [[0, 2 * π]]

Tactic:
apply ContinuousOn.log

Premises used: ContinuousOn.log
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
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.{0, u_1} (Y := E) (fun (x : ℝ) ↦ g (circleMap c R x)) [[0, 2 * π]]
⊢ ContinuousOn (Y := ℝ) (fun (x : ℝ) ↦ ‖g (circleMap c R x)‖) [[0, 2 * π]]

Tactic:
apply ContinuousOn.norm

Premises used: ContinuousOn.norm
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
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 : Set.MapsTo (circleMap c R) [[0, 2 * π]] (sphere c |R|)
⊢ ContinuousOn.{0, u_1} (Y := E) (fun (x : ℝ) ↦ g (circleMap c R x)) [[0, 2 * π]]

Tactic:
apply h₁g.continuousOn.comp (t := sphere c |R|) (continuous_circleMap c R).continuousOn

Premises used: Continuous.continuousOn, continuous_circleMap, ContinuousOn.comp, AnalyticOnNhd.continuousOn
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
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 * π]]
⊢ circleMap c R x ∈ sphere c |R|

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
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 * π]]
pos : ¬g (circleMap c R x) = 0
⊢ ‖g (circleMap c R x)‖ ≠ 0

Tactic:
rw [ne_eq, norm_eq_zero]

Premises used: norm_eq_zero, ne_eq
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
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

Tactic:
apply h₂g ⟨circleMap c R x, circleMap_mem_sphere' c R x⟩

Premises used: circleMap, Subtype.mk, circleMap_mem_sphere'
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
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 : ℂ) ≠ ⊤
⊢ 1 < Module.rank ℝ ℂ

Tactic:
simp
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
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 : ℂ) ≠ ⊤
⊢ ¬∃ (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₀

Premises used: isConnected_sphere, MeromorphicOn.exists_meromorphicOrderAt_ne_top_iff_forall, abs_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
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 : ℂ) ≠ ⊤
⊢ ∀ (u : (↑(sphere c |R|) : Type)), meromorphicOrderAt f (↑u : ℂ) = ⊤

Tactic:
push Not at t₀

Premises used: Not
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
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 : ℂ) = ⊤
h : ∀ (x : ℂ) (h₁x : MeromorphicNFAt f x) (h₂x : x ∈ sphere c |R|), log ‖f x‖ = 0 x
⊢ (codiscreteWithin (sphere c |R|)).EventuallyEq (β := ℝ) (fun (x : ℂ) ↦ log ‖f x‖) 0

Tactic:
filter_upwards [hf.meromorphicNFAt_mem_codiscreteWithin,
        self_mem_codiscreteWithin (sphere c |R|)] with x h₁x h₂x

Premises used: abs, MeromorphicOn.meromorphicNFAt_mem_codiscreteWithin, Filter.self_mem_codiscreteWithin, Metric.sphere
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
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|
h : f x = 0 ∨ ‖f x‖ = 1 ∨ ‖f x‖ = -1
⊢ log ‖f x‖ = 0 x

Tactic:
simp only [Pi.zero_apply, log_eq_zero, norm_eq_zero]

Premises used: norm_eq_zero, Pi.zero_apply, Real.log_eq_zero
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
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|
h : f x = 0
⊢ f x = 0 ∨ ‖f x‖ = 1 ∨ ‖f x‖ = -1

Tactic:
left
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
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|
h : ∀ (hCon : ¬f x = 0), False
⊢ f x = 0

Tactic:
by_contra hCon
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
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|
hCon : ¬f x = 0
⊢ False

Tactic:
simp_all [← h₁x.meromorphicOrderAt_eq_zero_iff, t₀ ⟨x, h₂x⟩]

Premises used: Subtype.mk, MeromorphicNFAt.meromorphicOrderAt_eq_zero_iff
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
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

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⟩]
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
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 : ℂ) = ⊤
this : (codiscreteWithin (sphere c |R|)).EventuallyEq (β := ℝ) (fun (x : ℂ) ↦ log ‖f x‖) 0
⊢ CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log ‖f x‖) c R

Tactic:
apply CircleIntegrable.congr_codiscreteWithin this.symm (circleIntegrable_const 0 c R)

Premises used: CircleIntegrable.congr_codiscreteWithin, OfNat.ofNat, circleIntegrable_const, Filter.EventuallyEq.symm
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
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
⊢ MeromorphicOn f (sphere c |R|)

Tactic:
rw [← abs_of_nonneg hR] at hf

Premises used: abs_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
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
hf₁ : MeromorphicOn f (sphere c |R|)
⊢ 0 ≤ R

Tactic:
rw [← abs_of_nonneg hR] at hf

Premises used: abs_of_nonneg
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
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

Tactic:
hf.circleIntegrable_log_norm

Premises used: MeromorphicOn.circleIntegrable_log_norm
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
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

Tactic:
exact hf.circleIntegrable_log_norm

Premises used: MeromorphicOn.circleIntegrable_log_norm
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
Goal:
R : ℝ
c : ℂ
D : ℂ → ℤ
⊢ CircleIntegrable (E := ℝ) (∑ᶠ (u : ℂ), fun (x : ℂ) ↦ (↑(D u) : ℝ) * log ‖x - u‖) c R

Tactic:
CircleIntegrable.finsum (fun _ ↦
    ((analyticOnNhd_id.sub analyticOnNhd_const).meromorphicOn.circleIntegrable_log_norm).const_smul)

Premises used: CircleIntegrable.const_smul, analyticOnNhd_id, analyticOnNhd_const, MeromorphicOn.circleIntegrable_log_norm, AnalyticOnNhd.meromorphicOn, CircleIntegrable.finsum, AnalyticOnNhd.sub
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
Goal:
E : Type u_1
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℂ E
c : ℂ
R : ℝ
f : ℂ → E
hf : MeromorphicOn f (sphere c |R|)
simp_rw : CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ 2⁻¹ * log ‖f x‖ + 2⁻¹ * |log ‖f x‖|) c R
⊢ CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ log⁺ ‖f x‖) c R

Tactic:
simp_rw [← half_mul_log_add_log_abs, mul_add]

Premises used: mul_add, Real.half_mul_log_add_log_abs
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
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
hg : CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ 2⁻¹ * |log ‖f x‖|) c R
⊢ CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ 2⁻¹ * log ‖f x‖ + 2⁻¹ * |log ‖f x‖|) c R

Tactic:
apply CircleIntegrable.add

Premises used: CircleIntegrable.add
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
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‖) c R

Tactic:
apply hf.circleIntegrable_log_norm.const_mul

Premises used: MeromorphicOn.circleIntegrable_log_norm, IntervalIntegrable.const_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
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‖|) c R

Tactic:
apply hf.circleIntegrable_log_norm.abs.const_mul

Premises used: CircleIntegrable.abs, MeromorphicOn.circleIntegrable_log_norm, IntervalIntegrable.const_mul
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
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

Tactic:
hf.circleIntegrable_posLog_norm

Premises used: MeromorphicOn.circleIntegrable_posLog_norm
-- Module: Mathlib.Analysis.SpecialFunctions.Integrability.LogMeromorphic
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

Tactic:
exact hf.circleIntegrable_posLog_norm

Premises used: MeromorphicOn.circleIntegrable_posLog_norm