awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (hypothesis)
Goal:
w ρ : ℂ
R : ℝ
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
hR : 0 < R
r : ℕ → ℝ := fun (n : ℕ) ↦ R - (R - ‖w‖) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 2
hr_lt : ∀ (n : ℕ), r n < R
hr_pos : ∀ (n : ℕ), 0 < r n
hr_tendsto : Tendsto r atTop (𝓝 R)
DCT :
  Tendsto (fun (n : ℕ) ↦ circleAverage (herglotzLogIntegrand w ρ) 0 (r n)) atTop
    (𝓝 (circleAverage (herglotzLogIntegrand w ρ) 0 R))
⊢ circleAverage (HSMul.hSMul (β := ℂ → ℝ) (Complex.re ∘ herglotzRieszKernel 0 w) fun (x : ℂ) ↦ log ‖x - ρ‖) 0 R =
    log ‖w - ρ‖
have this : ∀ {n : ℕ}, circleAverage (herglotzLogIntegrand w ρ) 0 (r n) = log ‖w - ρ‖
Tactic: have {n : ℕ} : circleAverage (herglotzLogIntegrand w ρ) 0 (r n) = log ‖w - ρ‖ := by
    unfold herglotzLogIntegrand
    apply InnerProductSpace.HarmonicContOnCl.circleAverage_re_herglotzRieszKernel_smul
    · refine ⟨fun z hz ↦ ?_, fun x hx ↦ ?_⟩
      · exact AnalyticAt.harmonicAt_log_norm (by fun_prop) (by grind [mem_ball, dist_zero_right])
      · suffices ‖x - ρ‖ ≠ 0 by fun_prop
        suffices x ≠ ρ by simpa [sub_eq_zero]
        have key := by simpa using closure_ball_subset_closedBall hx
        grind
    · simp only [mem_ball, dist_zero_right, lt_sub_iff_add_lt, r]
      field_simp
      calc ‖w‖ * (n + 2) + (R - ‖w‖) = ‖w‖ * (n + 1) + R := by ring
        _ < R * (n + 1) + R := by gcongr
        _ = R * (n + 2) := by ring
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
Goal:
w ρ c : ℂ
R : ℝ
hρ : ρ ∈ sphere c R
hw : w ∈ ball c R
⊢ circleAverage (Complex.re ∘ herglotzRieszKernel c w * fun (x : ℂ) ↦ log ‖x - ρ‖) c R = log ‖w - ρ‖
have simp : circleAverage (fun (z : ℂ) ↦ (herglotzRieszKernel c w (z + 0 + c)).re * log ‖z + 0 + c - ρ‖) 0 R = log ‖w - ρ‖
Tactic: simp only [← circleAverage_map_add_const, Pi.mul_apply, Function.comp_apply, add_zero]
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
Goal:
w ρ c : ℂ
R : ℝ
hρ : ρ ∈ sphere c R
hw : w ∈ ball c R
| circleAverage (fun (z : ℂ) ↦ (herglotzRieszKernel c w (z + 0 + c)).re * log ‖z + 0 + c - ρ‖) 0 R = log ‖w - ρ‖
have left : circleAverage (fun (z : ℂ) ↦ (herglotzRieszKernel c w (z + 0 + c)).re * log ‖z + 0 + c - ρ‖) 0 R
Tactic: left
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
Goal:
w ρ c : ℂ
R : ℝ
hρ : ρ ∈ sphere c R
hw : w ∈ ball c R
| circleAverage (fun (z : ℂ) ↦ (herglotzRieszKernel c w (z + 0 + c)).re * log ‖z + 0 + c - ρ‖) 0 R
have arg : fun (z : ℂ) ↦ (herglotzRieszKernel c w (z + 0 + c)).re * log ‖z + 0 + c - ρ‖
Tactic: arg 1
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
Goal:
w ρ c : ℂ
R : ℝ
hρ : ρ ∈ sphere c R
hw : w ∈ ball c R
z : ℂ
| (herglotzRieszKernel c w (z + 0 + c)).re * log ‖z + 0 + c - ρ‖
have h : (herglotzRieszKernel c w (z + 0 + c)).re * log ‖z - (ρ - c)‖
Tactic: rw [(by ring : (z + 0 + c) - ρ = z - (ρ - c))]
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
Goal:
w ρ c : ℂ
R : ℝ
hρ : ρ ∈ sphere c R
hw : w ∈ ball c R
z : ℂ
| (herglotzRieszKernel c w (z + 0 + c)).re * log ‖z - (ρ - c)‖
have h : (herglotzRieszKernel c w (z + 0 + c)).re
Tactic: arg 1
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
Goal:
w ρ c : ℂ
R : ℝ
hρ : ρ ∈ sphere c R
hw : w ∈ ball c R
z : ℂ
| (herglotzRieszKernel c w (z + 0 + c)).re
have h : herglotzRieszKernel c w (z + 0 + c)
Tactic: arg 1
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
Goal:
w ρ c : ℂ
R : ℝ
hρ : ρ ∈ sphere c R
hw : w ∈ ball c R
z : ℂ
| herglotzRieszKernel c w (z + 0 + c)
have h : herglotzRieszKernel 0 (w - c) z
Tactic: rw [add_zero, herglotzRieszKernel_add_const c w z]
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
Goal:
w ρ c : ℂ
R : ℝ
hρ : ρ ∈ sphere c R
hw : w ∈ ball c R
| circleAverage (fun (z : ℂ) ↦ (herglotzRieszKernel c w (z + 0 + c)).re * log ‖z + 0 + c - ρ‖) 0 R = log ‖w - ρ‖
have h : ∀ (z : ℂ), herglotzRieszKernel 0 (w - c) z
Tactic: left; arg 1
    intro z
    rw [(by ring : (z + 0 + c) - ρ = z - (ρ - c))]
    arg 1; arg 1
    rw [add_zero, herglotzRieszKernel_add_const c w z]
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
Goal:
w ρ c : ℂ
R : ℝ
hρ : ρ ∈ sphere c R
hw : w ∈ ball c R
⊢ circleAverage (fun (z : ℂ) ↦ (herglotzRieszKernel c w (z + 0 + c)).re * log ‖z + 0 + c - ρ‖) 0 R = log ‖w - ρ‖
have conv : circleAverage (fun (z : ℂ) ↦ (herglotzRieszKernel 0 (w - c) z).re * log ‖z - (ρ - c)‖) 0 R = log ‖w - ρ‖
Tactic: conv =>
    left; arg 1
    intro z
    rw [(by ring : (z + 0 + c) - ρ = z - (ρ - c))]
    arg 1; arg 1
    rw [add_zero, herglotzRieszKernel_add_const c w z]
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (hypothesis)
Goal:
w ρ c : ℂ
R : ℝ
hρ : ρ ∈ sphere c R
hw : w ∈ ball c R
⊢ circleAverage (fun (z : ℂ) ↦ (herglotzRieszKernel 0 (w - c) z).re * log ‖z - (ρ - c)‖) 0 R = log ‖w - ρ‖
have this : (fun (z : ℂ) ↦ (herglotzRieszKernel 0 (w - c) z).re * log ‖z - (ρ - c)‖) =
  HSMul.hSMul (β := ℂ → ℝ) (Complex.re ∘ herglotzRieszKernel 0 (w - c)) fun (x : ℂ) ↦ log ‖x - (ρ - c)‖
