awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
R : ℝ
c : ℂ
g : ℂ → ℂ
h₁g : AnalyticOnNhd ℂ g (closedBall c |R|)
h₂g : ∀ u ∈ closedBall c |R|, g u ≠ 0
⊢ circleAverage (fun (x : ℂ) ↦ Real.log ‖g x‖) c R = Real.log ‖g c‖

Tactic:
HarmonicOnNhd.circleAverage_eq (fun x hx ↦ (h₁g x hx).harmonicAt_log_norm (h₂g x hx))

Premises used: HarmonicOnNhd.circleAverage_eq, AnalyticAt.harmonicAt_log_norm
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
c : ℂ
R : ℝ
D : ℂ → ℤ
hR : R ≠ 0
hD : Function.HasFiniteSupport D
pos :
  ∀ (h : c ∈ Function.support D),
    ∑ᶠ (u : ℂ), (↑(D u) : ℝ) * (log R - log ‖c - u‖) =
      ∑ᶠ (u : ℂ), (↑(D u) : ℝ) * log (R * ‖c - u‖⁻¹) + (↑(D c) : ℝ) * log R
neg :
  ∀ (h : c ∉ Function.support D),
    ∑ᶠ (u : ℂ), (↑(D u) : ℝ) * (log R - log ‖c - u‖) =
      ∑ᶠ (u : ℂ), (↑(D u) : ℝ) * log (R * ‖c - u‖⁻¹) + (↑(D c) : ℝ) * log R
⊢ ∑ᶠ (u : ℂ), (↑(D u) : ℝ) * (log R - log ‖c - u‖) =
    ∑ᶠ (u : ℂ), (↑(D u) : ℝ) * log (R * ‖c - u‖⁻¹) + (↑(D c) : ℝ) * log R

Tactic:
by_cases h : c ∈ D.support

Premises used: Function.support
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
c : ℂ
R : ℝ
D : ℂ → ℤ
hR : R ≠ 0
hD : Function.HasFiniteSupport D
h : c ∈ Function.support D
g : ℂ → ℝ
x : ℂ
⊢ Membership.mem (γ := Set ℂ) (Function.support (M := ℝ) fun (u : ℂ) ↦ (↑(D u) : ℝ) * g u) x →
    x ∈ (↑(Finite.toFinset (s := Function.support D) hD) : Set ℂ)

Tactic:
simp +contextual
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
c : ℂ
R : ℝ
D : ℂ → ℤ
hR : R ≠ 0
hD : Function.HasFiniteSupport D
h : c ∈ Function.support D
⊢ ∀ {g : ℂ → ℝ},
    (Function.support (M := ℝ) fun (u : ℂ) ↦ (↑(D u) : ℝ) * g u) ⊆
      (↑(Finite.toFinset (s := Function.support D) hD) : Set ℂ)

Tactic:
have {g : ℂ → ℝ} : (fun u ↦ D u * g u).support ⊆ hD.toFinset :=
      fun x ↦ by simp +contextual
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
c : ℂ
R : ℝ
D : ℂ → ℤ
hR : R ≠ 0
hD : Function.HasFiniteSupport D
h : c ∈ Function.support D
this :
  ∀ {g : ℂ → ℝ},
    (Function.support (M := ℝ) fun (u : ℂ) ↦ (↑(D u) : ℝ) * g u) ⊆
      (↑(Finite.toFinset (s := Function.support D) hD) : Set ℂ)
pos :
  Eq (α := ℝ) (∑ u ∈ Finite.toFinset (s := Function.support D) hD \ {c}, (↑(D u) : ℝ) * (log R - log ‖c - u‖))
    (∑ u ∈ Finite.toFinset (s := Function.support D) hD \ {c}, (↑(D u) : ℝ) * log (R * ‖c - u‖⁻¹))
⊢ ∑ᶠ (u : ℂ), (↑(D u) : ℝ) * (log R - log ‖c - u‖) =
    ∑ᶠ (u : ℂ), (↑(D u) : ℝ) * log (R * ‖c - u‖⁻¹) + (↑(D c) : ℝ) * log R

