awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.JensenFormula
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))
n : ℕ
x : ℂ
hx : Membership.mem (γ := Set ℂ) (closure (ball 0 (r n))) x
this : x ≠ ρ
⊢ ‖x - ρ‖ ≠ 0

Tactic:
simpa [sub_eq_zero]

Premises used: sub_eq_zero
-- Module: Mathlib.Analysis.Complex.JensenFormula
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))
n : ℕ
x : ℂ
hx : Membership.mem (γ := Set ℂ) (closure (ball 0 (r n))) x
hf : x ≠ ρ
⊢ ‖x - ρ‖ ≠ 0

Tactic:
suffices x ≠ ρ by simpa [sub_eq_zero]
-- Module: Mathlib.Analysis.Complex.JensenFormula
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))
n : ℕ
x : ℂ
hx : Membership.mem (γ := Set ℂ) (closure (ball 0 (r n))) x
⊢ ‖x‖ ≤ r n

Tactic:
simpa using closure_ball_subset_closedBall hx

Premises used: Metric.closure_ball_subset_closedBall
-- Module: Mathlib.Analysis.Complex.JensenFormula
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))
n : ℕ
x : ℂ
hx : Membership.mem (γ := Set ℂ) (closure (ball 0 (r n))) x
⊢ ‖x‖ ≤ r n

Tactic:
have key := by simpa using closure_ball_subset_closedBall hx
-- Module: Mathlib.Analysis.Complex.JensenFormula
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))
n : ℕ
x : ℂ
hx : Membership.mem (γ := Set ℂ) (closure (ball 0 (r n))) x
key : ‖x‖ ≤ r n
⊢ x ≠ ρ

Tactic:
grind
-- Module: Mathlib.Analysis.Complex.JensenFormula
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))
n : ℕ
hw₁ : ‖w‖ + (R - ‖w‖) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 < R
⊢ Membership.mem (γ := Set ℂ) (ball 0 (r n)) w

Tactic:
simp only [mem_ball, dist_zero_right, lt_sub_iff_add_lt, r]

Premises used: Metric.mem_ball, lt_sub_iff_add_lt, dist_zero_right
-- Module: Mathlib.Analysis.Complex.JensenFormula
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))
n : ℕ
hw₁ : ‖w‖ * HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 + (R - ‖w‖) < R * HAdd.hAdd (α := ℝ) (↑n : ℝ) 2
⊢ ‖w‖ + (R - ‖w‖) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 < R

Tactic:
field_simp
-- Module: Mathlib.Analysis.Complex.JensenFormula
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))
n : ℕ
⊢ ‖w‖ * HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 + (R - ‖w‖) = ‖w‖ * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + R

Tactic:
ring
-- Module: Mathlib.Analysis.Complex.JensenFormula
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))
n : ℕ
bc : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
⊢ ‖w‖ * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + R < R * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + R

Tactic:
gcongr
-- Module: Mathlib.Analysis.Complex.JensenFormula
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))
n : ℕ
⊢ R * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + R = R * HAdd.hAdd (α := ℝ) (↑n : ℝ) 2

Tactic:
ring
-- Module: Mathlib.Analysis.Complex.JensenFormula
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))
n : ℕ
calc : ‖w‖ * HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 + (R - ‖w‖) = ‖w‖ * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + R
calc₁ : ‖w‖ * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + R < R * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + R
calc₂ : R * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + R = R * HAdd.hAdd (α := ℝ) (↑n : ℝ) 2
⊢ ‖w‖ * HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 + (R - ‖w‖) < R * HAdd.hAdd (α := ℝ) (↑n : ℝ) 2

Tactic:
calc ‖w‖ * (n + 2) + (R - ‖w‖) = ‖w‖ * (n + 1) + R := by ring
        _ < R * (n + 1) + R := by gcongr
        _ = R * (n + 2) := by ring

Premises used: Norm.norm, HSub.hSub, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.JensenFormula
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))
⊢ ∀ {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
-- Module: Mathlib.Analysis.Complex.JensenFormula
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))
this : ∀ {n : ℕ}, circleAverage (herglotzLogIntegrand w ρ) 0 (r n) = log ‖w - ρ‖
⊢ circleAverage (HSMul.hSMul (β := ℂ → ℝ) (Complex.re ∘ herglotzRieszKernel 0 w) fun (x : ℂ) ↦ log ‖x - ρ‖) 0 R =
    log ‖w - ρ‖

