awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
a : Circle
a₁ :
  ∀ (i j : Fin 2),
    (LinearMap.toMatrix basisOneI basisOneI : (a : ℂ →ₗ[ℝ] ℂ) → Matrix (Fin 2) (Fin 2) ℝ)
        (↑(LinearIsometryEquiv.toLinearEquiv ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a)) : ℂ →ₗ[ℝ] ℂ) i j =
      (↑(Matrix.planeConformalMatrix (↑a : ℂ).re (↑a : ℂ).im ⋯) : Matrix (Fin 2) (Fin 2) ℝ) i j
⊢ (LinearMap.toMatrix basisOneI basisOneI : (a : ℂ →ₗ[ℝ] ℂ) → Matrix (Fin 2) (Fin 2) ℝ)
      (↑(LinearIsometryEquiv.toLinearEquiv ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a)) : ℂ →ₗ[ℝ] ℂ) =
    (↑(Matrix.planeConformalMatrix (↑a : ℂ).re (↑a : ℂ).im ⋯) : Matrix (Fin 2) (Fin 2) ℝ)

Tactic:
ext i j
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
a : Circle
i j : Fin 2
a₁ :
  ![(↑a : ℂ).re * (![1, I] j).re - (↑a : ℂ).im * (![1, I] j).im,
        (↑a : ℂ).re * (![1, I] j).im + (↑a : ℂ).im * (![1, I] j).re]
      i =
    Matrix.vecCons (![(↑a : ℂ).re, -(↑a : ℂ).im] j) (fun (i : Fin 1) ↦ ![(↑a : ℂ).im, (↑a : ℂ).re] j) i
⊢ (LinearMap.toMatrix basisOneI basisOneI : (a : ℂ →ₗ[ℝ] ℂ) → Matrix (Fin 2) (Fin 2) ℝ)
      (↑(LinearIsometryEquiv.toLinearEquiv ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a)) : ℂ →ₗ[ℝ] ℂ) i j =
    (↑(Matrix.planeConformalMatrix (↑a : ℂ).re (↑a : ℂ).im ⋯) : Matrix (Fin 2) (Fin 2) ℝ) i j

Tactic:
simp only [LinearMap.toMatrix_apply, coe_basisOneI, LinearEquiv.coe_coe,
    LinearIsometryEquiv.coe_toLinearEquiv, rotation_apply, coe_basisOneI_repr, mul_re, mul_im,
    Matrix.val_planeConformalMatrix, Matrix.of_apply, Matrix.cons_val', Matrix.empty_val',
    Matrix.cons_val_fin_one]

Premises used: Complex.mul_im, Complex.mul_re, rotation_apply, LinearIsometryEquiv.coe_toLinearEquiv, Matrix.empty_val', Matrix.cons_val_fin_one, Matrix.of_apply, Matrix.val_planeConformalMatrix, Complex.coe_basisOneI_repr, Complex.coe_basisOneI, LinearMap.toMatrix_apply, LinearEquiv.coe_coe, Matrix.cons_val'
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
a : Circle
i j : Fin 2
a₁ :
  ![(↑a : ℂ).re * (![1, I] j).re - (↑a : ℂ).im * (![1, I] j).im,
        (↑a : ℂ).re * (![1, I] j).im + (↑a : ℂ).im * (![1, I] j).re]
      ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) =
    Matrix.vecCons (n := 1) (![(↑a : ℂ).re, -(↑a : ℂ).im] j) (fun (i : Fin 1) ↦ ![(↑a : ℂ).im, (↑a : ℂ).re] j)
      ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
a₂ :
  ![(↑a : ℂ).re * (![1, I] j).re - (↑a : ℂ).im * (![1, I] j).im,
        (↑a : ℂ).re * (![1, I] j).im + (↑a : ℂ).im * (![1, I] j).re]
      ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) =
    Matrix.vecCons (n := 1) (![(↑a : ℂ).re, -(↑a : ℂ).im] j) (fun (i : Fin 1) ↦ ![(↑a : ℂ).im, (↑a : ℂ).re] j)
      ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
⊢ ![(↑a : ℂ).re * (![1, I] j).re - (↑a : ℂ).im * (![1, I] j).im,
        (↑a : ℂ).re * (![1, I] j).im + (↑a : ℂ).im * (![1, I] j).re]
      i =
    Matrix.vecCons (![(↑a : ℂ).re, -(↑a : ℂ).im] j) (fun (i : Fin 1) ↦ ![(↑a : ℂ).im, (↑a : ℂ).re] j) i

