awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
⊢ ∀ᵐ (θ : ℝ) ∂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])
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
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‖
h : ∀ (θ : ℝ) (hθ : 0 < ‖eval (circleMap 0 1 θ) p‖), rexp (log ‖eval (circleMap 0 1 θ) p‖) = ‖eval (circleMap 0 1 θ) p‖
⊢ ∀ᵐ (θ : ℝ) ∂Measure.restrict volume (uIoc 0 (2 * π)),
    rexp (log ‖eval (circleMap 0 1 θ) p‖) = ‖eval (circleMap 0 1 θ) p‖

Tactic:
filter_upwards [this] with θ hθ
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
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‖
θ : ℝ
hθ : 0 < ‖eval (circleMap 0 1 θ) p‖
⊢ rexp (log ‖eval (circleMap 0 1 θ) p‖) = ‖eval (circleMap 0 1 θ) p‖

Tactic:
exp_log hθ

Premises used: Real.exp_log
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
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‖
θ : ℝ
hθ : 0 < ‖eval (circleMap 0 1 θ) p‖
⊢ rexp (log ‖eval (circleMap 0 1 θ) p‖) = ‖eval (circleMap 0 1 θ) p‖

Tactic:
exact exp_log hθ

Premises used: Real.exp_log
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
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‖

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θ
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
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‖
⊢ Continuous (Y := ℝ) fun (x : ℝ) ↦ ‖eval (circleMap 0 1 x) p‖

Tactic:
fun_prop
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
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‖
⊢ 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
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
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‖
neg : rexp (circleAverage (fun (x : ℂ) ↦ log ‖eval x p‖) 0 1) ≤ √(∑ i ∈ p.support, HPow.hPow (β := ℕ) ‖p.coeff i‖ 2)
⊢ p.mahlerMeasure ≤ √(∑ i ∈ p.support, HPow.hPow (β := ℕ) ‖p.coeff i‖ 2)

Tactic:
simp only [mahlerMeasure, logMahlerMeasure, ne_eq, hp, not_false_eq_true, ↓reduceIte]

Premises used: ne_eq, Polynomial.mahlerMeasure, reduceIte, Polynomial.logMahlerMeasure, not_false_eq_true
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
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‖
neg :
  rexp (⨍ (θ : ℝ) in 0..2 * π, log ‖eval (circleMap 0 1 θ) p‖) ≤ √(∑ i ∈ p.support, HPow.hPow (β := ℕ) ‖p.coeff i‖ 2)
⊢ rexp (circleAverage (fun (x : ℂ) ↦ log ‖eval x p‖) 0 1) ≤ √(∑ i ∈ p.support, HPow.hPow (β := ℕ) ‖p.coeff i‖ 2)

Tactic:
rw [circleAverage_eq_intervalAverage]

Premises used: Real.circleAverage_eq_intervalAverage
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
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 ℝ) univ (log ‖eval (circleMap 0 1 x) p‖)

Tactic:
simp
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
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 * π)))
refine_2 :
  @Integrable _ _ _ _ MeasureSpace.toMeasurableSpace (rexp ∘ 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‖)

Tactic:
refine convexOn_exp.map_average_le continuousOn_exp isClosed_univ (by simp) ?_ ?_

Premises used: isClosed_univ, Real.continuousOn_exp, convexOn_exp, ConvexOn.map_average_le
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
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‖
⊢ 0 ≤ 2 * π

Tactic:
positivity
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
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 (Ioc 0 (2 * π)))
⊢ @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (θ : ℝ) ↦ log ‖eval (circleMap 0 1 θ) p‖)
    (Measure.restrict volume (uIoc 0 (2 * π)))

Tactic:
rw [Set.uIoc_of_le (by positivity : 0 ≤ 2 * Real.pi)]

Premises used: Set.uIoc_of_le
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
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 (Ioc 0 (2 * π)))

Tactic:
((analyticOnNhd_id.aeval_polynomial p).meromorphicOn.circleIntegrable_log_norm).1

Premises used: Polynomial.eval, MeasureTheory.IntegrableOn, MonoidHomClass.toMonoidHom, And.left, RingHomClass.toRingHom, MeromorphicOn.circleIntegrable_log_norm, AnalyticOnNhd.meromorphicOn
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
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 (Ioc 0 (2 * π)))

Tactic:
exact ((analyticOnNhd_id.aeval_polynomial p).meromorphicOn.circleIntegrable_log_norm).1

Premises used: And.left, MeromorphicOn.circleIntegrable_log_norm, AnalyticOnNhd.meromorphicOn
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
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 (rexp ∘ fun (θ : ℝ) ↦ log ‖eval (circleMap 0 1 θ) p‖)
    (Measure.restrict volume (uIoc 0 (2 * π)))

Tactic:
(integrable_congr hlogAe).mpr hcont.integrableOn_uIoc

Premises used: Iff.mpr, MeasureTheory.integrable_congr, Real.exp, Continuous.integrableOn_uIoc
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
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 (rexp ∘ fun (θ : ℝ) ↦ log ‖eval (circleMap 0 1 θ) p‖)
    (Measure.restrict volume (uIoc 0 (2 * π)))

Tactic:
exact (integrable_congr hlogAe).mpr hcont.integrableOn_uIoc

Premises used: Iff.mpr, MeasureTheory.integrable_congr, Continuous.integrableOn_uIoc
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
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‖
⊢ Eq (α := ℝ) (⨍ (θ : ℝ) in 0..2 * π, rexp (log ‖eval (circleMap 0 1 θ) p‖))
    (⨍ (θ : ℝ) in 0..2 * π, ‖eval (circleMap 0 1 θ) p‖)

Tactic:
average_congr hlogAe

