awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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 : @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (fun (θ : ℝ) ↦ ‖eval (circleMap 0 1 θ) p‖)
  (Measure.restrict volume (uIoc 0 (2 * π)))
Tactic: refine (convexOn_pow 2).map_average_le (continuousOn_pow 2)
            isClosed_Ici (by filter_upwards; 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‖
a :
  @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace (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
have a₁ : @Integrable ℝ _ _ _ MeasureSpace.toMeasurableSpace
  ((fun (x : ℝ) ↦ HPow.hPow (β := ℕ) x 2) ∘ fun (θ : ℝ) ↦ ‖eval (circleMap 0 1 θ) p‖)
  (Measure.restrict volume (uIoc 0 (2 * π)))
Tactic: refine (convexOn_pow 2).map_average_le (continuousOn_pow 2)
            isClosed_Ici (by filter_upwards; 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‖
⊢ rexp (⨍ (θ : ℝ) in 0..2 * π, log ‖eval (circleMap 0 1 θ) p‖) ≤ √(∑ i ∈ p.support, HPow.hPow (β := ℕ) ‖p.coeff i‖ 2)
have calc : rexp (⨍ (θ : ℝ) in 0..2 * π, log ‖eval (circleMap 0 1 θ) p‖) ≤
  ⨍ (θ : ℝ) in 0..2 * π, rexp (log ‖eval (circleMap 0 1 θ) p‖)
Tactic: calc exp (⨍ (θ : ℝ) in 0..(2 * π), log ‖p.eval (circleMap 0 1 θ)‖)
    ≤ ⨍ (θ : ℝ) in 0..(2 * π), exp (log ‖p.eval (circleMap 0 1 θ)‖) := by
        -- First Jensen's inequality invocation
        refine convexOn_exp.map_average_le continuousOn_exp isClosed_univ (by simp) ?_ ?_
        · rw [Set.uIoc_of_le (by positivity : 0 ≤ 2 * Real.pi)]
          exact ((analyticOnNhd_id.aeval_polynomial p).meromorphicOn.circleIntegrable_log_norm).1
        · exact (integrable_congr hlogAe).mpr hcont.integrableOn_uIoc
    _ = ⨍ (θ : ℝ) in 0..(2 * π), ‖p.eval (circleMap 0 1 θ)‖ := average_congr hlogAe
    _ = √((⨍ (θ : ℝ) in 0..(2 * π), ‖p.eval (circleMap 0 1 θ)‖) ^ 2) := by
        rw [sqrt_sq]; exact integral_nonneg (fun _ ↦ norm_nonneg _)
    _ ≤ √(⨍ (θ : ℝ) in 0..(2 * π), ‖p.eval (circleMap 0 1 θ)‖ ^ 2) := by
        -- Second Jensen's inequality invocation
        gcongr
        refine (convexOn_pow 2).map_average_le (continuousOn_pow 2)
            isClosed_Ici (by filter_upwards; simp) ?_ ?_
        · exact hcont.integrableOn_Icc.mono_set Set.Ioc_subset_Icc_self
        · exact ((continuous_pow 2).comp hcont).integrableOn_Icc.mono_set Set.Ioc_subset_Icc_self
    _ = √(circleAverage (fun θ ↦ ‖p.eval θ‖ ^ 2) 0 1) := by simp [circleAverage_eq_intervalAverage]
    _ = √(∑ i ∈ p.support, ‖p.coeff i‖ ^ 2) := by simp [p.sum_sq_norm_coeff_eq_circleAverage]
-- 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‖
calc :
  rexp (⨍ (θ : ℝ) in 0..2 * π, log ‖eval (circleMap 0 1 θ) p‖) ≤
    ⨍ (θ : ℝ) in 0..2 * π, rexp (log ‖eval (circleMap 0 1 θ) p‖)
⊢ rexp (⨍ (θ : ℝ) in 0..2 * π, log ‖eval (circleMap 0 1 θ) p‖) ≤ √(∑ i ∈ p.support, HPow.hPow (β := ℕ) ‖p.coeff i‖ 2)
have calc₁ : ⨍ (θ : ℝ) in 0..2 * π, ‖eval (circleMap 0 1 θ) p‖ =
  √(HPow.hPow (α := ℝ) (β := ℕ) (⨍ (θ : ℝ) in 0..2 * π, ‖eval (circleMap 0 1 θ) p‖) 2)
Tactic: calc exp (⨍ (θ : ℝ) in 0..(2 * π), log ‖p.eval (circleMap 0 1 θ)‖)
    ≤ ⨍ (θ : ℝ) in 0..(2 * π), exp (log ‖p.eval (circleMap 0 1 θ)‖) := by
        -- First Jensen's inequality invocation
        refine convexOn_exp.map_average_le continuousOn_exp isClosed_univ (by simp) ?_ ?_
        · rw [Set.uIoc_of_le (by positivity : 0 ≤ 2 * Real.pi)]
          exact ((analyticOnNhd_id.aeval_polynomial p).meromorphicOn.circleIntegrable_log_norm).1
        · exact (integrable_congr hlogAe).mpr hcont.integrableOn_uIoc
    _ = ⨍ (θ : ℝ) in 0..(2 * π), ‖p.eval (circleMap 0 1 θ)‖ := average_congr hlogAe
    _ = √((⨍ (θ : ℝ) in 0..(2 * π), ‖p.eval (circleMap 0 1 θ)‖) ^ 2) := by
        rw [sqrt_sq]; exact integral_nonneg (fun _ ↦ norm_nonneg _)
    _ ≤ √(⨍ (θ : ℝ) in 0..(2 * π), ‖p.eval (circleMap 0 1 θ)‖ ^ 2) := by
        -- Second Jensen's inequality invocation
        gcongr
        refine (convexOn_pow 2).map_average_le (continuousOn_pow 2)
            isClosed_Ici (by filter_upwards; simp) ?_ ?_
        · exact hcont.integrableOn_Icc.mono_set Set.Ioc_subset_Icc_self
        · exact ((continuous_pow 2).comp hcont).integrableOn_Icc.mono_set Set.Ioc_subset_Icc_self
    _ = √(circleAverage (fun θ ↦ ‖p.eval θ‖ ^ 2) 0 1) := by simp [circleAverage_eq_intervalAverage]
    _ = √(∑ i ∈ p.support, ‖p.coeff i‖ ^ 2) := by simp [p.sum_sq_norm_coeff_eq_circleAverage]
-- 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‖
calc :
  rexp (⨍ (θ : ℝ) in 0..2 * π, log ‖eval (circleMap 0 1 θ) p‖) ≤
    ⨍ (θ : ℝ) in 0..2 * π, rexp (log ‖eval (circleMap 0 1 θ) p‖)
calc₁ :
  ⨍ (θ : ℝ) in 0..2 * π, ‖eval (circleMap 0 1 θ) p‖ =
    √(HPow.hPow (α := ℝ) (β := ℕ) (⨍ (θ : ℝ) in 0..2 * π, ‖eval (circleMap 0 1 θ) p‖) 2)
⊢ rexp (⨍ (θ : ℝ) in 0..2 * π, log ‖eval (circleMap 0 1 θ) p‖) ≤ √(∑ i ∈ p.support, HPow.hPow (β := ℕ) ‖p.coeff i‖ 2)
have calc₂ : √(HPow.hPow (α := ℝ) (β := ℕ) (⨍ (θ : ℝ) in 0..2 * π, ‖eval (circleMap 0 1 θ) p‖) 2) ≤
  √(⨍ (θ : ℝ) in 0..2 * π, HPow.hPow (β := ℕ) ‖eval (circleMap 0 1 θ) p‖ 2)
Tactic: calc exp (⨍ (θ : ℝ) in 0..(2 * π), log ‖p.eval (circleMap 0 1 θ)‖)
    ≤ ⨍ (θ : ℝ) in 0..(2 * π), exp (log ‖p.eval (circleMap 0 1 θ)‖) := by
        -- First Jensen's inequality invocation
        refine convexOn_exp.map_average_le continuousOn_exp isClosed_univ (by simp) ?_ ?_
        · rw [Set.uIoc_of_le (by positivity : 0 ≤ 2 * Real.pi)]
          exact ((analyticOnNhd_id.aeval_polynomial p).meromorphicOn.circleIntegrable_log_norm).1
        · exact (integrable_congr hlogAe).mpr hcont.integrableOn_uIoc
    _ = ⨍ (θ : ℝ) in 0..(2 * π), ‖p.eval (circleMap 0 1 θ)‖ := average_congr hlogAe
    _ = √((⨍ (θ : ℝ) in 0..(2 * π), ‖p.eval (circleMap 0 1 θ)‖) ^ 2) := by
        rw [sqrt_sq]; exact integral_nonneg (fun _ ↦ norm_nonneg _)
    _ ≤ √(⨍ (θ : ℝ) in 0..(2 * π), ‖p.eval (circleMap 0 1 θ)‖ ^ 2) := by
        -- Second Jensen's inequality invocation
        gcongr
        refine (convexOn_pow 2).map_average_le (continuousOn_pow 2)
            isClosed_Ici (by filter_upwards; simp) ?_ ?_
        · exact hcont.integrableOn_Icc.mono_set Set.Ioc_subset_Icc_self
        · exact ((continuous_pow 2).comp hcont).integrableOn_Icc.mono_set Set.Ioc_subset_Icc_self
    _ = √(circleAverage (fun θ ↦ ‖p.eval θ‖ ^ 2) 0 1) := by simp [circleAverage_eq_intervalAverage]
    _ = √(∑ i ∈ p.support, ‖p.coeff i‖ ^ 2) := by simp [p.sum_sq_norm_coeff_eq_circleAverage]
-- 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‖
calc :
  rexp (⨍ (θ : ℝ) in 0..2 * π, log ‖eval (circleMap 0 1 θ) p‖) ≤
    ⨍ (θ : ℝ) in 0..2 * π, rexp (log ‖eval (circleMap 0 1 θ) p‖)
calc₁ :
  ⨍ (θ : ℝ) in 0..2 * π, ‖eval (circleMap 0 1 θ) p‖ =
    √(HPow.hPow (α := ℝ) (β := ℕ) (⨍ (θ : ℝ) in 0..2 * π, ‖eval (circleMap 0 1 θ) p‖) 2)
calc₂ :
  √(HPow.hPow (α := ℝ) (β := ℕ) (⨍ (θ : ℝ) in 0..2 * π, ‖eval (circleMap 0 1 θ) p‖) 2) ≤
    √(⨍ (θ : ℝ) in 0..2 * π, HPow.hPow (β := ℕ) ‖eval (circleMap 0 1 θ) p‖ 2)
⊢ rexp (⨍ (θ : ℝ) in 0..2 * π, log ‖eval (circleMap 0 1 θ) p‖) ≤ √(∑ i ∈ p.support, HPow.hPow (β := ℕ) ‖p.coeff i‖ 2)
have calc₃ : √(⨍ (θ : ℝ) in 0..2 * π, HPow.hPow (β := ℕ) ‖eval (circleMap 0 1 θ) p‖ 2) =
  √(circleAverage (fun (θ : ℂ) ↦ HPow.hPow (β := ℕ) ‖eval θ p‖ 2) 0 1)
Tactic: calc exp (⨍ (θ : ℝ) in 0..(2 * π), log ‖p.eval (circleMap 0 1 θ)‖)
    ≤ ⨍ (θ : ℝ) in 0..(2 * π), exp (log ‖p.eval (circleMap 0 1 θ)‖) := by
        -- First Jensen's inequality invocation
        refine convexOn_exp.map_average_le continuousOn_exp isClosed_univ (by simp) ?_ ?_
        · rw [Set.uIoc_of_le (by positivity : 0 ≤ 2 * Real.pi)]
          exact ((analyticOnNhd_id.aeval_polynomial p).meromorphicOn.circleIntegrable_log_norm).1
        · exact (integrable_congr hlogAe).mpr hcont.integrableOn_uIoc
    _ = ⨍ (θ : ℝ) in 0..(2 * π), ‖p.eval (circleMap 0 1 θ)‖ := average_congr hlogAe
    _ = √((⨍ (θ : ℝ) in 0..(2 * π), ‖p.eval (circleMap 0 1 θ)‖) ^ 2) := by
        rw [sqrt_sq]; exact integral_nonneg (fun _ ↦ norm_nonneg _)
    _ ≤ √(⨍ (θ : ℝ) in 0..(2 * π), ‖p.eval (circleMap 0 1 θ)‖ ^ 2) := by
        -- Second Jensen's inequality invocation
        gcongr
        refine (convexOn_pow 2).map_average_le (continuousOn_pow 2)
            isClosed_Ici (by filter_upwards; simp) ?_ ?_
        · exact hcont.integrableOn_Icc.mono_set Set.Ioc_subset_Icc_self
        · exact ((continuous_pow 2).comp hcont).integrableOn_Icc.mono_set Set.Ioc_subset_Icc_self
    _ = √(circleAverage (fun θ ↦ ‖p.eval θ‖ ^ 2) 0 1) := by simp [circleAverage_eq_intervalAverage]
    _ = √(∑ i ∈ p.support, ‖p.coeff i‖ ^ 2) := by simp [p.sum_sq_norm_coeff_eq_circleAverage]
-- 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‖
calc :
  rexp (⨍ (θ : ℝ) in 0..2 * π, log ‖eval (circleMap 0 1 θ) p‖) ≤
    ⨍ (θ : ℝ) in 0..2 * π, rexp (log ‖eval (circleMap 0 1 θ) p‖)
calc₁ :
  ⨍ (θ : ℝ) in 0..2 * π, ‖eval (circleMap 0 1 θ) p‖ =
    √(HPow.hPow (α := ℝ) (β := ℕ) (⨍ (θ : ℝ) in 0..2 * π, ‖eval (circleMap 0 1 θ) p‖) 2)
calc₂ :
  √(HPow.hPow (α := ℝ) (β := ℕ) (⨍ (θ : ℝ) in 0..2 * π, ‖eval (circleMap 0 1 θ) p‖) 2) ≤
    √(⨍ (θ : ℝ) in 0..2 * π, HPow.hPow (β := ℕ) ‖eval (circleMap 0 1 θ) p‖ 2)
calc₃ :
  √(⨍ (θ : ℝ) in 0..2 * π, HPow.hPow (β := ℕ) ‖eval (circleMap 0 1 θ) p‖ 2) =
    √(circleAverage (fun (θ : ℂ) ↦ HPow.hPow (β := ℕ) ‖eval θ p‖ 2) 0 1)
⊢ rexp (⨍ (θ : ℝ) in 0..2 * π, log ‖eval (circleMap 0 1 θ) p‖) ≤ √(∑ i ∈ p.support, HPow.hPow (β := ℕ) ‖p.coeff i‖ 2)
have calc₄ : √(circleAverage (fun (θ : ℂ) ↦ HPow.hPow (β := ℕ) ‖eval θ p‖ 2) 0 1) =
  √(∑ i ∈ p.support, HPow.hPow (β := ℕ) ‖p.coeff i‖ 2)
Tactic: calc exp (⨍ (θ : ℝ) in 0..(2 * π), log ‖p.eval (circleMap 0 1 θ)‖)
    ≤ ⨍ (θ : ℝ) in 0..(2 * π), exp (log ‖p.eval (circleMap 0 1 θ)‖) := by
        -- First Jensen's inequality invocation
        refine convexOn_exp.map_average_le continuousOn_exp isClosed_univ (by simp) ?_ ?_
        · rw [Set.uIoc_of_le (by positivity : 0 ≤ 2 * Real.pi)]
          exact ((analyticOnNhd_id.aeval_polynomial p).meromorphicOn.circleIntegrable_log_norm).1
        · exact (integrable_congr hlogAe).mpr hcont.integrableOn_uIoc
    _ = ⨍ (θ : ℝ) in 0..(2 * π), ‖p.eval (circleMap 0 1 θ)‖ := average_congr hlogAe
    _ = √((⨍ (θ : ℝ) in 0..(2 * π), ‖p.eval (circleMap 0 1 θ)‖) ^ 2) := by
        rw [sqrt_sq]; exact integral_nonneg (fun _ ↦ norm_nonneg _)
    _ ≤ √(⨍ (θ : ℝ) in 0..(2 * π), ‖p.eval (circleMap 0 1 θ)‖ ^ 2) := by
        -- Second Jensen's inequality invocation
        gcongr
        refine (convexOn_pow 2).map_average_le (continuousOn_pow 2)
            isClosed_Ici (by filter_upwards; simp) ?_ ?_
        · exact hcont.integrableOn_Icc.mono_set Set.Ioc_subset_Icc_self
        · exact ((continuous_pow 2).comp hcont).integrableOn_Icc.mono_set Set.Ioc_subset_Icc_self
    _ = √(circleAverage (fun θ ↦ ‖p.eval θ‖ ^ 2) 0 1) := by simp [circleAverage_eq_intervalAverage]
    _ = √(∑ i ∈ p.support, ‖p.coeff i‖ ^ 2) := by simp [p.sum_sq_norm_coeff_eq_circleAverage]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
p : ℂ[X]
⊢ √(HAdd.hAdd (α := ℝ) (↑p.natDegree : ℝ) 1) * p.supNorm =
    √(HAdd.hAdd (α := ℝ) (↑p.natDegree : ℝ) 1 * HPow.hPow (β := ℕ) p.supNorm 2)
have rw : √(HAdd.hAdd (α := ℝ) (↑p.natDegree : ℝ) 1) * p.supNorm =
  √(HAdd.hAdd (α := ℝ) (↑p.natDegree : ℝ) 1) * √(HPow.hPow (β := ℕ) p.supNorm 2)
Tactic: rw [Real.sqrt_mul (by positivity), Real.sqrt_sq p.supNorm_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
p : ℂ[X]
rw :
  √(HAdd.hAdd (α := ℝ) (↑p.natDegree : ℝ) 1) * p.supNorm =
    √(HAdd.hAdd (α := ℝ) (↑p.natDegree : ℝ) 1) * √(HPow.hPow (β := ℕ) p.supNorm 2)
⊢ √(HAdd.hAdd (α := ℝ) (↑p.natDegree : ℝ) 1) * p.supNorm =
    √(HAdd.hAdd (α := ℝ) (↑p.natDegree : ℝ) 1 * HPow.hPow (β := ℕ) p.supNorm 2)
have rw₁ : √(HAdd.hAdd (α := ℝ) (↑p.natDegree : ℝ) 1) * p.supNorm = √(HAdd.hAdd (α := ℝ) (↑p.natDegree : ℝ) 1) * p.supNorm
Tactic: rw [Real.sqrt_mul (by positivity), Real.sqrt_sq p.supNorm_nonneg]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
p : ℂ[X]
⊢ √(∑ i ∈ p.support, HPow.hPow (β := ℕ) ‖p.coeff i‖ 2) ≤ √(HAdd.hAdd (α := ℝ) (↑p.natDegree : ℝ) 1) * p.supNorm
have rw : √(∑ i ∈ p.support, HPow.hPow (β := ℕ) ‖p.coeff i‖ 2) ≤
  √(HAdd.hAdd (α := ℝ) (↑p.natDegree : ℝ) 1 * HPow.hPow (β := ℕ) p.supNorm 2)
Tactic: rw [show √(↑(p.natDegree) + 1) * p.supNorm = √((p.natDegree + 1) * p.supNorm ^ 2) from by
      rw [Real.sqrt_mul (by positivity), Real.sqrt_sq p.supNorm_nonneg]]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
p : ℂ[X]
⊢ √(∑ i ∈ p.support, HPow.hPow (β := ℕ) ‖p.coeff i‖ 2) ≤
    √(HAdd.hAdd (α := ℝ) (↑p.natDegree : ℝ) 1 * HPow.hPow (β := ℕ) p.supNorm 2)
have a : ∑ i ∈ p.support, HPow.hPow (β := ℕ) ‖p.coeff i‖ 2 ≤
  HAdd.hAdd (α := ℝ) (↑p.natDegree : ℝ) 1 * HPow.hPow (β := ℕ) p.supNorm 2
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
p : ℂ[X]
⊢ ∑ i ∈ p.support, HPow.hPow (β := ℕ) ‖p.coeff i‖ 2 ≤
    HAdd.hAdd (α := ℝ) (↑p.natDegree : ℝ) 1 * HPow.hPow (β := ℕ) p.supNorm 2
have a : ∀ i ∈ p.support, HPow.hPow (β := ℕ) ‖p.coeff i‖ 2 ≤ HPow.hPow (β := ℕ) p.supNorm 2
Tactic: refine (p.support.sum_le_card_nsmul _ (p.supNorm ^ 2) fun i _ ↦ ?_).trans ?_
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
p : ℂ[X]
a : ∀ i ∈ p.support, HPow.hPow (β := ℕ) ‖p.coeff i‖ 2 ≤ HPow.hPow (β := ℕ) p.supNorm 2
⊢ ∑ i ∈ p.support, HPow.hPow (β := ℕ) ‖p.coeff i‖ 2 ≤
    HAdd.hAdd (α := ℝ) (↑p.natDegree : ℝ) 1 * HPow.hPow (β := ℕ) p.supNorm 2
have a₁ : p.support.card • HPow.hPow (β := ℕ) p.supNorm 2 ≤
  HAdd.hAdd (α := ℝ) (↑p.natDegree : ℝ) 1 * HPow.hPow (β := ℕ) p.supNorm 2
Tactic: refine (p.support.sum_le_card_nsmul _ (p.supNorm ^ 2) fun i _ ↦ ?_).trans ?_
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
p : ℂ[X]
i : ℕ
h : i ∈ p.support
⊢ HPow.hPow (β := ℕ) ‖p.coeff i‖ 2 ≤ HPow.hPow (β := ℕ) p.supNorm 2
have a : ‖p.coeff i‖ ≤ p.supNorm
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
p : ℂ[X]
⊢ p.support.card • HPow.hPow (β := ℕ) p.supNorm 2 ≤
    HAdd.hAdd (α := ℝ) (↑p.natDegree : ℝ) 1 * HPow.hPow (β := ℕ) p.supNorm 2
have a : (↑p.support.card : ℝ) * HPow.hPow (β := ℕ) p.supNorm 2 ≤
  HAdd.hAdd (α := ℝ) (↑p.natDegree : ℝ) 1 * HPow.hPow (β := ℕ) p.supNorm 2
Tactic: simp only [nsmul_eq_mul]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
p : ℂ[X]
⊢ (↑p.support.card : ℝ) * HPow.hPow (β := ℕ) p.supNorm 2 ≤
    HAdd.hAdd (α := ℝ) (↑p.natDegree : ℝ) 1 * HPow.hPow (β := ℕ) p.supNorm 2
have a : (↑p.support.card : ℝ) ≤ HAdd.hAdd (α := ℝ) (↑p.natDegree : ℝ) 1
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
n : ℕ
p : ℂ[X]
⊢ ‖p.coeff n‖ ≤ (↑(p.natDegree.choose n) : ℝ) * p.mahlerMeasure
have pos : ∀ (hp : p = 0), ‖p.coeff n‖ ≤ (↑(p.natDegree.choose n) : ℝ) * p.mahlerMeasure
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
n : ℕ
p : ℂ[X]
pos : ∀ (hp : p = 0), ‖p.coeff n‖ ≤ (↑(p.natDegree.choose n) : ℝ) * p.mahlerMeasure
⊢ ‖p.coeff n‖ ≤ (↑(p.natDegree.choose n) : ℝ) * p.mahlerMeasure
have neg : ∀ (hp : ¬p = 0), ‖p.coeff n‖ ≤ (↑(p.natDegree.choose n) : ℝ) * p.mahlerMeasure
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
n : ℕ
p : ℂ[X]
hp : ¬p = 0
⊢ ‖p.coeff n‖ ≤ (↑(p.natDegree.choose n) : ℝ) * p.mahlerMeasure
have neg : ∀ (hlt : p.natDegree < n), ‖p.coeff n‖ ≤ (↑(p.natDegree.choose n) : ℝ) * p.mahlerMeasure
Tactic: rcases lt_or_ge p.natDegree n with hlt | hn
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
n : ℕ
p : ℂ[X]
hp : ¬p = 0
neg : ∀ (hlt : p.natDegree < n), ‖p.coeff n‖ ≤ (↑(p.natDegree.choose n) : ℝ) * p.mahlerMeasure
⊢ ‖p.coeff n‖ ≤ (↑(p.natDegree.choose n) : ℝ) * p.mahlerMeasure
have neg₁ : ∀ (hn : n ≤ p.natDegree), ‖p.coeff n‖ ≤ (↑(p.natDegree.choose n) : ℝ) * p.mahlerMeasure
Tactic: rcases lt_or_ge p.natDegree n with hlt | hn
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
n : ℕ
p : ℂ[X]
hp : ¬p = 0
hn : n ≤ p.natDegree
⊢ ‖p.coeff n‖ ≤ (↑(p.natDegree.choose n) : ℝ) * p.mahlerMeasure
have neg : Norm.norm (E := ℂ)
    (∑ m ∈ (powersetCard (p.natDegree - n) p.roots).toFinset,
      count m (powersetCard (p.natDegree - n) p.roots) • m.prod) ≤
  HMul.hMul (α := ℝ) (↑(p.natDegree.choose n) : ℝ) (prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots))
Tactic: rw [mahlerMeasure_eq_leadingCoeff_mul_prod_roots, mul_left_comm,
    coeff_eq_esymm_roots_of_card (splits_iff_card_roots.mp (IsAlgClosed.splits p)) hn, mul_assoc,
    norm_mul, norm_mul, norm_pow, norm_neg, norm_one, one_pow, one_mul,
    mul_le_mul_iff_right₀ (by simp [leadingCoeff_ne_zero.mpr hp]), esymm,
    Finset.sum_multiset_map_count]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
n : ℕ
p : ℂ[X]
hp : ¬p = 0
hn : n ≤ p.natDegree
⊢ Norm.norm (E := ℂ)
      (∑ m ∈ (powersetCard (p.natDegree - n) p.roots).toFinset,
        count m (powersetCard (p.natDegree - n) p.roots) • m.prod) ≤
    HMul.hMul (α := ℝ) (↑(p.natDegree.choose n) : ℝ) (prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots))
have neg : ∑ i ∈ (powersetCard (p.natDegree - n) p.roots).toFinset, ‖count i (powersetCard (p.natDegree - n) p.roots) • i.prod‖ ≤
  HMul.hMul (α := ℝ) (↑(p.natDegree.choose n) : ℝ) (prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots))
Tactic: apply le_trans <| norm_sum_le _ _
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
n : ℕ
p : ℂ[X]
hp : ¬p = 0
hn : n ≤ p.natDegree
⊢ ∑ i ∈ (powersetCard (p.natDegree - n) p.roots).toFinset, ‖count i (powersetCard (p.natDegree - n) p.roots) • i.prod‖ ≤
    HMul.hMul (α := ℝ) (↑(p.natDegree.choose n) : ℝ) (prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots))
