awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
w ρ : ℂ
R r₀ r : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hw : ‖w‖ < r₀
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
hdR : 0 < ‖circleMap 0 R θ - ρ‖
hrw : 0 < r₀ - ‖w‖
hr : 0 < r
⊢ √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖

Tactic:
have h_norm_sub₁ := const_mul_norm_sub_circleMap_le_norm_sub_circleMap hρ hr₀ hR hr₀r hrR θ
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
w ρ : ℂ
R r₀ r : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hw : ‖w‖ < r₀
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
hdR : 0 < ‖circleMap 0 R θ - ρ‖
hrw : 0 < r₀ - ‖w‖
hr : 0 < r
h_norm_sub₁ : √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
⊢ 0 < √(r₀ / R) * ‖circleMap 0 R θ - ρ‖

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
w ρ : ℂ
R r₀ r : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hw : ‖w‖ < r₀
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
hdR : 0 < ‖circleMap 0 R θ - ρ‖
hrw : 0 < r₀ - ‖w‖
hr : 0 < r
h_norm_sub₁ : √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
⊢ 0 < ‖circleMap 0 r θ - ρ‖

Tactic:
have h_norm_sub₂ : 0 < ‖circleMap 0 r θ - ρ‖ := lt_of_lt_of_le (by positivity) h_norm_sub₁
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
w ρ : ℂ
R r₀ r : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hw : ‖w‖ < r₀
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
hdR : 0 < ‖circleMap 0 R θ - ρ‖
hrw : 0 < r₀ - ‖w‖
hr : 0 < r
h_norm_sub₁ : √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
h_norm_sub₂ : 0 < ‖circleMap 0 r θ - ρ‖
h₁ : |(herglotzRieszKernel 0 w (circleMap 0 r θ)).re| ≤ (R + ‖w‖) / (r₀ - ‖w‖)
h₂ : |log ‖circleMap 0 r θ - ρ‖| ≤ |log (2 * R)| + |log √(r₀ / R)| + |log ‖circleMap 0 R θ - ρ‖|
⊢ |(herglotzRieszKernel 0 w (circleMap 0 r θ)).re| * |log ‖circleMap 0 r θ - ρ‖| ≤
    (R + ‖w‖) / (r₀ - ‖w‖) * (|log (2 * R)| + |log √(r₀ / R)| + |log ‖circleMap 0 R θ - ρ‖|)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
w ρ : ℂ
R r₀ r : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hw : ‖w‖ < r₀
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
hdR : 0 < ‖circleMap 0 R θ - ρ‖
hrw : 0 < r₀ - ‖w‖
hr : 0 < r
h_norm_sub₁ : √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
h_norm_sub₂ : 0 < ‖circleMap 0 r θ - ρ‖
h₁ : |((circleMap 0 r θ + w) / (circleMap 0 r θ - w)).re| ≤ (R + ‖w‖) / (r₀ - ‖w‖)
⊢ |(herglotzRieszKernel 0 w (circleMap 0 r θ)).re| ≤ (R + ‖w‖) / (r₀ - ‖w‖)

Tactic:
simp only [herglotzRieszKernel_def, sub_zero]

Premises used: sub_zero, herglotzRieszKernel_def
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
w ρ : ℂ
R r₀ r : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hw : ‖w‖ < r₀
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
hdR : 0 < ‖circleMap 0 R θ - ρ‖
hrw : 0 < r₀ - ‖w‖
hr : 0 < r
h_norm_sub₁ : √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
h_norm_sub₂ : 0 < ‖circleMap 0 r θ - ρ‖
grw : ‖(circleMap 0 r θ + w) / (circleMap 0 r θ - w)‖ ≤ ‖circleMap 0 r θ + w‖ / ‖circleMap 0 r θ - w‖
grw₁ grw₂ : ‖circleMap 0 r θ + w‖ / ‖circleMap 0 r θ - w‖ ≤ ‖circleMap 0 r θ + w‖ / ‖circleMap 0 r θ - w‖
⊢ |((circleMap 0 r θ + w) / (circleMap 0 r θ - w)).re| ≤ ‖circleMap 0 r θ + w‖ / ‖circleMap 0 r θ - w‖