Tactic: have : (fun z ↦ (herglotzRieszKernel 0 (w - c) z).re * log ‖z - (ρ - c)‖) =
    (Complex.re ∘ herglotzRieszKernel 0 (w - c)) • (log ‖· - (ρ - c)‖) := by rfl
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
Goal:
w ρ c : ℂ
R : ℝ
hρ : ρ ∈ sphere c R
hw : w ∈ ball c R
this :
  (fun (z : ℂ) ↦ (herglotzRieszKernel 0 (w - c) z).re * log ‖z - (ρ - c)‖) =
    HSMul.hSMul (β := ℂ → ℝ) (Complex.re ∘ herglotzRieszKernel 0 (w - c)) fun (x : ℂ) ↦ log ‖x - (ρ - c)‖
⊢ circleAverage (fun (z : ℂ) ↦ (herglotzRieszKernel 0 (w - c) z).re * log ‖z - (ρ - c)‖) 0 R = log ‖w - ρ‖
have rw : log ‖w - c - (ρ - c)‖ = log ‖w - ρ‖
Tactic: rw [this, circleAverage_re_herglotzRieszKernel_mul_log₀ (by simp_all)
    (by simp_all [mem_ball_iff_norm.1 hw])]
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (hypothesis)
Goal:
R : ℝ
c : ℂ
D : Function.locallyFinsuppWithin (closedBall c |R|) ℤ
⊢ Eq (α := ℝ) (circleAverage (∑ᶠ (u : ℂ), fun (x : ℂ) ↦ (↑((D : (a : ℂ) → ℤ) u) : ℝ) * log ‖x - u‖) c R)
    (∑ᶠ (u : ℂ), (↑((D : (a : ℂ) → ℤ) u) : ℝ) * log R)
