awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- 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
h1 : ∀ a ∈ p.roots.toFinset, 1 ≤ max 1 ‖a‖
⊢ 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, x ≤ p.roots
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, ‖x_1‖ ^ count x_1 x) (∏ m ∈ p.roots.toFinset, max 1 ‖m‖ ^ count m p.roots)
have z : LE.le (α := ℝ) (∏ z ∈ x.toFinset, ‖z‖ ^ count z x) (∏ z ∈ x.toFinset, max 1 ‖z‖ ^ count z x)
Tactic: calc
    ∏ z ∈ x.toFinset, ‖z‖ ^ count z x
      ≤ ∏ z ∈ x.toFinset, (1 ⊔ ‖z‖) ^ count z x := by
      gcongr with a
      exact le_max_right 1 ‖a‖
    _ ≤ ∏ z ∈ p.roots.toFinset, (1 ⊔ ‖z‖) ^ count z x := by
      simp_rw [← coe_nnnorm]
      norm_cast
      exact Finset.prod_le_prod_of_subset_of_one_le' (toFinset_subset.mpr (subset_of_le hx.1))
        (fun a _ _ ↦ one_le_pow₀ (le_max_left 1 ‖a‖))
    _ ≤ ∏ z ∈ p.roots.toFinset, (1 ⊔ ‖z‖) ^ count z p.roots := by
      gcongr with a
      · exact le_max_left 1 ‖a‖
      · exact hx.1
-- 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
z : LE.le (α := ℝ) (∏ z ∈ x.toFinset, ‖z‖ ^ count z x) (∏ z ∈ x.toFinset, max 1 ‖z‖ ^ count z x)
⊢ LE.le (α := ℝ) (∏ x_1 ∈ x.toFinset, ‖x_1‖ ^ count x_1 x) (∏ m ∈ p.roots.toFinset, max 1 ‖m‖ ^ count m p.roots)
have z₁ : LE.le (α := ℝ) (∏ z ∈ x.toFinset, max 1 ‖z‖ ^ count z x) (∏ z ∈ p.roots.toFinset, max 1 ‖z‖ ^ count z x)
Tactic: calc
    ∏ z ∈ x.toFinset, ‖z‖ ^ count z x
      ≤ ∏ z ∈ x.toFinset, (1 ⊔ ‖z‖) ^ count z x := by
      gcongr with a
      exact le_max_right 1 ‖a‖
    _ ≤ ∏ z ∈ p.roots.toFinset, (1 ⊔ ‖z‖) ^ count z x := by
      simp_rw [← coe_nnnorm]
      norm_cast
      exact Finset.prod_le_prod_of_subset_of_one_le' (toFinset_subset.mpr (subset_of_le hx.1))
        (fun a _ _ ↦ one_le_pow₀ (le_max_left 1 ‖a‖))
    _ ≤ ∏ z ∈ p.roots.toFinset, (1 ⊔ ‖z‖) ^ count z p.roots := by
      gcongr with a
      · exact le_max_left 1 ‖a‖
      · exact hx.1
-- 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
z : LE.le (α := ℝ) (∏ z ∈ x.toFinset, ‖z‖ ^ count z x) (∏ z ∈ x.toFinset, max 1 ‖z‖ ^ count z x)
z₁ : LE.le (α := ℝ) (∏ z ∈ x.toFinset, max 1 ‖z‖ ^ count z x) (∏ z ∈ p.roots.toFinset, max 1 ‖z‖ ^ count z x)
⊢ LE.le (α := ℝ) (∏ x_1 ∈ x.toFinset, ‖x_1‖ ^ count x_1 x) (∏ m ∈ p.roots.toFinset, max 1 ‖m‖ ^ count m p.roots)
have z₂ : LE.le (α := ℝ) (∏ z ∈ p.roots.toFinset, max 1 ‖z‖ ^ count z x) (∏ z ∈ p.roots.toFinset, max 1 ‖z‖ ^ count z p.roots)
Tactic: calc
    ∏ z ∈ x.toFinset, ‖z‖ ^ count z x
      ≤ ∏ z ∈ x.toFinset, (1 ⊔ ‖z‖) ^ count z x := by
      gcongr with a
      exact le_max_right 1 ‖a‖
    _ ≤ ∏ z ∈ p.roots.toFinset, (1 ⊔ ‖z‖) ^ count z x := by
      simp_rw [← coe_nnnorm]
      norm_cast
      exact Finset.prod_le_prod_of_subset_of_one_le' (toFinset_subset.mpr (subset_of_le hx.1))
        (fun a _ _ ↦ one_le_pow₀ (le_max_left 1 ‖a‖))
    _ ≤ ∏ z ∈ p.roots.toFinset, (1 ⊔ ‖z‖) ^ count z p.roots := by
      gcongr with a
      · exact le_max_left 1 ‖a‖
      · exact hx.1