Tactic:
aesop
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
w ρ c : ℂ
R : ℝ
hρ : ρ ∈ sphere c R
hw : w ∈ ball c R
simp : circleAverage (fun (z : ℂ) ↦ (herglotzRieszKernel c w (z + 0 + c)).re * log ‖z + 0 + c - ρ‖) 0 R = log ‖w - ρ‖
⊢ circleAverage (Complex.re ∘ herglotzRieszKernel c w * fun (x : ℂ) ↦ log ‖x - ρ‖) c R = log ‖w - ρ‖

Tactic:
simp only [← circleAverage_map_add_const, Pi.mul_apply, Function.comp_apply, add_zero]

Premises used: Real.circleAverage_map_add_const, Pi.mul_apply, Function.comp_apply, add_zero
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
w ρ c : ℂ
R : ℝ
hρ : ρ ∈ sphere c R
hw : w ∈ ball c R
left : circleAverage (fun (z : ℂ) ↦ (herglotzRieszKernel c w (z + 0 + c)).re * log ‖z + 0 + c - ρ‖) 0 R
| circleAverage (fun (z : ℂ) ↦ (herglotzRieszKernel c w (z + 0 + c)).re * log ‖z + 0 + c - ρ‖) 0 R = log ‖w - ρ‖

Tactic:
left
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
w ρ c : ℂ
R : ℝ
hρ : ρ ∈ sphere c R
hw : w ∈ ball c R
arg : fun (z : ℂ) ↦ (herglotzRieszKernel c w (z + 0 + c)).re * log ‖z + 0 + c - ρ‖
| circleAverage (fun (z : ℂ) ↦ (herglotzRieszKernel c w (z + 0 + c)).re * log ‖z + 0 + c - ρ‖) 0 R

Tactic:
arg 1
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
w ρ c : ℂ
R : ℝ
hρ : ρ ∈ sphere c R
hw : w ∈ ball c R
z : ℂ
⊢ z + 0 + c - ρ = z - (ρ - c)

Tactic:
ring
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
w ρ c : ℂ
R : ℝ
hρ : ρ ∈ sphere c R
hw : w ∈ ball c R
z : ℂ
h : (herglotzRieszKernel c w (z + 0 + c)).re * log ‖z - (ρ - c)‖
| (herglotzRieszKernel c w (z + 0 + c)).re * log ‖z + 0 + c - ρ‖

Tactic:
rw [(by ring : (z + 0 + c) - ρ = z - (ρ - c))]
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
w ρ c : ℂ
R : ℝ
hρ : ρ ∈ sphere c R
hw : w ∈ ball c R
z : ℂ
h : (herglotzRieszKernel c w (z + 0 + c)).re
| (herglotzRieszKernel c w (z + 0 + c)).re * log ‖z - (ρ - c)‖

Tactic:
arg 1
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
w ρ c : ℂ
R : ℝ
hρ : ρ ∈ sphere c R
hw : w ∈ ball c R
z : ℂ
h : herglotzRieszKernel c w (z + 0 + c)
| (herglotzRieszKernel c w (z + 0 + c)).re

Tactic:
arg 1
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
w ρ c : ℂ
R : ℝ
hρ : ρ ∈ sphere c R
hw : w ∈ ball c R
z : ℂ
h : herglotzRieszKernel 0 (w - c) z
| herglotzRieszKernel c w (z + 0 + c)

Tactic:
rw [add_zero, herglotzRieszKernel_add_const c w z]

Premises used: herglotzRieszKernel_add_const, add_zero
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
w ρ c : ℂ
R : ℝ
hρ : ρ ∈ sphere c R
hw : w ∈ ball c R
h : ∀ (z : ℂ), herglotzRieszKernel 0 (w - c) z
| circleAverage (fun (z : ℂ) ↦ (herglotzRieszKernel c w (z + 0 + c)).re * log ‖z + 0 + c - ρ‖) 0 R = log ‖w - ρ‖

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]

Premises used: add_zero
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
w ρ c : ℂ
R : ℝ
hρ : ρ ∈ sphere c R
hw : w ∈ ball c R
conv : circleAverage (fun (z : ℂ) ↦ (herglotzRieszKernel 0 (w - c) z).re * log ‖z - (ρ - c)‖) 0 R = log ‖w - ρ‖
⊢ circleAverage (fun (z : ℂ) ↦ (herglotzRieszKernel c w (z + 0 + c)).re * log ‖z + 0 + 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]