have h : D.support (U := closedBall c |R|).Finite
Tactic: have h := D.finiteSupport (isCompact_closedBall c |R|)
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
Goal:
R : ℝ
c : ℂ
D : Function.locallyFinsuppWithin (closedBall c |R|) ℤ
h : D.support (U := closedBall c |R|).Finite
⊢ Eq (α := ℝ) (circleAverage (∑ᶠ (u : ℂ), fun (x : ℂ) ↦ (↑((D : (a : ℂ) → ℤ) u) : ℝ) * log ‖x - u‖) c R)
    (circleAverage
      (∑ u ∈ h.toFinset (s := D.support (U := closedBall c |R|)), fun (x : ℂ) ↦
        (↑((D : (a : ℂ) → ℤ) u) : ℝ) * log ‖x - u‖)
      c R)
have h₁ : (Function.support (M := ℂ → ℝ) fun (u x : ℂ) ↦ (↑((D : (a : ℂ) → ℤ) u) : ℝ) * log ‖x - u‖) ⊆
  (↑(h.toFinset (s := D.support (U := closedBall c |R|))) : Set ℂ)
Tactic: rw [finsum_eq_sum_of_support_subset]
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
Goal:
R : ℝ
c : ℂ
D : Function.locallyFinsuppWithin (closedBall c |R|) ℤ
h : D.support (U := closedBall c |R|).Finite
u : ℂ
⊢ Membership.mem (γ := Set ℂ) (Function.support (M := ℂ → ℝ) fun (u x : ℂ) ↦ (↑((D : (a : ℂ) → ℤ) u) : ℝ) * log ‖x - u‖)
      u →
    u ∈ (↑(h.toFinset (s := D.support (U := closedBall c |R|))) : Set ℂ)
have h₁ : u ∉ (↑(h.toFinset (s := D.support (U := closedBall c |R|))) : Set ℂ) →
  u ∉ Function.support (M := ℂ → ℝ) fun (u x : ℂ) ↦ (↑((D : (a : ℂ) → ℤ) u) : ℝ) * log ‖x - u‖
Tactic: contrapose
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
Goal:
R : ℝ
c : ℂ
D : Function.locallyFinsuppWithin (closedBall c |R|) ℤ
h : D.support (U := closedBall c |R|).Finite
⊢ Eq (α := ℝ)
    (circleAverage
      (∑ u ∈ h.toFinset (s := D.support (U := closedBall c |R|)), fun (x : ℂ) ↦
        (↑((D : (a : ℂ) → ℤ) u) : ℝ) * log ‖x - u‖)
      c R)
    (∑ i ∈ h.toFinset (s := D.support (U := closedBall c |R|)),
      circleAverage (fun (x : ℂ) ↦ (↑((D : (a : ℂ) → ℤ) i) : ℝ) * log ‖x - i‖) c R)