-- 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 ∈ (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))
have this : ∀ (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)
Tactic: have (x : Multiset ℂ) (hx : x ∈ S.toFinset) : ∏ x_1 ∈ x.toFinset, ‖x_1‖ ^ count x_1 x
      ≤ ∏ m ∈ p.roots.toFinset, max 1 ‖m‖ ^ count m p.roots := by
    rw [mem_toFinset, mem_powersetCard] at hx
    calc
    ∏ z ∈ x.toFinset, ‖z‖ ^ count z x
      ≤ ∏ z ∈ x.toFinset, (1 ⊔ ‖z‖) ^ count z x := by
      gcongr with a
      exact le_max_right 1 ‖a‖
    _ ≤ ∏ z ∈ p.roots.toFinset, (1 ⊔ ‖z‖) ^ count z x := by
      simp_rw [← coe_nnnorm]
      norm_cast
      exact Finset.prod_le_prod_of_subset_of_one_le' (toFinset_subset.mpr (subset_of_le hx.1))
        (fun a _ _ ↦ one_le_pow₀ (le_max_left 1 ‖a‖))
    _ ≤ ∏ z ∈ p.roots.toFinset, (1 ⊔ ‖z‖) ^ count z p.roots := by
      gcongr with a
      · exact le_max_left 1 ‖a‖
      · exact hx.1
-- 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
this :
  ∀ (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)
⊢ LE.le (α := ℝ) (∑ x ∈ S.toFinset, (↑(count x S) : ℝ) * ‖x.prod‖)
    (∑ x ∈ S.toFinset, HMul.hMul (α := ℝ) (↑(count x S) : ℝ) (prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots)))
have h : ∀ (x : Multiset ℂ) (hx : x ∈ S.toFinset), ‖x.prod‖ ≤ prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots)
Tactic: gcongr with x 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
this :
  ∀ (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)
x : Multiset ℂ
hx : x ∈ S.toFinset
⊢ ‖x.prod‖ ≤ prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots)
have h : LE.le (α := ℝ) (∏ b ∈ x.toFinset, ‖b ^ count b x‖) (∏ m ∈ p.roots.toFinset, max 1 ‖m‖ ^ count m p.roots)
Tactic: rw [Finset.prod_multiset_map_count, Finset.prod_multiset_count, norm_prod]
-- 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
this :
  ∀ (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)
x : Multiset ℂ
hx : x ∈ S.toFinset
⊢ LE.le (α := ℝ) (∏ b ∈ x.toFinset, ‖b ^ count b x‖) (∏ m ∈ p.roots.toFinset, max 1 ‖m‖ ^ count m p.roots)
have h : LE.le (α := ℝ) (∏ x_1 ∈ x.toFinset, ‖x_1‖ ^ count x_1 x) (∏ m ∈ p.roots.toFinset, max 1 ‖m‖ ^ count m p.roots)
Tactic: simp_rw [norm_pow]
-- 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
this :
  ∀ (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)
⊢ ∑ x ∈ S.toFinset, HMul.hMul (α := ℝ) (↑(count x S) : ℝ) (prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots)) =
    HMul.hMul (α := ℝ) (↑(p.natDegree.choose n) : ℝ) (prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots))
have rw : HMul.hMul (α := ℝ) (∑ i ∈ S.toFinset, (↑(count i S) : ℝ)) (prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots)) =
  HMul.hMul (α := ℝ) (↑(p.natDegree.choose n) : ℝ) (prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots))
