UniqueExtensionCoefficients.lean

def IsUniqueNonarchimedeanAbsoluteValueExtension
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    (v : AbsoluteValue K ℝ) (w : AbsoluteValue L ℝ) : Prop

theorem uniqueNonarchimedeanAbsoluteValueExtension_map_algEquiv_eq
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    {v : AbsoluteValue K ℝ} {w : AbsoluteValue L ℝ}
    (huniq : IsUniqueNonarchimedeanAbsoluteValueExtension v w)
    (σ : L ≃ₐ[K] L) (x : L) :
    w (σ x) = w x

theorem uniqueNonarchimedeanAbsoluteValueExtension_eq_on_roots_of_irreducible
    {K L : Type*} [Field K] [Field L] [Algebra K L] [Normal K L]
    {v : AbsoluteValue K ℝ} {w : AbsoluteValue L ℝ}
    (huniq : IsUniqueNonarchimedeanAbsoluteValueExtension v w)
    {p : Polynomial K} (hp : Irreducible p)
    {α β : L}
    (hα : α ∈ (p.map (algebraMap K L)).roots)
    (hβ : β ∈ (p.map (algebraMap K L)).roots) :
    w α = w β

theorem abs_coeff_prod_X_sub_C_le_pow_card
    {L : Type*} [Field L]
    (w : AbsoluteValue L ℝ) (hstrong : LubinTate.Valuations.StrongTriangle w)
    (B : ℝ) (hB : 1 ≤ B) (s : Multiset L)
    (hs : ∀ α ∈ s, w α ≤ B) (i : ℕ) :
    w (((s.map (fun α => X - C α)).prod).coeff i) ≤ B ^ s.card := by
  induction s using Multiset.induction_on generalizing i with
  | empty =>
      cases i <;> simp [Polynomial.coeff_one]
  | @cons α s ih =>
      have hα : w α ≤ B := hs α (by simp)
      have hs' : ∀ β ∈ s, w β ≤ B := by
        intro β hβ
        exact hs β (by simp [hβ])
      have hB0 : 0 ≤ B := zero_le_one.trans hB
      have hpow_step : B ^ s.card ≤ B ^ (s.card + 1) := by
        rw [pow_succ]
        exact le_mul_of_one_le_right (pow_nonneg hB0 _) hB
      simp only [Multiset.map_cons, Multiset.prod_cons, Multiset.card_cons]
      cases i with
      | zero =>
          have hq := ih hs' 0
          calc
            w (((X - C α) * (s.map (fun β => X - C β)).prod).coeff 0) =
                w α * w (((s.map (fun β => X - C β)).prod).coeff 0) := by
              simp [Polynomial.coeff_zero_eq_eval_zero]
            _ ≤ B * B ^ s.card :=
              mul_le_mul hα hq (w.nonneg _) hB0
            _ = B ^ (s.card + 1) := by
              rw [pow_succ]
              ac_rfl
      | succ j =>
          rw [Polynomial.coeff_X_sub_C_mul]
          have hqj := ih hs' j
          have hqsucc := ih hs' (j + 1)
          have hterm :
              w (α * ((s.map (fun β => X - C β)).prod).coeff (j + 1)) ≤
                B ^ (s.card + 1) := by
            rw [w.map_mul]
            calc
              w α * w (((s.map (fun β => X - C β)).prod).coeff (j + 1)) ≤
                  B * B ^ s.card :=
                mul_le_mul hα hqsucc (w.nonneg _) hB0
              _ = B ^ (s.card + 1) := by
                rw [pow_succ]
                ac_rfl
          have hsum := hstrong
            (((s.map (fun β => X - C β)).prod).coeff j)
            (-α * ((s.map (fun β => X - C β)).prod).coeff (j + 1))
          calc
            w (((s.map (fun β => X - C β)).prod).coeff j -
                α * ((s.map (fun β => X - C β)).prod).coeff (j + 1)) ≤
                max
                  (w (((s.map (fun β => X - C β)).prod).coeff j))
                  (w (α * ((s.map (fun β => X - C β)).prod).coeff (j + 1))) := by
              simpa [sub_eq_add_neg] using hsum
            _ ≤ B ^ (s.card + 1) :=
              max_le (hqj.trans hpow_step) hterm

theorem abs_multiset_prod_eq_pow_card_of_eq
    {L : Type*} [Field L] (w : AbsoluteValue L ℝ)
    (t : ℝ) (s : Multiset L) (hs : ∀ α ∈ s, w α = t) :
    w s.prod = t ^ s.card

theorem uniqueExtensionCoefficients_coeff_abs_le_endpoint_max_of_unique_extension
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    (v : AbsoluteValue K ℝ) (w : AbsoluteValue L ℝ)
    (f : Polynomial K) [IsSplittingField K L f]
    (huniq : IsUniqueNonarchimedeanAbsoluteValueExtension v w)
    (hirr : Irreducible f) :
    ∀ i : ℕ, v (f.coeff i) ≤ max (v (f.coeff 0)) (v f.leadingCoeff)

theorem uniqueExtensionCoefficients_polynomialCoeffAbsMax_eq_endpoint_max
    {K L : Type*} [Field K] [Field L] [Algebra K L]
    (v : AbsoluteValue K ℝ) (w : AbsoluteValue L ℝ)
    (f : Polynomial K) [IsSplittingField K L f]
    (huniq : IsUniqueNonarchimedeanAbsoluteValueExtension v w)
    (hirr : Irreducible f) :
    polynomialCoeffAbsMax v f =
      max (v (f.coeff 0)) (v f.leadingCoeff)