awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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_bound : ∀ {θ : ℝ}, ‖herglotzLogIntegrand w ρ (circleMap 0 (r n) θ)‖ ≤ bound θ ∨ ‖circleMap 0 R θ - ρ‖ = 0
⊢ Subset (α := Set ℝ)
    {x : ℝ | (fun (x : ℝ) ↦ x ∈ uIoc 0 (2 * π) → ‖herglotzLogIntegrand w ρ (circleMap 0 (r n) x)‖ ≤ bound x) x}ᶜ
    {θ : ℝ | ‖circleMap 0 R θ - ρ‖ = 0}

Tactic:
grind
-- 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_bound : ∀ {θ : ℝ}, ‖herglotzLogIntegrand w ρ (circleMap 0 (r n) θ)‖ ≤ bound θ ∨ ‖circleMap 0 R θ - ρ‖ = 0
h : Eq (α := ENNReal) ((volume : (a : Set ℝ) → ENNReal) {θ : ℝ | ‖circleMap 0 R θ - ρ‖ = 0} : ENNReal) (0 : ENNReal)
⊢ ∀ᵐ (x : ℝ), x ∈ uIoc 0 (2 * π) → ‖herglotzLogIntegrand w ρ (circleMap 0 (r n) x)‖ ≤ bound x

Tactic:
apply measure_mono_null (t := {θ | ‖circleMap 0 R θ - ρ‖ = 0}) (by grind)

Premises used: MeasureTheory.measure_mono_null
-- 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_bound : ∀ {θ : ℝ}, ‖herglotzLogIntegrand w ρ (circleMap 0 (r n) θ)‖ ≤ bound θ ∨ ‖circleMap 0 R θ - ρ‖ = 0
⊢ Eq (α := ENNReal) ((volume : (a : Set ℝ) → ENNReal) {θ : ℝ | ‖circleMap 0 R θ - ρ‖ = 0} : ENNReal) (0 : ENNReal)

Tactic:
simpa [sub_eq_zero] using
      (countable_singleton ρ).preimage_circleMap 0 (hR.ne') |>.measure_zero _

Premises used: sub_eq_zero, Set.Countable.measure_zero, LT.lt.ne', Set.Countable.preimage_circleMap, Set.countable_singleton, 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 θ - ρ‖|)
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ |log (2 * R)|) volume 0 (2 * π)

Tactic:
simp
-- 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 θ - ρ‖|)
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ |log √((R + ‖w‖) / 2 / R)|) volume 0 (2 * π)

Tactic:
simp
-- 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 : IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ |log ‖circleMap 0 R x - ρ‖|) volume 0 (2 * π)
⊢ IntervalIntegrable bound volume 0 (2 * π)

Tactic:
apply (IntervalIntegrable.add (by simp) (by simp)).add ?_ |>.const_mul

Premises used: IntervalIntegrable.add, IntervalIntegrable.const_mul
-- 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 θ - ρ‖|)
x : ℂ
⊢ Membership.mem (γ := Set ℂ) (sphere 0 |R|) x → MeromorphicAt (E := ℂ) (fun (z : ℂ) ↦ z - ρ) x

Tactic:
fun_prop
-- 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 θ - ρ‖|)
⊢ IntervalIntegrable (ε := ℝ) (fun (x : ℝ) ↦ |log ‖circleMap 0 R x - ρ‖|) volume 0 (2 * π)

Tactic:
exact .abs <| MeromorphicOn.circleIntegrable_log_norm (f := fun z ↦ z - ρ) (by intro; fun_prop)

Premises used: MeromorphicOn.circleIntegrable_log_norm
-- 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 θ - ρ‖|)
⊢ 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 _
-- 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_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 θ)))
⊢ θ ∈ uIoc 0 (2 * π) →
    Tendsto (fun (n : ℕ) ↦ herglotzLogIntegrand w ρ (circleMap 0 (r n) θ)) atTop
      (𝓝 (herglotzLogIntegrand w ρ (circleMap 0 R θ)))