Tactic: rw [← Finset.sum_mul]
-- 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
this :
  ∀ (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)
⊢ HMul.hMul (α := ℝ) (∑ i ∈ S.toFinset, (↑(count i S) : ℝ)) (prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots)) =
    HMul.hMul (α := ℝ) (↑(p.natDegree.choose n) : ℝ) (prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots))
have e_a : Eq (α := ℝ) (∑ i ∈ S.toFinset, (↑(count i S) : ℝ)) (↑(p.natDegree.choose n) : ℝ)
Tactic: congr
-- 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
this :
  ∀ (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)
⊢ Eq (α := ℝ) (∑ i ∈ S.toFinset, (↑(count i S) : ℝ)) (↑(p.natDegree.choose n) : ℝ)
have e_a : ∑ x ∈ S.toFinset, count x S = p.natDegree.choose n
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
this :
  ∀ (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)
⊢ ∑ x ∈ S.toFinset, count x S = p.natDegree.choose n
have e_a : p.roots.card.choose (p.natDegree - n) = p.natDegree.choose (p.natDegree - n)
Tactic: simp only [mem_powersetCard, mem_toFinset, imp_self, implies_true, sum_count_eq_card,
        card_powersetCard, S, ← Nat.choose_symm hn]
-- 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
this :
  ∀ (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)
⊢ p.roots.card.choose (p.natDegree - n) = p.natDegree.choose (p.natDegree - n)
have e_a : p.roots.card = p.natDegree
Tactic: congr
-- 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
this :
  ∀ (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)
⊢ ∑ 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))
have calc : LE.le (α := ℝ) (∑ x ∈ S.toFinset, (↑(count x S) : ℝ) * ‖x.prod‖)
  (∑ x ∈ S.toFinset, HMul.hMul (α := ℝ) (↑(count x S) : ℝ) (prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots)))
Tactic: calc ∑ x ∈ S.toFinset, count x S * ‖x.prod‖
    _ ≤ ∑ x ∈ S.toFinset, count x S * ((p.roots).map (fun a ↦ max 1 ‖a‖)).prod := by
      gcongr with x hx
      rw [Finset.prod_multiset_map_count, Finset.prod_multiset_count, norm_prod]
      simp_rw [norm_pow]
      exact this x hx
    _ = p.natDegree.choose n * (p.roots.map (fun a ↦ 1 ⊔ ‖a‖)).prod := by
      rw [← Finset.sum_mul]
      congr
      norm_cast
      simp only [mem_powersetCard, mem_toFinset, imp_self, implies_true, sum_count_eq_card,
        card_powersetCard, S, ← Nat.choose_symm hn]
      congr
      exact splits_iff_card_roots.mp <| IsAlgClosed.splits p
-- 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
this :
  ∀ (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)
calc :
  LE.le (α := ℝ) (∑ x ∈ S.toFinset, (↑(count x S) : ℝ) * ‖x.prod‖)
    (∑ x ∈ S.toFinset, HMul.hMul (α := ℝ) (↑(count x S) : ℝ) (prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots)))
⊢ ∑ 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))
have calc₁ : ∑ x ∈ S.toFinset, HMul.hMul (α := ℝ) (↑(count x S) : ℝ) (prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots)) =
  HMul.hMul (α := ℝ) (↑(p.natDegree.choose n) : ℝ) (prod (Multiset.map (fun (a : ℂ) ↦ max 1 ‖a‖) p.roots))
