awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
hp : ¬p = 0
this :
  rexp (log p.mahlerMeasure) =
    rexp (log ‖p.leadingCoeff‖ + Multiset.sum (Multiset.map (fun (a : ℂ) ↦ log⁺ ‖a‖) p.roots))
⊢ p.mahlerMeasure = ‖p.leadingCoeff‖ * rexp (Multiset.sum (Multiset.map (fun (a : ℂ) ↦ log⁺ ‖a‖) p.roots))

Tactic:
rw [exp_add, exp_log <| mahlerMeasure_pos_of_ne_zero hp,
    exp_log <| norm_pos_iff.mpr <| leadingCoeff_ne_zero.mpr hp] at this

Premises used: Iff.mpr, norm_pos_iff, Polynomial.mahlerMeasure_pos_of_ne_zero, Real.exp_log, Polynomial.leadingCoeff_ne_zero, Real.exp_add
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
hp : ¬p = 0
this : p.mahlerMeasure = ‖p.leadingCoeff‖ * rexp (Multiset.sum (Multiset.map (fun (a : ℂ) ↦ log⁺ ‖a‖) p.roots))
⊢ p.mahlerMeasure = ‖p.leadingCoeff‖ * Multiset.prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots)

Tactic:
simp [this, exp_multiset_sum, posLog_eq_log_max_one, exp_log]

Premises used: Real.exp_log, Real.exp_multiset_sum, Real.posLog_eq_log_max_one
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
⊢ LE.le (α := ℝ) 1 (Multiset.prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots))

Tactic:
grind [Multiset.one_le_prod, Multiset.mem_map]

Premises used: Multiset.mem_map, Multiset.one_le_prod
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
rw : ‖p.leadingCoeff‖ * 1 ≤ ‖p.leadingCoeff‖ * Multiset.prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots)
⊢ ‖p.leadingCoeff‖ ≤ p.mahlerMeasure

Tactic:
rw [← mul_one ‖_‖, mahlerMeasure_eq_leadingCoeff_mul_prod_roots]

Premises used: Norm.norm, Polynomial.mahlerMeasure_eq_leadingCoeff_mul_prod_roots, mul_one
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
hbc : LE.le (α := ℝ) 1 (Multiset.prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots))
⊢ ‖p.leadingCoeff‖ * 1 ≤ ‖p.leadingCoeff‖ * Multiset.prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
⊢ LE.le (α := ℝ) 1 (Multiset.prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots))

Tactic:
one_le_prod_max_one_norm_roots p

Premises used: Polynomial.one_le_prod_max_one_norm_roots
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
⊢ LE.le (α := ℝ) 1 (Multiset.prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots))

Tactic:
exact one_le_prod_max_one_norm_roots p

Premises used: Polynomial.one_le_prod_max_one_norm_roots
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
hlc : 1 ≤ ‖p.leadingCoeff‖
rw :
  HMul.hMul (α := ℝ) 1 (Multiset.prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots)) ≤
    ‖p.leadingCoeff‖ * Multiset.prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots)
⊢ Multiset.prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots) ≤ p.mahlerMeasure

Tactic:
rw [← one_mul (Multiset.prod _), mahlerMeasure_eq_leadingCoeff_mul_prod_roots]

Premises used: Polynomial.mahlerMeasure_eq_leadingCoeff_mul_prod_roots, Multiset.prod, one_mul
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
hlc : 1 ≤ ‖p.leadingCoeff‖
ha : LE.le (α := ℝ) 0 (Multiset.prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots))
⊢ HMul.hMul (α := ℝ) 1 (Multiset.prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots)) ≤
    ‖p.leadingCoeff‖ * Multiset.prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
hlc : 1 ≤ ‖p.leadingCoeff‖
⊢ LE.le (α := ℝ) 0 (Multiset.prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots))

Tactic:
zero_le_one.trans <| one_le_prod_max_one_norm_roots p

Premises used: Polynomial.one_le_prod_max_one_norm_roots, zero_le_one, LE.le.trans
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
hlc : 1 ≤ ‖p.leadingCoeff‖
⊢ LE.le (α := ℝ) 0 (Multiset.prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots))

Tactic:
exact zero_le_one.trans <| one_le_prod_max_one_norm_roots p