Tactic:
_
-- 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_measure_zero :
  Eq (α := ENNReal) ((volume : (a : Set ℝ) → ENNReal) {θ : ℝ | circleMap 0 R θ = w ∨ circleMap 0 R θ = ρ} : ENNReal)
    (0 : ENNReal)
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 θ)))
⊢ ∀ᵐ (x : ℝ),
    x ∈ uIoc 0 (2 * π) →
      Tendsto (fun (n : ℕ) ↦ herglotzLogIntegrand w ρ (circleMap 0 (r n) x)) atTop
        (𝓝 (herglotzLogIntegrand w ρ (circleMap 0 R x)))

Tactic:
filter_upwards [measure_eq_zero_iff_ae_notMem.mp h_measure_zero] with θ hθ _

Premises used: Iff.mp, MeasureTheory.measure_eq_zero_iff_ae_notMem
-- 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_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 * π)
tauto : θ ∈ uIoc 0 (2 * π) → circleMap 0 R θ = w → ¬circleMap 0 R θ = w → ¬circleMap 0 R θ = ρ → False
⊢ circleMap 0 R θ ≠ w

Tactic:
tauto
-- 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_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 * π)
tauto : θ ∈ uIoc 0 (2 * π) → circleMap 0 R θ = ρ → ¬circleMap 0 R θ = w → ¬circleMap 0 R θ = ρ → False
⊢ circleMap 0 R θ ≠ ρ

Tactic:
tauto
-- 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_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_1 : θ ∈ uIoc 0 (2 * π)
h : Tendsto (fun (n : ℕ) ↦ circleMap 0 (r n) θ) atTop (𝓝 (circleMap 0 R θ))
⊢ Tendsto (fun (n : ℕ) ↦ herglotzLogIntegrand w ρ (circleMap 0 (r n) θ)) atTop
    (𝓝 (herglotzLogIntegrand w ρ (circleMap 0 R θ)))

Tactic:
apply (continuousAt_herglotzLogIntegrand (by tauto) (by tauto)).tendsto.comp

Premises used: ContinuousAt.tendsto, _private.0.continuousAt_herglotzLogIntegrand, Filter.Tendsto.comp
-- 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_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 : ℕ) ↦ circleMap 0 (r n) θ) atTop (𝓝 (circleMap 0 R θ))

Tactic:
tendsto_const_nhds.add <|
      (Complex.continuous_ofReal.continuousAt.tendsto.comp hr_tendsto).mul tendsto_const_nhds

Premises used: tendsto_const_nhds, circleMap, Continuous.continuousAt, Filter.Tendsto.mul, ContinuousAt.tendsto, Complex.continuous_ofReal, Filter.Tendsto.add, Filter.Tendsto.comp
-- 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_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 : ℕ) ↦ circleMap 0 (r n) θ) atTop (𝓝 (circleMap 0 R θ))

Tactic:
exact tendsto_const_nhds.add <|
      (Complex.continuous_ofReal.continuousAt.tendsto.comp hr_tendsto).mul tendsto_const_nhds

Premises used: tendsto_const_nhds, Continuous.continuousAt, Filter.Tendsto.mul, ContinuousAt.tendsto, Complex.continuous_ofReal, Filter.Tendsto.add, Filter.Tendsto.comp
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
w ρ : ℂ
R : ℝ
hρ : Membership.mem (γ := Set ℂ) (sphere 0 R) ρ
hw : Membership.mem (γ := Set ℂ) (ball 0 R) w
⊢ 0 < R

Tactic:
have hR : 0 < R := pos_of_mem_ball hw
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
w ρ : ℂ
R : ℝ
hρ : Membership.mem (γ := Set ℂ) (sphere 0 R) ρ
hw : Membership.mem (γ := Set ℂ) (ball 0 R) w
hR : 0 < R
⊢ ‖ρ‖ = R

Tactic:
rw [mem_sphere_iff_norm, sub_zero] at hρ