have rw : ∀ i ∈ h.toFinset (s := D.support (U := closedBall c |R|)),
  CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ (↑((D : (a : ℂ) → ℤ) i) : ℝ) * log ‖x - i‖) c R
Tactic: rw [circleAverage_sum]
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
Goal:
R : ℝ
c : ℂ
D : Function.locallyFinsuppWithin (closedBall c |R|) ℤ
h : D.support (U := closedBall c |R|).Finite
u : ℂ
hu : u ∈ h.toFinset (s := D.support (U := closedBall c |R|))
⊢ CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ (↑((D : (a : ℂ) → ℤ) u) : ℝ) * log ‖x - u‖) c R
have hf : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log ‖circleMap c R x - u‖) volume 0 (2 * π)
Tactic: apply IntervalIntegrable.const_mul
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
Goal:
R : ℝ
c : ℂ
D : Function.locallyFinsuppWithin (closedBall c |R|) ℤ
h : D.support (U := closedBall c |R|).Finite
⊢ Eq (α := ℝ)
    (∑ i ∈ h.toFinset (s := D.support (U := closedBall c |R|)),
      circleAverage (fun (x : ℂ) ↦ (↑((D : (a : ℂ) → ℤ) i) : ℝ) * log ‖x - i‖) c R)
    (∑ u ∈ h.toFinset (s := D.support (U := closedBall c |R|)), (↑((D : (a : ℂ) → ℤ) u) : ℝ) * log R)
have apply : ∀ x ∈ h.toFinset (s := D.support (U := closedBall c |R|)),
  circleAverage (fun (x_1 : ℂ) ↦ (↑((D : (a : ℂ) → ℤ) x) : ℝ) * log ‖x_1 - x‖) c R =
    (↑((D : (a : ℂ) → ℤ) x) : ℝ) * log R
Tactic: apply Finset.sum_congr rfl
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
Goal:
R : ℝ
c : ℂ
D : Function.locallyFinsuppWithin (closedBall c |R|) ℤ
h : D.support (U := closedBall c |R|).Finite
u : ℂ
hu : u ∈ h.toFinset (s := D.support (U := closedBall c |R|))
⊢ circleAverage (fun (x : ℂ) ↦ (↑((D : (a : ℂ) → ℤ) u) : ℝ) * log ‖x - u‖) c R = (↑((D : (a : ℂ) → ℤ) u) : ℝ) * log R
have simp_rw : HSMul.hSMul (α := ℝ) (β := ℝ) (↑((D : (a : ℂ) → ℤ) u) : ℝ) (circleAverage (fun (z : ℂ) ↦ log ‖z - u‖) c R) =
  HSMul.hSMul (α := ℝ) (↑((D : (a : ℂ) → ℤ) u) : ℝ) (log R)
Tactic: simp_rw [← smul_eq_mul, circleAverage_fun_smul]
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
Goal:
R : ℝ
c : ℂ
D : Function.locallyFinsuppWithin (closedBall c |R|) ℤ
h : D.support (U := closedBall c |R|).Finite
u : ℂ
hu : u ∈ h.toFinset (s := D.support (U := closedBall c |R|))
⊢ HSMul.hSMul (α := ℝ) (β := ℝ) (↑((D : (a : ℂ) → ℤ) u) : ℝ) (circleAverage (fun (z : ℂ) ↦ log ‖z - u‖) c R) =
    HSMul.hSMul (α := ℝ) (↑((D : (a : ℂ) → ℤ) u) : ℝ) (log R)