Tactic:
fin_cases i
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
a : Circle
j : Fin 2
a₁ :
  ![(↑a : ℂ).re * (![1, I] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))).re -
          (↑a : ℂ).im * (![1, I] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))).im,
        (↑a : ℂ).re * (![1, I] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))).im +
          (↑a : ℂ).im * (![1, I] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))).re]
      ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) =
    Matrix.vecCons (n := 1) (![(↑a : ℂ).re, -(↑a : ℂ).im] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩))
      (fun (i : Fin 1) ↦ ![(↑a : ℂ).im, (↑a : ℂ).re] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
a₂ :
  ![(↑a : ℂ).re * (![1, I] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))).re -
          (↑a : ℂ).im * (![1, I] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))).im,
        (↑a : ℂ).re * (![1, I] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))).im +
          (↑a : ℂ).im * (![1, I] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))).re]
      ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) =
    Matrix.vecCons (n := 1) (![(↑a : ℂ).re, -(↑a : ℂ).im] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩))
      (fun (i : Fin 1) ↦ ![(↑a : ℂ).im, (↑a : ℂ).re] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)
⊢ ![(↑a : ℂ).re * (![1, I] j).re - (↑a : ℂ).im * (![1, I] j).im,
        (↑a : ℂ).re * (![1, I] j).im + (↑a : ℂ).im * (![1, I] j).re]
      ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) =
    Matrix.vecCons (n := 1) (![(↑a : ℂ).re, -(↑a : ℂ).im] j) (fun (i : Fin 1) ↦ ![(↑a : ℂ).im, (↑a : ℂ).re] j)
      ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)

Tactic:
fin_cases j
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
a : Circle
j : Fin 2
a₁ :
  ![(↑a : ℂ).re * (![1, I] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))).re -
          (↑a : ℂ).im * (![1, I] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))).im,
        (↑a : ℂ).re * (![1, I] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))).im +
          (↑a : ℂ).im * (![1, I] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))).re]
      ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) =
    Matrix.vecCons (n := 1) (![(↑a : ℂ).re, -(↑a : ℂ).im] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩))
      (fun (i : Fin 1) ↦ ![(↑a : ℂ).im, (↑a : ℂ).re] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
a₂ :
  ![(↑a : ℂ).re * (![1, I] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))).re -
          (↑a : ℂ).im * (![1, I] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))).im,
        (↑a : ℂ).re * (![1, I] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))).im +
          (↑a : ℂ).im * (![1, I] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))).re]
      ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) =
    Matrix.vecCons (n := 1) (![(↑a : ℂ).re, -(↑a : ℂ).im] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩))
      (fun (i : Fin 1) ↦ ![(↑a : ℂ).im, (↑a : ℂ).re] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)
⊢ ![(↑a : ℂ).re * (![1, I] j).re - (↑a : ℂ).im * (![1, I] j).im,
        (↑a : ℂ).re * (![1, I] j).im + (↑a : ℂ).im * (![1, I] j).re]
      ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) =
    Matrix.vecCons (n := 1) (![(↑a : ℂ).re, -(↑a : ℂ).im] j) (fun (i : Fin 1) ↦ ![(↑a : ℂ).im, (↑a : ℂ).re] j)
      ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)

Tactic:
fin_cases j
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
a : Circle
⊢ ![(↑a : ℂ).re * (![1, I] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))).re -
          (↑a : ℂ).im * (![1, I] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))).im,
        (↑a : ℂ).re * (![1, I] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))).im +
          (↑a : ℂ).im * (![1, I] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))).re]
      ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) =
    Matrix.vecCons (n := 1) (![(↑a : ℂ).re, -(↑a : ℂ).im] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩))
      (fun (i : Fin 1) ↦ ![(↑a : ℂ).im, (↑a : ℂ).re] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
a : Circle
⊢ ![(↑a : ℂ).re * (![1, I] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))).re -
          (↑a : ℂ).im * (![1, I] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))).im,
        (↑a : ℂ).re * (![1, I] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))).im +
          (↑a : ℂ).im * (![1, I] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))).re]
      ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2)) =
    Matrix.vecCons (n := 1) (![(↑a : ℂ).re, -(↑a : ℂ).im] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩))
      (fun (i : Fin 1) ↦ ![(↑a : ℂ).im, (↑a : ℂ).re] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)) ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
