awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
p : ℂ[X]
hp : ¬p = 0
this : LT.lt (α := ℝ) 0 (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‖))
have 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‖)
Tactic: apply intervalIntegral.integral_mono_ae_restrict (by positivity)
    p.intervalIntegrable_mahlerMeasure (by simp)
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
p : ℂ[X]
hp : ¬p = 0
this : LT.lt (α := ℝ) 0 (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‖)
have 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‖)
Tactic: rw [EventuallyLE, eventually_iff_exists_mem]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
p : ℂ[X]
hp : ¬p = 0
this : LT.lt (α := ℝ) 0 (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‖)
have 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‖)
Tactic: use {x : ℝ | eval (circleMap 0 1 x) p ≠ 0}
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
p : ℂ[X]
hp : ¬p = 0
this : LT.lt (α := ℝ) 0 (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‖)
have h : {x : ℝ | eval (circleMap 0 1 x) p ≠ 0} ∈ ae (F := Measure ℝ) (Measure.restrict volume (Icc 0 (2 * π)))
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
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 * π)))
⊢ {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‖)
have 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‖)
Tactic: constructor
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
p : ℂ[X]
hp : ¬p = 0
this : LT.lt (α := ℝ) 0 (p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖)
⊢ {x : ℝ | eval (circleMap 0 1 x) p ≠ 0} ∈ ae (F := Measure ℝ) (Measure.restrict volume (Icc 0 (2 * π)))
have h : Eq (α := ENNReal)
  ((volume : (a : Set ℝ) → ENNReal) ({x : ℝ | x ∉ {x : ℝ | eval (circleMap 0 1 x) p ≠ 0}} ∩ Icc 0 (2 * π)) : ENNReal)
  (0 : ENNReal)