have e_a : circleAverage (fun (z : ℂ) ↦ log ‖z - u‖) c R = log R
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
Goal:
R : ℝ
c : ℂ
D : Function.locallyFinsuppWithin (closedBall c |R|) ℤ
h : D.support (U := closedBall c |R|).Finite
u : ℂ
hu : u ∈ h.toFinset (s := D.support (U := closedBall c |R|))
⊢ circleAverage (fun (z : ℂ) ↦ log ‖z - u‖) c R = log R
have e_a : u ∈ closedBall c |R|
Tactic: rw [circleAverage_log_norm_sub_const_of_mem_closedBall]
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
Goal:
R : ℝ
c : ℂ
D : Function.locallyFinsuppWithin (closedBall c |R|) ℤ
h : D.support (U := closedBall c |R|).Finite
u : ℂ
hu : u ∈ h.toFinset (s := D.support (U := closedBall c |R|))
⊢ u ∈ closedBall c |R|
have e_a : u ∈ D.support (U := closedBall c |R|)
Tactic: apply D.supportWithinDomain
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
Goal:
R : ℝ
c : ℂ
D : Function.locallyFinsuppWithin (closedBall c |R|) ℤ
h : D.support (U := closedBall c |R|).Finite
⊢ Eq (α := ℝ) (∑ u ∈ h.toFinset (s := D.support (U := closedBall c |R|)), (↑((D : (a : ℂ) → ℤ) u) : ℝ) * log R)
    (∑ᶠ (u : ℂ), (↑((D : (a : ℂ) → ℤ) u) : ℝ) * log R)
have h₁ : (Function.support (M := ℝ) fun (u : ℂ) ↦ (↑((D : (a : ℂ) → ℤ) u) : ℝ) * log R) ⊆
  (↑(h.toFinset (s := D.support (U := closedBall c |R|))) : Set ℂ)
Tactic: rw [finsum_eq_sum_of_support_subset]
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
Goal:
R : ℝ
c : ℂ
D : Function.locallyFinsuppWithin (closedBall c |R|) ℤ
h : D.support (U := closedBall c |R|).Finite
⊢ Eq (α := ℝ) (circleAverage (∑ᶠ (u : ℂ), fun (x : ℂ) ↦ (↑((D : (a : ℂ) → ℤ) u) : ℝ) * log ‖x - u‖) c R)
    (∑ᶠ (u : ℂ), (↑((D : (a : ℂ) → ℤ) u) : ℝ) * log R)
have calc : Eq (α := ℝ) (circleAverage (∑ᶠ (u : ℂ), fun (x : ℂ) ↦ (↑((D : (a : ℂ) → ℤ) u) : ℝ) * log ‖x - u‖) c R)
  (circleAverage
    (∑ u ∈ h.toFinset (s := D.support (U := closedBall c |R|)), fun (x : ℂ) ↦
      (↑((D : (a : ℂ) → ℤ) u) : ℝ) * log ‖x - u‖)
    c R)
Tactic: calc circleAverage (∑ᶠ u, (D u * log ‖· - u‖)) c R
  _ = circleAverage (∑ u ∈ h.toFinset, (D u * log ‖· - u‖)) c R := by
    rw [finsum_eq_sum_of_support_subset]
    intro u
    contrapose
    aesop
  _ = ∑ i ∈ h.toFinset, circleAverage (fun x ↦ D i * log ‖x - i‖) c R := by
    rw [circleAverage_sum]
    intro u hu
    apply IntervalIntegrable.const_mul
    apply (analyticOnNhd_id.sub analyticOnNhd_const).meromorphicOn.circleIntegrable_log_norm
  _ = ∑ u ∈ h.toFinset, D u * log R := by
    apply Finset.sum_congr rfl
    intro u hu
    simp_rw [← smul_eq_mul, circleAverage_fun_smul]
    congr
    rw [circleAverage_log_norm_sub_const_of_mem_closedBall]
    apply D.supportWithinDomain
    simp_all
  _ = ∑ᶠ u, D u * log R := by
    rw [finsum_eq_sum_of_support_subset]
    intro u
    aesop
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
Goal:
R : ℝ
c : ℂ
D : Function.locallyFinsuppWithin (closedBall c |R|) ℤ
h : D.support (U := closedBall c |R|).Finite
calc :
  Eq (α := ℝ) (circleAverage (∑ᶠ (u : ℂ), fun (x : ℂ) ↦ (↑((D : (a : ℂ) → ℤ) u) : ℝ) * log ‖x - u‖) c R)
    (circleAverage
      (∑ u ∈ h.toFinset (s := D.support (U := closedBall c |R|)), fun (x : ℂ) ↦
        (↑((D : (a : ℂ) → ℤ) u) : ℝ) * log ‖x - u‖)
      c R)
