awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Fourier (hypothesis)
Goal:
p : ℂ[X]
⊢ Eq (α := ℝ) (∑ i ∈ p.support, HPow.hPow (β := ℕ) ‖p.coeff i‖ 2)
    (Real.circleAverage (fun (θ : ℂ) ↦ HPow.hPow (β := ℕ) ‖eval θ p‖ 2) 0 1)
have this : Eq (α := ℝ)
  (∑' (i : ℤ),
    HPow.hPow (β := ℕ)
      (norm (E := ℂ)
        (fourierCoeff (T := 2 * π)
          (↑(↑((ContinuousMap.toLp 2 haarAddCircle ℂ : (a : C(AddCircle (2 * π), ℂ)) → ↥(Lp ℂ 2 haarAddCircle))
                    ((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) p)) :
                AddCircle (2 * π) →ₘ[haarAddCircle] ℂ) :
            AddCircle (2 * π) → ℂ)
          i))
      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)
Tactic: have := tsum_sq_fourierCoeff (T := 2 * π) (p.toAddCircle.toLp 2 haarAddCircle ℂ)
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Fourier (hypothesis)
Goal:
p : ℂ[X]
this :
  Eq (α := ℝ)
    (∑' (i : ℤ),
      HPow.hPow (β := ℕ)
        (norm (E := ℂ)
          (fourierCoeff (T := 2 * π)
            (↑(↑((ContinuousMap.toLp 2 haarAddCircle ℂ : (a : C(AddCircle (2 * π), ℂ)) → ↥(Lp ℂ 2 haarAddCircle))
                      ((toAddCircle : (a : ℂ[X]) → C(AddCircle (2 * π), ℂ)) p)) :
                  AddCircle (2 * π) →ₘ[haarAddCircle] ℂ) :
              AddCircle (2 * π) → ℂ)
            i))
        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 (α := ℝ) (∑ i ∈ p.support, HPow.hPow (β := ℕ) ‖p.coeff i‖ 2)
    (Real.circleAverage (fun (θ : ℂ) ↦ HPow.hPow (β := ℕ) ‖eval θ p‖ 2) 0 1)
have 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)
Tactic: simp_rw [fourierCoeff_toLp, fourierCoeff_toAddCircle] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Fourier (goal)
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)
⊢ Eq (α := ℝ) (∑ i ∈ p.support, HPow.hPow (β := ℕ) ‖p.coeff i‖ 2)
    (Real.circleAverage (fun (θ : ℂ) ↦ HPow.hPow (β := ℕ) ‖eval θ p‖ 2) 0 1)