Premises used: add_zero
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
w ρ c : ℂ
R : ℝ
hρ : ρ ∈ sphere c R
hw : w ∈ ball c R
⊢ (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:
rfl
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
w ρ c : ℂ
R : ℝ
hρ : ρ ∈ sphere c R
hw : w ∈ ball c R
⊢ (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
-- Module: Mathlib.Analysis.Complex.JensenFormula
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)‖
⊢ Membership.mem (γ := Set ℂ) (sphere 0 R) (ρ - c)

Tactic:
simp_all
-- Module: Mathlib.Analysis.Complex.JensenFormula
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)‖
⊢ Membership.mem (γ := Set ℂ) (ball 0 R) (w - c)

Tactic:
simp_all [mem_ball_iff_norm.1 hw]

Premises used: mem_ball_iff_norm, Iff.mp
-- Module: Mathlib.Analysis.Complex.JensenFormula
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)‖
rw : log ‖w - c - (ρ - c)‖ = log ‖w - ρ‖
⊢ circleAverage (fun (z : ℂ) ↦ (herglotzRieszKernel 0 (w - c) z).re * log ‖z - (ρ - c)‖) 0 R = log ‖w - ρ‖

Tactic:
rw [this, circleAverage_re_herglotzRieszKernel_mul_log₀ (by simp_all)
    (by simp_all [mem_ball_iff_norm.1 hw])]

Premises used: circleAverage_re_herglotzRieszKernel_mul_log₀
-- Module: Mathlib.Analysis.Complex.JensenFormula
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)‖
⊢ log ‖w - c - (ρ - c)‖ = log ‖w - ρ‖

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
R : ℝ
c : ℂ
D : Function.locallyFinsuppWithin (closedBall c |R|) ℤ
⊢ D.support (U := closedBall c |R|).Finite

Tactic:
have h := D.finiteSupport (isCompact_closedBall c |R|)
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
R : ℝ
c : ℂ
D : Function.locallyFinsuppWithin (closedBall c |R|) ℤ
h : D.support (U := closedBall c |R|).Finite
h₁ :
  (Function.support (M := ℂ → ℝ) fun (u x : ℂ) ↦ (↑((D : (a : ℂ) → ℤ) u) : ℝ) * log ‖x - u‖) ⊆
    (↑(h.toFinset (s := D.support (U := closedBall c |R|))) : Set ℂ)
⊢ 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:
rw [finsum_eq_sum_of_support_subset]

Premises used: finsum_eq_sum_of_support_subset
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
R : ℝ
c : ℂ
D : Function.locallyFinsuppWithin (closedBall c |R|) ℤ
h : D.support (U := closedBall c |R|).Finite
u : ℂ
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‖
⊢ 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 ℂ)

Tactic:
contrapose
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
R : ℝ
c : ℂ
D : Function.locallyFinsuppWithin (closedBall c |R|) ℤ
h : D.support (U := closedBall c |R|).Finite
u : ℂ
⊢ 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:
aesop
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
R : ℝ
c : ℂ
D : Function.locallyFinsuppWithin (closedBall c |R|) ℤ
h : D.support (U := closedBall c |R|).Finite
rw :
  ∀ i ∈ h.toFinset (s := D.support (U := closedBall c |R|)),
    CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ (↑((D : (a : ℂ) → ℤ) i) : ℝ) * log ‖x - i‖) c R
⊢ 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:
rw [circleAverage_sum]

Premises used: Real.circleAverage_sum
-- Module: Mathlib.Analysis.Complex.JensenFormula
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|))
hf : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log ‖circleMap c R x - u‖) volume 0 (2 * π)
⊢ CircleIntegrable (E := ℝ) (fun (x : ℂ) ↦ (↑((D : (a : ℂ) → ℤ) u) : ℝ) * log ‖x - u‖) c R

Tactic:
apply IntervalIntegrable.const_mul

Premises used: IntervalIntegrable.const_mul
-- Module: Mathlib.Analysis.Complex.JensenFormula
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|))
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ log ‖circleMap c R x - u‖) volume 0 (2 * π)

Tactic:
apply (analyticOnNhd_id.sub analyticOnNhd_const).meromorphicOn.circleIntegrable_log_norm

Premises used: analyticOnNhd_id, analyticOnNhd_const, MeromorphicOn.circleIntegrable_log_norm, AnalyticOnNhd.meromorphicOn, AnalyticOnNhd.sub
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
R : ℝ
c : ℂ
D : Function.locallyFinsuppWithin (closedBall c |R|) ℤ
h : D.support (U := closedBall c |R|).Finite
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
⊢ 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:
apply Finset.sum_congr rfl