Tactic: rw [mem_ae_iff, compl_def, Measure.restrict_apply' (by simp)]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
p : ℂ[X]
hp : ¬p = 0
this : LT.lt (α := ℝ) 0 (p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖)
⊢ Eq (α := ENNReal)
    ((volume : (a : Set ℝ) → ENNReal) ({x : ℝ | x ∉ {x : ℝ | eval (circleMap 0 1 x) p ≠ 0}} ∩ Icc 0 (2 * π)) : ENNReal)
    (0 : ENNReal)
have apply : (({x : ℝ | x ∉ {x : ℝ | eval (circleMap 0 1 x) p ≠ 0}} ∩ Icc 0 (2 * π)) \ {2 * π}).Finite
Tactic: apply (Finite.of_diff _ <| finite_singleton (2 * π)).measure_zero
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
p : ℂ[X]
hp : ¬p = 0
this : LT.lt (α := ℝ) 0 (p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖)
⊢ (({x : ℝ | x ∉ {x : ℝ | eval (circleMap 0 1 x) p ≠ 0}} ∩ Icc 0 (2 * π)) \ {2 * π}).Finite
have simp : ({x : ℝ | eval (circleMap 0 1 x) p = 0} ∩ Ico 0 (2 * π)).Finite
Tactic: simp only [ne_eq, mem_setOf_eq, Decidable.not_not, inter_diff_assoc, Icc_diff_right]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
p : ℂ[X]
hp : ¬p = 0
this : LT.lt (α := ℝ) 0 (p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖)
⊢ ({x : ℝ | eval (circleMap 0 1 x) p = 0} ∩ Ico 0 (2 * π)).Finite
have rw : Set.Finite (α := ℝ) {a : ℝ | a ∈ Ico 0 (2 * π) ∧ eval (circleMap 0 1 a) p = 0}
Tactic: rw [setOf_inter_eq_sep]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
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
⊢ 2 * π - 0 ≤ 2 * π
have linarith : 2 * π < 2 * π - 0 → 2 * π - (2 * π - 0) = 0
Tactic: linarith
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
p : ℂ[X]
hp : ¬p = 0
this : LT.lt (α := ℝ) 0 (p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖)
⊢ Set.Finite (α := ℝ) {a : ℝ | a ∈ Ico 0 (2 * π) ∧ eval (circleMap 0 1 a) p = 0}
have apply : circleMap 0 1 '' {a : ℝ | a ∈ Ico 0 (2 * π) ∧ eval (circleMap 0 1 a) p = 0} ⊆ {x : ℂ | x ∈ p.roots}
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
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
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‖)
have h : ‖eval (circleMap 0 1 y) p‖ ≤ p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
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
⊢ ‖eval (circleMap 0 1 y) p‖ ≤ p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖
have h : Norm.norm (E := ℂ) (p.sum fun (e : ℕ) (a : ℂ) ↦ a * circleMap 0 1 y ^ e) ≤ p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖
Tactic: rw [eval_eq_sum]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
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
⊢ Norm.norm (E := ℂ) (p.sum fun (e : ℕ) (a : ℂ) ↦ a * circleMap 0 1 y ^ e) ≤ p.sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖
have 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)
Tactic: apply norm_sum_le_of_le p.support
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
p : ℂ[X]
⊢ IsFiniteMeasure (m0 := MeasureSpace.toMeasurableSpace) (Measure.restrict volume (uIoc 0 (2 * π)))
have rw : IsFiniteMeasure (m0 := MeasureSpace.toMeasurableSpace) (Measure.restrict volume (Ioc 0 (2 * π)))
Tactic: rw [uIoc_of_le (by positivity)]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (hypothesis)
Goal:
p : ℂ[X]
⊢ p.mahlerMeasure ≤ √(∑ i ∈ p.support, HPow.hPow (β := ℕ) ‖p.coeff i‖ 2)
have this : 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
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (hypothesis)
Goal:
p : ℂ[X]
this : IsFiniteMeasure (m0 := MeasureSpace.toMeasurableSpace) (Measure.restrict volume (uIoc 0 (2 * π)))
⊢ p.mahlerMeasure ≤ √(∑ i ∈ p.support, HPow.hPow (β := ℕ) ‖p.coeff i‖ 2)
have this₁ : NeZero (R := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (uIoc 0 (2 * π)) : ENNReal)
Tactic: have : NeZero (volume (uIoc 0 (2 * π))) := ⟨by simp⟩
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
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)
⊢ p.mahlerMeasure ≤ √(∑ i ∈ p.support, HPow.hPow (β := ℕ) ‖p.coeff i‖ 2)
have pos : ∀ (hp : p = 0), p.mahlerMeasure ≤ √(∑ i ∈ p.support, HPow.hPow (β := ℕ) ‖p.coeff i‖ 2)
Tactic: by_cases! hp : p = 0
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
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)
⊢ p.mahlerMeasure ≤ √(∑ i ∈ p.support, HPow.hPow (β := ℕ) ‖p.coeff i‖ 2)
have neg : ∀ (hp : p ≠ 0), p.mahlerMeasure ≤ √(∑ i ∈ p.support, HPow.hPow (β := ℕ) ‖p.coeff i‖ 2)
Tactic: by_cases! hp : p = 0
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
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
⊢ ∀ᵐ (θ : ℝ) ∂Measure.restrict volume (uIoc 0 (2 * π)), 0 < ‖eval (circleMap 0 1 θ) p‖
have rw : ∀ᵐ (x : ℝ), x ∈ uIoc 0 (2 * π) → 0 < ‖eval (circleMap 0 1 x) p‖
Tactic: rw [ae_restrict_iff' measurableSet_uIoc]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
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‖
have refine : Set.Finite (α := ℝ) {x : ℝ | (fun (x : ℝ) ↦ x ∈ uIoc 0 (2 * π) → 0 < ‖eval (circleMap 0 1 x) p‖) x}ᶜ
Tactic: refine Set.Finite.measure_zero ?_ _
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
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 (α := ℝ) {x : ℝ | (fun (x : ℝ) ↦ x ∈ uIoc 0 (2 * π) → 0 < ‖eval (circleMap 0 1 x) p‖) x}ᶜ
have simp : Set.Finite (α := ℝ) {a : ℝ | a ∈ uIoc 0 (2 * π) ∧ eval (circleMap 0 1 a) p = 0}
Tactic: simp only [norm_pos_iff, ne_eq, compl_setOf, Classical.not_imp, Decidable.not_not]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
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}
have refine_1 : circleMap 0 1 '' {a : ℝ | a ∈ uIoc 0 (2 * π) ∧ eval (circleMap 0 1 a) p = 0} ⊆ {x : ℂ | x ∈ p.roots}
Tactic: refine Finite.of_finite_image (f := circleMap 0 1) (p.roots.finite_toSet.subset ?_) ?_
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
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}
⊢ Set.Finite (α := ℝ) {a : ℝ | a ∈ uIoc 0 (2 * π) ∧ eval (circleMap 0 1 a) p = 0}
have refine_2 : InjOn (circleMap 0 1) {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 ?_) ?_
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
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 * π) ∧ eval (circleMap 0 1 a) p = 0}
have refine_2 : InjOn (circleMap 0 1) {a : ℝ | a ∈ uIoc 0 (2 * π)}
Tactic: grw [setOf_and, inter_subset_left]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (hypothesis)
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)
have this₁ : ∀ᵐ (θ : ℝ) ∂Measure.restrict volume (uIoc 0 (2 * π)), 0 < ‖eval (circleMap 0 1 θ) p‖
Tactic: have : ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)), 0 < ‖p.eval (circleMap 0 1 θ)‖ := by
    rw [ae_restrict_iff' measurableSet_uIoc]
    refine Set.Finite.measure_zero ?_ _
    simp only [norm_pos_iff, ne_eq, compl_setOf, Classical.not_imp, Decidable.not_not]
    refine Finite.of_finite_image (f := circleMap 0 1) (p.roots.finite_toSet.subset ?_) ?_
    · rintro z ⟨θ, ⟨_, heval⟩, rfl⟩
      exact (mem_roots hp).mpr heval
    · grw [setOf_and, inter_subset_left]
      exact injOn_circleMap_of_abs_sub_le one_ne_zero (by simp [abs_of_pos pi_pos])
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
p : ℂ[X]
this_1 : IsFiniteMeasure (m0 := MeasureSpace.toMeasurableSpace) (Measure.restrict volume (uIoc 0 (2 * π)))
this_2 : NeZero (R := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (uIoc 0 (2 * π)) : ENNReal)
hp : p ≠ 0
this : ∀ᵐ (θ : ℝ) ∂Measure.restrict volume (uIoc 0 (2 * π)), 0 < ‖eval (circleMap 0 1 θ) p‖
⊢ ∀ᵐ (θ : ℝ) ∂Measure.restrict volume (uIoc 0 (2 * π)),
    rexp (log ‖eval (circleMap 0 1 θ) p‖) = ‖eval (circleMap 0 1 θ) p‖
have h : ∀ (θ : ℝ) (hθ : 0 < ‖eval (circleMap 0 1 θ) p‖), rexp (log ‖eval (circleMap 0 1 θ) p‖) = ‖eval (circleMap 0 1 θ) p‖
Tactic: filter_upwards [this] with θ hθ
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (hypothesis)
Goal:
p : ℂ[X]
this_1 : IsFiniteMeasure (m0 := MeasureSpace.toMeasurableSpace) (Measure.restrict volume (uIoc 0 (2 * π)))
this_2 : NeZero (R := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (uIoc 0 (2 * π)) : ENNReal)
hp : p ≠ 0
this : ∀ᵐ (θ : ℝ) ∂Measure.restrict volume (uIoc 0 (2 * π)), 0 < ‖eval (circleMap 0 1 θ) p‖
⊢ p.mahlerMeasure ≤ √(∑ i ∈ p.support, HPow.hPow (β := ℕ) ‖p.coeff i‖ 2)
have hlogAe : ∀ᵐ (θ : ℝ) ∂Measure.restrict volume (uIoc 0 (2 * π)), rexp (log ‖eval (circleMap 0 1 θ) p‖) = ‖eval (circleMap 0 1 θ) p‖
Tactic: have hlogAe : ∀ᵐ (θ : ℝ) ∂volume.restrict (uIoc 0 (2 * π)),
      exp (log ‖p.eval (circleMap 0 1 θ)‖) = ‖p.eval (circleMap 0 1 θ)‖ := by
    filter_upwards [this] with θ hθ
    exact exp_log hθ
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (hypothesis)
Goal:
p : ℂ[X]
this_1 : IsFiniteMeasure (m0 := MeasureSpace.toMeasurableSpace) (Measure.restrict volume (uIoc 0 (2 * π)))
this_2 : NeZero (R := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (uIoc 0 (2 * π)) : ENNReal)
hp : p ≠ 0
this : ∀ᵐ (θ : ℝ) ∂Measure.restrict volume (uIoc 0 (2 * π)), 0 < ‖eval (circleMap 0 1 θ) p‖
hlogAe :
  ∀ᵐ (θ : ℝ) ∂Measure.restrict volume (uIoc 0 (2 * π)),
    rexp (log ‖eval (circleMap 0 1 θ) p‖) = ‖eval (circleMap 0 1 θ) p‖
⊢ p.mahlerMeasure ≤ √(∑ i ∈ p.support, HPow.hPow (β := ℕ) ‖p.coeff i‖ 2)
have hcont : Continuous (Y := ℝ) fun (x : ℝ) ↦ ‖eval (circleMap 0 1 x) p‖
Tactic: have hcont : Continuous (fun x : ℝ ↦ ‖eval (circleMap 0 1 x) p‖) := by fun_prop
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
p : ℂ[X]
this_1 : IsFiniteMeasure (m0 := MeasureSpace.toMeasurableSpace) (Measure.restrict volume (uIoc 0 (2 * π)))
this_2 : NeZero (R := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (uIoc 0 (2 * π)) : ENNReal)
hp : p ≠ 0
this : ∀ᵐ (θ : ℝ) ∂Measure.restrict volume (uIoc 0 (2 * π)), 0 < ‖eval (circleMap 0 1 θ) p‖
hlogAe :
  ∀ᵐ (θ : ℝ) ∂Measure.restrict volume (uIoc 0 (2 * π)),
    rexp (log ‖eval (circleMap 0 1 θ) p‖) = ‖eval (circleMap 0 1 θ) p‖
hcont : Continuous (Y := ℝ) fun (x : ℝ) ↦ ‖eval (circleMap 0 1 x) p‖
⊢ p.mahlerMeasure ≤ √(∑ i ∈ p.support, HPow.hPow (β := ℕ) ‖p.coeff i‖ 2)
have neg : rexp (circleAverage (fun (x : ℂ) ↦ log ‖eval x p‖) 0 1) ≤ √(∑ i ∈ p.support, HPow.hPow (β := ℕ) ‖p.coeff i‖ 2)
Tactic: simp only [mahlerMeasure, logMahlerMeasure, ne_eq, hp, not_false_eq_true, ↓reduceIte]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
p : ℂ[X]
this_1 : IsFiniteMeasure (m0 := MeasureSpace.toMeasurableSpace) (Measure.restrict volume (uIoc 0 (2 * π)))
this_2 : NeZero (R := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (uIoc 0 (2 * π)) : ENNReal)
hp : p ≠ 0
this : ∀ᵐ (θ : ℝ) ∂Measure.restrict volume (uIoc 0 (2 * π)), 0 < ‖eval (circleMap 0 1 θ) p‖
hlogAe :
  ∀ᵐ (θ : ℝ) ∂Measure.restrict volume (uIoc 0 (2 * π)),
    rexp (log ‖eval (circleMap 0 1 θ) p‖) = ‖eval (circleMap 0 1 θ) p‖
hcont : Continuous (Y := ℝ) fun (x : ℝ) ↦ ‖eval (circleMap 0 1 x) p‖
⊢ rexp (circleAverage (fun (x : ℂ) ↦ log ‖eval x p‖) 0 1) ≤ √(∑ i ∈ p.support, HPow.hPow (β := ℕ) ‖p.coeff i‖ 2)
have neg : rexp (⨍ (θ : ℝ) in 0..2 * π, log ‖eval (circleMap 0 1 θ) p‖) ≤ √(∑ i ∈ p.support, HPow.hPow (β := ℕ) ‖p.coeff i‖ 2)
Tactic: rw [circleAverage_eq_intervalAverage]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
p : ℂ[X]
this_1 : IsFiniteMeasure (m0 := MeasureSpace.toMeasurableSpace) (Measure.restrict volume (uIoc 0 (2 * π)))
this_2 : NeZero (R := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (uIoc 0 (2 * π)) : ENNReal)
hp : p ≠ 0
this : ∀ᵐ (θ : ℝ) ∂Measure.restrict volume (uIoc 0 (2 * π)), 0 < ‖eval (circleMap 0 1 θ) p‖
hlogAe :
  ∀ᵐ (θ : ℝ) ∂Measure.restrict volume (uIoc 0 (2 * π)),
    rexp (log ‖eval (circleMap 0 1 θ) p‖) = ‖eval (circleMap 0 1 θ) p‖
hcont : Continuous (Y := ℝ) fun (x : ℝ) ↦ ‖eval (circleMap 0 1 x) p‖
⊢ rexp (⨍ (θ : ℝ) in 0..2 * π, log ‖eval (circleMap 0 1 θ) p‖) ≤
    ⨍ (θ : ℝ) in 0..2 * π, rexp (log ‖eval (circleMap 0 1 θ) p‖)
have refine_1 : @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (θ : ℝ) ↦ log ‖eval (circleMap 0 1 θ) p‖)
  (Measure.restrict volume (uIoc 0 (2 * π)))
