awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
integral_bound : circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R ≤ Real.log M
⊢ Function.HasFiniteSupport (M := ℝ) fun (u : ℂ) ↦
    (↑((divisor f (closedBall c |r|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R / r)

Tactic:
exact (divisor f (closedBall c |r|)).finiteSupport (isCompact_closedBall ..) |>.subset
        fun _ _ ↦ (by simp_all)

Premises used: abs, Function.locallyFinsuppWithin.finiteSupport, MeromorphicOn.divisor, Set.Finite.subset, ProperSpace.isCompact_closedBall, Metric.closedBall
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
integral_bound : circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R ≤ Real.log M
x : ℂ
h :
  Membership.mem (γ := Set ℂ)
    (Function.support (M := ℝ) fun (u : ℂ) ↦
      (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹))
    x
⊢ x ∈ Function.locallyFinsuppWithin.support (U := closedBall c |R|) (divisor f (closedBall c |R|))

Tactic:
simp_all
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
integral_bound : circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R ≤ Real.log M
⊢ Function.HasFiniteSupport (M := ℝ) fun (u : ℂ) ↦
    (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹)

Tactic:
exact (divisor f (closedBall c |R|)).finiteSupport (isCompact_closedBall ..) |>.subset
        fun _ _ ↦ (by simp_all)

Premises used: abs, Function.locallyFinsuppWithin.finiteSupport, MeromorphicOn.divisor, Set.Finite.subset, ProperSpace.isCompact_closedBall, Metric.closedBall
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
integral_bound : circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R ≤ Real.log M
u : ℂ
pos :
  ∀ (h1 : u ∈ closedBall c |R|),
    (↑((divisor f (closedBall c |r|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R / r) ≤
      (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹)
neg :
  ∀ (h1 : u ∉ closedBall c |R|),
    (↑((divisor f (closedBall c |r|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R / r) ≤
      (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹)
⊢ (↑((divisor f (closedBall c |r|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R / r) ≤
    (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹)

Tactic:
by_cases h1 : u ∈ closedBall c |R|

Premises used: abs, Metric.closedBall
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
integral_bound : circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R ≤ Real.log M
u : ℂ
h1 : u ∈ closedBall c |R|
pos :
  ∀ (h2 : u ∈ closedBall c |r|),
    (↑((divisor f (closedBall c |r|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R / r) ≤
      (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹)
neg :
  ∀ (h2 : u ∉ closedBall c |r|),
    (↑((divisor f (closedBall c |r|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R / r) ≤
      (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹)
⊢ (↑((divisor f (closedBall c |r|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R / r) ≤
    (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹)

Tactic:
by_cases h2 : u ∈ closedBall c |r|

Premises used: abs, Metric.closedBall
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
integral_bound : circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R ≤ Real.log M
u : ℂ
h1 : u ∈ closedBall c |R|
h2 : u ∈ closedBall c |r|
pos :
  (↑(WithTop.untop₀ (ENat.map Nat.cast (analyticOrderAt f u))) : ℝ) * Real.log (R / r) ≤
    (↑(WithTop.untop₀ (ENat.map Nat.cast (analyticOrderAt f u))) : ℝ) * Real.log (R * ‖c - u‖⁻¹)
⊢ (↑((divisor f (closedBall c |r|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R / r) ≤
    (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹)

Tactic:
simp only [(h₁f.mono (closedBall_subset_closedBall r_lt_R.le)), h2,
            AnalyticOnNhd.divisor_apply, h₁f, h1]

Premises used: LT.lt.le, AnalyticOnNhd.mono, Metric.closedBall_subset_closedBall, MeromorphicOn.AnalyticOnNhd.divisor_apply
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
integral_bound : circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R ≤ Real.log M
u : ℂ
h1 : u ∈ closedBall c |R|
h2 : u ∈ closedBall c |r|
pos :
  ∀ (h3 : u = c),
    (↑(WithTop.untop₀ (ENat.map Nat.cast (analyticOrderAt f u))) : ℝ) * Real.log (R / r) ≤
      (↑(WithTop.untop₀ (ENat.map Nat.cast (analyticOrderAt f u))) : ℝ) * Real.log (R * ‖c - u‖⁻¹)
neg :
  ∀ (h3 : u ≠ c),
    (↑(WithTop.untop₀ (ENat.map Nat.cast (analyticOrderAt f u))) : ℝ) * Real.log (R / r) ≤
      (↑(WithTop.untop₀ (ENat.map Nat.cast (analyticOrderAt f u))) : ℝ) * Real.log (R * ‖c - u‖⁻¹)
⊢ (↑(WithTop.untop₀ (ENat.map Nat.cast (analyticOrderAt f u))) : ℝ) * Real.log (R / r) ≤
    (↑(WithTop.untop₀ (ENat.map Nat.cast (analyticOrderAt f u))) : ℝ) * Real.log (R * ‖c - u‖⁻¹)

Tactic:
by_cases! h3 : u = c
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
integral_bound : circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R ≤ Real.log M
u : ℂ
h1 : u ∈ closedBall c |R|
h2 : u ∈ closedBall c |r|
h3 : u = c
⊢ c ∈ closedBall c |R|

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
integral_bound : circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R ≤ Real.log M
u : ℂ
h1 : u ∈ closedBall c |R|
h2 : u ∈ closedBall c |r|
h3 : u = c
pos :
  (↑(WithTop.untop₀ (ENat.map Nat.cast 0)) : ℝ) * Real.log (R / r) ≤
    (↑(WithTop.untop₀ (ENat.map Nat.cast 0)) : ℝ) * Real.log (R * ‖c - c‖⁻¹)
⊢ (↑(WithTop.untop₀ (ENat.map Nat.cast (analyticOrderAt f u))) : ℝ) * Real.log (R / r) ≤
    (↑(WithTop.untop₀ (ENat.map Nat.cast (analyticOrderAt f u))) : ℝ) * Real.log (R * ‖c - u‖⁻¹)

Tactic:
rw [h3, (h₁f c (by simp)).analyticOrderAt_eq_zero.mpr h₂f]

Premises used: Iff.mpr, AnalyticAt.analyticOrderAt_eq_zero
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
integral_bound : circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R ≤ Real.log M
u : ℂ
h1 : u ∈ closedBall c |R|
h2 : u ∈ closedBall c |r|
h3 : u = c
⊢ (↑(WithTop.untop₀ (ENat.map Nat.cast 0)) : ℝ) * Real.log (R / r) ≤
    (↑(WithTop.untop₀ (ENat.map Nat.cast 0)) : ℝ) * Real.log (R * ‖c - c‖⁻¹)

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
integral_bound : circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R ≤ Real.log M
u : ℂ
h1 : u ∈ closedBall c |R|
h2 : u ∈ closedBall c |r|
h3 : u ≠ c
neg :
  (↑(WithTop.untop₀ (ENat.map Nat.cast (analyticOrderAt f u))) : ℝ) * Real.log |R / r| ≤
    (↑(WithTop.untop₀ (ENat.map Nat.cast (analyticOrderAt f u))) : ℝ) * Real.log |R * ‖c - u‖⁻¹|
⊢ (↑(WithTop.untop₀ (ENat.map Nat.cast (analyticOrderAt f u))) : ℝ) * Real.log (R / r) ≤
    (↑(WithTop.untop₀ (ENat.map Nat.cast (analyticOrderAt f u))) : ℝ) * Real.log (R * ‖c - u‖⁻¹)

Tactic:
simp +singlePass only [← log_abs]

Premises used: Real.log_abs
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
integral_bound : circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R ≤ Real.log M
u : ℂ
h1 : u ∈ closedBall c |R|
h2 : u ∈ closedBall c |r|
h3 : u ≠ c
neg : LE.le (α := ℝ) 0 (↑(WithTop.untop₀ (ENat.map Nat.cast (analyticOrderAt f u))) : ℝ)
neg₁ : |R / r| ≤ |R * ‖c - u‖⁻¹|
⊢ (↑(WithTop.untop₀ (ENat.map Nat.cast (analyticOrderAt f u))) : ℝ) * Real.log |R / r| ≤
    (↑(WithTop.untop₀ (ENat.map Nat.cast (analyticOrderAt f u))) : ℝ) * Real.log |R * ‖c - u‖⁻¹|

Tactic:
gcongr 2
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
integral_bound : circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R ≤ Real.log M
u : ℂ
h1 : u ∈ closedBall c |R|
h2 : u ∈ closedBall c |r|
h3 : u ≠ c
⊢ LE.le (α := ℝ) 0 (↑(WithTop.untop₀ (ENat.map Nat.cast (analyticOrderAt f u))) : ℝ)

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
integral_bound : circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R ≤ Real.log M
u : ℂ
h1 : u ∈ closedBall c |R|
h2 : u ∈ closedBall c |r|
h3 : u ≠ c
⊢ ‖c - u‖ ≠ 0

Tactic:
simpa [sub_eq_zero] using h3.symm

Premises used: sub_eq_zero, Ne.symm
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
integral_bound : circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R ≤ Real.log M
u : ℂ
h1 : u ∈ closedBall c |R|
h2 : u ∈ closedBall c |r|
h3 : u ≠ c
⊢ ‖c - u‖ ≠ 0

Tactic:
have : ‖c - u‖ ≠ 0 := by simpa [sub_eq_zero] using h3.symm
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
integral_bound : circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R ≤ Real.log M
u : ℂ
h1 : u ∈ closedBall c |R|
h2 : u ∈ closedBall c |r|
h3 : u ≠ c
this : ‖c - u‖ ≠ 0
⊢ |R / r| ≤ |R * ‖c - u‖⁻¹|

Tactic:
simpa [field, abs_div, r_pos.trans r_lt_R, dist_eq_norm'] using h2

Premises used: dist_eq_norm', abs_div, LT.lt.trans
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
integral_bound : circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R ≤ Real.log M
u : ℂ
h1 : u ∈ closedBall c |R|
h2 : u ∉ closedBall c |r|
neg : 0 ≤ (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹)
⊢ (↑((divisor f (closedBall c |r|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R / r) ≤
    (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹)

Tactic:
simp only [h2, not_false_eq_true, Function.locallyFinsuppWithin.apply_eq_zero_of_notMem,
            Int.cast_zero, zero_mul]

Premises used: Int.cast_zero, Function.locallyFinsuppWithin.apply_eq_zero_of_notMem, MulZeroClass.zero_mul, not_false_eq_true
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
integral_bound : circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R ≤ Real.log M
u : ℂ
h1 : u ∈ closedBall c |R|
h2 : u ∉ closedBall c |r|
⊢ 0 ≤ (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹)

Tactic:
mul_nonneg (mod_cast h₁f.divisor_nonneg ..) ?_

Premises used: Int.cast, mul_nonneg, abs, congrArg, Int.cast_zero, cast, MeromorphicOn.divisor, LE.le, Int.cast_le._simp_1, MeromorphicOn.AnalyticOnNhd.divisor_nonneg, congrFun', Nat.cast_zero, Metric.closedBall, Eq.symm, DFunLike.coe, Eq.trans
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
integral_bound : circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R ≤ Real.log M
u : ℂ
h1 : u ∈ closedBall c |R|
h2 : u ∉ closedBall c |r|
neg : 0 ≤ Real.log (R * ‖c - u‖⁻¹)
⊢ 0 ≤ (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹)

Tactic:
refine mul_nonneg (mod_cast h₁f.divisor_nonneg ..) ?_

Premises used: mul_nonneg
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
integral_bound : circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R ≤ Real.log M
u : ℂ
h1 : u ∈ closedBall c |R|
h2 : u ∉ closedBall c |r|
neg : 1 ≤ |R * ‖c - u‖⁻¹|
⊢ 0 ≤ Real.log (R * ‖c - u‖⁻¹)

Tactic:
apply log_abs _ ▸ log_nonneg
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
integral_bound : circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R ≤ Real.log M
u : ℂ
h1 : u ∈ closedBall c |R|
h2 : u ∉ closedBall c |r|
⊢ ‖c - u‖ ≤ |R|

Tactic:
simp only [mem_closedBall, dist_eq_norm', not_le] at h1 h2

Premises used: not_le, dist_eq_norm', Metric.mem_closedBall
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
integral_bound : circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R ≤ Real.log M
u : ℂ
h1 : u ∈ closedBall c |R|
h2 : u ∉ closedBall c |r|
h1₁ : ‖c - u‖ ≤ |R|
⊢ |r| < ‖c - u‖

Tactic:
simp only [mem_closedBall, dist_eq_norm', not_le] at h1 h2

Premises used: not_le, dist_eq_norm', Metric.mem_closedBall
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
integral_bound : circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R ≤ Real.log M
u : ℂ
h1 : ‖c - u‖ ≤ |R|
h2 : |r| < ‖c - u‖
⊢ ‖c - u‖ ≠ 0

Tactic:
have : ‖c - u‖ ≠ 0 := (r_pos.trans h2).ne'
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
integral_bound : circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R ≤ Real.log M
u : ℂ
h1 : ‖c - u‖ ≤ |R|
h2 : |r| < ‖c - u‖
this : ‖c - u‖ ≠ 0
⊢ 1 ≤ |R * ‖c - u‖⁻¹|

Tactic:
simpa [field]
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
integral_bound : circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R ≤ Real.log M
u : ℂ
h1 : u ∉ closedBall c |R|
simp_all :
  ∀ (r_pos : ¬r = 0) (r_lt_R : |r| < |R|) (hM : 1 ≤ M) (h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)) (h₂f : ¬f c = 0)
    (f_bound : ∀ (z : ℂ), ‖z - c‖ = |R| → ‖f z‖ ≤ M) (hrR : 1 < |R / r|)
    (jensen :
      circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R =
        ∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖)
    (integral_bound :
      ∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖ ≤
        Real.log M)
    (h1 : |R| < dist u c), |r| < dist u c
⊢ u ∉ closedBall c |r|

Tactic:
simp_all
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
c : ℂ
r R M : ℝ
f : ℂ → ℂ
u : ℂ
r_pos : ¬r = 0
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : ¬f c = 0
f_bound : ∀ (z : ℂ), ‖z - c‖ = |R| → ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
integral_bound :
  ∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖ ≤
    Real.log M
h1 : |R| < dist u c
linarith : dist u c ≤ |r| → |r| - |R| + (|R| - dist u c) + (dist u c - |r|) = 0
⊢ |r| < dist u c

Tactic:
linarith
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
integral_bound : circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R ≤ Real.log M
u : ℂ
h1 : u ∉ closedBall c |R|
⊢ u ∉ closedBall c |r|

Tactic:
have : u ∉ closedBall c |r| := by
          simp_all
          linarith
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
c : ℂ
r R M : ℝ
f : ℂ → ℂ
r_pos : 0 < |r|
r_lt_R : |r| < |R|
hM : 1 ≤ M
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
f_bound : ∀ z ∈ sphere c |R|, ‖f z‖ ≤ M
hrR : 1 < |R / r|
jensen :
  circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R =
    ∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
integral_bound : circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R ≤ Real.log M
u : ℂ
h1 : u ∉ closedBall c |R|
this : u ∉ closedBall c |r|
⊢ (↑((divisor f (closedBall c |r|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R / r) ≤
    (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹)

Tactic:
simp [h1, this]