Tactic:
simp only [finsum_eq_sum_of_support_subset _ this,
      Finset.sum_eq_sum_diff_singleton_add ((Set.Finite.mem_toFinset hD).mpr h), sub_self,
      norm_zero, log_zero, sub_zero, inv_zero, mul_zero, add_zero, add_left_inj]

Premises used: Iff.mpr, sub_self, sub_zero, Set.Finite.mem_toFinset, inv_zero, norm_zero, Finset.sum_eq_sum_diff_singleton_add, add_left_inj, MulZeroClass.mul_zero, finsum_eq_sum_of_support_subset, add_zero, Real.log_zero
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
c : ℂ
R : ℝ
D : ℂ → ℤ
hR : R ≠ 0
hD : Function.HasFiniteSupport D
h : c ∈ Function.support D
this :
  ∀ {g : ℂ → ℝ},
    (Function.support (M := ℝ) fun (u : ℂ) ↦ (↑(D u) : ℝ) * g u) ⊆
      (↑(Finite.toFinset (s := Function.support D) hD) : Set ℂ)
⊢ Eq (α := ℝ) (∑ u ∈ Finite.toFinset (s := Function.support D) hD \ {c}, (↑(D u) : ℝ) * (log R - log ‖c - u‖))
    (∑ u ∈ Finite.toFinset (s := Function.support D) hD \ {c}, (↑(D u) : ℝ) * log (R * ‖c - u‖⁻¹))

Tactic:
Finset.sum_congr rfl fun x hx ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
c : ℂ
R : ℝ
D : ℂ → ℤ
hR : R ≠ 0
hD : Function.HasFiniteSupport D
h : c ∈ Function.support D
this :
  ∀ {g : ℂ → ℝ},
    (Function.support (M := ℝ) fun (u : ℂ) ↦ (↑(D u) : ℝ) * g u) ⊆
      (↑(Finite.toFinset (s := Function.support D) hD) : Set ℂ)
pos :
  ∀ (x : ℂ) (hx : x ∈ Finite.toFinset (s := Function.support D) hD \ {c}),
    (↑(D x) : ℝ) * (log R - log ‖c - x‖) = (↑(D x) : ℝ) * log (R * ‖c - x‖⁻¹)
⊢ Eq (α := ℝ) (∑ u ∈ Finite.toFinset (s := Function.support D) hD \ {c}, (↑(D u) : ℝ) * (log R - log ‖c - u‖))
    (∑ u ∈ Finite.toFinset (s := Function.support D) hD \ {c}, (↑(D u) : ℝ) * log (R * ‖c - u‖⁻¹))

Tactic:
refine Finset.sum_congr rfl fun x hx ↦ ?_

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
c : ℂ
R : ℝ
D : ℂ → ℤ
hR : R ≠ 0
hD : Function.HasFiniteSupport D
h : c ∈ Function.support D
this :
  ∀ {g : ℂ → ℝ},
    (Function.support (M := ℝ) fun (u : ℂ) ↦ (↑(D u) : ℝ) * g u) ⊆
      (↑(Finite.toFinset (s := Function.support D) hD) : Set ℂ)
x : ℂ
hx : x ∈ Finite.toFinset (s := Function.support D) hD \ {c}
⊢ x ∈ Finite.toFinset (s := Function.support D) hD ∧ x ≠ c

Tactic:
simp only [Finset.mem_sdiff, Finset.notMem_singleton] at hx

Premises used: Finset.notMem_singleton, Finset.mem_sdiff
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
c : ℂ
R : ℝ
D : ℂ → ℤ
hR : R ≠ 0
hD : Function.HasFiniteSupport D
h : c ∈ Function.support D
this :
  ∀ {g : ℂ → ℝ},
    (Function.support (M := ℝ) fun (u : ℂ) ↦ (↑(D u) : ℝ) * g u) ⊆
      (↑(Finite.toFinset (s := Function.support D) hD) : Set ℂ)