⊢ Eq (α := ℝ) (circleAverage (∑ᶠ (u : ℂ), fun (x : ℂ) ↦ (↑((D : (a : ℂ) → ℤ) u) : ℝ) * log ‖x - u‖) c R)
    (∑ᶠ (u : ℂ), (↑((D : (a : ℂ) → ℤ) u) : ℝ) * log R)
have calc₁ : Eq (α := ℝ)
  (circleAverage
    (∑ u ∈ h.toFinset (s := D.support (U := closedBall c |R|)), fun (x : ℂ) ↦
      (↑((D : (a : ℂ) → ℤ) u) : ℝ) * log ‖x - u‖)
    c R)
  (∑ i ∈ h.toFinset (s := D.support (U := closedBall c |R|)),
    circleAverage (fun (x : ℂ) ↦ (↑((D : (a : ℂ) → ℤ) i) : ℝ) * log ‖x - i‖) c R)
Tactic: calc circleAverage (∑ᶠ u, (D u * log ‖· - u‖)) c R
  _ = circleAverage (∑ u ∈ h.toFinset, (D u * log ‖· - u‖)) c R := by
    rw [finsum_eq_sum_of_support_subset]
    intro u
    contrapose
    aesop
  _ = ∑ i ∈ h.toFinset, circleAverage (fun x ↦ D i * log ‖x - i‖) c R := by
    rw [circleAverage_sum]
    intro u hu
    apply IntervalIntegrable.const_mul
    apply (analyticOnNhd_id.sub analyticOnNhd_const).meromorphicOn.circleIntegrable_log_norm
  _ = ∑ u ∈ h.toFinset, D u * log R := by
    apply Finset.sum_congr rfl
    intro u hu
    simp_rw [← smul_eq_mul, circleAverage_fun_smul]
    congr
    rw [circleAverage_log_norm_sub_const_of_mem_closedBall]
    apply D.supportWithinDomain
    simp_all
  _ = ∑ᶠ u, D u * log R := by
    rw [finsum_eq_sum_of_support_subset]
    intro u
    aesop
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
Goal:
R : ℝ
c : ℂ
D : Function.locallyFinsuppWithin (closedBall c |R|) ℤ
h : D.support (U := closedBall c |R|).Finite
calc :
  Eq (α := ℝ) (circleAverage (∑ᶠ (u : ℂ), fun (x : ℂ) ↦ (↑((D : (a : ℂ) → ℤ) u) : ℝ) * log ‖x - u‖) c R)
    (circleAverage
      (∑ u ∈ h.toFinset (s := D.support (U := closedBall c |R|)), fun (x : ℂ) ↦
        (↑((D : (a : ℂ) → ℤ) u) : ℝ) * log ‖x - u‖)
      c R)
calc₁ :
  Eq (α := ℝ)
    (circleAverage
      (∑ u ∈ h.toFinset (s := D.support (U := closedBall c |R|)), fun (x : ℂ) ↦
        (↑((D : (a : ℂ) → ℤ) u) : ℝ) * log ‖x - u‖)
      c R)
    (∑ i ∈ h.toFinset (s := D.support (U := closedBall c |R|)),
      circleAverage (fun (x : ℂ) ↦ (↑((D : (a : ℂ) → ℤ) i) : ℝ) * log ‖x - i‖) c R)
