awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (hypothesis)
Goal:
ρ w : ℂ
R : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
r : ℕ → ℝ
hr_lt : ∀ (n : ℕ), r n < R
hr_tendsto : Tendsto r atTop (𝓝 R)
bound : (θ : ℝ) → ℝ :=
  fun (θ : ℝ) ↦
    (R + ‖w‖) / ((R + ‖w‖) / 2 - ‖w‖) * (|log (2 * R)| + |log √((R + ‖w‖) / 2 / R)| + |log ‖circleMap 0 R θ - ρ‖|)
n : ℕ
hn : (R + ‖w‖) / 2 ≤ r n
⊢ ∀ᵐ (x : ℝ), x ∈ uIoc 0 (2 * π) → ‖herglotzLogIntegrand w ρ (circleMap 0 (r n) x)‖ ≤ bound x
have h_bound : ∀ {θ : ℝ}, ‖herglotzLogIntegrand w ρ (circleMap 0 (r n) θ)‖ ≤ bound θ ∨ ‖circleMap 0 R θ - ρ‖ = 0
Tactic: have h_bound {θ : ℝ} :
        ‖herglotzLogIntegrand w ρ (circleMap 0 (r n) θ)‖ ≤ bound θ ∨ ‖circleMap 0 R θ - ρ‖ = 0 := by
      refine Classical.or_iff_not_imp_right.mpr fun h ↦ ?_
      apply norm_herglotzLogIntegrand_circleMap_le hR hρ (by positivity) (by linarith) hn
        (hr_lt n).le
      simpa using h
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
Goal:
ρ w : ℂ
R : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
r : ℕ → ℝ
hr_lt : ∀ (n : ℕ), r n < R
hr_tendsto : Tendsto r atTop (𝓝 R)
bound : (θ : ℝ) → ℝ :=
  fun (θ : ℝ) ↦
    (R + ‖w‖) / ((R + ‖w‖) / 2 - ‖w‖) * (|log (2 * R)| + |log √((R + ‖w‖) / 2 / R)| + |log ‖circleMap 0 R θ - ρ‖|)
n : ℕ
hn : (R + ‖w‖) / 2 ≤ r n
h_bound : ∀ {θ : ℝ}, ‖herglotzLogIntegrand w ρ (circleMap 0 (r n) θ)‖ ≤ bound θ ∨ ‖circleMap 0 R θ - ρ‖ = 0
⊢ ∀ᵐ (x : ℝ), x ∈ uIoc 0 (2 * π) → ‖herglotzLogIntegrand w ρ (circleMap 0 (r n) x)‖ ≤ bound x
have h : Eq (α := ENNReal) ((volume : (a : Set ℝ) → ENNReal) {θ : ℝ | ‖circleMap 0 R θ - ρ‖ = 0} : ENNReal) (0 : ENNReal)
Tactic: apply measure_mono_null (t := {θ | ‖circleMap 0 R θ - ρ‖ = 0}) (by grind)
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
Goal:
ρ w : ℂ
R : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
r : ℕ → ℝ
hr_lt : ∀ (n : ℕ), r n < R
hr_tendsto : Tendsto r atTop (𝓝 R)
bound : (θ : ℝ) → ℝ :=
  fun (θ : ℝ) ↦
    (R + ‖w‖) / ((R + ‖w‖) / 2 - ‖w‖) * (|log (2 * R)| + |log √((R + ‖w‖) / 2 / R)| + |log ‖circleMap 0 R θ - ρ‖|)
⊢ IntervalIntegrable bound volume 0 (2 * π)
have apply : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ |log ‖circleMap 0 R x - ρ‖|) volume 0 (2 * π)
Tactic: apply (IntervalIntegrable.add (by simp) (by simp)).add ?_ |>.const_mul
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (hypothesis)
Goal:
ρ w : ℂ
R : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
r : ℕ → ℝ
hr_lt : ∀ (n : ℕ), r n < R
hr_tendsto : Tendsto r atTop (𝓝 R)
bound : (θ : ℝ) → ℝ :=
  fun (θ : ℝ) ↦
    (R + ‖w‖) / ((R + ‖w‖) / 2 - ‖w‖) * (|log (2 * R)| + |log √((R + ‖w‖) / 2 / R)| + |log ‖circleMap 0 R θ - ρ‖|)