x : ℂ
hx : x ∈ Finite.toFinset (s := Function.support D) hD ∧ x ≠ c
pos : (↑(D x) : ℝ) * (log R - log ‖c - x‖) = (↑(D x) : ℝ) * (log R + -log ‖c - x‖)
⊢ (↑(D x) : ℝ) * (log R - log ‖c - x‖) = (↑(D x) : ℝ) * log (R * ‖c - x‖⁻¹)

Tactic:
rw [log_mul hR (inv_ne_zero (norm_ne_zero_iff.mpr (sub_eq_zero.not.2 hx.2.symm))), log_inv]

Premises used: Iff.mpr, sub_eq_zero, Iff.not, Ne.symm, norm_ne_zero_iff, And.right, inv_ne_zero, Real.log_inv, Real.log_mul
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
c : ℂ
R : ℝ
D : ℂ → ℤ
hR : R ≠ 0
hD : Function.HasFiniteSupport D
h : c ∈ Function.support D
this :
  ∀ {g : ℂ → ℝ},
    (Function.support (M := ℝ) fun (u : ℂ) ↦ (↑(D u) : ℝ) * g u) ⊆
      (↑(Finite.toFinset (s := Function.support D) hD) : Set ℂ)
x : ℂ
hx : x ∈ Finite.toFinset (s := Function.support D) hD ∧ x ≠ c
⊢ (↑(D x) : ℝ) * (log R - log ‖c - x‖) = (↑(D x) : ℝ) * (log R + -log ‖c - x‖)

Tactic:
ring
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
c : ℂ
R : ℝ
D : ℂ → ℤ
hR : R ≠ 0
hD : Function.HasFiniteSupport D
h : c ∉ Function.support D
neg :
  ∀ (h : D c = 0),
    Eq (α := ℝ) (∑ᶠ (u : ℂ), (↑(D u) : ℝ) * (log R - log ‖c - u‖)) (∑ᶠ (u : ℂ), (↑(D u) : ℝ) * log (R * ‖c - u‖⁻¹))
⊢ ∑ᶠ (u : ℂ), (↑(D u) : ℝ) * (log R - log ‖c - u‖) =
    ∑ᶠ (u : ℂ), (↑(D u) : ℝ) * log (R * ‖c - u‖⁻¹) + (↑(D c) : ℝ) * log R

Tactic:
simp_all only [Function.mem_support, Decidable.not_not, Int.cast_zero, zero_mul, add_zero]

Premises used: Int.cast_zero, MulZeroClass.zero_mul, Function.mem_support, Decidable.not_not, add_zero
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
c : ℂ
R : ℝ
D : ℂ → ℤ
hR : R ≠ 0
hD : Function.HasFiniteSupport D
h : D c = 0
⊢ Eq (α := ℝ) (∑ᶠ (u : ℂ), (↑(D u) : ℝ) * (log R - log ‖c - u‖)) (∑ᶠ (u : ℂ), (↑(D u) : ℝ) * log (R * ‖c - u‖⁻¹))

Tactic:
finsum_congr fun x ↦ ?_

Premises used: finsum_congr
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
c : ℂ
R : ℝ
D : ℂ → ℤ
hR : R ≠ 0
hD : Function.HasFiniteSupport D
h : D c = 0
neg : ∀ (x : ℂ), (↑(D x) : ℝ) * (log R - log ‖c - x‖) = (↑(D x) : ℝ) * log (R * ‖c - x‖⁻¹)
⊢ Eq (α := ℝ) (∑ᶠ (u : ℂ), (↑(D u) : ℝ) * (log R - log ‖c - u‖)) (∑ᶠ (u : ℂ), (↑(D u) : ℝ) * log (R * ‖c - u‖⁻¹))

Tactic:
refine finsum_congr fun x ↦ ?_