Tactic: refine convexOn_exp.map_average_le continuousOn_exp isClosed_univ (by simp) ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
p : ℂ[X]
this_1 : IsFiniteMeasure (m0 := MeasureSpace.toMeasurableSpace) (Measure.restrict volume (uIoc 0 (2 * π)))
this_2 : NeZero (R := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (uIoc 0 (2 * π)) : ENNReal)
hp : p ≠ 0
this : ∀ᵐ (θ : ℝ) ∂Measure.restrict volume (uIoc 0 (2 * π)), 0 < ‖eval (circleMap 0 1 θ) p‖
hlogAe :
  ∀ᵐ (θ : ℝ) ∂Measure.restrict volume (uIoc 0 (2 * π)),
    rexp (log ‖eval (circleMap 0 1 θ) p‖) = ‖eval (circleMap 0 1 θ) p‖
hcont : Continuous (Y := ℝ) fun (x : ℝ) ↦ ‖eval (circleMap 0 1 x) p‖
refine_1 :
  @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (θ : ℝ) ↦ log ‖eval (circleMap 0 1 θ) p‖)
    (Measure.restrict volume (uIoc 0 (2 * π)))
⊢ rexp (⨍ (θ : ℝ) in 0..2 * π, log ‖eval (circleMap 0 1 θ) p‖) ≤
    ⨍ (θ : ℝ) in 0..2 * π, rexp (log ‖eval (circleMap 0 1 θ) p‖)