Premises used: sub_zero, mem_sphere_iff_norm
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
w ρ : ℂ
R : ℝ
hρ : Membership.mem (γ := Set ℂ) (sphere 0 R) ρ
hw : Membership.mem (γ := Set ℂ) (ball 0 R) w
hR : 0 < R
hρ₁ : ‖ρ‖ = R
⊢ Membership.mem (γ := Set ℂ) (ball 0 R) w

Tactic:
rw [mem_sphere_iff_norm, sub_zero] at hρ

Premises used: sub_zero, mem_sphere_iff_norm
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
w ρ : ℂ
R : ℝ
hρ : Membership.mem (γ := Set ℂ) (sphere 0 R) ρ
hw : Membership.mem (γ := Set ℂ) (ball 0 R) w
hR : 0 < R
hρ₁ : ‖ρ‖ = R
hw₁ : Membership.mem (γ := Set ℂ) (ball 0 R) w
⊢ 0 < R

Tactic:
rw [mem_sphere_iff_norm, sub_zero] at hρ

Premises used: sub_zero, mem_sphere_iff_norm
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
w ρ : ℂ
R : ℝ
hρ : ‖ρ‖ = R
hw : Membership.mem (γ := Set ℂ) (ball 0 R) w
hR : 0 < R
⊢ ‖w‖ < R

Tactic:
rw [mem_ball_iff_norm, sub_zero] at hw

Premises used: sub_zero, mem_ball_iff_norm
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
w ρ : ℂ
R : ℝ
hρ : ‖ρ‖ = R
hw : Membership.mem (γ := Set ℂ) (ball 0 R) w
hR : 0 < R
hw₁ : ‖w‖ < R
⊢ 0 < R

Tactic:
rw [mem_ball_iff_norm, sub_zero] at hw

Premises used: sub_zero, mem_ball_iff_norm
-- 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
n : ℕ
simp_all : 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 2
⊢ r n < R

Tactic:
simp_all only [sub_lt_self_iff, sub_pos, div_pos_iff_of_pos_left, r]

Premises used: sub_pos, sub_lt_self_iff, div_pos_iff_of_pos_left
-- 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
n : ℕ
⊢ 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 2

Tactic:
positivity
-- 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
⊢ ∀ (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
-- 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
n : ℕ
simp_all : ∀ (hr_lt : ∀ (n : ℕ), 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 2), (R - ‖w‖) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 < R
⊢ 0 < r n

Tactic:
simp_all only [sub_lt_self_iff, sub_pos, div_pos_iff_of_pos_left, r]

Premises used: sub_pos, sub_lt_self_iff, div_pos_iff_of_pos_left
-- 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
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
linarith₁ : HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 ≤ 0 → GT.gt (α := ℝ) 2 0
⊢ 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 2

Tactic:
linarith
-- 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
n : ℕ
hr_lt : ∀ (n : ℕ), 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 2
apply : R - ‖w‖ < R * HAdd.hAdd (α := ℝ) (↑n : ℝ) 2
⊢ (R - ‖w‖) / HAdd.hAdd (α := ℝ) (↑n : ℝ) 2 < R

Tactic:
apply (div_lt_iff₀ (by linarith)).2

Premises used: Iff.mpr, div_lt_iff₀
-- 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
n : ℕ
hr_lt : ∀ (n : ℕ), 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 2
⊢ R - ‖w‖ ≤ R * 1

Tactic:
aesop
-- 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
n : ℕ
hr_lt : ∀ (n : ℕ), 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 2
hbc : 1 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 2
⊢ R * 1 < R * HAdd.hAdd (α := ℝ) (↑n : ℝ) 2

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
n : ℕ
hr_lt : ∀ (n : ℕ), 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 2
⊢ 1 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 2

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
n : ℕ
hr_lt : ∀ (n : ℕ), 0 < HAdd.hAdd (α := ℝ) (↑n : ℝ) 2
calc : R - ‖w‖ ≤ R * 1
calc₁ : R * 1 < R * HAdd.hAdd (α := ℝ) (↑n : ℝ) 2
⊢ R - ‖w‖ < R * HAdd.hAdd (α := ℝ) (↑n : ℝ) 2

Tactic:
calc R - ‖w‖
      _ ≤ R * 1 := by aesop
      _ < R * (n + 2) := by gcongr; grind

Premises used: 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
⊢ ∀ (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
-- 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
⊢ 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)
-- 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)
⊢ 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
-- 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 : ℕ
hf : InnerProductSpace.HarmonicContOnCl (F := ℝ) (fun (x : ℂ) ↦ log ‖x - ρ‖) (ball 0 (r n))
hw₁ : Membership.mem (γ := Set ℂ) (ball 0 (r n)) w
⊢ circleAverage (HSMul.hSMul (β := ℂ → ℝ) (Complex.re ∘ herglotzRieszKernel 0 w) fun (x : ℂ) ↦ log ‖x - ρ‖) 0 (r n) =
    log ‖w - ρ‖