Premises used: finsum_congr
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
c : ℂ
R : ℝ
D : ℂ → ℤ
hR : R ≠ 0
hD : Function.HasFiniteSupport D
h : D c = 0
x : ℂ
pos : ∀ (h₁ : c = x), (↑(D x) : ℝ) * (log R - log ‖c - x‖) = (↑(D x) : ℝ) * log (R * ‖c - x‖⁻¹)
neg : ∀ (h₁ : ¬c = x), (↑(D x) : ℝ) * (log R - log ‖c - x‖) = (↑(D x) : ℝ) * log (R * ‖c - x‖⁻¹)
⊢ (↑(D x) : ℝ) * (log R - log ‖c - x‖) = (↑(D x) : ℝ) * log (R * ‖c - x‖⁻¹)

Tactic:
by_cases h₁ : c = x
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
c : ℂ
R : ℝ
D : ℂ → ℤ
hR : R ≠ 0
hD : Function.HasFiniteSupport D
h : D c = 0
x : ℂ
h₁ : c = x
⊢ (↑(D x) : ℝ) * (log R - log ‖c - x‖) = (↑(D x) : ℝ) * log (R * ‖c - x‖⁻¹)

Tactic:
simp_all
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
c : ℂ
R : ℝ
D : ℂ → ℤ
hR : R ≠ 0
hD : Function.HasFiniteSupport D
h : D c = 0
x : ℂ
h₁ : ¬c = x
neg : (↑(D x) : ℝ) * (log R - log ‖c - x‖) = (↑(D x) : ℝ) * (log R + -log ‖c - x‖)
⊢ (↑(D x) : ℝ) * (log R - log ‖c - x‖) = (↑(D x) : ℝ) * log (R * ‖c - x‖⁻¹)

Tactic:
rw [log_mul hR (inv_ne_zero (norm_ne_zero_iff.mpr (sub_eq_zero.not.2 h₁))), log_inv]

Premises used: Iff.mpr, sub_eq_zero, Iff.not, norm_ne_zero_iff, inv_ne_zero, Real.log_inv, Real.log_mul
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
c : ℂ
R : ℝ
D : ℂ → ℤ
hR : R ≠ 0
hD : Function.HasFiniteSupport D
h : D c = 0
x : ℂ
h₁ : ¬c = x
⊢ (↑(D x) : ℝ) * (log R - log ‖c - x‖) = (↑(D x) : ℝ) * (log R + -log ‖c - x‖)

Tactic:
ring
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
⊢ c ∈ closedBall c |R|

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
rw :
  ∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹) +
        (↑(WithTop.untop₀ (ENat.map Nat.cast 0)) : ℝ) * Real.log R +
      Real.log ‖f c‖ =
    ∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f c‖
⊢ 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‖

Tactic:
rw [h₁f.meromorphicOn.circleAverage_log_norm hR, h₁f.divisor_apply (by simp),
    (h₁f c (by simp)).analyticOrderAt_eq_zero.mpr h₂f,
    (h₁f c (by simp)).meromorphicTrailingCoeffAt_of_ne_zero h₂f]

Premises used: Iff.mpr, AnalyticAt.meromorphicTrailingCoeffAt_of_ne_zero, MeromorphicOn.circleAverage_log_norm, MeromorphicOn.AnalyticOnNhd.divisor_apply, AnalyticOnNhd.meromorphicOn, AnalyticAt.analyticOrderAt_eq_zero
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
⊢ ∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹) +
        (↑(WithTop.untop₀ (ENat.map Nat.cast 0)) : ℝ) * Real.log R +
      Real.log ‖f c‖ =
    ∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹) + Real.log ‖f 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
trans :
  LE.le (α := ℝ) (↑(∑ᶠ (u : ℂ), (divisor f (closedBall c |r|) : (a : ℂ) → ℤ) u) : ℝ)
    (∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |r|) : (a : ℂ) → ℤ) u) : ℝ))
trans₁ : ∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |r|) : (a : ℂ) → ℤ) u) : ℝ) ≤ Real.log (M / ‖f c‖) / Real.log (R / r)
⊢ (↑(∑ᶠ (u : ℂ), (divisor f (closedBall c |r|) : (a : ℂ) → ℤ) u) : ℝ) ≤ Real.log (M / ‖f c‖) / Real.log (R / r)

