awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
Goal:
c : ℂ
R : ℝ
D : ℂ → ℤ
hR : R ≠ 0
hD : Function.HasFiniteSupport D
h : c ∉ Function.support D
⊢ ∑ᶠ (u : ℂ), (↑(D u) : ℝ) * (log R - log ‖c - u‖) =
    ∑ᶠ (u : ℂ), (↑(D u) : ℝ) * log (R * ‖c - u‖⁻¹) + (↑(D c) : ℝ) * log R
have neg : ∀ (h : D c = 0),
  Eq (α := ℝ) (∑ᶠ (u : ℂ), (↑(D u) : ℝ) * (log R - log ‖c - u‖)) (∑ᶠ (u : ℂ), (↑(D u) : ℝ) * log (R * ‖c - u‖⁻¹))
Tactic: simp_all only [Function.mem_support, Decidable.not_not, Int.cast_zero, zero_mul, add_zero]
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
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‖⁻¹))
have neg : ∀ (x : ℂ), (↑(D x) : ℝ) * (log R - log ‖c - x‖) = (↑(D x) : ℝ) * log (R * ‖c - x‖⁻¹)
Tactic: refine finsum_congr fun x ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
Goal:
c : ℂ
R : ℝ
D : ℂ → ℤ
hR : R ≠ 0
hD : Function.HasFiniteSupport D
h : D c = 0
x : ℂ
⊢ (↑(D x) : ℝ) * (log R - log ‖c - x‖) = (↑(D x) : ℝ) * log (R * ‖c - x‖⁻¹)
have pos : ∀ (h₁ : c = x), (↑(D x) : ℝ) * (log R - log ‖c - x‖) = (↑(D x) : ℝ) * log (R * ‖c - x‖⁻¹)
Tactic: by_cases h₁ : c = x
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
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‖⁻¹)
⊢ (↑(D x) : ℝ) * (log R - log ‖c - x‖) = (↑(D x) : ℝ) * log (R * ‖c - x‖⁻¹)
have neg : ∀ (h₁ : ¬c = x), (↑(D x) : ℝ) * (log R - log ‖c - x‖) = (↑(D x) : ℝ) * log (R * ‖c - x‖⁻¹)
Tactic: by_cases h₁ : c = x
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
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‖⁻¹)
have neg : (↑(D x) : ℝ) * (log R - log ‖c - x‖) = (↑(D x) : ℝ) * (log R + -log ‖c - x‖)
Tactic: rw [log_mul hR (inv_ne_zero (norm_ne_zero_iff.mpr (sub_eq_zero.not.2 h₁))), log_inv]
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
Goal:
c : ℂ
R : ℝ
f : ℂ → ℂ
hR : R ≠ 0
h₁f : AnalyticOnNhd ℂ f (closedBall c |R|)
h₂f : f c ≠ 0
⊢ 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‖
have 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‖
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]
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
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
⊢ (↑(∑ᶠ (u : ℂ), (divisor f (closedBall c |r|) : (a : ℂ) → ℤ) u) : ℝ) ≤ Real.log (M / ‖f c‖) / Real.log (R / r)
have trans : LE.le (α := ℝ) (↑(∑ᶠ (u : ℂ), (divisor f (closedBall c |r|) : (a : ℂ) → ℤ) u) : ℝ)
  (∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |r|) : (a : ℂ) → ℤ) u) : ℝ))
Tactic: trans ∑ᶠ u, (divisor f (closedBall c |r|) u : ℝ)
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
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) : ℝ))
⊢ (↑(∑ᶠ (u : ℂ), (divisor f (closedBall c |r|) : (a : ℂ) → ℤ) u) : ℝ) ≤ Real.log (M / ‖f c‖) / Real.log (R / r)
have trans₁ : ∑ᶠ (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 : ℝ)
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (hypothesis)
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
⊢ ∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |r|) : (a : ℂ) → ℤ) u) : ℝ) ≤ Real.log (M / ‖f c‖) / Real.log (R / r)
have hrR : 1 < |R / r|
Tactic: have hrR : 1 < |R / r| := by simpa [abs_div, one_lt_div r_pos]
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
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‖)
⊢ ∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |r|) : (a : ℂ) → ℤ) u) : ℝ) ≤ Real.log (M / ‖f c‖) / Real.log (R / r)
have rwa : ∀
  (this :
    (∑ᶠ (a : ℂ), (↑((divisor f (closedBall c |r|) : (a : ℂ) → ℤ) a) : ℝ)) * Real.log (R / r) ≤ Real.log (M / ‖f c‖)),
  0 < Real.log (R / r)