⊢ Eq (α := ℝ) (circleAverage (∑ᶠ (u : ℂ), fun (x : ℂ) ↦ (↑((D : (a : ℂ) → ℤ) u) : ℝ) * log ‖x - u‖) c R)
    (∑ᶠ (u : ℂ), (↑((D : (a : ℂ) → ℤ) u) : ℝ) * log R)
have calc₂ : Eq (α := ℝ)
  (∑ i ∈ h.toFinset (s := D.support (U := closedBall c |R|)),
    circleAverage (fun (x : ℂ) ↦ (↑((D : (a : ℂ) → ℤ) i) : ℝ) * log ‖x - i‖) c R)
  (∑ u ∈ h.toFinset (s := D.support (U := closedBall c |R|)), (↑((D : (a : ℂ) → ℤ) u) : ℝ) * log R)
Tactic: calc circleAverage (∑ᶠ u, (D u * log ‖· - u‖)) c R
  _ = circleAverage (∑ u ∈ h.toFinset, (D u * log ‖· - u‖)) c R := by
    rw [finsum_eq_sum_of_support_subset]
    intro u
    contrapose
    aesop
  _ = ∑ i ∈ h.toFinset, circleAverage (fun x ↦ D i * log ‖x - i‖) c R := by
    rw [circleAverage_sum]
    intro u hu
    apply IntervalIntegrable.const_mul
    apply (analyticOnNhd_id.sub analyticOnNhd_const).meromorphicOn.circleIntegrable_log_norm
  _ = ∑ u ∈ h.toFinset, D u * log R := by
    apply Finset.sum_congr rfl
    intro u hu
    simp_rw [← smul_eq_mul, circleAverage_fun_smul]
    congr
    rw [circleAverage_log_norm_sub_const_of_mem_closedBall]
    apply D.supportWithinDomain
    simp_all
  _ = ∑ᶠ u, D u * log R := by
    rw [finsum_eq_sum_of_support_subset]
    intro u
    aesop
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
Goal:
R : ℝ
c : ℂ
D : Function.locallyFinsuppWithin (closedBall c |R|) ℤ
h : D.support (U := closedBall c |R|).Finite
calc :
  Eq (α := ℝ) (circleAverage (∑ᶠ (u : ℂ), fun (x : ℂ) ↦ (↑((D : (a : ℂ) → ℤ) u) : ℝ) * log ‖x - u‖) c R)
    (circleAverage
      (∑ u ∈ h.toFinset (s := D.support (U := closedBall c |R|)), fun (x : ℂ) ↦
        (↑((D : (a : ℂ) → ℤ) u) : ℝ) * log ‖x - u‖)
      c R)
calc₁ :
  Eq (α := ℝ)
    (circleAverage
      (∑ u ∈ h.toFinset (s := D.support (U := closedBall c |R|)), fun (x : ℂ) ↦
        (↑((D : (a : ℂ) → ℤ) u) : ℝ) * log ‖x - u‖)
      c R)
    (∑ i ∈ h.toFinset (s := D.support (U := closedBall c |R|)),
      circleAverage (fun (x : ℂ) ↦ (↑((D : (a : ℂ) → ℤ) i) : ℝ) * log ‖x - i‖) c R)
calc₂ :
  Eq (α := ℝ)
    (∑ i ∈ h.toFinset (s := D.support (U := closedBall c |R|)),
      circleAverage (fun (x : ℂ) ↦ (↑((D : (a : ℂ) → ℤ) i) : ℝ) * log ‖x - i‖) c R)
    (∑ u ∈ h.toFinset (s := D.support (U := closedBall c |R|)), (↑((D : (a : ℂ) → ℤ) u) : ℝ) * log R)