a : Circle
⊢ ![(↑a : ℂ).re * (![1, I] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))).re -
          (↑a : ℂ).im * (![1, I] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))).im,
        (↑a : ℂ).re * (![1, I] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))).im +
          (↑a : ℂ).im * (![1, I] ((fun (i : Fin 2) ↦ i) (⟨0, ⋯⟩ : Fin 2))).re]
      ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) =
    Matrix.vecCons (n := 1) (![(↑a : ℂ).re, -(↑a : ℂ).im] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩))
      (fun (i : Fin 1) ↦ ![(↑a : ℂ).im, (↑a : ℂ).re] ((fun (i : Fin 2) ↦ i) ⟨0, ⋯⟩)) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
a : Circle
⊢ ![(↑a : ℂ).re * (![1, I] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))).re -
          (↑a : ℂ).im * (![1, I] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))).im,
        (↑a : ℂ).re * (![1, I] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))).im +
          (↑a : ℂ).im * (![1, I] ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2))).re]
      ((fun (i : Fin 2) ↦ i) (⟨1, ⋯⟩ : Fin 2)) =
    Matrix.vecCons (n := 1) (![(↑a : ℂ).re, -(↑a : ℂ).im] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩))
      (fun (i : Fin 1) ↦ ![(↑a : ℂ).im, (↑a : ℂ).re] ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)) ((fun (i : Fin 2) ↦ i) ⟨1, ⋯⟩)

Tactic:
simp
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
a : Circle
rw :
  (↑(Matrix.planeConformalMatrix (↑a : ℂ).re (↑a : ℂ).im ⋯) : Matrix (Fin 2) (Fin 2) ℝ) 0 0 *
        (↑(Matrix.planeConformalMatrix (↑a : ℂ).re (↑a : ℂ).im ⋯) : Matrix (Fin 2) (Fin 2) ℝ) 1 1 -
      (↑(Matrix.planeConformalMatrix (↑a : ℂ).re (↑a : ℂ).im ⋯) : Matrix (Fin 2) (Fin 2) ℝ) 0 1 *
        (↑(Matrix.planeConformalMatrix (↑a : ℂ).re (↑a : ℂ).im ⋯) : Matrix (Fin 2) (Fin 2) ℝ) 1 0 =
    1
⊢ Eq (α := ℝ)
    ((LinearMap.det : (a : ℂ →ₗ[ℝ] ℂ) → ℝ)
        (↑(LinearIsometryEquiv.toLinearEquiv ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a)) : ℂ →ₗ[ℝ] ℂ) :
      ℝ)
    (1 : ℝ)

Tactic:
rw [← LinearMap.det_toMatrix basisOneI, toMatrix_rotation, Matrix.det_fin_two]

Premises used: toMatrix_rotation, Complex.basisOneI, Matrix.det_fin_two, LinearMap.det_toMatrix
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
a : Circle
⊢ (↑(Matrix.planeConformalMatrix (↑a : ℂ).re (↑a : ℂ).im ⋯) : Matrix (Fin 2) (Fin 2) ℝ) 0 0 *
        (↑(Matrix.planeConformalMatrix (↑a : ℂ).re (↑a : ℂ).im ⋯) : Matrix (Fin 2) (Fin 2) ℝ) 1 1 -
      (↑(Matrix.planeConformalMatrix (↑a : ℂ).re (↑a : ℂ).im ⋯) : Matrix (Fin 2) (Fin 2) ℝ) 0 1 *
        (↑(Matrix.planeConformalMatrix (↑a : ℂ).re (↑a : ℂ).im ⋯) : Matrix (Fin 2) (Fin 2) ℝ) 1 0 =
    1

Tactic:
simp [← normSq_apply]

Premises used: Complex.normSq_apply
-- Module: Mathlib.Analysis.Complex.Isometry
Goal:
a : Circle
rw :
  Eq (α := ℝ)
    (↑((LinearEquiv.det : (a : ℂ ≃ₗ[ℝ] ℂ) → ℝˣ)
          (LinearIsometryEquiv.toLinearEquiv ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a))) :
      ℝ)
    (↑1 : ℝ)