have rw : ∀
  (this :
    Eq (α := ℝ)
      (∑ b ∈ Finset.map { toFun := Nat.cast, inj' := sorry } 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 (α := ℝ) (∑ i ∈ p.support, HPow.hPow (β := ℕ) ‖p.coeff i‖ 2)
    (Real.circleAverage (fun (θ : ℂ) ↦ HPow.hPow (β := ℕ) ‖eval θ p‖ 2) 0 1)
Tactic: rw [tsum_eq_sum (s := p.support.map ⟨_, Nat.cast_injective⟩) (fun b hb => ?eq_zero)] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Fourier (goal)
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)
rw :
  ∀
    (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 (α := ℝ) (∑ i ∈ p.support, HPow.hPow (β := ℕ) ‖p.coeff i‖ 2)
      (Real.circleAverage (fun (θ : ℂ) ↦ HPow.hPow (β := ℕ) ‖eval θ p‖ 2) 0 1)
⊢ Eq (α := ℝ) (∑ i ∈ p.support, HPow.hPow (β := ℕ) ‖p.coeff i‖ 2)
    (Real.circleAverage (fun (θ : ℂ) ↦ HPow.hPow (β := ℕ) ‖eval θ p‖ 2) 0 1)
have rw₁ : ∀ (b : ℤ) (hb : b ∉ Finset.map { toFun := Nat.cast, inj' := sorry } p.support),
  HPow.hPow (β := ℕ) ‖if 0 ≤ b then p.coeff b.natAbs else 0‖ 2 = 0
Tactic: rw [tsum_eq_sum (s := p.support.map ⟨_, Nat.cast_injective⟩) (fun b hb => ?eq_zero)] at this
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Fourier (goal)
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
have inl : ∀ (h : 0 ≤ b), HPow.hPow (β := ℕ) ‖if 0 ≤ b then p.coeff b.natAbs else 0‖ 2 = 0
Tactic: obtain h | h := le_or_gt 0 b
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Fourier (goal)
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
inl : ∀ (h : 0 ≤ b), HPow.hPow (β := ℕ) ‖if 0 ≤ b then p.coeff b.natAbs else 0‖ 2 = 0
⊢ HPow.hPow (β := ℕ) ‖if 0 ≤ b then p.coeff b.natAbs else 0‖ 2 = 0
have inr : ∀ (h : b < 0), HPow.hPow (β := ℕ) ‖if 0 ≤ b then p.coeff b.natAbs else 0‖ 2 = 0
Tactic: obtain h | h := le_or_gt 0 b
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Fourier (goal)
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
⊢ HPow.hPow (β := ℕ) ‖if 0 ≤ b then p.coeff b.natAbs else 0‖ 2 = 0
have inl : ∀ (b : ℕ) (hb : (↑b : ℤ) ∉ Finset.map { toFun := Nat.cast, inj' := sorry } p.support),
  HPow.hPow (β := ℕ) ‖if LE.le (α := ℤ) 0 (↑b : ℤ) then p.coeff (Int.natAbs (↑b : ℤ)) else 0‖ 2 = 0
Tactic: lift b to ℕ using h
Cleared hypotheses: b, hb, h
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Fourier (hypothesis)
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 (α := ℝ) (∑ i ∈ p.support, HPow.hPow (β := ℕ) ‖p.coeff i‖ 2)
    (Real.circleAverage (fun (θ : ℂ) ↦ HPow.hPow (β := ℕ) ‖eval θ p‖ 2) 0 1)
have 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)
Tactic: simp only [Finset.sum_map, Function.Embedding.coeFn_mk, Nat.cast_nonneg,
    ↓reduceIte, Int.natAbs_natCast, ContinuousMap.coe_toLp] at this
Cleared hypotheses: this
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Fourier (goal)
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)
have 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
Tactic: refine integral_congr_ae ?_
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Fourier (goal)
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)
⊢ (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
have 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
Tactic: filter_upwards [ContinuousMap.coeFn_toAEEqFun haarAddCircle (toAddCircle p)] with t ht
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Fourier (goal)
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 :
      ℂ)
⊢ 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
have 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
Tactic: rw [← ht]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Fourier (hypothesis)
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 (α := ℝ) (∑ i ∈ p.support, HPow.hPow (β := ℕ) ‖p.coeff i‖ 2)
    (Real.circleAverage (fun (θ : ℂ) ↦ HPow.hPow (β := ℕ) ‖eval θ p‖ 2) 0 1)
have 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)
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]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.Fourier (goal)
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)
⊢ Eq (α := ℝ) (∑ i ∈ p.support, HPow.hPow (β := ℕ) ‖p.coeff i‖ 2)
    (Real.circleAverage (fun (θ : ℂ) ↦ HPow.hPow (β := ℕ) ‖eval θ p‖ 2) 0 1)
have 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)
Tactic: rw [this, ← h1, AddCircle.integral_haarAddCircle, Real.circleAverage,
    ← AddCircle.intervalIntegral_preimage (2 * π) 0]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