Tactic:
grw [Complex.abs_re_le_norm, norm_div]

Premises used: Complex.abs_re_le_norm, norm_div
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
w ρ : ℂ
R r₀ r : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hw : ‖w‖ < r₀
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
hdR : 0 < ‖circleMap 0 R θ - ρ‖
hrw : 0 < r₀ - ‖w‖
hr : 0 < r
h_norm_sub₁ : √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
h_norm_sub₂ : 0 < ‖circleMap 0 r θ - ρ‖
grw : (‖circleMap 0 r θ‖ + ‖w‖) / (‖circleMap 0 r θ‖ - ‖w‖) ≤ (r + ‖w‖) / (r - ‖w‖)
h₁ : 0 < ‖circleMap 0 r θ‖ - ‖w‖
⊢ ‖circleMap 0 r θ + w‖ / ‖circleMap 0 r θ - w‖ ≤ (r + ‖w‖) / (r - ‖w‖)

Tactic:
grw [norm_add_le, ← norm_sub_norm_le]

Premises used: norm_add_le, norm_sub_norm_le
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
w ρ : ℂ
R r₀ r : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hw : ‖w‖ < r₀
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
hdR : 0 < ‖circleMap 0 R θ - ρ‖
hrw : 0 < r₀ - ‖w‖
hr : 0 < r
h_norm_sub₁ : √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
h_norm_sub₂ : 0 < ‖circleMap 0 r θ - ρ‖
simp : (r + ‖w‖) / (r - ‖w‖) ≤ (r + ‖w‖) / (r - ‖w‖)
⊢ (‖circleMap 0 r θ‖ + ‖w‖) / (‖circleMap 0 r θ‖ - ‖w‖) ≤ (r + ‖w‖) / (r - ‖w‖)

Tactic:
simp only [norm_circleMap_zero, abs_of_pos hr]

Premises used: norm_circleMap_zero, abs_of_pos
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
w ρ : ℂ
R r₀ r : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hw : ‖w‖ < r₀
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
hdR : 0 < ‖circleMap 0 R θ - ρ‖
hrw : 0 < r₀ - ‖w‖
hr : 0 < r
h_norm_sub₁ : √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
h_norm_sub₂ : 0 < ‖circleMap 0 r θ - ρ‖
⊢ (r + ‖w‖) / (r - ‖w‖) ≤ (r + ‖w‖) / (r - ‖w‖)

Tactic:
grind
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
w ρ : ℂ
R r₀ r : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hw : ‖w‖ < r₀
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
hdR : 0 < ‖circleMap 0 R θ - ρ‖
hrw : 0 < r₀ - ‖w‖
hr : 0 < r
h_norm_sub₁ : √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
h_norm_sub₂ : 0 < ‖circleMap 0 r θ - ρ‖
h₁ : 0 < r - ‖w‖
⊢ 0 < ‖circleMap 0 r θ‖ - ‖w‖

Tactic:
simp only [norm_circleMap_zero, abs_of_pos hr]

Premises used: norm_circleMap_zero, abs_of_pos
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
w ρ : ℂ
R r₀ r : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hw : ‖w‖ < r₀
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
hdR : 0 < ‖circleMap 0 R θ - ρ‖
hrw : 0 < r₀ - ‖w‖
hr : 0 < r
h_norm_sub₁ : √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
h_norm_sub₂ : 0 < ‖circleMap 0 r θ - ρ‖
⊢ 0 < r - ‖w‖