Tactic: calc ∑ x ∈ S.toFinset, count x S * ‖x.prod‖
    _ ≤ ∑ x ∈ S.toFinset, count x S * ((p.roots).map (fun a ↦ max 1 ‖a‖)).prod := by
      gcongr with x hx
      rw [Finset.prod_multiset_map_count, Finset.prod_multiset_count, norm_prod]
      simp_rw [norm_pow]
      exact this x hx
    _ = p.natDegree.choose n * (p.roots.map (fun a ↦ 1 ⊔ ‖a‖)).prod := by
      rw [← Finset.sum_mul]
      congr
      norm_cast
      simp only [mem_powersetCard, mem_toFinset, imp_self, implies_true, sum_count_eq_card,
        card_powersetCard, S, ← Nat.choose_symm hn]
      congr
      exact splits_iff_card_roots.mp <| IsAlgClosed.splits p
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
p : ℂ[X]
⊢ p.supNorm ≤ (↑(p.natDegree.choose (p.natDegree / 2)) : ℝ) * p.mahlerMeasure
have obtain : ∀ (i : ℕ) (hi : p.supNorm = ‖p.coeff i‖), p.supNorm ≤ (↑(p.natDegree.choose (p.natDegree / 2)) : ℝ) * p.mahlerMeasure
Tactic: obtain ⟨i, hi⟩ := p.exists_eq_supNorm
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
n : ℕ
g h : ℂ[X]
hh : 1 ≤ h.mahlerMeasure
⊢ (↑(g.natDegree.choose n) : ℝ) * g.mahlerMeasure ≤ (↑(g.natDegree.choose n) : ℝ) * (g * h).mahlerMeasure
have hbc : g.mahlerMeasure ≤ (g * h).mahlerMeasure
Tactic: gcongr
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
n : ℕ
g h : ℂ[X]
hh : 1 ≤ h.mahlerMeasure
⊢ g.mahlerMeasure ≤ (g * h).mahlerMeasure
have hbc : g.mahlerMeasure ≤ g.mahlerMeasure * h.mahlerMeasure
Tactic: rw [mahlerMeasure_mul]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
A : Type u_2
inst : NormedRing A
p : A[X]
v : A →+* ℂ
hv : Isometry (α := A) (β := ℂ) (⇑v : (a : A) → ℂ)
⊢ ‖p.leadingCoeff‖ ≤ p.mapMahlerMeasure v
have pos : ∀ (hp : p.leadingCoeff = 0), ‖p.leadingCoeff‖ ≤ p.mapMahlerMeasure v
Tactic: by_cases hp : p.leadingCoeff = 0
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
A : Type u_2
inst : NormedRing A
p : A[X]
v : A →+* ℂ
hv : Isometry (α := A) (β := ℂ) (⇑v : (a : A) → ℂ)
pos : ∀ (hp : p.leadingCoeff = 0), ‖p.leadingCoeff‖ ≤ p.mapMahlerMeasure v
⊢ ‖p.leadingCoeff‖ ≤ p.mapMahlerMeasure v
have neg : ∀ (hp : ¬p.leadingCoeff = 0), ‖p.leadingCoeff‖ ≤ p.mapMahlerMeasure v
Tactic: by_cases hp : p.leadingCoeff = 0
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (hypothesis)
Goal:
A : Type u_2
inst : NormedRing A
p : A[X]
v : A →+* ℂ
hv : Isometry (α := A) (β := ℂ) (⇑v : (a : A) → ℂ)
hp : ¬p.leadingCoeff = 0
⊢ ‖p.leadingCoeff‖ ≤ p.mapMahlerMeasure v
have hv_ne : Ne (α := ℂ) ((v : (a : A) → ℂ) p.leadingCoeff : ℂ) (0 : ℂ)
Tactic: have hv_ne : v p.leadingCoeff ≠ 0 :=
      fun h ↦ hp <| hv.injective <| h.trans (map_zero _).symm
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (hypothesis)
Goal:
A : Type u_2
inst : NormedRing A
p : A[X]
v : A →+* ℂ
hv : Isometry (α := A) (β := ℂ) (⇑v : (a : A) → ℂ)
hp : ¬p.leadingCoeff = 0
hv_ne : Ne (α := ℂ) ((v : (a : A) → ℂ) p.leadingCoeff : ℂ) (0 : ℂ)
⊢ ‖p.leadingCoeff‖ ≤ p.mapMahlerMeasure v
have hv_norm : norm (E := ℂ) ((v : (a : A) → ℂ) p.leadingCoeff : ℂ) = ‖p.leadingCoeff‖
Tactic: have hv_norm : ‖v p.leadingCoeff‖ = ‖p.leadingCoeff‖ := hv.norm_map_of_map_zero (map_zero _) _
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
A : Type u_2
inst : NormedRing A
p : A[X]
v : A →+* ℂ
hv : Isometry (α := A) (β := ℂ) (⇑v : (a : A) → ℂ)
hp : ¬p.leadingCoeff = 0
hv_ne : Ne (α := ℂ) ((v : (a : A) → ℂ) p.leadingCoeff : ℂ) (0 : ℂ)
hv_norm : norm (E := ℂ) ((v : (a : A) → ℂ) p.leadingCoeff : ℂ) = ‖p.leadingCoeff‖
⊢ ‖p.leadingCoeff‖ ≤ p.mapMahlerMeasure v
have neg : norm (E := ℂ) ((v : (a : A) → ℂ) p.leadingCoeff : ℂ) ≤ p.mapMahlerMeasure v
Tactic: grw [← hv_norm, ← leadingCoeff_map_of_leadingCoeff_ne_zero v hv_ne,
      leadingCoeff_le_mahlerMeasure, mapMahlerMeasure]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