Premises used: Finset.sum_congr, rfl
-- Module: Mathlib.Analysis.Complex.JensenFormula
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|))
simp_rw :
  HSMul.hSMul (α := ℝ) (β := ℝ) (↑((D : (a : ℂ) → ℤ) u) : ℝ) (circleAverage (fun (z : ℂ) ↦ log ‖z - u‖) c R) =
    HSMul.hSMul (α := ℝ) (↑((D : (a : ℂ) → ℤ) u) : ℝ) (log R)
⊢ circleAverage (fun (x : ℂ) ↦ (↑((D : (a : ℂ) → ℤ) u) : ℝ) * log ‖x - u‖) c R = (↑((D : (a : ℂ) → ℤ) u) : ℝ) * log R

Tactic:
simp_rw [← smul_eq_mul, circleAverage_fun_smul]

Premises used: Real.circleAverage_fun_smul, smul_eq_mul
-- Module: Mathlib.Analysis.Complex.JensenFormula
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|))
e_a : circleAverage (fun (z : ℂ) ↦ log ‖z - u‖) c R = log R
⊢ HSMul.hSMul (α := ℝ) (β := ℝ) (↑((D : (a : ℂ) → ℤ) u) : ℝ) (circleAverage (fun (z : ℂ) ↦ log ‖z - u‖) c R) =
    HSMul.hSMul (α := ℝ) (↑((D : (a : ℂ) → ℤ) u) : ℝ) (log R)

Tactic:
congr
-- Module: Mathlib.Analysis.Complex.JensenFormula
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|))
e_a : u ∈ closedBall c |R|
⊢ circleAverage (fun (z : ℂ) ↦ log ‖z - u‖) c R = log R

Tactic:
rw [circleAverage_log_norm_sub_const_of_mem_closedBall]

Premises used: circleAverage_log_norm_sub_const_of_mem_closedBall
-- Module: Mathlib.Analysis.Complex.JensenFormula
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|))
e_a : u ∈ D.support (U := closedBall c |R|)
⊢ u ∈ closedBall c |R|

Tactic:
apply D.supportWithinDomain

Premises used: Function.locallyFinsuppWithin.supportWithinDomain
-- Module: Mathlib.Analysis.Complex.JensenFormula
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 ∈ D.support (U := closedBall c |R|)

Tactic:
simp_all
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
R : ℝ
c : ℂ
D : Function.locallyFinsuppWithin (closedBall c |R|) ℤ
h : D.support (U := closedBall c |R|).Finite
h₁ :
  (Function.support (M := ℝ) fun (u : ℂ) ↦ (↑((D : (a : ℂ) → ℤ) u) : ℝ) * log R) ⊆
    (↑(h.toFinset (s := D.support (U := closedBall c |R|))) : Set ℂ)
⊢ Eq (α := ℝ) (∑ u ∈ h.toFinset (s := D.support (U := closedBall c |R|)), (↑((D : (a : ℂ) → ℤ) u) : ℝ) * log R)
    (∑ᶠ (u : ℂ), (↑((D : (a : ℂ) → ℤ) u) : ℝ) * log R)

Tactic:
rw [finsum_eq_sum_of_support_subset]

Premises used: finsum_eq_sum_of_support_subset
-- Module: Mathlib.Analysis.Complex.JensenFormula
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 : ℂ) ↦ (↑((D : (a : ℂ) → ℤ) u) : ℝ) * log R) u →
    u ∈ (↑(h.toFinset (s := D.support (U := closedBall c |R|))) : Set ℂ)

Tactic:
aesop
-- Module: Mathlib.Analysis.Complex.JensenFormula
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)
calc₃ :
  Eq (α := ℝ) (∑ u ∈ h.toFinset (s := D.support (U := closedBall c |R|)), (↑((D : (a : ℂ) → ℤ) u) : ℝ) * log R)
    (∑ᶠ (u : ℂ), (↑((D : (a : ℂ) → ℤ) u) : ℝ) * log R)
⊢ Eq (α := ℝ) (circleAverage (∑ᶠ (u : ℂ), fun (x : ℂ) ↦ (↑((D : (a : ℂ) → ℤ) u) : ℝ) * log ‖x - u‖) c 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

Premises used: Norm.norm, Int.cast, HMul.hMul, finsum, HSub.hSub, Real.log, Set.Finite.toFinset, DFunLike.coe, Finset.sum, Real.circleAverage