Tactic:
grind
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
w ρ : ℂ
R r₀ r : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hw : ‖w‖ < r₀
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
hdR : 0 < ‖circleMap 0 R θ - ρ‖
hrw : 0 < r₀ - ‖w‖
hr : 0 < r
h_norm_sub₁ : √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
h_norm_sub₂ : 0 < ‖circleMap 0 r θ - ρ‖
hc : 0 ≤ R + ‖w‖
hd : 0 < r₀ - ‖w‖
⊢ (r + ‖w‖) / (r - ‖w‖) ≤ (R + ‖w‖) / (r₀ - ‖w‖)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
w ρ : ℂ
R r₀ r : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hw : ‖w‖ < r₀
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
hdR : 0 < ‖circleMap 0 R θ - ρ‖
hrw : 0 < r₀ - ‖w‖
hr : 0 < r
h_norm_sub₁ : √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
h_norm_sub₂ : 0 < ‖circleMap 0 r θ - ρ‖
r₁ : |((circleMap 0 r θ + w) / (circleMap 0 r θ - w)).re| ≤ ‖circleMap 0 r θ + w‖ / ‖circleMap 0 r θ - w‖
r₂ : ‖circleMap 0 r θ + w‖ / ‖circleMap 0 r θ - w‖ ≤ (r + ‖w‖) / (r - ‖w‖)
r₃ : (r + ‖w‖) / (r - ‖w‖) ≤ (R + ‖w‖) / (r₀ - ‖w‖)
⊢ |((circleMap 0 r θ + w) / (circleMap 0 r θ - w)).re| ≤ (R + ‖w‖) / (r₀ - ‖w‖)

Tactic:
calc
     |((circleMap 0 r θ + w) / (circleMap 0 r θ - w)).re|
     _ ≤ ‖circleMap 0 r θ + w‖ / ‖circleMap 0 r θ - w‖ := by grw [Complex.abs_re_le_norm, norm_div]
     _ ≤ (r + ‖w‖) / (r - ‖w‖) := by
        grw [norm_add_le, ← norm_sub_norm_le]
        all_goals simp only [norm_circleMap_zero, abs_of_pos hr]; grind
      _ ≤ (R + ‖w‖) / (r₀ - ‖w‖) := by gcongr

Premises used: Norm.norm, HSub.hSub, circleMap, HDiv.hDiv, Complex.re, HAdd.hAdd, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
w ρ : ℂ
R r₀ r : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hw : ‖w‖ < r₀
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
hdR : 0 < ‖circleMap 0 R θ - ρ‖
hrw : 0 < r₀ - ‖w‖
hr : 0 < r
h_norm_sub₁ : √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
h_norm_sub₂ : 0 < ‖circleMap 0 r θ - ρ‖
apply : -(|log (2 * R)| + |log √(r₀ / R)| + |log ‖circleMap 0 R θ - ρ‖|) ≤ log ‖circleMap 0 r θ - ρ‖
apply₁ : log ‖circleMap 0 r θ - ρ‖ ≤ |log (2 * R)| + |log √(r₀ / R)| + |log ‖circleMap 0 R θ - ρ‖|
⊢ |log ‖circleMap 0 r θ - ρ‖| ≤ |log (2 * R)| + |log √(r₀ / R)| + |log ‖circleMap 0 R θ - ρ‖|

Tactic:
apply abs_le.mpr ⟨_, _⟩

Premises used: Iff.mpr, abs_le, And.intro
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
w ρ : ℂ
R r₀ r : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hw : ‖w‖ < r₀
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
hdR : 0 < ‖circleMap 0 R θ - ρ‖
hrw : 0 < r₀ - ‖w‖
hr : 0 < r
h_norm_sub₁ : √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
h_norm_sub₂ : 0 < ‖circleMap 0 r θ - ρ‖
⊢ √(r₀ / R) ≠ 0

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
w ρ : ℂ
R r₀ r : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hw : ‖w‖ < r₀
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
hdR : 0 < ‖circleMap 0 R θ - ρ‖
hrw : 0 < r₀ - ‖w‖
hr : 0 < r
h_norm_sub₁ : √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
h_norm_sub₂ : 0 < ‖circleMap 0 r θ - ρ‖
⊢ ‖circleMap 0 R θ - ρ‖ ≠ 0

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
w ρ : ℂ
R r₀ r : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hw : ‖w‖ < r₀
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
hdR : 0 < ‖circleMap 0 R θ - ρ‖
hrw : 0 < r₀ - ‖w‖
hr : 0 < r
h_norm_sub₁ : √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
h_norm_sub₂ : 0 < ‖circleMap 0 r θ - ρ‖
rw : log ‖circleMap 0 r θ - ρ‖ ≥ log (√(r₀ / R) * ‖circleMap 0 R θ - ρ‖)
⊢ log ‖circleMap 0 r θ - ρ‖ ≥ log √(r₀ / R) + log ‖circleMap 0 R θ - ρ‖