rw₁ :
  Eq (α := ℝ)
    ((LinearMap.det : (a : ℂ →ₗ[ℝ] ℂ) → ℝ)
        (↑(LinearIsometryEquiv.toLinearEquiv ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a)) : ℂ →ₗ[ℝ] ℂ) :
      ℝ)
    ((↑1 : ℝ) : ℝ)
rw₂ : Eq (α := ℝ) 1 (↑1 : ℝ)
rw₃ rw₄ : Eq (α := ℝ) 1 1
⊢ Eq (α := ℝˣ)
    ((LinearEquiv.det : (a : ℂ ≃ₗ[ℝ] ℂ) → ℝˣ)
        (LinearIsometryEquiv.toLinearEquiv ((rotation : (a : Circle) → ℂ ≃ₗᵢ[ℝ] ℂ) a)) :
      ℝˣ)
    (1 : ℝˣ)

Tactic:
rw [← Units.val_inj, LinearEquiv.coe_det, det_rotation, Units.val_one]

Premises used: Units.val_inj, Units.val_one, det_rotation, LinearEquiv.coe_det
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
w ρ z : ℂ
hz_w : z ≠ w
hz_ρ : z ≠ ρ
⊢ ‖z - ρ‖ ≠ 0

Tactic:
simp_all [sub_eq_zero]

Premises used: sub_eq_zero
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
w ρ z : ℂ
hz_w : z ≠ w
hz_ρ : z ≠ ρ
⊢ ‖z - ρ‖ ≠ 0

Tactic:
have : ‖z - ρ‖ ≠ 0 := by simp_all [sub_eq_zero]
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
w ρ z : ℂ
hz_w : z ≠ w
hz_ρ : z ≠ ρ
this : ‖z - ρ‖ ≠ 0
simp : ContinuousAt (HMul.hMul (α := ℂ → ℝ) (Complex.re ∘ fun (z : ℂ) ↦ (z + w) / (z - w)) fun (x : ℂ) ↦ log ‖x - ρ‖) z
⊢ ContinuousAt (herglotzLogIntegrand w ρ) z

Tactic:
simp only [herglotzLogIntegrand, herglotzRieszKernel_fun_def, sub_zero, smul_eq_mul]

Premises used: sub_zero, herglotzRieszKernel_fun_def, _private.0.herglotzLogIntegrand, smul_eq_mul
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
w ρ z : ℂ
hz_w : z ≠ w
hz_ρ : z ≠ ρ
this : ‖z - ρ‖ ≠ 0
⊢ z - w ≠ 0

Tactic:
grind
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
w ρ z : ℂ
hz_w : z ≠ w
hz_ρ : z ≠ ρ
this : ‖z - ρ‖ ≠ 0
funProp : z - w ≠ 0
funProp₁ : ‖z - ρ‖ ≠ 0
⊢ ContinuousAt (HMul.hMul (α := ℂ → ℝ) (Complex.re ∘ fun (z : ℂ) ↦ (z + w) / (z - w)) fun (x : ℂ) ↦ log ‖x - ρ‖) z

Tactic:
fun_prop (disch := grind)
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
w ρ : ℂ
R r : ℝ
hρ : ‖ρ‖ = R
hr_lt : r < R
hwr : ‖w‖ < r
rw : ∀ (x : ℝ), ContinuousAt (Y := ℝ) (fun (θ : ℝ) ↦ herglotzLogIntegrand w ρ (circleMap 0 r θ)) x
⊢ Continuous (Y := ℝ) fun (θ : ℝ) ↦ herglotzLogIntegrand w ρ (circleMap 0 r θ)

Tactic:
rw [continuous_iff_continuousAt]

Premises used: continuous_iff_continuousAt
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
w ρ : ℂ
R r : ℝ
hρ : ‖ρ‖ = R
hr_lt : r < R
hwr : ‖w‖ < r
θ : ℝ
⊢ ContinuousAt (circleMap 0 r) θ

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
w ρ : ℂ
R r : ℝ
hρ : ‖ρ‖ = R
hr_lt : r < R
hwr : ‖w‖ < r
θ : ℝ
apply : circleMap 0 r θ ≠ w
apply₁ : circleMap 0 r θ ≠ ρ
⊢ ContinuousAt (Y := ℝ) (fun (θ : ℝ) ↦ herglotzLogIntegrand w ρ (circleMap 0 r θ)) θ