⊢ ∀ᵐ (x : ℝ),
    x ∈ uIoc 0 (2 * π) →
      Tendsto (fun (n : ℕ) ↦ herglotzLogIntegrand w ρ (circleMap 0 (r n) x)) atTop
        (𝓝 (herglotzLogIntegrand w ρ (circleMap 0 R x)))
have h_measure_zero : Eq (α := ENNReal) ((volume : (a : Set ℝ) → ENNReal) {θ : ℝ | circleMap 0 R θ = w ∨ circleMap 0 R θ = ρ} : ENNReal)
  (0 : ENNReal)
Tactic: have h_measure_zero : volume {θ : ℝ | circleMap 0 R θ = w ∨ circleMap 0 R θ = ρ} = 0 :=
      countable_singleton w |>.preimage_circleMap 0 (hR.ne') |>.union
        ((countable_singleton ρ).preimage_circleMap 0 (hR.ne')) |>.measure_zero _
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
Goal:
ρ w : ℂ
R : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
r : ℕ → ℝ
hr_lt : ∀ (n : ℕ), r n < R
hr_tendsto : Tendsto r atTop (𝓝 R)
bound : (θ : ℝ) → ℝ :=
  fun (θ : ℝ) ↦
    (R + ‖w‖) / ((R + ‖w‖) / 2 - ‖w‖) * (|log (2 * R)| + |log √((R + ‖w‖) / 2 / R)| + |log ‖circleMap 0 R θ - ρ‖|)
h_measure_zero :
  Eq (α := ENNReal) ((volume : (a : Set ℝ) → ENNReal) {θ : ℝ | circleMap 0 R θ = w ∨ circleMap 0 R θ = ρ} : ENNReal)
    (0 : ENNReal)
⊢ ∀ᵐ (x : ℝ),
    x ∈ uIoc 0 (2 * π) →
      Tendsto (fun (n : ℕ) ↦ herglotzLogIntegrand w ρ (circleMap 0 (r n) x)) atTop
        (𝓝 (herglotzLogIntegrand w ρ (circleMap 0 R x)))
have h : ∀ (θ : ℝ) (hθ : ¬(circleMap 0 R θ = w ∨ circleMap 0 R θ = ρ)),
  θ ∈ uIoc 0 (2 * π) →
    Tendsto (fun (n : ℕ) ↦ herglotzLogIntegrand w ρ (circleMap 0 (r n) θ)) atTop
      (𝓝 (herglotzLogIntegrand w ρ (circleMap 0 R θ)))
Tactic: filter_upwards [measure_eq_zero_iff_ae_notMem.mp h_measure_zero] with θ hθ _
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
Goal:
ρ w : ℂ
R : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
r : ℕ → ℝ
hr_lt : ∀ (n : ℕ), r n < R
hr_tendsto : Tendsto r atTop (𝓝 R)
bound : (θ : ℝ) → ℝ :=
  fun (θ : ℝ) ↦
    (R + ‖w‖) / ((R + ‖w‖) / 2 - ‖w‖) * (|log (2 * R)| + |log √((R + ‖w‖) / 2 / R)| + |log ‖circleMap 0 R θ - ρ‖|)
h_measure_zero :
  Eq (α := ENNReal) ((volume : (a : Set ℝ) → ENNReal) {θ : ℝ | circleMap 0 R θ = w ∨ circleMap 0 R θ = ρ} : ENNReal)
    (0 : ENNReal)
θ : ℝ
hθ : ¬(circleMap 0 R θ = w ∨ circleMap 0 R θ = ρ)
h : θ ∈ uIoc 0 (2 * π)
⊢ circleMap 0 R θ ≠ w
have tauto : θ ∈ uIoc 0 (2 * π) → circleMap 0 R θ = w → ¬circleMap 0 R θ = w → ¬circleMap 0 R θ = ρ → False
Tactic: tauto
Cleared hypotheses: hθ, h
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
Goal:
ρ w : ℂ
R : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
r : ℕ → ℝ
hr_lt : ∀ (n : ℕ), r n < R
hr_tendsto : Tendsto r atTop (𝓝 R)
bound : (θ : ℝ) → ℝ :=
  fun (θ : ℝ) ↦
    (R + ‖w‖) / ((R + ‖w‖) / 2 - ‖w‖) * (|log (2 * R)| + |log √((R + ‖w‖) / 2 / R)| + |log ‖circleMap 0 R θ - ρ‖|)
h_measure_zero :
  Eq (α := ENNReal) ((volume : (a : Set ℝ) → ENNReal) {θ : ℝ | circleMap 0 R θ = w ∨ circleMap 0 R θ = ρ} : ENNReal)
    (0 : ENNReal)
θ : ℝ
hθ : ¬(circleMap 0 R θ = w ∨ circleMap 0 R θ = ρ)
h : θ ∈ uIoc 0 (2 * π)
⊢ circleMap 0 R θ ≠ ρ
have tauto : θ ∈ uIoc 0 (2 * π) → circleMap 0 R θ = ρ → ¬circleMap 0 R θ = w → ¬circleMap 0 R θ = ρ → False
Tactic: tauto
Cleared hypotheses: hθ, h
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
Goal:
ρ w : ℂ
R : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
r : ℕ → ℝ
hr_lt : ∀ (n : ℕ), r n < R
hr_tendsto : Tendsto r atTop (𝓝 R)
bound : (θ : ℝ) → ℝ :=
  fun (θ : ℝ) ↦
    (R + ‖w‖) / ((R + ‖w‖) / 2 - ‖w‖) * (|log (2 * R)| + |log √((R + ‖w‖) / 2 / R)| + |log ‖circleMap 0 R θ - ρ‖|)
h_measure_zero :
  Eq (α := ENNReal) ((volume : (a : Set ℝ) → ENNReal) {θ : ℝ | circleMap 0 R θ = w ∨ circleMap 0 R θ = ρ} : ENNReal)
    (0 : ENNReal)
θ : ℝ
hθ : ¬(circleMap 0 R θ = w ∨ circleMap 0 R θ = ρ)
h : θ ∈ uIoc 0 (2 * π)
⊢ Tendsto (fun (n : ℕ) ↦ herglotzLogIntegrand w ρ (circleMap 0 (r n) θ)) atTop
    (𝓝 (herglotzLogIntegrand w ρ (circleMap 0 R θ)))
have h : Tendsto (fun (n : ℕ) ↦ circleMap 0 (r n) θ) atTop (𝓝 (circleMap 0 R θ))
Tactic: apply (continuousAt_herglotzLogIntegrand (by tauto) (by tauto)).tendsto.comp
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (hypothesis)
Goal:
w ρ : ℂ
R : ℝ
hρ : Membership.mem (γ := Set ℂ) (sphere 0 R) ρ
hw : Membership.mem (γ := Set ℂ) (ball 0 R) w
⊢ circleAverage (HSMul.hSMul (β := ℂ → ℝ) (Complex.re ∘ herglotzRieszKernel 0 w) fun (x : ℂ) ↦ log ‖x - ρ‖) 0 R =
    log ‖w - ρ‖
have hR : 0 < R
Tactic: have hR : 0 < R := pos_of_mem_ball hw
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (hypothesis)
Goal:
w ρ : ℂ
R : ℝ
hρ : Membership.mem (γ := Set ℂ) (sphere 0 R) ρ
hw : Membership.mem (γ := Set ℂ) (ball 0 R) w
hR : 0 < R
⊢ circleAverage (HSMul.hSMul (β := ℂ → ℝ) (Complex.re ∘ herglotzRieszKernel 0 w) fun (x : ℂ) ↦ log ‖x - ρ‖) 0 R =
    log ‖w - ρ‖
have hρ₁ : ‖ρ‖ = R
Tactic: rw [mem_sphere_iff_norm, sub_zero] at hρ
Cleared hypotheses: hρ, hw, hR
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (hypothesis)
Goal:
w ρ : ℂ
R : ℝ
hρ : ‖ρ‖ = R
hw : Membership.mem (γ := Set ℂ) (ball 0 R) w
hR : 0 < R
⊢ circleAverage (HSMul.hSMul (β := ℂ → ℝ) (Complex.re ∘ herglotzRieszKernel 0 w) fun (x : ℂ) ↦ log ‖x - ρ‖) 0 R =
    log ‖w - ρ‖
have hw₁ : ‖w‖ < R
Tactic: rw [mem_ball_iff_norm, sub_zero] at hw
Cleared hypotheses: hw, hR
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
Goal:
w ρ : ℂ
R : ℝ
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
hR : 0 < R
r : ℕ → ℝ := fun (n : ℕ) ↦ R - (R - ‖w‖) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 2
n : ℕ
⊢ r n < R
have simp_all : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 2
Tactic: simp_all only [sub_lt_self_iff, sub_pos, div_pos_iff_of_pos_left, r]
-- 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
⊢ circleAverage (HSMul.hSMul (β := ℂ → ℝ) (Complex.re ∘ herglotzRieszKernel 0 w) fun (x : ℂ) ↦ log ‖x - ρ‖) 0 R =
    log ‖w - ρ‖
have hr_lt : ∀ (n : ℕ), r n < R
Tactic: have hr_lt (n : ℕ) : r n < R := by
    simp_all only [sub_lt_self_iff, sub_pos, div_pos_iff_of_pos_left, r]
    positivity
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
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
n : ℕ
⊢ 0 < r n
have simp_all : ∀ (hr_lt : ∀ (n : ℕ), 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 2), (R - ‖w‖) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 < R
Tactic: simp_all only [sub_lt_self_iff, sub_pos, div_pos_iff_of_pos_left, r]
Cleared hypotheses: hr_lt
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
Goal:
w ρ : ℂ
R : ℝ
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
hR : 0 < R
r : ℕ → ℝ := fun (n : ℕ) ↦ R - (R - ‖w‖) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 2
n : ℕ
hr_lt : ∀ (n : ℕ), 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 2
⊢ 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 2
have linarith : HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 ≤ 0 →
  HMul.hMul (α := ℝ) 2 (-1) + HSub.hSub (α := ℝ) 0 (↑n : ℝ) + (HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
Goal:
w ρ : ℂ
R : ℝ
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
hR : 0 < R
r : ℕ → ℝ := fun (n : ℕ) ↦ R - (R - ‖w‖) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 2
n : ℕ
hr_lt : ∀ (n : ℕ), 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 2
linarith :
  HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 ≤ 0 →
    HMul.hMul (α := ℝ) 2 (-1) + HSub.hSub (α := ℝ) 0 (↑n : ℝ) + (HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 - 0) = 0
⊢ 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 2
have linarith₁ : HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 ≤ 0 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
Goal:
w ρ : ℂ
R : ℝ
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
hR : 0 < R
r : ℕ → ℝ := fun (n : ℕ) ↦ R - (R - ‖w‖) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 2
n : ℕ
hr_lt : ∀ (n : ℕ), 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 2
⊢ (R - ‖w‖) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 < R
have apply : R - ‖w‖ < R * HAdd.hAdd (α := ℝ) (↑n : ℝ) 2
Tactic: apply (div_lt_iff₀ (by linarith)).2
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
Goal:
w ρ : ℂ
R : ℝ
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
hR : 0 < R
r : ℕ → ℝ := fun (n : ℕ) ↦ R - (R - ‖w‖) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 2
n : ℕ
hr_lt : ∀ (n : ℕ), 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 2
⊢ R * 1 < R * HAdd.hAdd (α := ℝ) (↑n : ℝ) 2
have hbc : 1 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
Goal:
w ρ : ℂ
R : ℝ
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
hR : 0 < R
r : ℕ → ℝ := fun (n : ℕ) ↦ R - (R - ‖w‖) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 2
n : ℕ
hr_lt : ∀ (n : ℕ), 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 2
⊢ R - ‖w‖ < R * HAdd.hAdd (α := ℝ) (↑n : ℝ) 2
have calc : R - ‖w‖ ≤ R * 1
Tactic: calc R - ‖w‖
      _ ≤ R * 1 := by aesop
      _ < R * (n + 2) := by gcongr; grind
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
Goal:
w ρ : ℂ
R : ℝ
hρ : ‖ρ‖ = R
hw : ‖w‖ < R
hR : 0 < R
r : ℕ → ℝ := fun (n : ℕ) ↦ R - (R - ‖w‖) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 2
n : ℕ
hr_lt : ∀ (n : ℕ), 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 2
calc : R - ‖w‖ ≤ R * 1
⊢ R - ‖w‖ < R * HAdd.hAdd (α := ℝ) (↑n : ℝ) 2
have calc₁ : R * 1 < R * HAdd.hAdd (α := ℝ) (↑n : ℝ) 2
Tactic: calc R - ‖w‖
      _ ≤ R * 1 := by aesop
      _ < R * (n + 2) := by gcongr; grind
-- 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
⊢ circleAverage (HSMul.hSMul (β := ℂ → ℝ) (Complex.re ∘ herglotzRieszKernel 0 w) fun (x : ℂ) ↦ log ‖x - ρ‖) 0 R =
    log ‖w - ρ‖
have hr_pos : ∀ (n : ℕ), 0 < r n
Tactic: have hr_pos (n : ℕ) : 0 < r n := by
    simp_all only [sub_lt_self_iff, sub_pos, div_pos_iff_of_pos_left, r]
    apply (div_lt_iff₀ (by linarith)).2
    calc R - ‖w‖
      _ ≤ R * 1 := by aesop
      _ < R * (n + 2) := by gcongr; grind
-- 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
⊢ circleAverage (HSMul.hSMul (β := ℂ → ℝ) (Complex.re ∘ herglotzRieszKernel 0 w) fun (x : ℂ) ↦ log ‖x - ρ‖) 0 R =
    log ‖w - ρ‖
have hr_tendsto : Tendsto r atTop (𝓝 R)
Tactic: have hr_tendsto : Tendsto r atTop (nhds R) :=
    sub_zero R ▸ (tendsto_const_nhds.sub <| tendsto_const_nhds.div_atTop <|
      tendsto_atTop_add_const_right _ _ tendsto_natCast_atTop_atTop)
-- 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)
⊢ circleAverage (HSMul.hSMul (β := ℂ → ℝ) (Complex.re ∘ herglotzRieszKernel 0 w) fun (x : ℂ) ↦ log ‖x - ρ‖) 0 R =
    log ‖w - ρ‖
have DCT : Tendsto (fun (n : ℕ) ↦ circleAverage (herglotzLogIntegrand w ρ) 0 (r n)) atTop
  (𝓝 (circleAverage (herglotzLogIntegrand w ρ) 0 R))
Tactic: have DCT := herglotzLogIntegrand_circleAverage_tendsto hR hρ hw hr_lt hr_tendsto
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
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 (HSMul.hSMul (β := ℂ → ℝ) (Complex.re ∘ herglotzRieszKernel 0 w) fun (x : ℂ) ↦ log ‖x - ρ‖) 0 (r n) =
    log ‖w - ρ‖
have hf : InnerProductSpace.HarmonicContOnCl (F := ℝ) (fun (x : ℂ) ↦ log ‖x - ρ‖) (ball 0 (r n))
Tactic: apply InnerProductSpace.HarmonicContOnCl.circleAverage_re_herglotzRieszKernel_smul
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
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 : ℕ
hf : InnerProductSpace.HarmonicContOnCl (F := ℝ) (fun (x : ℂ) ↦ log ‖x - ρ‖) (ball 0 (r n))
⊢ circleAverage (HSMul.hSMul (β := ℂ → ℝ) (Complex.re ∘ herglotzRieszKernel 0 w) fun (x : ℂ) ↦ log ‖x - ρ‖) 0 (r n) =
    log ‖w - ρ‖
have hw₁ : Membership.mem (γ := Set ℂ) (ball 0 (r n)) w
Tactic: apply InnerProductSpace.HarmonicContOnCl.circleAverage_re_herglotzRieszKernel_smul
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
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 : ℕ
⊢ InnerProductSpace.HarmonicContOnCl (F := ℝ) (fun (x : ℂ) ↦ log ‖x - ρ‖) (ball 0 (r n))
have hf : ∀ (z : ℂ) (hz : Membership.mem (γ := Set ℂ) (ball 0 (r n)) z),
  InnerProductSpace.HarmonicAt (F := ℝ) (fun (x : ℂ) ↦ log ‖x - ρ‖) z
Tactic: refine ⟨fun z hz ↦ ?_, fun x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
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 : ℕ
hf :
  ∀ (z : ℂ) (hz : Membership.mem (γ := Set ℂ) (ball 0 (r n)) z),
    InnerProductSpace.HarmonicAt (F := ℝ) (fun (x : ℂ) ↦ log ‖x - ρ‖) z
⊢ InnerProductSpace.HarmonicContOnCl (F := ℝ) (fun (x : ℂ) ↦ log ‖x - ρ‖) (ball 0 (r n))
have hf₁ : ∀ (x : ℂ) (hx : Membership.mem (γ := Set ℂ) (closure (ball 0 (r n))) x),
  ContinuousWithinAt (Y := ℝ) (fun (x : ℂ) ↦ log ‖x - ρ‖) (closure (ball 0 (r n))) x
Tactic: refine ⟨fun z hz ↦ ?_, fun x hx ↦ ?_⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
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
⊢ ContinuousWithinAt (Y := ℝ) (fun (x : ℂ) ↦ log ‖x - ρ‖) (closure (ball 0 (r n))) x
have hf : ‖x - ρ‖ ≠ 0
Tactic: suffices ‖x - ρ‖ ≠ 0 by fun_prop
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
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 - ρ‖ ≠ 0
have hf : x ≠ ρ
Tactic: suffices x ≠ ρ by simpa [sub_eq_zero]
-- 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))
n : ℕ
x : ℂ
hx : Membership.mem (γ := Set ℂ) (closure (ball 0 (r n))) x
⊢ x ≠ ρ
have key : ‖x‖ ≤ r n
Tactic: have key := by simpa using closure_ball_subset_closedBall hx
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
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 : ℕ
⊢ Membership.mem (γ := Set ℂ) (ball 0 (r n)) w
have hw₁ : ‖w‖ + (R - ‖w‖) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 < R
Tactic: simp only [mem_ball, dist_zero_right, lt_sub_iff_add_lt, r]
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
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‖ + (R - ‖w‖) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 < R
have hw₁ : ‖w‖ * HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 + (R - ‖w‖) < R * HAdd.hAdd (α := ℝ) (↑n : ℝ) 2
Tactic: field_simp
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
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 : ℝ) 1 + R < R * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + R
have bc : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
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‖) < R * HAdd.hAdd (α := ℝ) (↑n : ℝ) 2
have calc : ‖w‖ * HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 + (R - ‖w‖) = ‖w‖ * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + R
Tactic: 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 ρ : ℂ
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
⊢ ‖w‖ * HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 + (R - ‖w‖) < R * HAdd.hAdd (α := ℝ) (↑n : ℝ) 2
have calc₁ : ‖w‖ * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + R < R * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + R
Tactic: 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 ρ : ℂ
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
⊢ ‖w‖ * HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 + (R - ‖w‖) < R * HAdd.hAdd (α := ℝ) (↑n : ℝ) 2
have calc₂ : R * HAdd.hAdd (α := ℝ) (↑n : ℝ) 1 + R = 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