Tactic:
rw [← log_mul (by positivity) (by positivity)]

Premises used: Real.log_mul
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
w ρ : ℂ
R r₀ r : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hw : ‖w‖ < r₀
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
hdR : 0 < ‖circleMap 0 R θ - ρ‖
hrw : 0 < r₀ - ‖w‖
hr : 0 < r
h_norm_sub₁ : √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
h_norm_sub₂ : 0 < ‖circleMap 0 r θ - ρ‖
hx : 0 < √(r₀ / R) * ‖circleMap 0 R θ - ρ‖
⊢ log ‖circleMap 0 r θ - ρ‖ ≥ log (√(r₀ / R) * ‖circleMap 0 R θ - ρ‖)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
w ρ : ℂ
R r₀ r : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hw : ‖w‖ < r₀
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
hdR : 0 < ‖circleMap 0 R θ - ρ‖
hrw : 0 < r₀ - ‖w‖
hr : 0 < r
h_norm_sub₁ : √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
h_norm_sub₂ : 0 < ‖circleMap 0 r θ - ρ‖
⊢ log ‖circleMap 0 r θ - ρ‖ ≥ log √(r₀ / R) + log ‖circleMap 0 R θ - ρ‖

Tactic:
have h_log_lower_bound :
          log ‖circleMap 0 r θ - ρ‖ ≥ log (sqrt (r₀ / R)) + log ‖circleMap 0 R θ - ρ‖ := by
        rw [← log_mul (by positivity) (by positivity)]
        gcongr
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
w ρ : ℂ
R r₀ r : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hw : ‖w‖ < r₀
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
hdR : 0 < ‖circleMap 0 R θ - ρ‖
hrw : 0 < r₀ - ‖w‖
hr : 0 < r
h_norm_sub₁ : √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
h_norm_sub₂ : 0 < ‖circleMap 0 r θ - ρ‖
h_log_lower_bound : log ‖circleMap 0 r θ - ρ‖ ≥ log √(r₀ / R) + log ‖circleMap 0 R θ - ρ‖
⊢ -(|log (2 * R)| + |log √(r₀ / R)| + |log ‖circleMap 0 R θ - ρ‖|) ≤ log ‖circleMap 0 r θ - ρ‖

Tactic:
grind
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
w ρ : ℂ
R r₀ r : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hw : ‖w‖ < r₀
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
hdR : 0 < ‖circleMap 0 R θ - ρ‖
hrw : 0 < r₀ - ‖w‖
hr : 0 < r
h_norm_sub₁ : √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
h_norm_sub₂ : 0 < ‖circleMap 0 r θ - ρ‖
grw : log (R + R) ≤ log (R + R) + 0 + 0
⊢ log ‖circleMap 0 r θ - ρ‖ ≤ |log (2 * R)| + 0 + 0

Tactic:
grw [← le_abs_self, norm_sub_le, hρ, two_mul, norm_circleMap_zero, abs_of_pos hr, hrR]

Premises used: le_abs_self, norm_sub_le, norm_circleMap_zero, two_mul, abs_of_pos
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
w ρ : ℂ
R r₀ r : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hw : ‖w‖ < r₀
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
hdR : 0 < ‖circleMap 0 R θ - ρ‖
hrw : 0 < r₀ - ‖w‖
hr : 0 < r
h_norm_sub₁ : √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
h_norm_sub₂ : 0 < ‖circleMap 0 r θ - ρ‖
⊢ log (R + R) ≤ log (R + R) + 0 + 0

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
w ρ : ℂ
R r₀ r : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hw : ‖w‖ < r₀
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
hdR : 0 < ‖circleMap 0 R θ - ρ‖
hrw : 0 < r₀ - ‖w‖
hr : 0 < r
h_norm_sub₁ : √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
h_norm_sub₂ : 0 < ‖circleMap 0 r θ - ρ‖
h₁ : 0 ≤ |log √(r₀ / R)|
h₂ : 0 ≤ |log ‖circleMap 0 R θ - ρ‖|
⊢ |log (2 * R)| + 0 + 0 ≤ |log (2 * R)| + |log √(r₀ / R)| + |log ‖circleMap 0 R θ - ρ‖|

