awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
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 θ + w‖ / ‖circleMap 0 r θ - w‖ ≤ (r + ‖w‖) / (r - ‖w‖)
have grw : (‖circleMap 0 r θ‖ + ‖w‖) / (‖circleMap 0 r θ‖ - ‖w‖) ≤ (r + ‖w‖) / (r - ‖w‖)
Tactic: grw [norm_add_le, ← norm_sub_norm_le]
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
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‖)
⊢ ‖circleMap 0 r θ + w‖ / ‖circleMap 0 r θ - w‖ ≤ (r + ‖w‖) / (r - ‖w‖)
have h₁ : 0 < ‖circleMap 0 r θ‖ - ‖w‖
Tactic: grw [norm_add_le, ← norm_sub_norm_le]
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
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 θ‖ + ‖w‖) / (‖circleMap 0 r θ‖ - ‖w‖) ≤ (r + ‖w‖) / (r - ‖w‖)
have simp : (r + ‖w‖) / (r - ‖w‖) ≤ (r + ‖w‖) / (r - ‖w‖)
Tactic: simp only [norm_circleMap_zero, abs_of_pos hr]
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
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 < ‖circleMap 0 r θ‖ - ‖w‖
have h₁ : 0 < r - ‖w‖
Tactic: simp only [norm_circleMap_zero, abs_of_pos hr]
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
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‖)
have hc : 0 ≤ R + ‖w‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
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 θ + w) / (circleMap 0 r θ - w)).re| ≤ (R + ‖w‖) / (r₀ - ‖w‖)
have r₁ : |((circleMap 0 r θ + w) / (circleMap 0 r θ - w)).re| ≤ ‖circleMap 0 r θ + w‖ / ‖circleMap 0 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
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
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‖
⊢ |((circleMap 0 r θ + w) / (circleMap 0 r θ - w)).re| ≤ (R + ‖w‖) / (r₀ - ‖w‖)
have r₂ : ‖circleMap 0 r θ + w‖ / ‖circleMap 0 r θ - w‖ ≤ (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
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
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‖)
⊢ |((circleMap 0 r θ + w) / (circleMap 0 r θ - w)).re| ≤ (R + ‖w‖) / (r₀ - ‖w‖)
have r₃ : (r + ‖w‖) / (r - ‖w‖) ≤ (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
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
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 (2 * R)| + |log √(r₀ / R)| + |log ‖circleMap 0 R θ - ρ‖|
have apply : -(|log (2 * R)| + |log √(r₀ / R)| + |log ‖circleMap 0 R θ - ρ‖|) ≤ log ‖circleMap 0 r θ - ρ‖
Tactic: apply abs_le.mpr ⟨_, _⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
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 θ - ρ‖
⊢ |log ‖circleMap 0 r θ - ρ‖| ≤ |log (2 * R)| + |log √(r₀ / R)| + |log ‖circleMap 0 R θ - ρ‖|
have apply₁ : log ‖circleMap 0 r θ - ρ‖ ≤ |log (2 * R)| + |log √(r₀ / R)| + |log ‖circleMap 0 R θ - ρ‖|
Tactic: apply abs_le.mpr ⟨_, _⟩
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
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 θ - ρ‖
have rw : log ‖circleMap 0 r θ - ρ‖ ≥ log (√(r₀ / R) * ‖circleMap 0 R θ - ρ‖)
Tactic: rw [← log_mul (by positivity) (by positivity)]
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
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) * ‖circleMap 0 R θ - ρ‖)
have hx : 0 < √(r₀ / R) * ‖circleMap 0 R θ - ρ‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (hypothesis)
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 (2 * R)| + |log √(r₀ / R)| + |log ‖circleMap 0 R θ - ρ‖|) ≤ log ‖circleMap 0 r θ - ρ‖
have h_log_lower_bound : 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
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
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 (2 * R)| + 0 + 0
have grw : log (R + R) ≤ log (R + R) + 0 + 0
Tactic: grw [← le_abs_self, norm_sub_le, hρ, two_mul, norm_circleMap_zero, abs_of_pos hr, hrR]
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
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 (2 * R)| + 0 + 0 ≤ |log (2 * R)| + |log √(r₀ / R)| + |log ‖circleMap 0 R θ - ρ‖|
have h₁ : 0 ≤ |log √(r₀ / R)|
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
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)|
⊢ |log (2 * R)| + 0 + 0 ≤ |log (2 * R)| + |log √(r₀ / R)| + |log ‖circleMap 0 R θ - ρ‖|
have h₂ : 0 ≤ |log ‖circleMap 0 R θ - ρ‖|
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
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 (2 * R)| + |log √(r₀ / R)| + |log ‖circleMap 0 R θ - ρ‖|
have calc : log ‖circleMap 0 r θ - ρ‖ ≤ |log (2 * R)| + 0 + 0
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
-- Lean 4 proof step from Mathlib.Analysis.Complex.JensenFormula (goal)
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
⊢ log ‖circleMap 0 r θ - ρ‖ ≤ |log (2 * R)| + |log √(r₀ / R)| + |log ‖circleMap 0 R θ - ρ‖|
have calc₁ : |log (2 * R)| + 0 + 0 ≤ |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
-- 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 θ - ρ‖|)
⊢ Tendsto (fun (n : ℕ) ↦ circleAverage (herglotzLogIntegrand w ρ) 0 (r n)) atTop
    (𝓝 (circleAverage (herglotzLogIntegrand w ρ) 0 R))