Premises used: Polynomial.one_le_prod_max_one_norm_roots, zero_le_one, LE.le.trans
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
hlc : 1 ≤ ‖p.leadingCoeff‖
⊢ 1 ≤ p.mahlerMeasure

Tactic:
hlc.trans (leadingCoeff_le_mahlerMeasure p)

Premises used: Polynomial.leadingCoeff_le_mahlerMeasure, LE.le.trans
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
pos : ∀ (hp : p = 0), p.mahlerMeasure ≤ p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖
neg : ∀ (hp : ¬p = 0), p.mahlerMeasure ≤ p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖
⊢ p.mahlerMeasure ≤ p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖

Tactic:
by_cases hp : p = 0
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
hp : p = 0
⊢ p.mahlerMeasure ≤ p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖

Tactic:
simp [hp]
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
hp : ¬p = 0
⊢ p.natDegree ∈ p.support ∧ LT.lt (α := ℝ) 0 ((fun (x : ℕ) (a : ℂ) ↦ ‖a‖) p.natDegree (p.coeff p.natDegree))

Tactic:
simp [hp]
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
hp : ¬p = 0
⊢ LT.lt (α := ℝ) 0 (p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖)

Tactic:
have : 0 < p.sum fun _ a ↦ ‖a‖ :=
    Finset.sum_pos' (fun i _ ↦ norm_nonneg (p.coeff i)) ⟨p.natDegree, by simp [hp]⟩
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
hp : ¬p = 0
this : LT.lt (α := ℝ) 0 (p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖)
⊢ (p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖) = rexp (circleAverage (fun (x : ℂ) ↦ log (p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖)) 0 1)

Tactic:
simp [circleAverage_def, mul_assoc, exp_log this]

Premises used: mul_assoc, Real.circleAverage_def, Real.exp_log
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
hp : ¬p = 0
this : LT.lt (α := ℝ) 0 (p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖)
neg :
  rexp ((2 * π)⁻¹ * ∫ (x : ℝ) in 0..2 * π, log ‖eval (circleMap 0 1 x) p‖) ≤
    rexp ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, log (p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖))
⊢ p.mahlerMeasure ≤ p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖

Tactic:
rw [show (p.sum fun _ a ↦ ‖a‖) = rexp (circleAverage (fun _ ↦ log (p.sum fun _ a ↦ ‖a‖)) 0 1)
    by simp [circleAverage_def, mul_assoc, exp_log this], mahlerMeasure_def_of_ne_zero hp,
    circleAverage_def, smul_eq_mul]

Premises used: Polynomial.mahlerMeasure_def_of_ne_zero, Real.circleAverage_def, smul_eq_mul
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
hp : ¬p = 0
this : LT.lt (α := ℝ) 0 (p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖)
neg :
  LE.le (α := ℝ) (∫ (x : ℝ) in 0..2 * π, log ‖eval (circleMap 0 1 x) p‖)
    (∫ (θ : ℝ) in 0..2 * π, log (p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖))
⊢ rexp ((2 * π)⁻¹ * ∫ (x : ℝ) in 0..2 * π, log ‖eval (circleMap 0 1 x) p‖) ≤
    rexp ((2 * π)⁻¹ * ∫ (θ : ℝ) in 0..2 * π, log (p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖))

Tactic:
gcongr
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
hp : ¬p = 0
this : LT.lt (α := ℝ) 0 (p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖)
⊢ 0 ≤ 2 * π

Tactic:
positivity
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
hp : ¬p = 0
this : LT.lt (α := ℝ) 0 (p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖)
⊢ IntervalIntegrable (ε := ℝ) (fun (u : ℝ) ↦ log (p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖)) volume 0 (2 * π)

Tactic:
simp
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
hp : ¬p = 0
this : LT.lt (α := ℝ) 0 (p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖)
neg :
  (ae (F := Measure ℝ) (Measure.restrict volume (Icc 0 (2 * π)))).EventuallyLE (β := ℝ)
    (fun (x : ℝ) ↦ log ‖eval (circleMap 0 1 x) p‖) fun (u : ℝ) ↦ log (p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖)
⊢ LE.le (α := ℝ) (∫ (x : ℝ) in 0..2 * π, log ‖eval (circleMap 0 1 x) p‖)
    (∫ (θ : ℝ) in 0..2 * π, log (p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖))

Tactic:
apply intervalIntegral.integral_mono_ae_restrict (by positivity)
    p.intervalIntegrable_mahlerMeasure (by simp)