Tactic:
gcongr
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
w ρ : ℂ
R r₀ r : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hw : ‖w‖ < r₀
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
hdR : 0 < ‖circleMap 0 R θ - ρ‖
hrw : 0 < r₀ - ‖w‖
hr : 0 < r
h_norm_sub₁ : √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
h_norm_sub₂ : 0 < ‖circleMap 0 r θ - ρ‖
⊢ 0 ≤ |log √(r₀ / R)|

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
w ρ : ℂ
R r₀ r : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hw : ‖w‖ < r₀
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
hdR : 0 < ‖circleMap 0 R θ - ρ‖
hrw : 0 < r₀ - ‖w‖
hr : 0 < r
h_norm_sub₁ : √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
h_norm_sub₂ : 0 < ‖circleMap 0 r θ - ρ‖
⊢ 0 ≤ |log ‖circleMap 0 R θ - ρ‖|

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
w ρ : ℂ
R r₀ r : ℝ
hR : 0 < R
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hw : ‖w‖ < r₀
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
hdR : 0 < ‖circleMap 0 R θ - ρ‖
hrw : 0 < r₀ - ‖w‖
hr : 0 < r
h_norm_sub₁ : √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
h_norm_sub₂ : 0 < ‖circleMap 0 r θ - ρ‖
calc : log ‖circleMap 0 r θ - ρ‖ ≤ |log (2 * R)| + 0 + 0
calc₁ : |log (2 * R)| + 0 + 0 ≤ |log (2 * R)| + |log √(r₀ / R)| + |log ‖circleMap 0 R θ - ρ‖|
⊢ log ‖circleMap 0 r θ - ρ‖ ≤ |log (2 * R)| + |log √(r₀ / R)| + |log ‖circleMap 0 R θ - ρ‖|

Tactic:
calc log ‖circleMap 0 r θ - ρ‖
      _ ≤ |log (2 * R)| + 0 + 0 := by
        grw [← le_abs_self, norm_sub_le, hρ, two_mul, norm_circleMap_zero, abs_of_pos hr, hrR]
        simp
      _ ≤ |log (2 * R)| + |log √(r₀ / R)| + |log ‖circleMap 0 R θ - ρ‖| := by
        gcongr <;> positivity

Premises used: Norm.norm, HMul.hMul, HSub.hSub, circleMap, HDiv.hDiv, Real.log, Real.sqrt, OfNat.ofNat
-- Module: Mathlib.Analysis.Complex.JensenFormula
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 θ - ρ‖|)
apply :
  Tendsto (β := ℝ) (fun (x : ℕ) ↦ ∫ (θ : ℝ) in 0..2 * π, herglotzLogIntegrand w ρ (circleMap 0 (r x) θ)) atTop
    (𝓝 (∫ (θ : ℝ) in 0..2 * π, herglotzLogIntegrand w ρ (circleMap 0 R θ)))
⊢ Tendsto (fun (n : ℕ) ↦ circleAverage (herglotzLogIntegrand w ρ) 0 (r n)) atTop
    (𝓝 (circleAverage (herglotzLogIntegrand w ρ) 0 R))

Tactic:
apply Filter.Tendsto.smul tendsto_const_nhds _

Premises used: tendsto_const_nhds, Filter.Tendsto.smul
-- Module: Mathlib.Analysis.Complex.JensenFormula
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 θ - ρ‖|)
hF_meas :
  ∀ᶠ (n : ℕ) in atTop,
    AEStronglyMeasurable (β := ℝ) (m₀ := measurableSpace) (fun (x : ℝ) ↦ herglotzLogIntegrand w ρ (circleMap 0 (r n) x))
      (Measure.restrict volume (uIoc 0 (2 * π)))