have refine_2 : @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (rexp ∘ fun (θ : ℝ) ↦ log ‖eval (circleMap 0 1 θ) p‖)
  (Measure.restrict volume (uIoc 0 (2 * π)))
Tactic: refine convexOn_exp.map_average_le continuousOn_exp isClosed_univ (by simp) ?_ ?_
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
p : ℂ[X]
this_1 : IsFiniteMeasure (m0 := MeasureSpace.toMeasurableSpace) (Measure.restrict volume (uIoc 0 (2 * π)))
this_2 : NeZero (R := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (uIoc 0 (2 * π)) : ENNReal)
hp : p ≠ 0
this : ∀ᵐ (θ : ℝ) ∂Measure.restrict volume (uIoc 0 (2 * π)), 0 < ‖eval (circleMap 0 1 θ) p‖
hlogAe :
  ∀ᵐ (θ : ℝ) ∂Measure.restrict volume (uIoc 0 (2 * π)),
    rexp (log ‖eval (circleMap 0 1 θ) p‖) = ‖eval (circleMap 0 1 θ) p‖
hcont : Continuous (Y := ℝ) fun (x : ℝ) ↦ ‖eval (circleMap 0 1 x) p‖
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (θ : ℝ) ↦ log ‖eval (circleMap 0 1 θ) p‖)
    (Measure.restrict volume (uIoc 0 (2 * π)))
