awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.Analysis.Polynomial.Fourier
Goal:
p : ℂ[X]
this :
  Eq (α := ℝ) (∑' (i : ℤ), HPow.hPow (β := ℕ) ‖if 0 ≤ i then p.coeff i.natAbs else 0‖ 2)
    (∫ (t : AddCircle (2 * π)),
      HPow.hPow (β := ℕ)
        (norm (E := ℂ)
          ((↑(↑((ContinuousMap.toLp 2 haarAddCircle ℂ : (a : C(AddCircle (2 * π), ℂ)) → ↥(Lp ℂ 2 haarAddCircle))
                      ((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) p)) :
                  AddCircle (2 * π) →ₘ[haarAddCircle] ℂ) :
              AddCircle (2 * π) → ℂ)
            t))
        2 ∂haarAddCircle)
b : ℤ
hb : b ∉ Finset.map { toFun := Nat.cast, inj' := ⋯ } p.support
h : 0 ≤ b
inl :
  ∀ (b : ℕ) (hb : (↑b : ℤ) ∉ Finset.map { toFun := Nat.cast, inj' := ⋯ } p.support),
    HPow.hPow (β := ℕ) ‖if LE.le (α := ℤ) 0 (↑b : ℤ) then p.coeff (Int.natAbs (↑b : ℤ)) else 0‖ 2 = 0
⊢ HPow.hPow (β := ℕ) ‖if 0 ≤ b then p.coeff b.natAbs else 0‖ 2 = 0

Tactic:
lift b to ℕ using h
-- Module: Mathlib.Analysis.Polynomial.Fourier
Goal:
p : ℂ[X]
this :
  Eq (α := ℝ) (∑' (i : ℤ), HPow.hPow (β := ℕ) ‖if 0 ≤ i then p.coeff i.natAbs else 0‖ 2)
    (∫ (t : AddCircle (2 * π)),
      HPow.hPow (β := ℕ)
        (norm (E := ℂ)
          ((↑(↑((ContinuousMap.toLp 2 haarAddCircle ℂ : (a : C(AddCircle (2 * π), ℂ)) → ↥(Lp ℂ 2 haarAddCircle))
                      ((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) p)) :
                  AddCircle (2 * π) →ₘ[haarAddCircle] ℂ) :
              AddCircle (2 * π) → ℂ)
            t))
        2 ∂haarAddCircle)
b : ℕ
hb : (↑b : ℤ) ∉ Finset.map { toFun := Nat.cast, inj' := ⋯ } p.support
⊢ HPow.hPow (β := ℕ) ‖if LE.le (α := ℤ) 0 (↑b : ℤ) then p.coeff (Int.natAbs (↑b : ℤ)) else 0‖ 2 = 0

Tactic:
simpa using hb
-- Module: Mathlib.Analysis.Polynomial.Fourier
Goal:
p : ℂ[X]
this :
  Eq (α := ℝ) (∑' (i : ℤ), HPow.hPow (β := ℕ) ‖if 0 ≤ i then p.coeff i.natAbs else 0‖ 2)
    (∫ (t : AddCircle (2 * π)),
      HPow.hPow (β := ℕ)
        (norm (E := ℂ)
          ((↑(↑((ContinuousMap.toLp 2 haarAddCircle ℂ : (a : C(AddCircle (2 * π), ℂ)) → ↥(Lp ℂ 2 haarAddCircle))
                      ((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) p)) :
                  AddCircle (2 * π) →ₘ[haarAddCircle] ℂ) :
              AddCircle (2 * π) → ℂ)
            t))
        2 ∂haarAddCircle)
b : ℤ
hb : b ∉ Finset.map { toFun := Nat.cast, inj' := ⋯ } p.support
h : b < 0
⊢ HPow.hPow (β := ℕ) ‖if 0 ≤ b then p.coeff b.natAbs else 0‖ 2 = 0

Tactic:
simp [h]
-- Module: Mathlib.Analysis.Polynomial.Fourier
Goal:
p : ℂ[X]
this :
  Eq (α := ℝ) (∑' (i : ℤ), HPow.hPow (β := ℕ) ‖if 0 ≤ i then p.coeff i.natAbs else 0‖ 2)
    (∫ (t : AddCircle (2 * π)),
      HPow.hPow (β := ℕ)
        (norm (E := ℂ)
          ((↑(↑((ContinuousMap.toLp 2 haarAddCircle ℂ : (a : C(AddCircle (2 * π), ℂ)) → ↥(Lp ℂ 2 haarAddCircle))
                      ((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) p)) :
                  AddCircle (2 * π) →ₘ[haarAddCircle] ℂ) :
              AddCircle (2 * π) → ℂ)
            t))
        2 ∂haarAddCircle)
b : ℤ
hb : b ∉ Finset.map { toFun := Nat.cast, inj' := ⋯ } p.support
⊢ HPow.hPow (β := ℕ) ‖if 0 ≤ b then p.coeff b.natAbs else 0‖ 2 = 0

Tactic:
case eq_zero =>
    obtain h | h := le_or_gt 0 b
    · lift b to ℕ using h
      simpa using hb
    · simp [h]

Premises used: le_or_gt, OfNat.ofNat
-- Module: Mathlib.Analysis.Polynomial.Fourier
Goal:
p : ℂ[X]
this :
  Eq (α := ℝ)
    (∑ b ∈ Finset.map { toFun := Nat.cast, inj' := ⋯ } p.support,
      HPow.hPow (β := ℕ) ‖if 0 ≤ b then p.coeff b.natAbs else 0‖ 2)
    (∫ (t : AddCircle (2 * π)),
      HPow.hPow (β := ℕ)
        (norm (E := ℂ)
          ((↑(↑((ContinuousMap.toLp 2 haarAddCircle ℂ : (a : C(AddCircle (2 * π), ℂ)) → ↥(Lp ℂ 2 haarAddCircle))
                      ((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) p)) :
                  AddCircle (2 * π) →ₘ[haarAddCircle] ℂ) :
              AddCircle (2 * π) → ℂ)
            t))
        2 ∂haarAddCircle)
⊢ Eq (α := ℝ) (∑ x ∈ p.support, HPow.hPow (β := ℕ) ‖p.coeff x‖ 2)
    (∫ (t : AddCircle (2 * π)),
      HPow.hPow (β := ℕ)
        (norm (E := ℂ)
          ((↑(ContinuousMap.toAEEqFun haarAddCircle ((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) p)) :
              AddCircle (2 * π) → ℂ)
            t))
        2 ∂haarAddCircle)

Tactic:
simp only [Finset.sum_map, Function.Embedding.coeFn_mk, Nat.cast_nonneg,
    ↓reduceIte, Int.natAbs_natCast, ContinuousMap.coe_toLp] at this

Premises used: Nat.cast_nonneg, Finset.sum_map, ContinuousMap.coe_toLp, Function.Embedding.coeFn_mk, reduceIte, Int.natAbs_natCast
-- Module: Mathlib.Analysis.Polynomial.Fourier
Goal:
p : ℂ[X]
this :
  Eq (α := ℝ) (∑ x ∈ p.support, HPow.hPow (β := ℕ) ‖p.coeff x‖ 2)
    (∫ (t : AddCircle (2 * π)),
      HPow.hPow (β := ℕ)
        (norm (E := ℂ)
          ((↑(ContinuousMap.toAEEqFun haarAddCircle ((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) p)) :
              AddCircle (2 * π) → ℂ)
            t))
        2 ∂haarAddCircle)
⊢ Eq (α := ℝ)
    (∫ (t : AddCircle (2 * π)),
      HPow.hPow (β := ℕ)
        (norm (E := ℂ)
          ((((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) p : C(AddCircle (2 * π), ℂ)) :
                (a : AddCircle (2 * π)) → ℂ)
              t :
            ℂ))
        2 ∂haarAddCircle)
    (∫ (t : AddCircle (2 * π)),
      HPow.hPow (β := ℕ)
        (norm (E := ℂ)
          ((↑(ContinuousMap.toAEEqFun haarAddCircle ((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) p)) :
              AddCircle (2 * π) → ℂ)
            t))
        2 ∂haarAddCircle)

Tactic:
integral_congr_ae ?_

Premises used: MeasureTheory.integral_congr_ae
-- Module: Mathlib.Analysis.Polynomial.Fourier
Goal:
p : ℂ[X]
this :
  Eq (α := ℝ) (∑ x ∈ p.support, HPow.hPow (β := ℕ) ‖p.coeff x‖ 2)
    (∫ (t : AddCircle (2 * π)),
      HPow.hPow (β := ℕ)
        (norm (E := ℂ)
          ((↑(ContinuousMap.toAEEqFun haarAddCircle ((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) p)) :
              AddCircle (2 * π) → ℂ)
            t))
        2 ∂haarAddCircle)
refine :
  (ae (F := Measure (AddCircle (2 * π))) haarAddCircle).EventuallyEq (β := ℝ)
    (fun (t : AddCircle (2 * π)) ↦
      HPow.hPow (β := ℕ)
        (norm (E := ℂ)
          ((((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) p : C(AddCircle (2 * π), ℂ)) :
                (a : AddCircle (2 * π)) → ℂ)
              t :
            ℂ))
        2)
    fun (t : AddCircle (2 * π)) ↦
    HPow.hPow (β := ℕ)
      (norm (E := ℂ)
        ((↑(ContinuousMap.toAEEqFun haarAddCircle ((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) p)) :
            AddCircle (2 * π) → ℂ)
          t))
      2
⊢ Eq (α := ℝ)
    (∫ (t : AddCircle (2 * π)),
      HPow.hPow (β := ℕ)
        (norm (E := ℂ)
          ((((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) p : C(AddCircle (2 * π), ℂ)) :
                (a : AddCircle (2 * π)) → ℂ)
              t :
            ℂ))
        2 ∂haarAddCircle)
    (∫ (t : AddCircle (2 * π)),
      HPow.hPow (β := ℕ)
        (norm (E := ℂ)
          ((↑(ContinuousMap.toAEEqFun haarAddCircle ((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) p)) :
              AddCircle (2 * π) → ℂ)
            t))
        2 ∂haarAddCircle)

Tactic:
refine integral_congr_ae ?_

Premises used: MeasureTheory.integral_congr_ae
-- Module: Mathlib.Analysis.Polynomial.Fourier
Goal:
p : ℂ[X]
this :
  Eq (α := ℝ) (∑ x ∈ p.support, HPow.hPow (β := ℕ) ‖p.coeff x‖ 2)
    (∫ (t : AddCircle (2 * π)),
      HPow.hPow (β := ℕ)
        (norm (E := ℂ)
          ((↑(ContinuousMap.toAEEqFun haarAddCircle ((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) p)) :
              AddCircle (2 * π) → ℂ)
            t))
        2 ∂haarAddCircle)
h :
  ∀ (t : AddCircle (2 * π))
    (ht :
      Eq (α := ℂ)
        ((↑(ContinuousMap.toAEEqFun haarAddCircle ((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) p)) :
              AddCircle (2 * π) → ℂ)
            t :
          ℂ)
        ((((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) p : C(AddCircle (2 * π), ℂ)) :
              (a : AddCircle (2 * π)) → ℂ)
            t :
          ℂ)),
    HPow.hPow (β := ℕ)
        (norm (E := ℂ)
          ((((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) p : C(AddCircle (2 * π), ℂ)) :
                (a : AddCircle (2 * π)) → ℂ)
              t :
            ℂ))
        2 =
      HPow.hPow (β := ℕ)
        (norm (E := ℂ)
          ((↑(ContinuousMap.toAEEqFun haarAddCircle ((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) p)) :
              AddCircle (2 * π) → ℂ)
            t))
        2
⊢ (ae (F := Measure (AddCircle (2 * π))) haarAddCircle).EventuallyEq (β := ℝ)
    (fun (t : AddCircle (2 * π)) ↦
      HPow.hPow (β := ℕ)
        (norm (E := ℂ)
          ((((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) p : C(AddCircle (2 * π), ℂ)) :
                (a : AddCircle (2 * π)) → ℂ)
              t :
            ℂ))
        2)
    fun (t : AddCircle (2 * π)) ↦
    HPow.hPow (β := ℕ)
      (norm (E := ℂ)
        ((↑(ContinuousMap.toAEEqFun haarAddCircle ((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) p)) :
            AddCircle (2 * π) → ℂ)
          t))
      2

Tactic:
filter_upwards [ContinuousMap.coeFn_toAEEqFun haarAddCircle (toAddCircle p)] with t ht

Premises used: ContinuousMap.coeFn_toAEEqFun, AddCircle.haarAddCircle, Polynomial.toAddCircle, DFunLike.coe
-- Module: Mathlib.Analysis.Polynomial.Fourier
Goal:
p : ℂ[X]
this :
  Eq (α := ℝ) (∑ x ∈ p.support, HPow.hPow (β := ℕ) ‖p.coeff x‖ 2)
    (∫ (t : AddCircle (2 * π)),
      HPow.hPow (β := ℕ)
        (norm (E := ℂ)
          ((↑(ContinuousMap.toAEEqFun haarAddCircle ((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) p)) :
              AddCircle (2 * π) → ℂ)
            t))
        2 ∂haarAddCircle)
t : AddCircle (2 * π)
ht :
  Eq (α := ℂ)
    ((↑(ContinuousMap.toAEEqFun haarAddCircle ((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) p)) :
          AddCircle (2 * π) → ℂ)
        t :
      ℂ)
    ((((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) p : C(AddCircle (2 * π), ℂ)) : (a : AddCircle (2 * π)) → ℂ)
        t :
      ℂ)
h h₁ :
  HPow.hPow (β := ℕ)
      (norm (E := ℂ)
        ((↑(ContinuousMap.toAEEqFun haarAddCircle ((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) p)) :
            AddCircle (2 * π) → ℂ)
          t))
      2 =
    HPow.hPow (β := ℕ)
      (norm (E := ℂ)
        ((↑(ContinuousMap.toAEEqFun haarAddCircle ((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) p)) :
            AddCircle (2 * π) → ℂ)
          t))
      2
⊢ HPow.hPow (β := ℕ)
      (norm (E := ℂ)
        ((((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) p : C(AddCircle (2 * π), ℂ)) :
              (a : AddCircle (2 * π)) → ℂ)
            t :
          ℂ))
      2 =
    HPow.hPow (β := ℕ)
      (norm (E := ℂ)
        ((↑(ContinuousMap.toAEEqFun haarAddCircle ((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) p)) :
            AddCircle (2 * π) → ℂ)
          t))
      2

Tactic:
rw [← ht]
-- Module: Mathlib.Analysis.Polynomial.Fourier
Goal:
p : ℂ[X]
this :
  Eq (α := ℝ) (∑ x ∈ p.support, HPow.hPow (β := ℕ) ‖p.coeff x‖ 2)
    (∫ (t : AddCircle (2 * π)),
      HPow.hPow (β := ℕ)
        (norm (E := ℂ)
          ((↑(ContinuousMap.toAEEqFun haarAddCircle ((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) p)) :
              AddCircle (2 * π) → ℂ)
            t))
        2 ∂haarAddCircle)
⊢ Eq (α := ℝ)
    (∫ (t : AddCircle (2 * π)),
      HPow.hPow (β := ℕ)
        (norm (E := ℂ)
          ((((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) p : C(AddCircle (2 * π), ℂ)) :
                (a : AddCircle (2 * π)) → ℂ)
              t :
            ℂ))
        2 ∂haarAddCircle)
    (∫ (t : AddCircle (2 * π)),
      HPow.hPow (β := ℕ)
        (norm (E := ℂ)
          ((↑(ContinuousMap.toAEEqFun haarAddCircle ((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) p)) :
              AddCircle (2 * π) → ℂ)
            t))
        2 ∂haarAddCircle)

Tactic:
have h1 : ∫ (t : AddCircle (2 * π)), ‖toAddCircle p t‖ ^ 2 ∂haarAddCircle =
      ∫ (t : AddCircle (2 * π)),
        ‖(ContinuousMap.toAEEqFun haarAddCircle (toAddCircle p)) t‖ ^ 2 ∂haarAddCircle := by
    refine integral_congr_ae ?_
    filter_upwards [ContinuousMap.coeFn_toAEEqFun haarAddCircle (toAddCircle p)] with t ht
    rw [← ht]
-- Module: Mathlib.Analysis.Polynomial.Fourier
Goal:
p : ℂ[X]
this :
  Eq (α := ℝ) (∑ x ∈ p.support, HPow.hPow (β := ℕ) ‖p.coeff x‖ 2)
    (∫ (t : AddCircle (2 * π)),
      HPow.hPow (β := ℕ)
        (norm (E := ℂ)
          ((↑(ContinuousMap.toAEEqFun haarAddCircle ((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) p)) :
              AddCircle (2 * π) → ℂ)
            t))
        2 ∂haarAddCircle)
h1 :
  Eq (α := ℝ)
    (∫ (t : AddCircle (2 * π)),
      HPow.hPow (β := ℕ)
        (norm (E := ℂ)
          ((((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) p : C(AddCircle (2 * π), ℂ)) :
                (a : AddCircle (2 * π)) → ℂ)
              t :
            ℂ))
        2 ∂haarAddCircle)
    (∫ (t : AddCircle (2 * π)),
      HPow.hPow (β := ℕ)
        (norm (E := ℂ)
          ((↑(ContinuousMap.toAEEqFun haarAddCircle ((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) p)) :
              AddCircle (2 * π) → ℂ)
            t))
        2 ∂haarAddCircle)
rw :
  HSMul.hSMul (β := ℝ) (2 * π)⁻¹
      (∫ (a : ℝ) in 0..0 + 2 * π,
        HPow.hPow (β := ℕ)
          (norm (E := ℂ)
            ((((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) p : C(AddCircle (2 * π), ℂ)) :
                  (a : AddCircle (2 * π)) → ℂ)
                (↑a : ℝ ⧸ AddSubgroup.zmultiples (2 * π)) :
              ℂ))
          2) =
    HSMul.hSMul (β := ℝ) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, HPow.hPow (β := ℕ) ‖eval (circleMap 0 1 θ) p‖ 2)
⊢ Eq (α := ℝ) (∑ i ∈ p.support, HPow.hPow (β := ℕ) ‖p.coeff i‖ 2)
    (Real.circleAverage (fun (θ : ℂ) ↦ HPow.hPow (β := ℕ) ‖eval θ p‖ 2) 0 1)

Tactic:
rw [this, ← h1, AddCircle.integral_haarAddCircle, Real.circleAverage,
    ← AddCircle.intervalIntegral_preimage (2 * π) 0]

Premises used: Real.pi, HMul.hMul, AddCircle.integral_haarAddCircle, AddCircle.intervalIntegral_preimage, OfNat.ofNat, Real.circleAverage
-- Module: Mathlib.Analysis.Polynomial.Fourier
Goal:
p : ℂ[X]
this :
  Eq (α := ℝ) (∑ x ∈ p.support, HPow.hPow (β := ℕ) ‖p.coeff x‖ 2)
    (∫ (t : AddCircle (2 * π)),
      HPow.hPow (β := ℕ)
        (norm (E := ℂ)
          ((↑(ContinuousMap.toAEEqFun haarAddCircle ((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) p)) :
              AddCircle (2 * π) → ℂ)
            t))
        2 ∂haarAddCircle)
h1 :
  Eq (α := ℝ)
    (∫ (t : AddCircle (2 * π)),
      HPow.hPow (β := ℕ)
        (norm (E := ℂ)
          ((((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) p : C(AddCircle (2 * π), ℂ)) :
                (a : AddCircle (2 * π)) → ℂ)
              t :
            ℂ))
        2 ∂haarAddCircle)
    (∫ (t : AddCircle (2 * π)),
      HPow.hPow (β := ℕ)
        (norm (E := ℂ)
          ((↑(ContinuousMap.toAEEqFun haarAddCircle ((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) p)) :
              AddCircle (2 * π) → ℂ)
            t))
        2 ∂haarAddCircle)
⊢ HSMul.hSMul (β := ℝ) (2 * π)⁻¹
      (∫ (a : ℝ) in 0..0 + 2 * π,
        HPow.hPow (β := ℕ)
          (norm (E := ℂ)
            ((((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) p : C(AddCircle (2 * π), ℂ)) :
                  (a : AddCircle (2 * π)) → ℂ)
                (↑a : ℝ ⧸ AddSubgroup.zmultiples (2 * π)) :
              ℂ))
          2) =
    HSMul.hSMul (β := ℝ) (2 * π)⁻¹ (∫ (θ : ℝ) in 0..2 * π, HPow.hPow (β := ℕ) ‖eval (circleMap 0 1 θ) p‖ 2)

Tactic:
simp [toAddCircle, toCircle, circleMap]

Premises used: circleMap, Polynomial.toAddCircle, AddCircle.toCircle
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
⊢ p.logMahlerMeasure = circleAverage (fun (x : ℂ) ↦ log ‖eval x p‖) 0 1

Tactic:
rfl

Premises used: Polynomial.logMahlerMeasure, rfl
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
⊢ logMahlerMeasure 0 = 0

Tactic:
simp [logMahlerMeasure_def, circleAverage_def]

Premises used: Real.circleAverage_def, Polynomial.logMahlerMeasure_def
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
⊢ logMahlerMeasure 1 = 0

Tactic:
simp [logMahlerMeasure_def, circleAverage_def]

Premises used: Real.circleAverage_def, Polynomial.logMahlerMeasure_def
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
z : ℂ
⊢ logMahlerMeasure ((C : (a : ℂ) → ℂ[X]) z) = log ‖z‖

Tactic:
simp [logMahlerMeasure_def, circleAverage_def, mul_assoc]

Premises used: mul_assoc, Real.circleAverage_def, Polynomial.logMahlerMeasure_def
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
⊢ logMahlerMeasure X = 0

Tactic:
simp [logMahlerMeasure_def, circleAverage_def]

Premises used: Real.circleAverage_def, Polynomial.logMahlerMeasure_def
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
n : ℕ
z : ℂ
⊢ logMahlerMeasure ((monomial n : (a : ℂ) → ℂ[X]) z) = log ‖z‖

Tactic:
simp [logMahlerMeasure_def, circleAverage_def, mul_assoc]

Premises used: mul_assoc, Real.circleAverage_def, Polynomial.logMahlerMeasure_def
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
hp : p ≠ 0
⊢ p.mahlerMeasure = rexp ((2 * π)⁻¹ * ∫ (x : ℝ) in 0..2 * π, log ‖eval (circleMap 0 1 x) p‖)

Tactic:
simp [mahlerMeasure, hp, logMahlerMeasure_def, circleAverage_def]

Premises used: Real.circleAverage_def, Polynomial.logMahlerMeasure_def, Polynomial.mahlerMeasure
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
pos : p ≠ 0 → p.logMahlerMeasure = log (rexp p.logMahlerMeasure)
neg : ¬p ≠ 0 → p.logMahlerMeasure = log 0
⊢ p.logMahlerMeasure = log (if p ≠ 0 then rexp p.logMahlerMeasure else 0)

Tactic:
split_ifs
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
h : p ≠ 0
⊢ p.logMahlerMeasure = log (rexp p.logMahlerMeasure)

Tactic:
simp_all [logMahlerMeasure_def, circleAverage_def]

Premises used: Real.circleAverage_def, Polynomial.logMahlerMeasure_def
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
h : ¬p ≠ 0
⊢ p.logMahlerMeasure = log 0

Tactic:
simp_all [logMahlerMeasure_def, circleAverage_def]

Premises used: Real.circleAverage_def, Polynomial.logMahlerMeasure_def
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
⊢ mahlerMeasure 0 = 0

Tactic:
simp [mahlerMeasure]

Premises used: Polynomial.mahlerMeasure
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
⊢ mahlerMeasure 1 = 1

Tactic:
simp [mahlerMeasure]

Premises used: Polynomial.mahlerMeasure
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
z : ℂ
simp : (if z = 0 then 0 else rexp (log ‖z‖)) = ‖z‖
⊢ mahlerMeasure ((C : (a : ℂ) → ℂ[X]) z) = ‖z‖

Tactic:
simp only [mahlerMeasure, ne_eq, map_eq_zero, logMahlerMeasure_const, ite_not]

Premises used: map_eq_zero, ne_eq, Polynomial.mahlerMeasure, ite_not, Polynomial.logMahlerMeasure_const
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
z : ℂ
pos : ∀ (h : z = 0), 0 = ‖z‖
neg : ∀ (h : ¬z = 0), rexp (log ‖z‖) = ‖z‖
⊢ (if z = 0 then 0 else rexp (log ‖z‖)) = ‖z‖

Tactic:
split_ifs with h
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
z : ℂ
h : z = 0
⊢ 0 = ‖z‖

Tactic:
simp [h]
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
z : ℂ
h : ¬z = 0
⊢ rexp (log ‖z‖) = ‖z‖

Tactic:
simp [h, exp_log]

Premises used: Real.exp_log
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
pos : ∀ (hp : p = 0), 0 ≤ p.mahlerMeasure
neg : ∀ (hp : ¬p = 0), 0 ≤ p.mahlerMeasure
⊢ 0 ≤ p.mahlerMeasure

Tactic:
by_cases hp : p = 0
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
hp : p = 0
⊢ 0 ≤ p.mahlerMeasure

Tactic:
simp [hp, mahlerMeasure_def_of_ne_zero, exp_nonneg]

Premises used: Polynomial.mahlerMeasure_def_of_ne_zero, Real.exp_nonneg
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
hp : ¬p = 0
⊢ 0 ≤ p.mahlerMeasure

Tactic:
simp [hp, mahlerMeasure_def_of_ne_zero, exp_nonneg]

Premises used: Polynomial.mahlerMeasure_def_of_ne_zero, Real.exp_nonneg
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
hp : p ≠ 0
⊢ 0 < p.mahlerMeasure

Tactic:
grind [exp_pos, mahlerMeasure_def_of_ne_zero]

Premises used: Polynomial.mahlerMeasure_def_of_ne_zero, Real.exp_pos
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
⊢ p = 0 → p.mahlerMeasure = 0

Tactic:
simp_all [mahlerMeasure_zero]

Premises used: Polynomial.mahlerMeasure_zero
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
refine : p.mahlerMeasure = 0 → p = 0
⊢ p.mahlerMeasure = 0 ↔ p = 0

Tactic:
refine ⟨?_, by simp_all [mahlerMeasure_zero]⟩
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
contrapose : ¬p = 0 → ¬p.mahlerMeasure = 0
⊢ p.mahlerMeasure = 0 → p = 0

Tactic:
contrapose
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
h : ¬p = 0
⊢ ¬p.mahlerMeasure = 0

Tactic:
simp [mahlerMeasure_def_of_ne_zero h]

Premises used: Polynomial.mahlerMeasure_def_of_ne_zero
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
⊢ ¬p = 0 → ¬p.mahlerMeasure = 0

Tactic:
exact fun h ↦ by simp [mahlerMeasure_def_of_ne_zero h]
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
⊢ CircleIntegrable (E := ℝ) (fun (z : ℂ) ↦ log ‖eval z p‖) 0 1

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

Premises used: MeromorphicOn.circleIntegrable_log_norm, AnalyticOnNhd.meromorphicOn
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p : ℂ[X]
⊢ CircleIntegrable (E := ℝ) (fun (z : ℂ) ↦ log ‖eval z p‖) 0 1

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

Premises used: MeromorphicOn.circleIntegrable_log_norm, AnalyticOnNhd.meromorphicOn
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p q : ℂ[X]
pos : ∀ (hpq : p * q = 0), (p * q).mahlerMeasure = p.mahlerMeasure * q.mahlerMeasure
neg : ∀ (hpq : ¬p * q = 0), (p * q).mahlerMeasure = p.mahlerMeasure * q.mahlerMeasure
⊢ (p * q).mahlerMeasure = p.mahlerMeasure * q.mahlerMeasure

Tactic:
by_cases hpq : p * q = 0
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p q : ℂ[X]
hpq : p * q = 0
⊢ (p * q).mahlerMeasure = p.mahlerMeasure * q.mahlerMeasure

Tactic:
simpa [hpq, mahlerMeasure_zero] using mul_eq_zero.mp hpq

Premises used: mul_eq_zero, Polynomial.mahlerMeasure_zero, Iff.mp
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p q : ℂ[X]
hpq : ¬p * q = 0
⊢ ¬p = 0 ∧ ¬q = 0

Tactic:
rw [mul_eq_zero, not_or] at hpq

Premises used: mul_eq_zero, not_or
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p q : ℂ[X]
hpq : ¬p = 0 ∧ ¬q = 0
neg :
  rexp (π⁻¹ * 2⁻¹ * ∫ (θ : ℝ) in 0..2 * π, log (‖eval (circleMap 0 1 θ) p‖ * ‖eval (circleMap 0 1 θ) q‖)) =
    rexp (π⁻¹ * 2⁻¹ * ∫ (θ : ℝ) in 0..2 * π, log ‖eval (circleMap 0 1 θ) p‖) *
      rexp (π⁻¹ * 2⁻¹ * ∫ (θ : ℝ) in 0..2 * π, log ‖eval (circleMap 0 1 θ) q‖)
⊢ (p * q).mahlerMeasure = p.mahlerMeasure * q.mahlerMeasure

Tactic:
simp only [mahlerMeasure, ne_eq, mul_eq_zero, hpq, or_self, not_false_eq_true, ↓reduceIte,
    logMahlerMeasure, eval_mul, Complex.norm_mul, circleAverage_def, mul_inv_rev, smul_eq_mul]

Premises used: Polynomial.eval_mul, Real.circleAverage_def, mul_eq_zero, ne_eq, Polynomial.mahlerMeasure, or_self, reduceIte, mul_inv_rev, smul_eq_mul, Polynomial.logMahlerMeasure, not_false_eq_true, Complex.norm_mul
-- Module: Mathlib.Analysis.Polynomial.MahlerMeasure
Goal:
p q : ℂ[X]
hpq : ¬p = 0 ∧ ¬q = 0
neg :
  rexp (π⁻¹ * 2⁻¹ * ∫ (θ : ℝ) in 0..2 * π, log (‖eval (circleMap 0 1 θ) p‖ * ‖eval (circleMap 0 1 θ) q‖)) =
    rexp
      (π⁻¹ * 2⁻¹ *
        HAdd.hAdd (α := ℝ) (∫ (θ : ℝ) in 0..2 * π, log ‖eval (circleMap 0 1 θ) p‖)
          (∫ (θ : ℝ) in 0..2 * π, log ‖eval (circleMap 0 1 θ) q‖))
⊢ rexp (π⁻¹ * 2⁻¹ * ∫ (θ : ℝ) in 0..2 * π, log (‖eval (circleMap 0 1 θ) p‖ * ‖eval (circleMap 0 1 θ) q‖)) =
    rexp (π⁻¹ * 2⁻¹ * ∫ (θ : ℝ) in 0..2 * π, log ‖eval (circleMap 0 1 θ) p‖) *
      rexp (π⁻¹ * 2⁻¹ * ∫ (θ : ℝ) in 0..2 * π, log ‖eval (circleMap 0 1 θ) q‖)

Tactic:
rw [← exp_add, ← left_distrib]

Premises used: Real.exp_add, left_distrib