Tactic:
apply ContinuousAt.comp (continuousAt_herglotzLogIntegrand _ _) (by fun_prop)

Premises used: _private.0.continuousAt_herglotzLogIntegrand, ContinuousAt.comp
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
w ρ : ℂ
R r : ℝ
hρ : ‖ρ‖ = R
hr_lt : r < R
hwr : ‖w‖ < r
θ : ℝ
by_contra : ∀ (h : circleMap 0 r θ = w), False
⊢ circleMap 0 r θ ≠ w

Tactic:
by_contra h
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
w ρ : ℂ
R r : ℝ
hρ : ‖ρ‖ = R
hr_lt : r < R
hwr : ‖w‖ < r
θ : ℝ
h : circleMap 0 r θ = w
⊢ False

Tactic:
grind [norm_circleMap_zero, lt_of_le_of_lt (Complex.norm_nonneg w) hwr]

Premises used: Complex.norm_nonneg, lt_of_le_of_lt, norm_circleMap_zero
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
w ρ : ℂ
R r : ℝ
hρ : ‖ρ‖ = R
hr_lt : r < R
hwr : ‖w‖ < r
θ : ℝ
by_contra : ∀ (h : circleMap 0 r θ = ρ), False
⊢ circleMap 0 r θ ≠ ρ

Tactic:
by_contra h
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
w ρ : ℂ
R r : ℝ
hρ : ‖ρ‖ = R
hr_lt : r < R
hwr : ‖w‖ < r
θ : ℝ
h : circleMap 0 r θ = ρ
⊢ False

Tactic:
grind [norm_circleMap_zero, lt_of_le_of_lt (Complex.norm_nonneg w) hwr]

Premises used: Complex.norm_nonneg, lt_of_le_of_lt, norm_circleMap_zero
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
r₀ r R : ℝ
ρ : ℂ
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hR : 0 < R
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ r₁ : ℝ
rw :
  (↑(HAdd.hAdd (α := ℝ) (β := ℝ) ((normSq : (a : ℂ) → ℝ) (circleMap 0 r₁ θ) : ℝ) ((normSq : (a : ℂ) → ℝ) ρ : ℝ) -
          2 * (HMul.hMul (β := ℂ) (circleMap 0 r₁ θ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ρ : ℂ)).re) :
      ℂ) =
    (↑(HPow.hPow (β := ℕ) r₁ 2 + HPow.hPow (β := ℕ) R 2 - 2 * r₁ * R * Real.cos (θ - ρ.arg)) : ℂ)
⊢ HPow.hPow (β := ℕ) ‖circleMap 0 r₁ θ - ρ‖ 2 =
    HPow.hPow (β := ℕ) r₁ 2 + HPow.hPow (β := ℕ) R 2 - 2 * r₁ * R * Real.cos (θ - ρ.arg)

Tactic:
rw [← ofReal_inj, ← normSq_eq_norm_sq, normSq_sub ]

Premises used: Complex.normSq_eq_norm_sq, Complex.normSq_sub, Complex.ofReal_inj
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
r₀ r R : ℝ
ρ : ℂ
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hR : 0 < R
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ r₁ : ℝ
this :
  (HMul.hMul (β := ℂ) (circleMap 0 r₁ θ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ρ : ℂ)).re = r₁ * ‖ρ‖ * Real.cos (θ - ρ.arg)
⊢ (↑(HAdd.hAdd (α := ℝ) (β := ℝ) ((normSq : (a : ℂ) → ℝ) (circleMap 0 r₁ θ) : ℝ) ((normSq : (a : ℂ) → ℝ) ρ : ℝ) -
          2 * (HMul.hMul (β := ℂ) (circleMap 0 r₁ θ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ρ : ℂ)).re) :
      ℂ) =
    (↑(HPow.hPow (β := ℕ) r₁ 2 + HPow.hPow (β := ℕ) R 2 - 2 * r₁ * R * Real.cos (θ - ρ.arg)) : ℂ)

Tactic:
simp [normSq_eq_norm_sq, hρ, -mul_re, this, mul_assoc]

Premises used: Complex.mul_re, mul_assoc, Complex.normSq_eq_norm_sq
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
r₀ r R : ℝ
ρ : ℂ
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hR : 0 < R
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ r₁ : ℝ
suffices :
  (HMul.hMul (β := ℂ) (circleMap 0 r₁ θ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ρ : ℂ)).re = r₁ * ‖ρ‖ * Real.cos (θ - ρ.arg)