have refine_1 : @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (θ : ℝ) ↦ log ‖eval (circleMap 0 1 θ) p‖)
  (Measure.restrict volume (Ioc 0 (2 * π)))
Tactic: rw [Set.uIoc_of_le (by positivity : 0 ≤ 2 * Real.pi)]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
p : ℂ[X]
this_1 : IsFiniteMeasure (m0 := MeasureSpace.toMeasurableSpace) (Measure.restrict volume (uIoc 0 (2 * π)))
this_2 : NeZero (R := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (uIoc 0 (2 * π)) : ENNReal)
hp : p ≠ 0
this : ∀ᵐ (θ : ℝ) ∂Measure.restrict volume (uIoc 0 (2 * π)), 0 < ‖eval (circleMap 0 1 θ) p‖
hlogAe :
  ∀ᵐ (θ : ℝ) ∂Measure.restrict volume (uIoc 0 (2 * π)),
    rexp (log ‖eval (circleMap 0 1 θ) p‖) = ‖eval (circleMap 0 1 θ) p‖
hcont : Continuous (Y := ℝ) fun (x : ℝ) ↦ ‖eval (circleMap 0 1 x) p‖
⊢ ⨍ (θ : ℝ) in 0..2 * π, ‖eval (circleMap 0 1 θ) p‖ =
    √(HPow.hPow (α := ℝ) (β := ℕ) (⨍ (θ : ℝ) in 0..2 * π, ‖eval (circleMap 0 1 θ) p‖) 2)