A : Type u_2
inst : NormedRing A
p : A[X]
v : A →+* ℂ
hv : Isometry (α := A) (β := ℂ) (⇑v : (a : A) → ℂ)
hp : ¬p.leadingCoeff = 0
hv_ne : Ne (α := ℂ) ((v : (a : A) → ℂ) p.leadingCoeff : ℂ) (0 : ℂ)
hv_norm : norm (E := ℂ) ((v : (a : A) → ℂ) p.leadingCoeff : ℂ) = ‖p.leadingCoeff‖
neg : norm (E := ℂ) ((v : (a : A) → ℂ) p.leadingCoeff : ℂ) ≤ p.mapMahlerMeasure v
⊢ ‖p.leadingCoeff‖ ≤ p.mapMahlerMeasure v
have neg₁ : ‖(map v p).leadingCoeff‖ ≤ p.mapMahlerMeasure v
Tactic: grw [← hv_norm, ← leadingCoeff_map_of_leadingCoeff_ne_zero v hv_ne,
      leadingCoeff_le_mahlerMeasure, mapMahlerMeasure]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
A : Type u_2
inst : NormedRing A
p : A[X]
v : A →+* ℂ
hv : Isometry (α := A) (β := ℂ) (⇑v : (a : A) → ℂ)
hp : ¬p.leadingCoeff = 0
hv_ne : Ne (α := ℂ) ((v : (a : A) → ℂ) p.leadingCoeff : ℂ) (0 : ℂ)
hv_norm : norm (E := ℂ) ((v : (a : A) → ℂ) p.leadingCoeff : ℂ) = ‖p.leadingCoeff‖
neg : norm (E := ℂ) ((v : (a : A) → ℂ) p.leadingCoeff : ℂ) ≤ p.mapMahlerMeasure v
neg₁ : ‖(map v p).leadingCoeff‖ ≤ p.mapMahlerMeasure v
⊢ ‖p.leadingCoeff‖ ≤ p.mapMahlerMeasure v
have neg₂ : (map v p).mahlerMeasure ≤ p.mapMahlerMeasure v
Tactic: grw [← hv_norm, ← leadingCoeff_map_of_leadingCoeff_ne_zero v hv_ne,
      leadingCoeff_le_mahlerMeasure, mapMahlerMeasure]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
A : Type u_2
inst : NormedRing A
p : A[X]
v : A →+* ℂ
hv : Isometry (α := A) (β := ℂ) (⇑v : (a : A) → ℂ)
hp : ¬p.leadingCoeff = 0
hv_ne : Ne (α := ℂ) ((v : (a : A) → ℂ) p.leadingCoeff : ℂ) (0 : ℂ)
hv_norm : norm (E := ℂ) ((v : (a : A) → ℂ) p.leadingCoeff : ℂ) = ‖p.leadingCoeff‖
neg : norm (E := ℂ) ((v : (a : A) → ℂ) p.leadingCoeff : ℂ) ≤ p.mapMahlerMeasure v
neg₁ : ‖(map v p).leadingCoeff‖ ≤ p.mapMahlerMeasure v
neg₂ : (map v p).mahlerMeasure ≤ p.mapMahlerMeasure v
⊢ ‖p.leadingCoeff‖ ≤ p.mapMahlerMeasure v
have neg₃ : (map v p).mahlerMeasure ≤ (map v p).mahlerMeasure
Tactic: grw [← hv_norm, ← leadingCoeff_map_of_leadingCoeff_ne_zero v hv_ne,
      leadingCoeff_le_mahlerMeasure, mapMahlerMeasure]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