Tactic: rwa [← finsum_mul, ← le_div_iff₀] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
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|
⊢ ∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |r|) : (a : ℂ) → ℤ) u) : ℝ) ≤ Real.log (M / ‖f c‖) / Real.log (R / r)
have suffices : ∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |r|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R / r) ≤ Real.log (M / ‖f c‖)
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
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
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|
⊢ |R| ≠ 0
have linarith : |R| = 0 → 0 - |r| + (|r| - |R|) + (|R| - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (hypothesis)
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|
⊢ ∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |r|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R / r) ≤ Real.log (M / ‖f c‖)
have 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‖
Tactic: have jensen := h₁f.circleAverage_log_norm (abs_ne_zero.mp (by linarith)) h₂f
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
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
have hf : CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ Real.log ‖f x‖) c R
Tactic: apply circleAverage_mono_on_of_le_circle
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
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
⊢ circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R ≤ Real.log M
have h₂f₁ : ∀ x ∈ sphere c |R|, Real.log ‖f x‖ ≤ Real.log M
Tactic: apply circleAverage_mono_on_of_le_circle
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
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‖
⊢ ∀ x ∈ sphere c |R|, Real.log ‖f x‖ ≤ Real.log M
have h₂f₁ : ∀ (z : ℂ) (hz : z ∈ sphere c |R|) (this : ‖f z‖ ≤ M), Real.log ‖f z‖ ≤ Real.log M
Tactic: peel f_bound with z hz _
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
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
⊢ Real.log ‖f z‖ ≤ Real.log M
have h₂f₁ : ∀ (h : f z = 0), Real.log ‖f z‖ ≤ Real.log M
Tactic: obtain (h | h) := eq_zero_or_norm_pos (f z)
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
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
⊢ Real.log ‖f z‖ ≤ Real.log M
have h₂f₂ : ∀ (h : 0 < ‖f z‖), Real.log ‖f z‖ ≤ Real.log M
Tactic: obtain (h | h) := eq_zero_or_norm_pos (f z)
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (hypothesis)
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‖
⊢ ∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |r|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R / r) ≤ Real.log (M / ‖f c‖)
have integral_bound : 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
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
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‖⁻¹))
have refine_1 : Function.HasFiniteSupport (M := ℝ) fun (u : ℂ) ↦
  (↑((divisor f (closedBall c |r|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R / r)
Tactic: refine finsum_le_finsum' ?_ ?_ fun u ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
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)
⊢ 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‖⁻¹))
have refine_2 : Function.HasFiniteSupport (M := ℝ) fun (u : ℂ) ↦
  (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹)
Tactic: refine finsum_le_finsum' ?_ ?_ fun u ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
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‖⁻¹)
⊢ 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‖⁻¹))
have 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‖⁻¹)
Tactic: refine finsum_le_finsum' ?_ ?_ fun u ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
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 : ℂ
⊢ (↑((divisor f (closedBall c |r|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R / r) ≤
    (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹)
have 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‖⁻¹)
Tactic: by_cases h1 : u ∈ closedBall c |R|
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
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‖⁻¹)
⊢ (↑((divisor f (closedBall c |r|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R / r) ≤
    (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹)
have 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‖⁻¹)
Tactic: by_cases h1 : u ∈ closedBall c |R|
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
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|
⊢ (↑((divisor f (closedBall c |r|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R / r) ≤
    (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹)
have 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‖⁻¹)
Tactic: by_cases h2 : u ∈ closedBall c |r|
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
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‖⁻¹)
⊢ (↑((divisor f (closedBall c |r|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R / r) ≤
    (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹)
have 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‖⁻¹)
Tactic: by_cases h2 : u ∈ closedBall c |r|
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
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|
⊢ (↑((divisor f (closedBall c |r|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R / r) ≤
    (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹)
have 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‖⁻¹)
Tactic: simp only [(h₁f.mono (closedBall_subset_closedBall r_lt_R.le)), h2,
            AnalyticOnNhd.divisor_apply, h₁f, h1]
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
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|
⊢ (↑(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‖⁻¹)
have 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‖⁻¹)
Tactic: by_cases! h3 : u = c
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
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‖⁻¹)
⊢ (↑(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‖⁻¹)
have 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‖⁻¹)
Tactic: by_cases! h3 : u = c
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
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 (analyticOrderAt f u))) : ℝ) * Real.log (R / r) ≤
    (↑(WithTop.untop₀ (ENat.map Nat.cast (analyticOrderAt f u))) : ℝ) * Real.log (R * ‖c - u‖⁻¹)
have pos : (↑(WithTop.untop₀ (ENat.map Nat.cast 0)) : ℝ) * Real.log (R / r) ≤
  (↑(WithTop.untop₀ (ENat.map Nat.cast 0)) : ℝ) * Real.log (R * ‖c - c‖⁻¹)
Tactic: rw [h3, (h₁f c (by simp)).analyticOrderAt_eq_zero.mpr h₂f]
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
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 (analyticOrderAt f u))) : ℝ) * Real.log (R / r) ≤
    (↑(WithTop.untop₀ (ENat.map Nat.cast (analyticOrderAt f u))) : ℝ) * Real.log (R * ‖c - u‖⁻¹)
have 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‖⁻¹|
Tactic: simp +singlePass only [← log_abs]