Premises used: intervalIntegral.integral_mono_ae_restrict, Polynomial.intervalIntegrable_mahlerMeasure
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
hp : ¬p = 0
this : LT.lt (α := ℝ) 0 (p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖)
neg :
  ∃ v ∈ ae (F := Measure ℝ) (Measure.restrict volume (Icc 0 (2 * π))),
    ∀ y ∈ v, log ‖eval (circleMap 0 1 y) p‖ ≤ log (p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖)
⊢ (ae (F := Measure ℝ) (Measure.restrict volume (Icc 0 (2 * π)))).EventuallyLE (β := ℝ)
    (fun (x : ℝ) ↦ log ‖eval (circleMap 0 1 x) p‖) fun (u : ℝ) ↦ log (p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖)

Tactic:
rw [EventuallyLE, eventually_iff_exists_mem]

Premises used: Filter.EventuallyLE, Filter.eventually_iff_exists_mem
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
hp : ¬p = 0
this : LT.lt (α := ℝ) 0 (p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖)
h :
  {x : ℝ | eval (circleMap 0 1 x) p ≠ 0} ∈ ae (F := Measure ℝ) (Measure.restrict volume (Icc 0 (2 * π))) ∧
    ∀ (y : ℝ),
      Membership.mem (γ := Set ℝ) {x : ℝ | eval (circleMap 0 1 x) p ≠ 0} y →
        log ‖eval (circleMap 0 1 y) p‖ ≤ log (p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖)
⊢ ∃ v ∈ ae (F := Measure ℝ) (Measure.restrict volume (Icc 0 (2 * π))),
    ∀ y ∈ v, log ‖eval (circleMap 0 1 y) p‖ ≤ log (p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖)

Tactic:
use {x : ℝ | eval (circleMap 0 1 x) p ≠ 0}
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
hp : ¬p = 0
this : LT.lt (α := ℝ) 0 (p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖)
h : {x : ℝ | eval (circleMap 0 1 x) p ≠ 0} ∈ ae (F := Measure ℝ) (Measure.restrict volume (Icc 0 (2 * π)))
h₁ :
  ∀ (y : ℝ),
    Membership.mem (γ := Set ℝ) {x : ℝ | eval (circleMap 0 1 x) p ≠ 0} y →
      log ‖eval (circleMap 0 1 y) p‖ ≤ log (p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖)
⊢ {x : ℝ | eval (circleMap 0 1 x) p ≠ 0} ∈ ae (F := Measure ℝ) (Measure.restrict volume (Icc 0 (2 * π))) ∧
    ∀ (y : ℝ),
      Membership.mem (γ := Set ℝ) {x : ℝ | eval (circleMap 0 1 x) p ≠ 0} y →
        log ‖eval (circleMap 0 1 y) p‖ ≤ log (p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖)

Tactic:
constructor
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
hp : ¬p = 0
this : LT.lt (α := ℝ) 0 (p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖)
⊢ MeasurableSet (Icc 0 (2 * π))

Tactic:
simp
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
hp : ¬p = 0
this : LT.lt (α := ℝ) 0 (p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖)
h :
  Eq (α := ENNReal)
    ((volume : (a : Set ℝ) → ENNReal) ({x : ℝ | x ∉ {x : ℝ | eval (circleMap 0 1 x) p ≠ 0}} ∩ Icc 0 (2 * π)) : ENNReal)
    (0 : ENNReal)
⊢ {x : ℝ | eval (circleMap 0 1 x) p ≠ 0} ∈ ae (F := Measure ℝ) (Measure.restrict volume (Icc 0 (2 * π)))