⊢ (↑(HAdd.hAdd (α := ℝ) (β := ℝ) ((normSq : (a : ℂ) → ℝ) (circleMap 0 r₁ θ) : ℝ) ((normSq : (a : ℂ) → ℝ) ρ : ℝ) -
          2 * (HMul.hMul (β := ℂ) (circleMap 0 r₁ θ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ρ : ℂ)).re) :
      ℂ) =
    (↑(HPow.hPow (β := ℕ) r₁ 2 + HPow.hPow (β := ℕ) R 2 - 2 * r₁ * R * Real.cos (θ - ρ.arg)) : ℂ)

Tactic:
suffices (circleMap 0 r₁ θ * (conj) ρ).re = r₁ * ‖ρ‖ * Real.cos (θ - ρ.arg) by
      simp [normSq_eq_norm_sq, hρ, -mul_re, this, mul_assoc]
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
r₀ r R : ℝ
ρ : ℂ
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hR : 0 < R
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ r₁ : ℝ
rw : r₁ * ‖ρ‖ * Real.cos (θ - ρ.arg)
| (HMul.hMul (β := ℂ) (circleMap 0 r₁ θ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ρ : ℂ)).re

Tactic:
rw [← norm_mul_exp_arg_mul_I ρ, ← circleMap_zero, conj_circleMap_zero,
      circleMap_zero_mul, circleMap_zero_re, ← sub_eq_add_neg]

Premises used: sub_eq_add_neg, circleMap_zero_re, conj_circleMap_zero, Complex.norm_mul_exp_arg_mul_I, circleMap_zero, circleMap_zero_mul
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
r₀ r R : ℝ
ρ : ℂ
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hR : 0 < R
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ r₁ : ℝ
conv_lhs :
  (HMul.hMul (β := ℂ) (circleMap 0 r₁ θ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ρ : ℂ)).re = r₁ * ‖ρ‖ * Real.cos (θ - ρ.arg)
conv_lhs₁ : r₁ * ‖ρ‖ * Real.cos (θ - ρ.arg) = r₁ * ‖ρ‖ * Real.cos (θ - ρ.arg)
⊢ (HMul.hMul (β := ℂ) (circleMap 0 r₁ θ) ((starRingEnd ℂ : (a : ℂ) → ℂ) ρ : ℂ)).re = r₁ * ‖ρ‖ * Real.cos (θ - ρ.arg)

Tactic:
conv_lhs => rw [← norm_mul_exp_arg_mul_I ρ, ← circleMap_zero, conj_circleMap_zero,
      circleMap_zero_mul, circleMap_zero_re, ← sub_eq_add_neg]

Premises used: sub_eq_add_neg, circleMap_zero_re, conj_circleMap_zero, Complex.norm_mul_exp_arg_mul_I, circleMap_zero, circleMap_zero_mul
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
r₀ r R : ℝ
ρ : ℂ
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hR : 0 < R
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
⊢ ∀ (r₁ : ℝ),
    HPow.hPow (β := ℕ) ‖circleMap 0 r₁ θ - ρ‖ 2 =
      HPow.hPow (β := ℕ) r₁ 2 + HPow.hPow (β := ℕ) R 2 - 2 * r₁ * R * Real.cos (θ - ρ.arg)

Tactic:
have h_cos_law (r₁ : ℝ) :
      ‖circleMap 0 r₁ θ - ρ‖ ^ 2 = r₁ ^ 2 + R ^ 2 - 2 * r₁ * R * Real.cos (θ - Complex.arg ρ) := by
    rw [← ofReal_inj, ← normSq_eq_norm_sq, normSq_sub ]
    suffices (circleMap 0 r₁ θ * (conj) ρ).re = r₁ * ‖ρ‖ * Real.cos (θ - ρ.arg) by
      simp [normSq_eq_norm_sq, hρ, -mul_re, this, mul_assoc]
    conv_lhs => rw [← norm_mul_exp_arg_mul_I ρ, ← circleMap_zero, conj_circleMap_zero,
      circleMap_zero_mul, circleMap_zero_re, ← sub_eq_add_neg]
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
r₀ r R : ℝ
ρ : ℂ
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hR : 0 < R
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
h_cos_law :
  ∀ (r₁ : ℝ),
    HPow.hPow (β := ℕ) ‖circleMap 0 r₁ θ - ρ‖ 2 =
      HPow.hPow (β := ℕ) r₁ 2 + HPow.hPow (β := ℕ) R 2 - 2 * r₁ * R * Real.cos (θ - ρ.arg)