⊢ Eq (α := ℝ) (circleAverage (∑ᶠ (u : ℂ), fun (x : ℂ) ↦ (↑((D : (a : ℂ) → ℤ) u) : ℝ) * log ‖x - u‖) c R)
    (∑ᶠ (u : ℂ), (↑((D : (a : ℂ) → ℤ) u) : ℝ) * log R)
have calc₃ : Eq (α := ℝ) (∑ u ∈ h.toFinset (s := D.support (U := closedBall c |R|)), (↑((D : (a : ℂ) → ℤ) u) : ℝ) * log R)
  (∑ᶠ (u : ℂ), (↑((D : (a : ℂ) → ℤ) u) : ℝ) * log R)
Tactic: calc circleAverage (∑ᶠ u, (D u * log ‖· - u‖)) c R
  _ = circleAverage (∑ u ∈ h.toFinset, (D u * log ‖· - u‖)) c R := by
    rw [finsum_eq_sum_of_support_subset]
    intro u
    contrapose
    aesop
  _ = ∑ i ∈ h.toFinset, circleAverage (fun x ↦ D i * log ‖x - i‖) c R := by
    rw [circleAverage_sum]
    intro u hu
    apply IntervalIntegrable.const_mul
    apply (analyticOnNhd_id.sub analyticOnNhd_const).meromorphicOn.circleIntegrable_log_norm
  _ = ∑ u ∈ h.toFinset, D u * log R := by
    apply Finset.sum_congr rfl
    intro u hu
    simp_rw [← smul_eq_mul, circleAverage_fun_smul]
    congr
    rw [circleAverage_log_norm_sub_const_of_mem_closedBall]
    apply D.supportWithinDomain
    simp_all
  _ = ∑ᶠ u, D u * log R := by
    rw [finsum_eq_sum_of_support_subset]
    intro u
    aesop
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
Goal:
c : ℂ
R : ℝ
D : ℂ → ℤ
hR : R ≠ 0
hD : Function.HasFiniteSupport D
⊢ ∑ᶠ (u : ℂ), (↑(D u) : ℝ) * (log R - log ‖c - u‖) =
    ∑ᶠ (u : ℂ), (↑(D u) : ℝ) * log (R * ‖c - u‖⁻¹) + (↑(D c) : ℝ) * log R
have 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
Tactic: by_cases h : c ∈ D.support
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
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
⊢ ∑ᶠ (u : ℂ), (↑(D u) : ℝ) * (log R - log ‖c - u‖) =
    ∑ᶠ (u : ℂ), (↑(D u) : ℝ) * log (R * ‖c - u‖⁻¹) + (↑(D c) : ℝ) * log R
have 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
Tactic: by_cases h : c ∈ D.support
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (hypothesis)
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 this : ∀ {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
-- 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
this :
  ∀ {g : ℂ → ℝ},
    (Function.support (M := ℝ) fun (u : ℂ) ↦ (↑(D u) : ℝ) * g u) ⊆
      (↑(Finite.toFinset (s := Function.support D) hD) : Set ℂ)
⊢ ∑ᶠ (u : ℂ), (↑(D u) : ℝ) * (log R - log ‖c - u‖) =
    ∑ᶠ (u : ℂ), (↑(D u) : ℝ) * log (R * ‖c - u‖⁻¹) + (↑(D c) : ℝ) * log R
have 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‖⁻¹))
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]
-- 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
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‖⁻¹))
have 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‖⁻¹)
Tactic: refine Finset.sum_congr rfl fun x hx ↦ ?_
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (hypothesis)
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}
⊢ (↑(D x) : ℝ) * (log R - log ‖c - x‖) = (↑(D x) : ℝ) * log (R * ‖c - x‖⁻¹)
have hx₁ : x ∈ Finite.toFinset (s := Function.support D) hD ∧ x ≠ c
Tactic: simp only [Finset.mem_sdiff, Finset.notMem_singleton] at hx
Cleared hypotheses: hx
-- 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
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 * ‖c - x‖⁻¹)
have pos : (↑(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 hx.2.symm))), log_inv]