Tactic:
trans ∑ᶠ u, (divisor f (closedBall c |r|) u : ℝ)
-- 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
⊢ LE.le (α := ℝ) (↑(∑ᶠ (u : ℂ), (divisor f (closedBall c |r|) : (a : ℂ) → ℤ) u) : ℝ)
    (∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |r|) : (a : ℂ) → ℤ) u) : ℝ))

Tactic:
map_finsum (Int.castRingHom ℝ)
      ((divisor _ _).finiteSupport <| isCompact_closedBall ..) |>.le

Premises used: Real, Set.Mem, Function.locallyFinsuppWithin.finiteSupport, MeromorphicOn.divisor, Eq.le, map_finsum, Int.castRingHom, ProperSpace.isCompact_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
⊢ LE.le (α := ℝ) (↑(∑ᶠ (u : ℂ), (divisor f (closedBall c |r|) : (a : ℂ) → ℤ) u) : ℝ)
    (∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |r|) : (a : ℂ) → ℤ) u) : ℝ))

Tactic:
exact map_finsum (Int.castRingHom ℝ)
      ((divisor _ _).finiteSupport <| isCompact_closedBall ..) |>.le

Premises used: Real, Function.locallyFinsuppWithin.finiteSupport, MeromorphicOn.divisor, Eq.le, map_finsum, Int.castRingHom, ProperSpace.isCompact_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
⊢ 1 < |R / r|

Tactic:
simpa [abs_div, one_lt_div r_pos]

Premises used: one_lt_div, abs_div
-- 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
⊢ 1 < |R / r|

Tactic:
have hrR : 1 < |R / r| := by simpa [abs_div, one_lt_div r_pos]
-- 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|
this : ∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |r|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R / r) ≤ Real.log (M / ‖f c‖)
rwa :
  ∀
    (this :
      (∑ᶠ (a : ℂ), (↑((divisor f (closedBall c |r|) : (a : ℂ) → ℤ) a) : ℝ)) * Real.log (R / r) ≤ Real.log (M / ‖f c‖)),
    0 < Real.log (R / r)
⊢ ∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |r|) : (a : ℂ) → ℤ) u) : ℝ) ≤ Real.log (M / ‖f c‖) / Real.log (R / r)

Tactic:
rwa [← finsum_mul, ← le_div_iff₀] at this

Premises used: finsum_mul, le_div_iff₀
-- 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|
this : (∑ᶠ (a : ℂ), (↑((divisor f (closedBall c |r|) : (a : ℂ) → ℤ) a) : ℝ)) * Real.log (R / r) ≤ Real.log (M / ‖f c‖)
⊢ 0 < Real.log (R / r)

Tactic:
simpa using log_pos hrR

Premises used: Real.log_pos
-- 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|
suffices : ∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |r|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R / r) ≤ Real.log (M / ‖f c‖)
⊢ ∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |r|) : (a : ℂ) → ℤ) u) : ℝ) ≤ Real.log (M / ‖f c‖) / Real.log (R / r)

Tactic:
suffices ∑ᶠ u, divisor f (closedBall c |r|) u * Real.log (R / r) ≤ Real.log (M / ‖f c‖) by
    rwa [← finsum_mul, ← le_div_iff₀] at this
    simpa using log_pos hrR
-- 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|
linarith : |R| = 0 → 0 - |r| + (|r| - |R|) + (|R| - 0) = 0
⊢ |R| ≠ 0

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|
⊢ 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‖

Tactic:
have jensen := h₁f.circleAverage_log_norm (abs_ne_zero.mp (by linarith)) h₂f
-- 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‖
hf : CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ Real.log ‖f x‖) c R
h₂f₁ : ∀ x ∈ sphere c |R|, Real.log ‖f x‖ ≤ Real.log M
⊢ circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R ≤ Real.log M