rw : r₀ * HPow.hPow (β := ℕ) ‖circleMap 0 R θ - ρ‖ 2 ≤ HPow.hPow (β := ℕ) ‖circleMap 0 r θ - ρ‖ 2 * R
⊢ r₀ / R * HPow.hPow (β := ℕ) ‖circleMap 0 R θ - ρ‖ 2 ≤ HPow.hPow (β := ℕ) ‖circleMap 0 r θ - ρ‖ 2

Tactic:
rw [div_mul_eq_mul_div, div_le_iff₀ hR]

Premises used: div_le_iff₀, div_mul_eq_mul_div
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
r₀ r R : ℝ
ρ : ℂ
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hR : 0 < R
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
h_cos_law :
  ∀ (r₁ : ℝ),
    HPow.hPow (β := ℕ) ‖circleMap 0 r₁ θ - ρ‖ 2 =
      HPow.hPow (β := ℕ) r₁ 2 + HPow.hPow (β := ℕ) R 2 - 2 * r₁ * R * Real.cos (θ - ρ.arg)
nlinarith :
  HPow.hPow (β := ℕ) ‖circleMap 0 r θ - ρ‖ 2 * R < r₀ * HPow.hPow (β := ℕ) ‖circleMap 0 R θ - ρ‖ 2 →
    HPow.hPow (β := ℕ) ‖circleMap 0 r θ - ρ‖ 2 * R - r₀ * HPow.hPow (β := ℕ) ‖circleMap 0 R θ - ρ‖ 2 +
                (0 - (0 - HPow.hPow (β := ℕ) ‖circleMap 0 R θ - ρ‖ 2) * (r₀ - r)) +
              -((0 - r₀) *
                    (HPow.hPow (β := ℕ) ‖circleMap 0 R θ - ρ‖ 2 -
                      (HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) R 2 - 2 * R * R * Real.cos (θ - ρ.arg))) -
                  0) +
            ((0 - R) *
                (HPow.hPow (β := ℕ) ‖circleMap 0 r θ - ρ‖ 2 -
                  (HPow.hPow (β := ℕ) r 2 + HPow.hPow (β := ℕ) R 2 - 2 * r * R * Real.cos (θ - ρ.arg))) -
              0) +
          -((r₀ - r) *
                (HPow.hPow (β := ℕ) ‖circleMap 0 R θ - ρ‖ 2 -
                  (HPow.hPow (β := ℕ) R 2 + HPow.hPow (β := ℕ) R 2 - 2 * R * R * Real.cos (θ - ρ.arg))) -
              0) +
        (0 - (r - R) * (R * r - R * R)) =
      0
⊢ r₀ * HPow.hPow (β := ℕ) ‖circleMap 0 R θ - ρ‖ 2 ≤ HPow.hPow (β := ℕ) ‖circleMap 0 r θ - ρ‖ 2 * R

Tactic:
nlinarith [h_cos_law r, h_cos_law R, mul_le_mul_of_nonneg_left hr₀r hR.le,
      mul_le_mul_of_nonneg_left hrR hR.le, neg_one_le_cos, cos_le_one]

Premises used: LT.lt.le, Real.neg_one_le_cos, mul_le_mul_of_nonneg_left, Real.cos_le_one
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
r₀ r R : ℝ
ρ : ℂ
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hR : 0 < R
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
h_cos_law :
  ∀ (r₁ : ℝ),
    HPow.hPow (β := ℕ) ‖circleMap 0 r₁ θ - ρ‖ 2 =
      HPow.hPow (β := ℕ) r₁ 2 + HPow.hPow (β := ℕ) R 2 - 2 * r₁ * R * Real.cos (θ - ρ.arg)
⊢ r₀ / R * HPow.hPow (β := ℕ) ‖circleMap 0 R θ - ρ‖ 2 ≤ HPow.hPow (β := ℕ) ‖circleMap 0 r θ - ρ‖ 2