have neg : ∑ x ∈ (powersetCard (p.natDegree - n) p.roots).toFinset,
    (↑(count x (powersetCard (p.natDegree - n) p.roots)) : ℝ) * ‖x.prod‖ ≤
  HMul.hMul (α := ℝ) (↑(p.natDegree.choose n) : ℝ) (prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots))
Tactic: simp_rw [nsmul_eq_mul, norm_mul, _root_.norm_natCast]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (hypothesis)
Goal:
n : ℕ
p : ℂ[X]
hp : ¬p = 0
hn : n ≤ p.natDegree
S : Multiset (Multiset ℂ) := powersetCard (p.natDegree - n) p.roots
x : Multiset ℂ
hx : x ∈ S.toFinset
⊢ LE.le (α := ℝ) (∏ x_1 ∈ x.toFinset, ‖x_1‖ ^ count x_1 x) (∏ m ∈ p.roots.toFinset, max 1 ‖m‖ ^ count m p.roots)
have hx₁ : x ≤ p.roots ∧ x.card = p.natDegree - n
Tactic: rw [mem_toFinset, mem_powersetCard] at hx
Cleared hypotheses: hx
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
n : ℕ
p : ℂ[X]
hp : ¬p = 0
hn : n ≤ p.natDegree
S : Multiset (Multiset ℂ) := powersetCard (p.natDegree - n) p.roots
x : Multiset ℂ
hx : x ≤ p.roots ∧ x.card = p.natDegree - n
⊢ LE.le (α := ℝ) (∏ z ∈ x.toFinset, ‖z‖ ^ count z x) (∏ z ∈ x.toFinset, max 1 ‖z‖ ^ count z x)
have h1 : ∀ a ∈ x.toFinset, ‖a‖ ≤ max 1 ‖a‖
Tactic: gcongr with a
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
n : ℕ
p : ℂ[X]
hp : ¬p = 0
hn : n ≤ p.natDegree
S : Multiset (Multiset ℂ) := powersetCard (p.natDegree - n) p.roots
x : Multiset ℂ
hx : x ≤ p.roots ∧ x.card = p.natDegree - n
⊢ LE.le (α := ℝ) (∏ x_1 ∈ x.toFinset, max 1 (↑‖x_1‖₊ : ℝ) ^ count x_1 x)
    (∏ x_1 ∈ p.roots.toFinset, max 1 (↑‖x_1‖₊ : ℝ) ^ count x_1 x)
have norm_cast : LE.le (α := NNReal) (∏ x_1 ∈ x.toFinset, max 1 ‖x_1‖₊ ^ count x_1 x)
  (∏ x_1 ∈ p.roots.toFinset, max 1 ‖x_1‖₊ ^ count x_1 x)
Tactic: norm_cast
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
n : ℕ
p : ℂ[X]
hp : ¬p = 0
hn : n ≤ p.natDegree
S : Multiset (Multiset ℂ) := powersetCard (p.natDegree - n) p.roots
x : Multiset ℂ
hx : x ≤ p.roots ∧ x.card = p.natDegree - n
⊢ LE.le (α := ℝ) (∏ z ∈ p.roots.toFinset, max 1 ‖z‖ ^ count z x) (∏ z ∈ p.roots.toFinset, max 1 ‖z‖ ^ count z p.roots)
have h1 : ∀ a ∈ p.roots.toFinset, 1 ≤ max 1 ‖a‖
Tactic: gcongr with a