A : Type u_2
inst : NormedRing A
p : A[X]
v : A →+* ℂ
inst_1 : NormOneClass A
hv : Isometry (α := A) (β := ℂ) (⇑v : (a : A) → ℂ)
hp : p.Monic
⊢ 1 ≤ p.mapMahlerMeasure v
have grw : 1 ≤ ‖p.leadingCoeff‖
Tactic: grw [← p.leadingCoeff_le_mapMahlerMeasure v hv, hp.leadingCoeff, norm_one]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
A : Type u_2
inst : NormedRing A
p : A[X]
v : A →+* ℂ
inst_1 : NormOneClass A
hv : Isometry (α := A) (β := ℂ) (⇑v : (a : A) → ℂ)
hp : p.Monic
grw : 1 ≤ ‖p.leadingCoeff‖
⊢ 1 ≤ p.mapMahlerMeasure v
have grw₁ : 1 ≤ norm.{u_2} (E := A) 1
Tactic: grw [← p.leadingCoeff_le_mapMahlerMeasure v hv, hp.leadingCoeff, norm_one]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
A : Type u_2
inst : NormedRing A
p : A[X]
v : A →+* ℂ
inst_1 : NormOneClass A
hv : Isometry (α := A) (β := ℂ) (⇑v : (a : A) → ℂ)
hp : p.Monic
grw : 1 ≤ ‖p.leadingCoeff‖
grw₁ : 1 ≤ norm.{u_2} (E := A) 1
⊢ 1 ≤ p.mapMahlerMeasure v
have grw₂ : LE.le (α := ℝ) 1 1
Tactic: grw [← p.leadingCoeff_le_mapMahlerMeasure v hv, hp.leadingCoeff, norm_one]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
A : Type u_2
inst : NormedRing A
p : A[X]
v : A →+* ℂ
hv : Isometry (α := A) (β := ℂ) (⇑v : (a : A) → ℂ)
⊢ p.mapMahlerMeasure v ≤ p.sum fun (x : ℕ) (a : A) ↦ ‖a‖
have apply : Eq (α := ℝ) ((map v p).sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖) (p.sum fun (x : ℕ) (a : A) ↦ ‖a‖)
Tactic: apply mahlerMeasure_le_sum_norm_coeff _ |>.trans_eq
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
A : Type u_2
inst : NormedRing A
p : A[X]
v : A →+* ℂ
hv : Isometry (α := A) (β := ℂ) (⇑v : (a : A) → ℂ)
⊢ Eq (α := ℝ) ((map v p).sum fun (x : ℕ) (a : ℂ) ↦ ‖a‖) (p.sum fun (x : ℕ) (a : A) ↦ ‖a‖)
have rw : Eq (α := ℝ) (∑ n ∈ p.support, ‖(map v p).coeff n‖) (∑ n ∈ p.support, ‖p.coeff n‖)
Tactic: rw [sum_def, sum_def, support_map_of_injective _ hv.injective]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (hypothesis)
Goal:
A : Type u_2
inst : NormedRing A
v : A →+* ℂ
hv : Isometry (α := A) (β := ℂ) (⇑v : (a : A) → ℂ)
n : ℕ
p : A[X]
⊢ ‖p.coeff n‖ ≤ (↑(p.natDegree.choose n) : ℝ) * p.mapMahlerMeasure v
have hv_norm : ‖p.coeff n‖ = norm (E := ℂ) ((v : (a : A) → ℂ) (p.coeff n) : ℂ)
Tactic: have hv_norm : ‖p.coeff n‖ = ‖v (p.coeff n)‖ :=
    (hv.norm_map_of_map_zero (map_zero _) _).symm
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (hypothesis)
Goal:
A : Type u_2
inst : NormedRing A
v : A →+* ℂ
hv : Isometry (α := A) (β := ℂ) (⇑v : (a : A) → ℂ)
n : ℕ
p : A[X]
hv_norm : ‖p.coeff n‖ = norm (E := ℂ) ((v : (a : A) → ℂ) (p.coeff n) : ℂ)
⊢ ‖p.coeff n‖ ≤ (↑(p.natDegree.choose n) : ℝ) * p.mapMahlerMeasure v
have hcoeff : norm (E := ℂ) ((v : (a : A) → ℂ) (p.coeff n) : ℂ) = ‖(map v p).coeff n‖
Tactic: have hcoeff : ‖v (p.coeff n)‖ = ‖(p.map v).coeff n‖ := by simp
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
A : Type u_2
inst : NormedRing A
v : A →+* ℂ
hv : Isometry (α := A) (β := ℂ) (⇑v : (a : A) → ℂ)
n : ℕ
p : A[X]
hv_norm : ‖p.coeff n‖ = norm (E := ℂ) ((v : (a : A) → ℂ) (p.coeff n) : ℂ)
hcoeff : norm (E := ℂ) ((v : (a : A) → ℂ) (p.coeff n) : ℂ) = ‖(map v p).coeff n‖
⊢ ‖p.coeff n‖ ≤ (↑(p.natDegree.choose n) : ℝ) * p.mapMahlerMeasure v
have grw : norm (E := ℂ) ((v : (a : A) → ℂ) (p.coeff n) : ℂ) ≤ (↑(p.natDegree.choose n) : ℝ) * p.mapMahlerMeasure v
Tactic: grw [hv_norm, hcoeff, norm_coeff_le_choose_mul_mahlerMeasure,
    natDegree_map_eq_of_injective hv.injective, mapMahlerMeasure]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
