awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : LE.le (α := ℝ) 0 (↑(WithTop.untop₀ (ENat.map Nat.cast (analyticOrderAt f u))) : ℝ)
Tactic: gcongr 2
-- 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
neg : LE.le (α := ℝ) 0 (↑(WithTop.untop₀ (ENat.map Nat.cast (analyticOrderAt f 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₁ : |R / r| ≤ |R * ‖c - u‖⁻¹|
Tactic: gcongr 2
-- 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‖
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
⊢ |R / r| ≤ |R * ‖c - u‖⁻¹|
have this : ‖c - u‖ ≠ 0
Tactic: have : ‖c - u‖ ≠ 0 := by simpa [sub_eq_zero] using h3.symm
-- 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 neg : 0 ≤ (↑((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]
-- 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|
⊢ 0 ≤ (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹)
have neg : 0 ≤ Real.log (R * ‖c - u‖⁻¹)
Tactic: refine mul_nonneg (mod_cast h₁f.divisor_nonneg ..) ?_
-- 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|
⊢ 0 ≤ Real.log (R * ‖c - u‖⁻¹)
have neg : 1 ≤ |R * ‖c - u‖⁻¹|
Tactic: apply log_abs _ ▸ log_nonneg
-- 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‖
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|
⊢ 1 ≤ |R * ‖c - u‖⁻¹|
have h1₁ : ‖c - u‖ ≤ |R|
Tactic: simp only [mem_closedBall, dist_eq_norm', not_le] at h1 h2
Cleared hypotheses: h1, h2
-- 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‖
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|
⊢ 1 ≤ |R * ‖c - u‖⁻¹|
have h2₁ : |r| < ‖c - u‖
Tactic: simp only [mem_closedBall, dist_eq_norm', not_le] at h1 h2
Cleared hypotheses: h1, h2
-- 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‖
integral_bound : circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R ≤ Real.log M
u : ℂ
h1 : ‖c - u‖ ≤ |R|
h2 : |r| < ‖c - u‖
⊢ 1 ≤ |R * ‖c - u‖⁻¹|
have this : ‖c - u‖ ≠ 0
Tactic: have : ‖c - u‖ ≠ 0 := (r_pos.trans h2).ne'
-- 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|
⊢ u ∉ closedBall c |r|
have 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
Tactic: simp_all
Cleared hypotheses: r_pos, r_lt_R, hM, h₁f, h₂f, f_bound, hrR, jensen, integral_bound, h1
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
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
⊢ |r| < dist u c
have linarith : dist u c ≤ |r| → |r| - |R| + (|R| - dist u c) + (dist u c - |r|) = 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|
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 this : u ∉ closedBall c |r|
Tactic: have : u ∉ closedBall c |r| := by
          simp_all
          linarith
-- 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 * ‖c - u‖⁻¹) ≤
    Real.log M - Real.log ‖f c‖
have linarith : Real.log M - Real.log ‖f c‖ <
    ∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹) →
  -(HMul.hMul (α := ℝ) 1 (circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R) -
            (HMul.hMul (α := ℝ) 1
                (∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹)) +
              1 * Real.log ‖f c‖)) +
        (circleAverage (fun (x : ℂ) ↦ Real.log ‖f x‖) c R - Real.log M) +
      (1 * Real.log M - 1 * Real.log ‖f c‖ -
        HMul.hMul (α := ℝ) 1
          (∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹))) =
    0
Tactic: linarith
-- 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
⊢ M ≠ 0
have linarith : M = 0 → -1 + (1 - M) + (M - 0) = 0
Tactic: linarith
-- 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
⊢ Real.log M - Real.log ‖f c‖ = Real.log (M / ‖f c‖)
have rw : Real.log (M / ‖f c‖) = Real.log (M / ‖f c‖)
Tactic: rw [← log_div (by linarith) (norm_ne_zero_iff.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 : ℂ), (↑((divisor f (closedBall c |r|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R / r) ≤ Real.log (M / ‖f c‖)
have Bound : 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: calc
  -- Bound by the sum from Jensen's formula
  _ ≤ ∑ᶠ u, ((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) := by
    refine finsum_le_finsum' ?_ ?_ fun u ↦ ?_
    · exact (divisor f (closedBall c |r|)).finiteSupport (isCompact_closedBall ..) |>.subset
        fun _ _ ↦ (by simp_all)
    · exact (divisor f (closedBall c |R|)).finiteSupport (isCompact_closedBall ..) |>.subset
        fun _ _ ↦ (by simp_all)
    · -- Core bound: estimate the summand by splitting on which ball u is in
      by_cases h1 : u ∈ closedBall c |R|
      · by_cases h2 : u ∈ closedBall c |r|
        · --In the smaller ball: the divisors agree and we bound the log factor
          simp only [(h₁f.mono (closedBall_subset_closedBall r_lt_R.le)), h2,
            AnalyticOnNhd.divisor_apply, h₁f, h1]
          by_cases! h3 : u = c --Need to use the divisor is 0 at c rather than comparing the logs
          · rw [h3, (h₁f c (by simp)).analyticOrderAt_eq_zero.mpr h₂f]
            simp
          simp +singlePass only [← log_abs]
          gcongr 2
          · simp
          · have : ‖c - u‖ ≠ 0 := by simpa [sub_eq_zero] using h3.symm
            simpa [field, abs_div, r_pos.trans r_lt_R, dist_eq_norm'] using h2
        · --In the larger ball but not the smaller so LHS is 0 and RHS nonnegative
          simp only [h2, not_false_eq_true, Function.locallyFinsuppWithin.apply_eq_zero_of_notMem,
            Int.cast_zero, zero_mul]
          refine mul_nonneg (mod_cast h₁f.divisor_nonneg ..) ?_
          apply log_abs _ ▸ log_nonneg
          simp only [mem_closedBall, dist_eq_norm', not_le] at h1 h2
          have : ‖c - u‖ ≠ 0 := (r_pos.trans h2).ne'
          simpa [field]
      · --Outside the larger ball so both sides are 0
        have : u ∉ closedBall c |r| := by
          simp_all
          linarith
        simp [h1, this]
  _ ≤ Real.log M - Real.log ‖f c‖ := by linarith --Uses jensen and integral_bound
  _ = _ := by rw [← log_div (by linarith) (norm_ne_zero_iff.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
Bound :
  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‖⁻¹))
⊢ ∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |r|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R / r) ≤ Real.log (M / ‖f c‖)
have Bound₁ : ∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹) ≤
  Real.log M - Real.log ‖f c‖
Tactic: calc
  -- Bound by the sum from Jensen's formula
  _ ≤ ∑ᶠ u, ((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) := by
    refine finsum_le_finsum' ?_ ?_ fun u ↦ ?_
    · exact (divisor f (closedBall c |r|)).finiteSupport (isCompact_closedBall ..) |>.subset
        fun _ _ ↦ (by simp_all)
    · exact (divisor f (closedBall c |R|)).finiteSupport (isCompact_closedBall ..) |>.subset
        fun _ _ ↦ (by simp_all)
    · -- Core bound: estimate the summand by splitting on which ball u is in
      by_cases h1 : u ∈ closedBall c |R|
      · by_cases h2 : u ∈ closedBall c |r|
        · --In the smaller ball: the divisors agree and we bound the log factor
          simp only [(h₁f.mono (closedBall_subset_closedBall r_lt_R.le)), h2,
            AnalyticOnNhd.divisor_apply, h₁f, h1]
          by_cases! h3 : u = c --Need to use the divisor is 0 at c rather than comparing the logs
          · rw [h3, (h₁f c (by simp)).analyticOrderAt_eq_zero.mpr h₂f]
            simp
          simp +singlePass only [← log_abs]
          gcongr 2
          · simp
          · have : ‖c - u‖ ≠ 0 := by simpa [sub_eq_zero] using h3.symm
            simpa [field, abs_div, r_pos.trans r_lt_R, dist_eq_norm'] using h2
        · --In the larger ball but not the smaller so LHS is 0 and RHS nonnegative
          simp only [h2, not_false_eq_true, Function.locallyFinsuppWithin.apply_eq_zero_of_notMem,
            Int.cast_zero, zero_mul]
          refine mul_nonneg (mod_cast h₁f.divisor_nonneg ..) ?_
          apply log_abs _ ▸ log_nonneg
          simp only [mem_closedBall, dist_eq_norm', not_le] at h1 h2
          have : ‖c - u‖ ≠ 0 := (r_pos.trans h2).ne'
          simpa [field]
      · --Outside the larger ball so both sides are 0
        have : u ∉ closedBall c |r| := by
          simp_all
          linarith
        simp [h1, this]
  _ ≤ Real.log M - Real.log ‖f c‖ := by linarith --Uses jensen and integral_bound
  _ = _ := by rw [← log_div (by linarith) (norm_ne_zero_iff.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
Bound :
  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‖⁻¹))
Bound₁ :
  ∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |R|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R * ‖c - u‖⁻¹) ≤
    Real.log M - Real.log ‖f c‖
⊢ ∑ᶠ (u : ℂ), (↑((divisor f (closedBall c |r|) : (a : ℂ) → ℤ) u) : ℝ) * Real.log (R / r) ≤ Real.log (M / ‖f c‖)
have Bound₂ : Real.log M - Real.log ‖f c‖ = Real.log (M / ‖f c‖)
Tactic: calc
  -- Bound by the sum from Jensen's formula
  _ ≤ ∑ᶠ u, ((divisor f (closedBall c |R|)) u) * Real.log (R * ‖c - u‖⁻¹) := by
    refine finsum_le_finsum' ?_ ?_ fun u ↦ ?_
    · exact (divisor f (closedBall c |r|)).finiteSupport (isCompact_closedBall ..) |>.subset
        fun _ _ ↦ (by simp_all)
    · exact (divisor f (closedBall c |R|)).finiteSupport (isCompact_closedBall ..) |>.subset
        fun _ _ ↦ (by simp_all)
    · -- Core bound: estimate the summand by splitting on which ball u is in
      by_cases h1 : u ∈ closedBall c |R|
      · by_cases h2 : u ∈ closedBall c |r|
        · --In the smaller ball: the divisors agree and we bound the log factor
          simp only [(h₁f.mono (closedBall_subset_closedBall r_lt_R.le)), h2,
            AnalyticOnNhd.divisor_apply, h₁f, h1]
          by_cases! h3 : u = c --Need to use the divisor is 0 at c rather than comparing the logs
          · rw [h3, (h₁f c (by simp)).analyticOrderAt_eq_zero.mpr h₂f]
            simp
          simp +singlePass only [← log_abs]
          gcongr 2
          · simp
          · have : ‖c - u‖ ≠ 0 := by simpa [sub_eq_zero] using h3.symm
            simpa [field, abs_div, r_pos.trans r_lt_R, dist_eq_norm'] using h2
        · --In the larger ball but not the smaller so LHS is 0 and RHS nonnegative
          simp only [h2, not_false_eq_true, Function.locallyFinsuppWithin.apply_eq_zero_of_notMem,
            Int.cast_zero, zero_mul]
          refine mul_nonneg (mod_cast h₁f.divisor_nonneg ..) ?_
          apply log_abs _ ▸ log_nonneg
          simp only [mem_closedBall, dist_eq_norm', not_le] at h1 h2
          have : ‖c - u‖ ≠ 0 := (r_pos.trans h2).ne'
          simpa [field]
      · --Outside the larger ball so both sides are 0
        have : u ∉ closedBall c |r| := by
          simp_all
          linarith
        simp [h1, this]
  _ ≤ Real.log M - Real.log ‖f c‖ := by linarith --Uses jensen and integral_bound
  _ = _ := by rw [← log_div (by linarith) (norm_ne_zero_iff.mpr h₂f)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Liouville (hypothesis)
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
inst_2 : CompleteSpace F
c : ℂ
R C : ℝ
f : ℂ → F
n : ℕ
hR : 0 < R
hf : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
⊢ ‖iteratedDeriv n f c‖ ≤ (↑n.factorial : ℝ) * C / R ^ n
have hp : ∀ (z : ℂ) (hz : z ∈ sphere c R), ‖(z - c)⁻¹ ^ (n + 1) • f z‖ ≤ C / (R ^ n * R)
Tactic: have hp (z) (hz : z ∈ sphere c R) : ‖(z - c)⁻¹ ^ (n + 1) • f z‖ ≤ C / (R ^ n * R) := by
    simpa [norm_smul, norm_pow, norm_inv, ← div_eq_inv_mul, mem_sphere_iff_norm.1 hz] using
      (div_le_div_iff_of_pos_right (mul_pos (pow_pos hR n) hR)).2 (hC z hz)
-- Lean 4 proof step from Mathlib.Analysis.Complex.Liouville (hypothesis)
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
inst_2 : CompleteSpace F
c : ℂ
R C : ℝ
f : ℂ → F
n : ℕ
hR : 0 < R
hf : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
hp : ∀ (z : ℂ) (hz : z ∈ sphere c R), ‖(z - c)⁻¹ ^ (n + 1) • f z‖ ≤ C / (R ^ n * R)
⊢ iteratedDeriv n f c =
    n.factorial • HSMul.hSMul (β := F) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z)
have this : 2 * (↑π : ℂ) * I / (↑n.factorial : ℂ) ≠ 0
Tactic: have : (2 * π * I / n.factorial) ≠ 0 := by simp [Nat.factorial_ne_zero]
-- Lean 4 proof step from Mathlib.Analysis.Complex.Liouville (goal)
Goal:
F : Type v
inst : NormedAddCommGroup F
inst_1 : NormedSpace ℂ F
inst_2 : CompleteSpace F
c : ℂ
R C : ℝ
f : ℂ → F
n : ℕ
hR : 0 < R
hf : DiffContOnCl ℂ f (ball c R)
hC : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
hp : ∀ (z : ℂ) (hz : z ∈ sphere c R), ‖(z - c)⁻¹ ^ (n + 1) • f z‖ ≤ C / (R ^ n * R)
this : 2 * (↑π : ℂ) * I / (↑n.factorial : ℂ) ≠ 0
⊢ iteratedDeriv n f c =
    n.factorial • HSMul.hSMul (β := F) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z)
have rw : n.factorial • (2 * (↑π : ℂ) * I)⁻¹ • (2 * (↑π : ℂ) * I / (↑n.factorial : ℂ)) • iteratedDeriv n f c =
  n.factorial • HSMul.hSMul (β := F) (2 * (↑π : ℂ) * I)⁻¹ (∮ (z : ℂ) in C(c, R), (z - c)⁻¹ ^ (n + 1) • f z)
Tactic: rw [← inv_smul_smul₀ this (iteratedDeriv n f c), inv_div, div_eq_inv_mul, mul_comm,
      ← nsmul_eq_mul, smul_assoc]