have apply : Tendsto (β := ℝ) (fun (x : ℕ) ↦ ∫ (θ : ℝ) in 0..2 * π, herglotzLogIntegrand w ρ (circleMap 0 (r x) θ)) atTop
  (𝓝 (∫ (θ : ℝ) in 0..2 * π, herglotzLogIntegrand w ρ (circleMap 0 R θ)))
Tactic: apply Filter.Tendsto.smul tendsto_const_nhds _
-- 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 θ - ρ‖|)
⊢ Tendsto (β := ℝ) (fun (x : ℕ) ↦ ∫ (θ : ℝ) in 0..2 * π, herglotzLogIntegrand w ρ (circleMap 0 (r x) θ)) atTop
    (𝓝 (∫ (θ : ℝ) in 0..2 * π, herglotzLogIntegrand w ρ (circleMap 0 R θ)))
have hF_meas : ∀ᶠ (n : ℕ) in atTop,
  AEStronglyMeasurable (β := ℝ) (m₀ := measurableSpace) (fun (x : ℝ) ↦ herglotzLogIntegrand w ρ (circleMap 0 (r n) x))
    (Measure.restrict volume (uIoc 0 (2 * π)))
Tactic: apply intervalIntegral.tendsto_integral_filter_of_dominated_convergence bound
-- 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 θ - ρ‖|)
hF_meas :
  ∀ᶠ (n : ℕ) in atTop,
    AEStronglyMeasurable (β := ℝ) (m₀ := measurableSpace) (fun (x : ℝ) ↦ herglotzLogIntegrand w ρ (circleMap 0 (r n) x))
      (Measure.restrict volume (uIoc 0 (2 * π)))
⊢ Tendsto (β := ℝ) (fun (x : ℕ) ↦ ∫ (θ : ℝ) in 0..2 * π, herglotzLogIntegrand w ρ (circleMap 0 (r x) θ)) atTop
    (𝓝 (∫ (θ : ℝ) in 0..2 * π, herglotzLogIntegrand w ρ (circleMap 0 R θ)))
have h_bound : ∀ᶠ (n : ℕ) in atTop, ∀ᵐ (x : ℝ), x ∈ uIoc 0 (2 * π) → ‖herglotzLogIntegrand w ρ (circleMap 0 (r n) x)‖ ≤ bound x
Tactic: apply intervalIntegral.tendsto_integral_filter_of_dominated_convergence bound
-- 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 θ - ρ‖|)
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
⊢ Tendsto (β := ℝ) (fun (x : ℕ) ↦ ∫ (θ : ℝ) in 0..2 * π, herglotzLogIntegrand w ρ (circleMap 0 (r x) θ)) atTop
    (𝓝 (∫ (θ : ℝ) in 0..2 * π, herglotzLogIntegrand w ρ (circleMap 0 R θ)))
have bound_integrable : IntervalIntegrable bound volume 0 (2 * π)
Tactic: apply intervalIntegral.tendsto_integral_filter_of_dominated_convergence bound
-- 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 θ - ρ‖|)
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 * π)
⊢ Tendsto (β := ℝ) (fun (x : ℕ) ↦ ∫ (θ : ℝ) in 0..2 * π, herglotzLogIntegrand w ρ (circleMap 0 (r x) θ)) atTop
    (𝓝 (∫ (θ : ℝ) in 0..2 * π, herglotzLogIntegrand w ρ (circleMap 0 R θ)))
have h_lim : ∀ᵐ (x : ℝ),
  x ∈ uIoc 0 (2 * π) →
    Tendsto (fun (n : ℕ) ↦ herglotzLogIntegrand w ρ (circleMap 0 (r n) x)) atTop
      (𝓝 (herglotzLogIntegrand w ρ (circleMap 0 R x)))