A : Type u_2
inst : NormedRing A
v : A →+* ℂ
hv : Isometry (α := A) (β := ℂ) (⇑v : (a : A) → ℂ)
n : ℕ
p : A[X]
hv_norm : ‖p.coeff n‖ = norm (E := ℂ) ((v : (a : A) → ℂ) (p.coeff n) : ℂ)
hcoeff : norm (E := ℂ) ((v : (a : A) → ℂ) (p.coeff n) : ℂ) = ‖(map v p).coeff n‖
grw : norm (E := ℂ) ((v : (a : A) → ℂ) (p.coeff n) : ℂ) ≤ (↑(p.natDegree.choose n) : ℝ) * p.mapMahlerMeasure v
⊢ ‖p.coeff n‖ ≤ (↑(p.natDegree.choose n) : ℝ) * p.mapMahlerMeasure v
have grw₁ : ‖(map v p).coeff n‖ ≤ (↑(p.natDegree.choose n) : ℝ) * p.mapMahlerMeasure v
Tactic: grw [hv_norm, hcoeff, norm_coeff_le_choose_mul_mahlerMeasure,
    natDegree_map_eq_of_injective hv.injective, mapMahlerMeasure]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
A : Type u_2
inst : NormedRing A
v : A →+* ℂ
hv : Isometry (α := A) (β := ℂ) (⇑v : (a : A) → ℂ)
n : ℕ
p : A[X]
hv_norm : ‖p.coeff n‖ = norm (E := ℂ) ((v : (a : A) → ℂ) (p.coeff n) : ℂ)
hcoeff : norm (E := ℂ) ((v : (a : A) → ℂ) (p.coeff n) : ℂ) = ‖(map v p).coeff n‖
grw : norm (E := ℂ) ((v : (a : A) → ℂ) (p.coeff n) : ℂ) ≤ (↑(p.natDegree.choose n) : ℝ) * p.mapMahlerMeasure v
grw₁ : ‖(map v p).coeff n‖ ≤ (↑(p.natDegree.choose n) : ℝ) * p.mapMahlerMeasure v
⊢ ‖p.coeff n‖ ≤ (↑(p.natDegree.choose n) : ℝ) * p.mapMahlerMeasure v
have grw₂ : (↑((map v p).natDegree.choose n) : ℝ) * (map v p).mahlerMeasure ≤ (↑(p.natDegree.choose n) : ℝ) * p.mapMahlerMeasure v
Tactic: grw [hv_norm, hcoeff, norm_coeff_le_choose_mul_mahlerMeasure,
    natDegree_map_eq_of_injective hv.injective, mapMahlerMeasure]