h_bound :
  ∀ᶠ (n : ℕ) in atTop, ∀ᵐ (x : ℝ), x ∈ uIoc 0 (2 * π) → ‖herglotzLogIntegrand w ρ (circleMap 0 (r n) x)‖ ≤ bound x
bound_integrable : IntervalIntegrable bound volume 0 (2 * π)
h_lim :
  ∀ᵐ (x : ℝ),
    x ∈ uIoc 0 (2 * π) →
      Tendsto (fun (n : ℕ) ↦ herglotzLogIntegrand w ρ (circleMap 0 (r n) x)) atTop
        (𝓝 (herglotzLogIntegrand w ρ (circleMap 0 R x)))
⊢ Tendsto (β := ℝ) (fun (x : ℕ) ↦ ∫ (θ : ℝ) in 0..2 * π, herglotzLogIntegrand w ρ (circleMap 0 (r x) θ)) atTop
    (𝓝 (∫ (θ : ℝ) in 0..2 * π, herglotzLogIntegrand w ρ (circleMap 0 R θ)))

Tactic:
apply intervalIntegral.tendsto_integral_filter_of_dominated_convergence bound

Premises used: intervalIntegral.tendsto_integral_filter_of_dominated_convergence
-- Module: Mathlib.Analysis.Complex.JensenFormula
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 :
  ∀ (n : ℕ) (hn : ‖w‖ < r n),
    AEStronglyMeasurable (β := ℝ) (m₀ := measurableSpace) (fun (x : ℝ) ↦ herglotzLogIntegrand w ρ (circleMap 0 (r n) x))
      (Measure.restrict volume (uIoc 0 (2 * π)))
⊢ ∀ᶠ (n : ℕ) in atTop,
    AEStronglyMeasurable (β := ℝ) (m₀ := measurableSpace) (fun (x : ℝ) ↦ herglotzLogIntegrand w ρ (circleMap 0 (r n) x))
      (Measure.restrict volume (uIoc 0 (2 * π)))

Tactic:
filter_upwards [hr_tendsto.eventually (lt_mem_nhds hw)] with n hn

Premises used: Filter.Tendsto.eventually, lt_mem_nhds
-- Module: Mathlib.Analysis.Complex.JensenFormula
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 : ‖w‖ < r n
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := measurableSpace) (fun (x : ℝ) ↦ herglotzLogIntegrand w ρ (circleMap 0 (r n) x))
    (Measure.restrict volume (uIoc 0 (2 * π)))

Tactic:
continuous_herglotzLogIntegrand_circle hρ (hr_lt n) hn |>.aestronglyMeasurable

Premises used: _private.0.continuous_herglotzLogIntegrand_circle, Continuous.aestronglyMeasurable
-- Module: Mathlib.Analysis.Complex.JensenFormula
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 : ‖w‖ < r n
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := measurableSpace) (fun (x : ℝ) ↦ herglotzLogIntegrand w ρ (circleMap 0 (r n) x))
    (Measure.restrict volume (uIoc 0 (2 * π)))

Tactic:
exact continuous_herglotzLogIntegrand_circle hρ (hr_lt n) hn |>.aestronglyMeasurable

Premises used: _private.0.continuous_herglotzLogIntegrand_circle, Continuous.aestronglyMeasurable
-- Module: Mathlib.Analysis.Complex.JensenFormula
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 θ - ρ‖|)
linarith : R ≤ (R + ‖w‖) / 2 → 2 / 2 = 1
linarith₁ : R ≤ (R + ‖w‖) / 2 → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : R ≤ (R + ‖w‖) / 2 → GT.gt (α := ℝ) 2 0
linarith₃ : R ≤ (R + ‖w‖) / 2 → ‖w‖ - R + (2 * R - (1 * R + 1 * ‖w‖)) = 0
⊢ (R + ‖w‖) / 2 < R