Tactic:
have : (r₀ / R) * ‖circleMap 0 R θ - ρ‖ ^ 2 ≤ ‖circleMap 0 r θ - ρ‖ ^ 2 := by
    rw [div_mul_eq_mul_div, div_le_iff₀ hR]
    nlinarith [h_cos_law r, h_cos_law R, mul_le_mul_of_nonneg_left hr₀r hR.le,
      mul_le_mul_of_nonneg_left hrR hR.le, neg_one_le_cos, cos_le_one]
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
r₀ r R : ℝ
ρ : ℂ
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hR : 0 < R
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
h_cos_law :
  ∀ (r₁ : ℝ),
    HPow.hPow (β := ℕ) ‖circleMap 0 r₁ θ - ρ‖ 2 =
      HPow.hPow (β := ℕ) r₁ 2 + HPow.hPow (β := ℕ) R 2 - 2 * r₁ * R * Real.cos (θ - ρ.arg)
this : r₀ / R * HPow.hPow (β := ℕ) ‖circleMap 0 R θ - ρ‖ 2 ≤ HPow.hPow (β := ℕ) ‖circleMap 0 r θ - ρ‖ 2
⊢ 0 ≤ r₀ / R

Tactic:
positivity
-- Module: Mathlib.Analysis.Complex.JensenFormula
Goal:
r₀ r R : ℝ
ρ : ℂ
hρ : ‖ρ‖ = R
hr₀ : 0 < r₀
hR : 0 < R
hr₀r : r₀ ≤ r
hrR : r ≤ R
θ : ℝ
h_cos_law :
  ∀ (r₁ : ℝ),
    HPow.hPow (β := ℕ) ‖circleMap 0 r₁ θ - ρ‖ 2 =
      HPow.hPow (β := ℕ) r₁ 2 + HPow.hPow (β := ℕ) R 2 - 2 * r₁ * R * Real.cos (θ - ρ.arg)
this : r₀ / R * HPow.hPow (β := ℕ) ‖circleMap 0 R θ - ρ‖ 2 ≤ HPow.hPow (β := ℕ) ‖circleMap 0 r θ - ρ‖ 2
grw : √(r₀ / R) * √(HPow.hPow (β := ℕ) ‖circleMap 0 R θ - ρ‖ 2) ≤ ‖circleMap 0 r θ - ρ‖
grw₁ : √(r₀ / R * HPow.hPow (β := ℕ) ‖circleMap 0 R θ - ρ‖ 2) ≤ ‖circleMap 0 r θ - ρ‖
grw₂ : √(HPow.hPow (β := ℕ) ‖circleMap 0 r θ - ρ‖ 2) ≤ ‖circleMap 0 r θ - ρ‖
grw₃ grw₄ : ‖circleMap 0 r θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖
⊢ √(r₀ / R) * ‖circleMap 0 R θ - ρ‖ ≤ ‖circleMap 0 r θ - ρ‖

Tactic:
grw [← sqrt_sq (norm_nonneg _), ← sqrt_mul (by positivity), this, sqrt_sq (norm_nonneg _)]

Premises used: Real.sqrt_mul, Real.sqrt_sq, norm_nonneg
-- 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 θ - ρ‖
simp :
  |(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 θ - ρ‖|)
⊢ ‖herglotzLogIntegrand w ρ (circleMap 0 r θ)‖ ≤
    (R + ‖w‖) / (r₀ - ‖w‖) * (|log (2 * R)| + |log √(r₀ / R)| + |log ‖circleMap 0 R θ - ρ‖|)

Tactic:
simp only [herglotzLogIntegrand, Pi.smul_apply', Function.comp_apply, smul_eq_mul, norm_mul,
    norm_eq_abs]

Premises used: Pi.smul_apply', norm_mul, _private.0.herglotzLogIntegrand, Function.comp_apply, smul_eq_mul, Real.norm_eq_abs
-- 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 θ - ρ‖
⊢ 0 < r₀ - ‖w‖ ∧ 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 θ - ρ‖
⊢ 0 < r₀ - ‖w‖

Tactic:
have ⟨hrw, hr⟩ : 0 < r₀ - ‖w‖ ∧ 0 < r := by 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‖
⊢ 0 < r

Tactic:
have ⟨hrw, hr⟩ : 0 < r₀ - ‖w‖ ∧ 0 < r := by grind