Tactic:
rw [mem_ae_iff, compl_def, Measure.restrict_apply' (by simp)]

Premises used: Set.compl_def, MeasureTheory.mem_ae_iff, MeasureTheory.Measure.restrict_apply'
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
hp : ¬p = 0
this : LT.lt (α := ℝ) 0 (p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖)
apply : (({x : ℝ | x ∉ {x : ℝ | eval (circleMap 0 1 x) p ≠ 0}} ∩ Icc 0 (2 * π)) \ {2 * π}).Finite
⊢ Eq (α := ENNReal)
    ((volume : (a : Set ℝ) → ENNReal) ({x : ℝ | x ∉ {x : ℝ | eval (circleMap 0 1 x) p ≠ 0}} ∩ Icc 0 (2 * π)) : ENNReal)
    (0 : ENNReal)

Tactic:
apply (Finite.of_diff _ <| finite_singleton (2 * π)).measure_zero

Premises used: Real.pi, HMul.hMul, Set.Finite.measure_zero, OfNat.ofNat, Set.finite_singleton, Set.Finite.of_diff
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
hp : ¬p = 0
this : LT.lt (α := ℝ) 0 (p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖)
simp : ({x : ℝ | eval (circleMap 0 1 x) p = 0} ∩ Ico 0 (2 * π)).Finite
⊢ (({x : ℝ | x ∉ {x : ℝ | eval (circleMap 0 1 x) p ≠ 0}} ∩ Icc 0 (2 * π)) \ {2 * π}).Finite

Tactic:
simp only [ne_eq, mem_setOf_eq, Decidable.not_not, inter_diff_assoc, Icc_diff_right]

Premises used: Set.mem_setOf_eq, ne_eq, Set.Icc_diff_right, Decidable.not_not, Set.inter_diff_assoc
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
hp : ¬p = 0
this : LT.lt (α := ℝ) 0 (p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖)
rw : Set.Finite (α := ℝ) {a : ℝ | a ∈ Ico 0 (2 * π) ∧ eval (circleMap 0 1 a) p = 0}
⊢ ({x : ℝ | eval (circleMap 0 1 x) p = 0} ∩ Ico 0 (2 * π)).Finite

Tactic:
rw [setOf_inter_eq_sep]

Premises used: Set.setOf_inter_eq_sep
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
hp : ¬p = 0
this : LT.lt (α := ℝ) 0 (p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖)
x : ℝ
h : Membership.mem (γ := Set ℝ) {a : ℝ | a ∈ Ico 0 (2 * π) ∧ eval (circleMap 0 1 a) p = 0} x
x_1 : ℝ
k : Membership.mem (γ := Set ℝ) {a : ℝ | a ∈ Ico 0 (2 * π) ∧ eval (circleMap 0 1 a) p = 0} x_1
l : circleMap 0 1 x = circleMap 0 1 x_1
linarith : 2 * π < 2 * π - 0 → 2 * π - (2 * π - 0) = 0
⊢ 2 * π - 0 ≤ 2 * π

Tactic:
linarith
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
hp : ¬p = 0
this : LT.lt (α := ℝ) 0 (p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖)
apply : circleMap 0 1 '' {a : ℝ | a ∈ Ico 0 (2 * π) ∧ eval (circleMap 0 1 a) p = 0} ⊆ {x : ℂ | x ∈ p.roots}
⊢ Set.Finite (α := ℝ) {a : ℝ | a ∈ Ico 0 (2 * π) ∧ eval (circleMap 0 1 a) p = 0}

Tactic:
apply Finite.of_finite_image (f := circleMap 0 1) ((Multiset.finite_toSet p.roots).subset _)
      <| fun _ h _ k l ↦ injOn_circleMap_of_abs_sub_le' one_ne_zero (by linarith) h.1 k.1 l

Premises used: Polynomial.roots, injOn_circleMap_of_abs_sub_le', Set.Finite.subset, Multiset.finite_toSet, Set.Finite.of_finite_image, one_ne_zero
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
hp : ¬p = 0
this : LT.lt (α := ℝ) 0 (p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖)
⊢ circleMap 0 1 '' {a : ℝ | a ∈ Ico 0 (2 * π) ∧ eval (circleMap 0 1 a) p = 0} ⊆ {x : ℂ | x ∈ p.roots}

Tactic:
simp [hp]
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
hp : ¬p = 0
this : LT.lt (α := ℝ) 0 (p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖)
y : ℝ
h :
  Membership.mem (γ := Set ℝ) {x : ℝ | eval (circleMap 0 1 x) p ≠ 0} y →
    log ‖eval (circleMap 0 1 y) p‖ ≤ log (p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖)
⊢ Membership.mem (γ := Set ℝ) {x : ℝ | eval (circleMap 0 1 x) p ≠ 0} y →
    log ‖eval (circleMap 0 1 y) p‖ ≤ log (p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖)

Tactic:
_
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
hp : ¬p = 0
this : LT.lt (α := ℝ) 0 (p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖)
y : ℝ
h_1 : Membership.mem (γ := Set ℝ) {x : ℝ | eval (circleMap 0 1 x) p ≠ 0} y
h : ‖eval (circleMap 0 1 y) p‖ ≤ p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖
⊢ log ‖eval (circleMap 0 1 y) p‖ ≤ log (p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
hp : ¬p = 0
this : LT.lt (α := ℝ) 0 (p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖)
y : ℝ
h_1 : Membership.mem (γ := Set ℝ) {x : ℝ | eval (circleMap 0 1 x) p ≠ 0} y
h : Norm.norm (E := ℂ) (p.sum fun (e : ℕ) (a : ℂ) ↦ a * circleMap 0 1 y ^ e) ≤ p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖
⊢ ‖eval (circleMap 0 1 y) p‖ ≤ p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖

Tactic:
rw [eval_eq_sum]

Premises used: Polynomial.eval_eq_sum
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
hp : ¬p = 0
this : LT.lt (α := ℝ) 0 (p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖)
y : ℝ
h_1 : Membership.mem (γ := Set ℝ) {x : ℝ | eval (circleMap 0 1 x) p ≠ 0} y
h :
  ∀ b ∈ p.support,
    Norm.norm (E := ℂ) ((fun (e : ℕ) (a : ℂ) ↦ a * circleMap 0 1 y ^ e) b (p.coeff b)) ≤
      (fun (x : ℕ) (a : ℂ) ↦ ‖a‖) b (p.coeff b)
⊢ Norm.norm (E := ℂ) (p.sum fun (e : ℕ) (a : ℂ) ↦ a * circleMap 0 1 y ^ e) ≤ p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖

Tactic:
apply norm_sum_le_of_le p.support

Premises used: norm_sum_le_of_le, Polynomial.support
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
hp : ¬p = 0
this : LT.lt (α := ℝ) 0 (p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖)
y : ℝ
h : Membership.mem (γ := Set ℝ) {x : ℝ | eval (circleMap 0 1 x) p ≠ 0} y
⊢ ∀ b ∈ p.support,
    Norm.norm (E := ℂ) ((fun (e : ℕ) (a : ℂ) ↦ a * circleMap 0 1 y ^ e) b (p.coeff b)) ≤
      (fun (x : ℕ) (a : ℂ) ↦ ‖a‖) b (p.coeff b)

Tactic:
simp
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
⊢ 0 ≤ 2 * π

Tactic:
positivity
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
rw : IsFiniteMeasure (m0 := MeasureSpace.toMeasurableSpace) (Measure.restrict volume (Ioc 0 (2 * π)))
⊢ IsFiniteMeasure (m0 := MeasureSpace.toMeasurableSpace) (Measure.restrict volume (uIoc 0 (2 * π)))

Tactic:
rw [uIoc_of_le (by positivity)]

Premises used: Set.uIoc_of_le
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
⊢ IsFiniteMeasure (m0 := MeasureSpace.toMeasurableSpace) (Measure.restrict volume (Ioc 0 (2 * π)))

Tactic:
infer_instance
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
⊢ IsFiniteMeasure (m0 := MeasureSpace.toMeasurableSpace) (Measure.restrict volume (uIoc 0 (2 * π)))

Tactic:
have : IsFiniteMeasure (volume.restrict (uIoc 0 (2 * π))) := by
    rw [uIoc_of_le (by positivity)]; infer_instance
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
this : IsFiniteMeasure (m0 := MeasureSpace.toMeasurableSpace) (Measure.restrict volume (uIoc 0 (2 * π)))
⊢ Ne (α := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (uIoc 0 (2 * π)) : ENNReal) (0 : ENNReal)

Tactic:
simp
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
this : IsFiniteMeasure (m0 := MeasureSpace.toMeasurableSpace) (Measure.restrict volume (uIoc 0 (2 * π)))
⊢ NeZero (R := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (uIoc 0 (2 * π)) : ENNReal)

Tactic:
have : NeZero (volume (uIoc 0 (2 * π))) := ⟨by simp⟩
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
this_1 : IsFiniteMeasure (m0 := MeasureSpace.toMeasurableSpace) (Measure.restrict volume (uIoc 0 (2 * π)))
this : NeZero (R := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (uIoc 0 (2 * π)) : ENNReal)
pos : ∀ (hp : p = 0), p.mahlerMeasure ≤ √(∑ i ∈ p.support, HPow.hPow (β := ℕ) ‖p.coeff i‖ 2)
neg : ∀ (hp : p ≠ 0), p.mahlerMeasure ≤ √(∑ i ∈ p.support, HPow.hPow (β := ℕ) ‖p.coeff i‖ 2)
⊢ p.mahlerMeasure ≤ √(∑ i ∈ p.support, HPow.hPow (β := ℕ) ‖p.coeff i‖ 2)

Tactic:
by_cases! hp : p = 0
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
this_1 : IsFiniteMeasure (m0 := MeasureSpace.toMeasurableSpace) (Measure.restrict volume (uIoc 0 (2 * π)))
this : NeZero (R := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (uIoc 0 (2 * π)) : ENNReal)
hp : p = 0
⊢ p.mahlerMeasure ≤ √(∑ i ∈ p.support, HPow.hPow (β := ℕ) ‖p.coeff i‖ 2)

Tactic:
simp [hp]
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
this_1 : IsFiniteMeasure (m0 := MeasureSpace.toMeasurableSpace) (Measure.restrict volume (uIoc 0 (2 * π)))
this : NeZero (R := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (uIoc 0 (2 * π)) : ENNReal)
hp : p ≠ 0
rw : ∀ᵐ (x : ℝ), x ∈ uIoc 0 (2 * π) → 0 < ‖eval (circleMap 0 1 x) p‖
⊢ ∀ᵐ (θ : ℝ) ∂Measure.restrict volume (uIoc 0 (2 * π)), 0 < ‖eval (circleMap 0 1 θ) p‖

Tactic:
rw [ae_restrict_iff' measurableSet_uIoc]

Premises used: measurableSet_uIoc, MeasureTheory.ae_restrict_iff'
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
this_1 : IsFiniteMeasure (m0 := MeasureSpace.toMeasurableSpace) (Measure.restrict volume (uIoc 0 (2 * π)))
this : NeZero (R := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (uIoc 0 (2 * π)) : ENNReal)
hp : p ≠ 0
⊢ ∀ᵐ (x : ℝ), x ∈ uIoc 0 (2 * π) → 0 < ‖eval (circleMap 0 1 x) p‖

Tactic:
Set.Finite.measure_zero ?_ _

Premises used: Set.Mem, Filter.Eventually, setOf, Set.Finite.measure_zero
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
this_1 : IsFiniteMeasure (m0 := MeasureSpace.toMeasurableSpace) (Measure.restrict volume (uIoc 0 (2 * π)))
this : NeZero (R := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (uIoc 0 (2 * π)) : ENNReal)
hp : p ≠ 0
refine : Set.Finite (α := ℝ) {x : ℝ | (fun (x : ℝ) ↦ x ∈ uIoc 0 (2 * π) → 0 < ‖eval (circleMap 0 1 x) p‖) x}ᶜ
⊢ ∀ᵐ (x : ℝ), x ∈ uIoc 0 (2 * π) → 0 < ‖eval (circleMap 0 1 x) p‖

Tactic:
refine Set.Finite.measure_zero ?_ _

Premises used: Set.Finite.measure_zero
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
this_1 : IsFiniteMeasure (m0 := MeasureSpace.toMeasurableSpace) (Measure.restrict volume (uIoc 0 (2 * π)))
this : NeZero (R := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (uIoc 0 (2 * π)) : ENNReal)
hp : p ≠ 0
simp : Set.Finite (α := ℝ) {a : ℝ | a ∈ uIoc 0 (2 * π) ∧ eval (circleMap 0 1 a) p = 0}
⊢ Set.Finite (α := ℝ) {x : ℝ | (fun (x : ℝ) ↦ x ∈ uIoc 0 (2 * π) → 0 < ‖eval (circleMap 0 1 x) p‖) x}ᶜ

Tactic:
simp only [norm_pos_iff, ne_eq, compl_setOf, Classical.not_imp, Decidable.not_not]

Premises used: norm_pos_iff, ne_eq, Classical.not_imp, Decidable.not_not, Set.compl_setOf
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
this_1 : IsFiniteMeasure (m0 := MeasureSpace.toMeasurableSpace) (Measure.restrict volume (uIoc 0 (2 * π)))
this : NeZero (R := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (uIoc 0 (2 * π)) : ENNReal)
hp : p ≠ 0
⊢ Set.Finite (α := ℝ) {a : ℝ | a ∈ uIoc 0 (2 * π) ∧ eval (circleMap 0 1 a) p = 0}

Tactic:
Finite.of_finite_image (f := circleMap 0 1) (p.roots.finite_toSet.subset ?_) ?_

Premises used: Polynomial.roots, Set.Finite.subset, Multiset.finite_toSet, Set.Finite.of_finite_image
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
this_1 : IsFiniteMeasure (m0 := MeasureSpace.toMeasurableSpace) (Measure.restrict volume (uIoc 0 (2 * π)))
this : NeZero (R := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (uIoc 0 (2 * π)) : ENNReal)
hp : p ≠ 0
refine_1 : circleMap 0 1 '' {a : ℝ | a ∈ uIoc 0 (2 * π) ∧ eval (circleMap 0 1 a) p = 0} ⊆ {x : ℂ | x ∈ p.roots}
refine_2 : InjOn (circleMap 0 1) {a : ℝ | a ∈ uIoc 0 (2 * π) ∧ eval (circleMap 0 1 a) p = 0}
⊢ Set.Finite (α := ℝ) {a : ℝ | a ∈ uIoc 0 (2 * π) ∧ eval (circleMap 0 1 a) p = 0}

Tactic:
refine Finite.of_finite_image (f := circleMap 0 1) (p.roots.finite_toSet.subset ?_) ?_

Premises used: Polynomial.roots, Set.Finite.subset, Multiset.finite_toSet, Set.Finite.of_finite_image
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
this_1 : IsFiniteMeasure (m0 := MeasureSpace.toMeasurableSpace) (Measure.restrict volume (uIoc 0 (2 * π)))
this : NeZero (R := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (uIoc 0 (2 * π)) : ENNReal)
hp : p ≠ 0
θ : ℝ
left : θ ∈ uIoc 0 (2 * π)
heval : eval (circleMap 0 1 θ) p = 0
⊢ Membership.mem (γ := Set ℂ) {x : ℂ | x ∈ p.roots} (circleMap 0 1 θ)

Tactic:
(mem_roots hp).mpr heval

Premises used: Iff.mpr, Set.Mem, setOf, Multiset.Mem, Polynomial.mem_roots
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
this_1 : IsFiniteMeasure (m0 := MeasureSpace.toMeasurableSpace) (Measure.restrict volume (uIoc 0 (2 * π)))
this : NeZero (R := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (uIoc 0 (2 * π)) : ENNReal)
hp : p ≠ 0
θ : ℝ
left : θ ∈ uIoc 0 (2 * π)
heval : eval (circleMap 0 1 θ) p = 0
⊢ Membership.mem (γ := Set ℂ) {x : ℂ | x ∈ p.roots} (circleMap 0 1 θ)

Tactic:
exact (mem_roots hp).mpr heval

Premises used: Iff.mpr, Polynomial.mem_roots
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
this_1 : IsFiniteMeasure (m0 := MeasureSpace.toMeasurableSpace) (Measure.restrict volume (uIoc 0 (2 * π)))
this : NeZero (R := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (uIoc 0 (2 * π)) : ENNReal)
hp : p ≠ 0
refine_2 : InjOn (circleMap 0 1) {a : ℝ | a ∈ uIoc 0 (2 * π)}
⊢ InjOn (circleMap 0 1) {a : ℝ | a ∈ uIoc 0 (2 * π) ∧ eval (circleMap 0 1 a) p = 0}

Tactic:
grw [setOf_and, inter_subset_left]

Premises used: Set.setOf_and, Set.inter_subset_left
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
this_1 : IsFiniteMeasure (m0 := MeasureSpace.toMeasurableSpace) (Measure.restrict volume (uIoc 0 (2 * π)))
this : NeZero (R := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (uIoc 0 (2 * π)) : ENNReal)
hp : p ≠ 0
⊢ |0 - 2 * π| ≤ 2 * π

Tactic:
simp [abs_of_pos pi_pos]

Premises used: Real.pi_pos, abs_of_pos
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
this_1 : IsFiniteMeasure (m0 := MeasureSpace.toMeasurableSpace) (Measure.restrict volume (uIoc 0 (2 * π)))
this : NeZero (R := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (uIoc 0 (2 * π)) : ENNReal)
hp : p ≠ 0
⊢ InjOn (circleMap 0 1) {a : ℝ | a ∈ uIoc 0 (2 * π)}

Tactic:
exact injOn_circleMap_of_abs_sub_le one_ne_zero (by simp [abs_of_pos pi_pos])

Premises used: injOn_circleMap_of_abs_sub_le, one_ne_zero