Premises used: MeasureTheory.average_congr
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
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‖
rw : LE.le (α := ℝ) 0 (⨍ (θ : ℝ) in 0..2 * π, ‖eval (circleMap 0 1 θ) p‖)
⊢ ⨍ (θ : ℝ) in 0..2 * π, ‖eval (circleMap 0 1 θ) p‖ =
    √(HPow.hPow (α := ℝ) (β := ℕ) (⨍ (θ : ℝ) in 0..2 * π, ‖eval (circleMap 0 1 θ) p‖) 2)

Tactic:
rw [sqrt_sq]

Premises used: Real.sqrt_sq
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
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‖
⊢ LE.le (α := ℝ) 0 (⨍ (θ : ℝ) in 0..2 * π, ‖eval (circleMap 0 1 θ) p‖)

Tactic:
integral_nonneg (fun _ ↦ norm_nonneg _)

Premises used: Polynomial.eval, MeasureTheory.integral_nonneg, circleMap, MeasureTheory.average, OfNat.ofNat, norm_nonneg
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
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‖
⊢ LE.le (α := ℝ) 0 (⨍ (θ : ℝ) in 0..2 * π, ‖eval (circleMap 0 1 θ) p‖)

Tactic:
exact integral_nonneg (fun _ ↦ norm_nonneg _)

Premises used: MeasureTheory.integral_nonneg
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
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‖
a :
  HPow.hPow (α := ℝ) (β := ℕ) (⨍ (θ : ℝ) in 0..2 * π, ‖eval (circleMap 0 1 θ) p‖) 2 ≤
    ⨍ (θ : ℝ) in 0..2 * π, HPow.hPow (β := ℕ) ‖eval (circleMap 0 1 θ) p‖ 2
⊢ √(HPow.hPow (α := ℝ) (β := ℕ) (⨍ (θ : ℝ) in 0..2 * π, ‖eval (circleMap 0 1 θ) p‖) 2) ≤
    √(⨍ (θ : ℝ) in 0..2 * π, HPow.hPow (β := ℕ) ‖eval (circleMap 0 1 θ) p‖ 2)

Tactic:
gcongr
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
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‖
h : ∀ (a : ℝ), Membership.mem (γ := Set ℝ) (Ici 0) ‖eval (circleMap 0 1 a) p‖
⊢ ∀ᵐ (x : ℝ) ∂Measure.restrict volume (uIoc 0 (2 * π)), Membership.mem (γ := Set ℝ) (Ici 0) ‖eval (circleMap 0 1 x) p‖

Tactic:
filter_upwards
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
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‖
⊢ ∀ (a : ℝ), Membership.mem (γ := Set ℝ) (Ici 0) ‖eval (circleMap 0 1 a) p‖

Tactic:
simp
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
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‖
a :
  @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (θ : ℝ) ↦ ‖eval (circleMap 0 1 θ) p‖)
    (Measure.restrict volume (uIoc 0 (2 * π)))
a₁ :
  @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace
    ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2) ∘ fun (θ : ℝ) ↦ ‖eval (circleMap 0 1 θ) p‖)
    (Measure.restrict volume (uIoc 0 (2 * π)))
⊢ HPow.hPow (α := ℝ) (β := ℕ) (⨍ (θ : ℝ) in 0..2 * π, ‖eval (circleMap 0 1 θ) p‖) 2 ≤
    ⨍ (θ : ℝ) in 0..2 * π, HPow.hPow (β := ℕ) ‖eval (circleMap 0 1 θ) p‖ 2

Tactic:
refine (convexOn_pow 2).map_average_le (continuousOn_pow 2)
            isClosed_Ici (by filter_upwards; simp) ?_ ?_

Premises used: continuousOn_pow, convexOn_pow, ConvexOn.map_average_le, OfNat.ofNat, isClosed_Ici
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
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 (θ : ℝ) ↦ ‖eval (circleMap 0 1 θ) p‖)
    (Measure.restrict volume (uIoc 0 (2 * π)))

Tactic:
hcont.integrableOn_Icc.mono_set Set.Ioc_subset_Icc_self

Premises used: Set.Ioc_subset_Icc_self, MeasureTheory.IntegrableOn, MeasureTheory.IntegrableOn.mono_set, Continuous.integrableOn_Icc
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
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 (θ : ℝ) ↦ ‖eval (circleMap 0 1 θ) p‖)
    (Measure.restrict volume (uIoc 0 (2 * π)))

Tactic:
exact hcont.integrableOn_Icc.mono_set Set.Ioc_subset_Icc_self

Premises used: Set.Ioc_subset_Icc_self, MeasureTheory.IntegrableOn.mono_set, Continuous.integrableOn_Icc
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
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 (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2) ∘ fun (θ : ℝ) ↦ ‖eval (circleMap 0 1 θ) p‖)
    (Measure.restrict volume (uIoc 0 (2 * π)))

Tactic:
((continuous_pow 2).comp hcont).integrableOn_Icc.mono_set Set.Ioc_subset_Icc_self

Premises used: Continuous.comp, Set.Ioc_subset_Icc_self, MeasureTheory.IntegrableOn, MeasureTheory.IntegrableOn.mono_set, OfNat.ofNat, continuous_pow, Continuous.integrableOn_Icc
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
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 (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2) ∘ fun (θ : ℝ) ↦ ‖eval (circleMap 0 1 θ) p‖)
    (Measure.restrict volume (uIoc 0 (2 * π)))

Tactic:
exact ((continuous_pow 2).comp hcont).integrableOn_Icc.mono_set Set.Ioc_subset_Icc_self

Premises used: Continuous.comp, Set.Ioc_subset_Icc_self, MeasureTheory.IntegrableOn.mono_set, OfNat.ofNat, continuous_pow, Continuous.integrableOn_Icc