Tactic:
linarith
-- Module: Mathlib.Analysis.Complex.JensenFormula
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 :
  ∀ (n : ℕ) (hn : (R + ‖w‖) / 2 ≤ r n),
    ∀ᵐ (x : ℝ), x ∈ uIoc 0 (2 * π) → ‖herglotzLogIntegrand w ρ (circleMap 0 (r n) x)‖ ≤ bound x
⊢ ∀ᶠ (n : ℕ) in atTop, ∀ᵐ (x : ℝ), x ∈ uIoc 0 (2 * π) → ‖herglotzLogIntegrand w ρ (circleMap 0 (r n) x)‖ ≤ bound x

Tactic:
filter_upwards [hr_tendsto.eventually (le_mem_nhds (by linarith : (R + ‖w‖) / 2 < R))] with n hn

Premises used: le_mem_nhds, Filter.Tendsto.eventually
-- Module: Mathlib.Analysis.Complex.JensenFormula
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
θ : ℝ
⊢ ‖herglotzLogIntegrand w ρ (circleMap 0 (r n) θ)‖ ≤ bound θ ∨ ‖circleMap 0 R θ - ρ‖ = 0

Tactic:
Classical.or_iff_not_imp_right.mpr fun h ↦ ?_

Premises used: Iff.mpr, Classical.or_iff_not_imp_right
-- Module: Mathlib.Analysis.Complex.JensenFormula
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
θ : ℝ
refine : ∀ (h : ¬‖circleMap 0 R θ - ρ‖ = 0), ‖herglotzLogIntegrand w ρ (circleMap 0 (r n) θ)‖ ≤ bound θ
⊢ ‖herglotzLogIntegrand w ρ (circleMap 0 (r n) θ)‖ ≤ bound θ ∨ ‖circleMap 0 R θ - ρ‖ = 0

Tactic:
refine Classical.or_iff_not_imp_right.mpr fun h ↦ ?_

Premises used: Iff.mpr, Classical.or_iff_not_imp_right
-- Module: Mathlib.Analysis.Complex.JensenFormula
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 : ¬‖circleMap 0 R θ - ρ‖ = 0
⊢ 0 < (R + ‖w‖) / 2

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.JensenFormula
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 : ¬‖circleMap 0 R θ - ρ‖ = 0
linarith : (R + ‖w‖) / 2 ≤ ‖w‖ → 2 / 2 = 1
linarith₁ : (R + ‖w‖) / 2 ≤ ‖w‖ → HMul.hMul (α := ℝ) 1 2 = 2
linarith₂ : (R + ‖w‖) / 2 ≤ ‖w‖ → GT.gt (α := ℝ) 2 0
linarith₃ : (R + ‖w‖) / 2 ≤ ‖w‖ → 2 / 2 = 1
linarith₄ : (R + ‖w‖) / 2 ≤ ‖w‖ → HMul.hMul (α := ℝ) 1 2 = 2
linarith₅ : (R + ‖w‖) / 2 ≤ ‖w‖ → GT.gt (α := ℝ) 2 0
linarith₆ : (R + ‖w‖) / 2 ≤ ‖w‖ → ‖w‖ - R + (1 * R + 1 * ‖w‖ - 2 * ‖w‖) = 0
⊢ ‖w‖ < (R + ‖w‖) / 2

Tactic:
linarith
-- Module: Mathlib.Analysis.Complex.JensenFormula
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 : ¬‖circleMap 0 R θ - ρ‖ = 0
hdR : 0 < ‖circleMap 0 R θ - ρ‖
⊢ ‖herglotzLogIntegrand w ρ (circleMap 0 (r n) θ)‖ ≤ bound θ

Tactic:
apply norm_herglotzLogIntegrand_circleMap_le hR hρ (by positivity) (by linarith) hn
        (hr_lt n).le

Premises used: LT.lt.le, _private.0.norm_herglotzLogIntegrand_circleMap_le
-- Module: Mathlib.Analysis.Complex.JensenFormula
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 : ¬‖circleMap 0 R θ - ρ‖ = 0
⊢ 0 < ‖circleMap 0 R θ - ρ‖

Tactic:
simpa using h
-- Module: Mathlib.Analysis.Complex.JensenFormula
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
⊢ ∀ {θ : ℝ}, ‖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