p : ℂ[X]
⊢ p.logMahlerMeasure = log (if p ≠ 0 then rexp p.logMahlerMeasure else 0)
have pos : p ≠ 0 → p.logMahlerMeasure = log (rexp p.logMahlerMeasure)
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
p : ℂ[X]
pos : p ≠ 0 → p.logMahlerMeasure = log (rexp p.logMahlerMeasure)
⊢ p.logMahlerMeasure = log (if p ≠ 0 then rexp p.logMahlerMeasure else 0)
have neg : ¬p ≠ 0 → p.logMahlerMeasure = log 0
Tactic: split_ifs
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
z : ℂ
⊢ mahlerMeasure ((C : (a : ℂ) → ℂ[X]) z) = ‖z‖
have simp : (if z = 0 then 0 else rexp (log ‖z‖)) = ‖z‖
Tactic: simp only [mahlerMeasure, ne_eq, map_eq_zero, logMahlerMeasure_const, ite_not]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
z : ℂ
⊢ (if z = 0 then 0 else rexp (log ‖z‖)) = ‖z‖
have pos : ∀ (h : z = 0), 0 = ‖z‖
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
z : ℂ
pos : ∀ (h : z = 0), 0 = ‖z‖
⊢ (if z = 0 then 0 else rexp (log ‖z‖)) = ‖z‖
have neg : ∀ (h : ¬z = 0), rexp (log ‖z‖) = ‖z‖
Tactic: split_ifs with h
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
p : ℂ[X]
⊢ 0 ≤ p.mahlerMeasure
have pos : ∀ (hp : p = 0), 0 ≤ p.mahlerMeasure
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
p : ℂ[X]
pos : ∀ (hp : p = 0), 0 ≤ p.mahlerMeasure
⊢ 0 ≤ p.mahlerMeasure
have neg : ∀ (hp : ¬p = 0), 0 ≤ p.mahlerMeasure
Tactic: by_cases hp : p = 0
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
p : ℂ[X]
⊢ p.mahlerMeasure = 0 ↔ p = 0
have refine : p.mahlerMeasure = 0 → p = 0
Tactic: refine ⟨?_, by simp_all [mahlerMeasure_zero]⟩
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
p : ℂ[X]
⊢ p.mahlerMeasure = 0 → p = 0
have contrapose : ¬p = 0 → ¬p.mahlerMeasure = 0
Tactic: contrapose
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
p q : ℂ[X]
⊢ (p * q).mahlerMeasure = p.mahlerMeasure * q.mahlerMeasure
have pos : ∀ (hpq : p * q = 0), (p * q).mahlerMeasure = p.mahlerMeasure * q.mahlerMeasure
Tactic: by_cases hpq : p * q = 0
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
p q : ℂ[X]
pos : ∀ (hpq : p * q = 0), (p * q).mahlerMeasure = p.mahlerMeasure * q.mahlerMeasure
⊢ (p * q).mahlerMeasure = p.mahlerMeasure * q.mahlerMeasure
have neg : ∀ (hpq : ¬p * q = 0), (p * q).mahlerMeasure = p.mahlerMeasure * q.mahlerMeasure
Tactic: by_cases hpq : p * q = 0
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (hypothesis)
Goal:
p q : ℂ[X]
hpq : ¬p * q = 0
⊢ (p * q).mahlerMeasure = p.mahlerMeasure * q.mahlerMeasure
have hpq₁ : ¬p = 0 ∧ ¬q = 0
Tactic: rw [mul_eq_zero, not_or] at hpq
Cleared hypotheses: hpq
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
p q : ℂ[X]
hpq : ¬p = 0 ∧ ¬q = 0
⊢ (p * q).mahlerMeasure = p.mahlerMeasure * q.mahlerMeasure
have 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‖)
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]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
p q : ℂ[X]
hpq : ¬p = 0 ∧ ¬q = 0
⊢ 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‖)
have 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‖))
Tactic: rw [← exp_add, ← left_distrib]
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
p q : ℂ[X]
hpq : ¬p = 0 ∧ ¬q = 0
⊢ 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‖))
have neg : ∫ (θ : ℝ) in 0..2 * π, log (‖eval (circleMap 0 1 θ) p‖ * ‖eval (circleMap 0 1 θ) q‖) =
  HAdd.hAdd (α := ℝ) (∫ (θ : ℝ) in 0..2 * π, log ‖eval (circleMap 0 1 θ) p‖)
    (∫ (θ : ℝ) in 0..2 * π, log ‖eval (circleMap 0 1 θ) q‖)
Tactic: congr
-- Lean 4 proof step from Mathlib.Analysis.Polynomial.MahlerMeasure (goal)
Goal:
p q : ℂ[X]
hpq : ¬p = 0 ∧ ¬q = 0
⊢ ∫ (θ : ℝ) in 0..2 * π, log (‖eval (circleMap 0 1 θ) p‖ * ‖eval (circleMap 0 1 θ) q‖) =
    HAdd.hAdd (α := ℝ) (∫ (θ : ℝ) in 0..2 * π, log ‖eval (circleMap 0 1 θ) p‖)
      (∫ (θ : ℝ) in 0..2 * π, log ‖eval (circleMap 0 1 θ) q‖)
have neg : Eq (α := ℝ) (∫ (θ : ℝ) in 0..2 * π, log (‖eval (circleMap 0 1 θ) p‖ * ‖eval (circleMap 0 1 θ) q‖))
  (∫ (x : ℝ) in 0..2 * π, log ‖eval (circleMap 0 1 x) p‖ + log ‖eval (circleMap 0 1 x) q‖)
Tactic: rw [← integral_add p.intervalIntegrable_mahlerMeasure q.intervalIntegrable_mahlerMeasure]