have rw : LE.le (α := ℝ) 0 (⨍ (θ : ℝ) in 0..2 * π, ‖eval (circleMap 0 1 θ) p‖)
Tactic: rw [sqrt_sq]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
p : ℂ[X]
this_1 : IsFiniteMeasure (m0 := MeasureSpace.toMeasurableSpace) (Measure.restrict volume (uIoc 0 (2 * π)))
this_2 : NeZero (R := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (uIoc 0 (2 * π)) : ENNReal)
hp : p ≠ 0
this : ∀ᵐ (θ : ℝ) ∂Measure.restrict volume (uIoc 0 (2 * π)), 0 < ‖eval (circleMap 0 1 θ) p‖
hlogAe :
  ∀ᵐ (θ : ℝ) ∂Measure.restrict volume (uIoc 0 (2 * π)),
    rexp (log ‖eval (circleMap 0 1 θ) p‖) = ‖eval (circleMap 0 1 θ) p‖
hcont : Continuous (Y := ℝ) fun (x : ℝ) ↦ ‖eval (circleMap 0 1 x) p‖
⊢ √(HPow.hPow (α := ℝ) (β := ℕ) (⨍ (θ : ℝ) in 0..2 * π, ‖eval (circleMap 0 1 θ) p‖) 2) ≤
    √(⨍ (θ : ℝ) in 0..2 * π, HPow.hPow (β := ℕ) ‖eval (circleMap 0 1 θ) p‖ 2)
have a : HPow.hPow (α := ℝ) (β := ℕ) (⨍ (θ : ℝ) in 0..2 * π, ‖eval (circleMap 0 1 θ) p‖) 2 ≤
  ⨍ (θ : ℝ) in 0..2 * π, HPow.hPow (β := ℕ) ‖eval (circleMap 0 1 θ) p‖ 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
p : ℂ[X]
this_1 : IsFiniteMeasure (m0 := MeasureSpace.toMeasurableSpace) (Measure.restrict volume (uIoc 0 (2 * π)))
this_2 : NeZero (R := ENNReal) ((volume : (a : Set ℝ) → ENNReal) (uIoc 0 (2 * π)) : ENNReal)
hp : p ≠ 0
this : ∀ᵐ (θ : ℝ) ∂Measure.restrict volume (uIoc 0 (2 * π)), 0 < ‖eval (circleMap 0 1 θ) p‖
hlogAe :
  ∀ᵐ (θ : ℝ) ∂Measure.restrict volume (uIoc 0 (2 * π)),
    rexp (log ‖eval (circleMap 0 1 θ) p‖) = ‖eval (circleMap 0 1 θ) p‖
hcont : Continuous (Y := ℝ) fun (x : ℝ) ↦ ‖eval (circleMap 0 1 x) p‖
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict volume (uIoc 0 (2 * π)), Membership.mem (γ := Set ℝ) (Ici 0) ‖eval (circleMap 0 1 x) p‖
have h : ∀ (a : ℝ), Membership.mem (γ := Set ℝ) (Ici 0) ‖eval (circleMap 0 1 a) p‖
Tactic: filter_upwards