Tactic:
apply circleAverage_mono_on_of_le_circle

Premises used: Real.circleAverage_mono_on_of_le_circle
-- 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‖
⊢ CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ Real.log ‖f x‖) c R

Tactic:
(h₁f.mono sphere_subset_closedBall).meromorphicOn.circleIntegrable_log_norm

Premises used: AnalyticOnNhd.mono, Metric.sphere_subset_closedBall, MeromorphicOn.circleIntegrable_log_norm, AnalyticOnNhd.meromorphicOn
-- 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‖
⊢ CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ Real.log ‖f x‖) c R

Tactic:
exact (h₁f.mono sphere_subset_closedBall).meromorphicOn.circleIntegrable_log_norm

Premises used: AnalyticOnNhd.mono, Metric.sphere_subset_closedBall, MeromorphicOn.circleIntegrable_log_norm, AnalyticOnNhd.meromorphicOn
-- 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‖
h₂f₁ : ∀ (z : ℂ) (hz : z ∈ sphere c |R|) (this : ‖f z‖ ≤ M), Real.log ‖f z‖ ≤ Real.log M
⊢ ∀ x ∈ sphere c |R|, Real.log ‖f x‖ ≤ Real.log M

Tactic:
peel f_bound with z hz _
-- 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‖
z : ℂ
hz : z ∈ sphere c |R|
this : ‖f z‖ ≤ M
h₂f₁ : ∀ (h : f z = 0), Real.log ‖f z‖ ≤ Real.log M
h₂f₂ : ∀ (h : 0 < ‖f z‖), Real.log ‖f z‖ ≤ Real.log M
⊢ Real.log ‖f z‖ ≤ Real.log M

Tactic:
obtain (h | h) := eq_zero_or_norm_pos (f z)

Premises used: eq_zero_or_norm_pos
-- 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‖
z : ℂ
hz : z ∈ sphere c |R|
this : ‖f z‖ ≤ M
h : f z = 0
⊢ Real.log ‖f z‖ ≤ Real.log M

Tactic:
simpa [h] using log_nonneg hM

Premises used: Real.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‖
z : ℂ
hz : z ∈ sphere c |R|
this : ‖f z‖ ≤ M
h : 0 < ‖f z‖
h₂f₁ : 0 < ‖f z‖
⊢ Real.log ‖f z‖ ≤ Real.log M

Tactic:
gcongr
-- 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‖
⊢ circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R ≤ Real.log M

Tactic:
have integral_bound : circleAverage (fun x ↦ Real.log ‖f x‖) c R ≤ Real.log M := by
    apply circleAverage_mono_on_of_le_circle
    · exact (h₁f.mono sphere_subset_closedBall).meromorphicOn.circleIntegrable_log_norm
    · peel f_bound with z hz _
      obtain (h | h) := eq_zero_or_norm_pos (f z)
      · simpa [h] using log_nonneg hM
      · gcongr
-- 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
⊢ LE.le (α := ℝ) (∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |r|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R / r))
    (∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹))

Tactic:
finsum_le_finsum' ?_ ?_ fun u ↦ ?_

Premises used: finsum_le_finsum'
-- 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
refine_1 :
  Function.HasFiniteSupport (M := ℝ) fun (u : ℂ) ↦
    (↑((divisor f (closedBall c |r|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R / r)
refine_2 :
  Function.HasFiniteSupport (M := ℝ) fun (u : ℂ) ↦
    (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹)
refine_3 :
  ∀ (u : ℂ),
    (↑((divisor f (closedBall c |r|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R / r) ≤
      (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹)
⊢ LE.le (α := ℝ) (∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |r|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R / r))
    (∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹))

Tactic:
refine finsum_le_finsum' ?_ ?_ fun u ↦ ?_

Premises used: finsum_le_finsum'
-- 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 / r))
    x
⊢ x ∈ Function.locallyFinsuppWithin.support (U := closedBall c |r|) (divisor f (closedBall c |r|))

Tactic:
simp_all