Tactic: apply intervalIntegral.tendsto_integral_filter_of_dominated_convergence bound
-- 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 : ℕ) in atTop,
    AEStronglyMeasurable (β := ℝ) (m₀ := measurableSpace) (fun (x : ℝ) ↦ herglotzLogIntegrand w ρ (circleMap 0 (r n) x))
      (Measure.restrict volume (uIoc 0 (2 * π)))
have h : ∀ (n : ℕ) (hn : ‖w‖ < r n),
  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
-- 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 θ - ρ‖|)
⊢ (R + ‖w‖) / 2 < R
have linarith : R ≤ (R + ‖w‖) / 2 → 2 / 2 = 1
Tactic: linarith
-- 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 θ - ρ‖|)
linarith : R ≤ (R + ‖w‖) / 2 → 2 / 2 = 1
⊢ (R + ‖w‖) / 2 < R
have linarith₁ : R ≤ (R + ‖w‖) / 2 → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- 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 θ - ρ‖|)
linarith : R ≤ (R + ‖w‖) / 2 → 2 / 2 = 1
linarith₁ : R ≤ (R + ‖w‖) / 2 → HMul.hMul (α := ℝ) 1 2 = 2
⊢ (R + ‖w‖) / 2 < R
have linarith₂ : R ≤ (R + ‖w‖) / 2 → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- 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 θ - ρ‖|)
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
⊢ (R + ‖w‖) / 2 < R
have linarith₃ : R ≤ (R + ‖w‖) / 2 → ‖w‖ - R + (2 * R - (1 * R + 1 * ‖w‖)) = 0
Tactic: linarith
-- 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 : ℕ) in atTop, ∀ᵐ (x : ℝ), x ∈ uIoc 0 (2 * π) → ‖herglotzLogIntegrand w ρ (circleMap 0 (r n) x)‖ ≤ bound x
have h : ∀ (n : ℕ) (hn : (R + ‖w‖) / 2 ≤ r n),
  ∀ᵐ (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
-- 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
θ : ℝ
⊢ ‖herglotzLogIntegrand w ρ (circleMap 0 (r n) θ)‖ ≤ bound θ ∨ ‖circleMap 0 R θ - ρ‖ = 0
have refine : ∀ (h : ¬‖circleMap 0 R θ - ρ‖ = 0), ‖herglotzLogIntegrand w ρ (circleMap 0 (r n) θ)‖ ≤ bound θ
Tactic: refine Classical.or_iff_not_imp_right.mpr fun 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 : ¬‖circleMap 0 R θ - ρ‖ = 0
⊢ ‖w‖ < (R + ‖w‖) / 2
have linarith : (R + ‖w‖) / 2 ≤ ‖w‖ → 2 / 2 = 1
Tactic: linarith
-- 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 : ¬‖circleMap 0 R θ - ρ‖ = 0
linarith : (R + ‖w‖) / 2 ≤ ‖w‖ → 2 / 2 = 1
⊢ ‖w‖ < (R + ‖w‖) / 2
have linarith₁ : (R + ‖w‖) / 2 ≤ ‖w‖ → HMul.hMul (α := ℝ) 1 2 = 2
Tactic: linarith
-- 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 : ¬‖circleMap 0 R θ - ρ‖ = 0
linarith : (R + ‖w‖) / 2 ≤ ‖w‖ → 2 / 2 = 1
linarith₁ : (R + ‖w‖) / 2 ≤ ‖w‖ → HMul.hMul (α := ℝ) 1 2 = 2
⊢ ‖w‖ < (R + ‖w‖) / 2
have linarith₂ : (R + ‖w‖) / 2 ≤ ‖w‖ → GT.gt (α := ℝ) 2 0
Tactic: linarith
-- 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 : ¬‖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
⊢ ‖w‖ < (R + ‖w‖) / 2
have linarith₆ : (R + ‖w‖) / 2 ≤ ‖w‖ → ‖w‖ - R + (1 * R + 1 * ‖w‖ - 2 * ‖w‖) = 0
Tactic: linarith
-- 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 : ¬‖circleMap 0 R θ - ρ‖ = 0
⊢ ‖herglotzLogIntegrand w ρ (circleMap 0 (r n) θ)‖ ≤ bound θ
have hdR : 0 < ‖circleMap 0 R θ - ρ‖
Tactic: apply norm_herglotzLogIntegrand_circleMap_le hR hρ (by positivity) (by linarith) hn
        (hr_lt n).le