Tactic:
apply InnerProductSpace.HarmonicContOnCl.circleAverage_re_herglotzRieszKernel_smul

Premises used: InnerProductSpace.HarmonicContOnCl.circleAverage_re_herglotzRieszKernel_smul
-- 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 : ℕ
⊢ InnerProductSpace.HarmonicContOnCl (F := ℝ) (fun (x : ℂ) ↦ log ‖x - ρ‖) (ball 0 (r n))

Tactic:
⟨fun z hz ↦ ?_, fun x hx ↦ ?_⟩

Premises used: InnerProductSpace.HarmonicContOnCl.mk
-- 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 : ℕ
hf :
  ∀ (z : ℂ) (hz : Membership.mem (γ := Set ℂ) (ball 0 (r n)) z),
    InnerProductSpace.HarmonicAt (F := ℝ) (fun (x : ℂ) ↦ log ‖x - ρ‖) z
hf₁ :
  ∀ (x : ℂ) (hx : Membership.mem (γ := Set ℂ) (closure (ball 0 (r n))) x),
    ContinuousWithinAt (Y := ℝ) (fun (x : ℂ) ↦ log ‖x - ρ‖) (closure (ball 0 (r n))) x
⊢ InnerProductSpace.HarmonicContOnCl (F := ℝ) (fun (x : ℂ) ↦ log ‖x - ρ‖) (ball 0 (r n))

Tactic:
refine ⟨fun z hz ↦ ?_, fun x 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 : ℕ
z : ℂ
hz : Membership.mem (γ := Set ℂ) (ball 0 (r n)) z
⊢ AnalyticAt ℂ (F := ℂ) (fun (x : ℂ) ↦ x - ρ) z

Tactic:
fun_prop
-- 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 : ℕ
z : ℂ
hz : Membership.mem (γ := Set ℂ) (ball 0 (r n)) z
⊢ z - ρ ≠ 0

Tactic:
grind [mem_ball, dist_zero_right]

Premises used: Metric.mem_ball, 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 : ℕ
z : ℂ
hz : Membership.mem (γ := Set ℂ) (ball 0 (r n)) z
⊢ InnerProductSpace.HarmonicAt (F := ℝ) (fun (x : ℂ) ↦ log ‖x - ρ‖) z

Tactic:
exact AnalyticAt.harmonicAt_log_norm (by fun_prop) (by grind [mem_ball, dist_zero_right])

Premises used: AnalyticAt.harmonicAt_log_norm
-- 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 funProp : ‖x - ρ‖ ≠ 0
⊢ ContinuousWithinAt (Y := ℝ) (fun (x : ℂ) ↦ log ‖x - ρ‖) (closure (ball 0 (r n))) x

Tactic:
fun_prop
-- 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 - ρ‖ ≠ 0
⊢ ContinuousWithinAt (Y := ℝ) (fun (x : ℂ) ↦ log ‖x - ρ‖) (closure (ball 0 (r n))) x

Tactic:
suffices ‖x - ρ‖ ≠ 0 by fun_prop