DegreeStabilization.lean

theorem truncTotal_succ_eq_iff_coeff_eq_degree_le
    {R : Type*} [CommSemiring R]
    {τ : Type*} [Finite τ]
    {H H' : MvPowerSeries τ R} (m : ℕ) :
    H.truncTotal (m + 1) = H'.truncTotal (m + 1) ↔
      ∀ d : τ →₀ ℕ, d.degree ≤ m →
        MvPowerSeries.coeff d H = MvPowerSeries.coeff d H'

theorem truncTotal_powerSeries_subst_eq_of_truncTotal_eq [Finite σ]
    (e : LubinTateSeries F π)
    {H H' : MvPowerSeries σ F.valuationSubring}
    (hH : MvPowerSeries.constantCoeff H = 0)
    (hH' : MvPowerSeries.constantCoeff H' = 0)
    {k : ℕ} (htrunc : H.truncTotal k = H'.truncTotal k) :
    (PowerSeries.subst H e.toPowerSeries).truncTotal k =
      (PowerSeries.subst H' e.toPowerSeries).truncTotal k

theorem truncTotal_inVariables_subst_eq_of_truncTotal_eq [Finite σ]
    (ebar : LubinTateSeries F π)
    {H H' : MvPowerSeries σ F.valuationSubring}
    {k : ℕ} (htrunc : H.truncTotal k = H'.truncTotal k) :
    (MvPowerSeries.subst (fun i : σ ↦ inVariable ebar i) H).truncTotal k =
      (MvPowerSeries.subst (fun i : σ ↦ inVariable ebar i) H').truncTotal k := by
  have hconstant :
      ∀ i : σ,
        MvPowerSeries.constantCoeff (inVariable ebar i) = 0 :=
    fun i ↦ constantCoeff_inVariable ebar i
  calc
    (MvPowerSeries.subst (fun i : σ ↦ inVariable ebar i) H).truncTotal k =
        (MvPowerSeries.subst (fun i : σ ↦ inVariable ebar i)
          (H.truncTotal k).toMvPowerSeries).truncTotal k := by
      exact
        MvPowerSeries.truncTotal_subst_eq_truncTotal_truncTotal_subst
          (f := H) (a := fun i : σ ↦ inVariable ebar i) hconstant
    _ = (MvPowerSeries.subst (fun i : σ ↦ inVariable ebar i)
          (H'.truncTotal k).toMvPowerSeries).truncTotal k := by
      rw [htrunc]
    _ = (MvPowerSeries.subst (fun i : σ ↦ inVariable ebar i) H').truncTotal k := by
      exact
        (MvPowerSeries.truncTotal_subst_eq_truncTotal_truncTotal_subst
          (f := H') (a := fun i : σ ↦ inVariable ebar i) hconstant).symm

theorem coeff_defect_eq_of_coeff_eq_degree_le [Finite σ]
    (e ebar : LubinTateSeries F π)
    {H H' : MvPowerSeries σ F.valuationSubring}
    (hH : MvPowerSeries.constantCoeff H = 0)
    (hH' : MvPowerSeries.constantCoeff H' = 0)
    {m : ℕ}
    (hcoeff : ∀ q : σ →₀ ℕ, q.degree ≤ m →
      MvPowerSeries.coeff q H = MvPowerSeries.coeff q H')
    {d : σ →₀ ℕ} (hd : d.degree ≤ m) :
    MvPowerSeries.coeff d (defect e ebar H) =
      MvPowerSeries.coeff d (defect e ebar H')

theorem degree_le_order_monomial_stabilization
    {R : Type*} [CommRing R] {τ : Type*}
    (d : τ →₀ ℕ) (c : R) :
    (d.degree : ℕ∞) ≤ (MvPowerSeries.monomial d c).order

theorem natCast_le_order_pow_of_one_le_order_stabilization
    {R : Type*} [CommRing R] {τ : Type*}
    (f : MvPowerSeries τ R) (n : ℕ)
    (hf : (1 : ℕ∞) ≤ f.order) :
    (n : ℕ∞) ≤ (f ^ n).order

theorem le_order_finset_sum_stabilization
    {R : Type*} [CommRing R] {τ ι : Type*}
    {s : Finset ι} {f : ι → MvPowerSeries τ R} {m : ℕ∞}
    (h : ∀ i ∈ s, m ≤ (f i).order) :
    m ≤ (∑ i ∈ s, f i).order

theorem natCast_sum_le_order_finset_prod_pow_stabilization
    {R : Type*} [CommRing R] {τ ι : Type*}
    {s : Finset ι} (f : ι → MvPowerSeries τ R) (n : ι → ℕ)
    (hf : ∀ i ∈ s, (1 : ℕ∞) ≤ (f i).order) :
    ((∑ i ∈ s, n i : ℕ) : ℕ∞) ≤
      (∏ i ∈ s, (f i) ^ n i).order

theorem order_sub_add_pred_le_order_pow_sub_pow_stabilization
    {R : Type*} [CommRing R] {τ : Type*}
    (f g : MvPowerSeries τ R)
    (hf : (1 : ℕ∞) ≤ f.order)
    (hg : (1 : ℕ∞) ≤ g.order)
    (n : ℕ) :
    (f - g).order + ((n - 1 : ℕ) : ℕ∞) ≤
      (f ^ n - g ^ n).order

theorem natCast_sum_add_one_le_order_prod_pow_sub_prod_pow_stabilization
    {R : Type*} [CommRing R] {τ ι : Type*}
    {s : Finset ι}
    (f g : ι → MvPowerSeries τ R) (n : ι → ℕ)
    (hn : ∀ i ∈ s, n i ≠ 0)
    (hf : ∀ i ∈ s, (1 : ℕ∞) ≤ (f i).order)
    (hg : ∀ i ∈ s, (1 : ℕ∞) ≤ (g i).order)
    (hfg : ∀ i ∈ s, (2 : ℕ∞) ≤ (f i - g i).order) :
    (((∑ i ∈ s, n i) + 1 : ℕ) : ℕ∞) ≤
      ((∏ i ∈ s, (f i) ^ n i) -
        ∏ i ∈ s, (g i) ^ n i).order

def linearInVariableStabilization
    (π : F.valuationSubring) (i : σ) :
    MvPowerSeries σ F.valuationSubring

theorem linearInVariableStabilization_constantCoeff
    (π : F.valuationSubring) (i : σ) :
    MvPowerSeries.constantCoeff
        (linearInVariableStabilization π i) = 0

theorem linearInVariableStabilization_hasSubst [Finite σ]
    (π : F.valuationSubring) :
    MvPowerSeries.HasSubst
      (linearInVariableStabilization (σ := σ) π)

theorem one_le_order_inVariable_stabilization
    (ebar : LubinTateSeries F π) (i : σ) :
    (1 : ℕ∞) ≤ (inVariable ebar i).order

theorem one_le_order_linearInVariableStabilization
    (π : F.valuationSubring) (i : σ) :
    (1 : ℕ∞) ≤ (linearInVariableStabilization π i).order

theorem two_le_order_inVariable_sub_linearInVariableStabilization
    (ebar : LubinTateSeries F π) (i : σ) :
    (2 : ℕ∞) ≤
      (inVariable ebar i -
        linearInVariableStabilization π i).order

theorem degree_add_one_le_order_subst_monomial_sub_linear_stabilization [Finite σ]
    (ebar : LubinTateSeries F π)
    (d : σ →₀ ℕ) (c : F.valuationSubring) :
    ((d.degree + 1 : ℕ) : ℕ∞) ≤
      (MvPowerSeries.subst (fun i : σ => inVariable ebar i)
          (MvPowerSeries.monomial d c) -
        MvPowerSeries.subst
          (linearInVariableStabilization (σ := σ) π)
          (MvPowerSeries.monomial d c)).order := by
  have hprod :
      ((d.degree + 1 : ℕ) : ℕ∞) ≤
        (d.prod (fun i n => (inVariable ebar i) ^ n) -
          d.prod (fun i n =>
            (linearInVariableStabilization π i) ^ n)).order := by
    simpa only [Finsupp.prod, Finsupp.degree_apply] using
      natCast_sum_add_one_le_order_prod_pow_sub_prod_pow_stabilization
        (s := d.support)
        (fun i : σ => inVariable ebar i)
        (linearInVariableStabilization (σ := σ) π)
        (fun i => d i)
        (fun i hi => Finsupp.mem_support_iff.mp hi)
        (fun i _ => one_le_order_inVariable_stabilization ebar i)
        (fun i _ =>
          one_le_order_linearInVariableStabilization π i)
        (fun i _ =>
          two_le_order_inVariable_sub_linearInVariableStabilization
            ebar i)
  rw [
    MvPowerSeries.subst_monomial
      (inVariable_hasSubst ebar) d c,
    MvPowerSeries.subst_monomial
      (linearInVariableStabilization_hasSubst (σ := σ) π) d c,
    ← MvPowerSeries.c_eq_algebraMap]
  rw [show
    MvPowerSeries.C c *
          d.prod (fun i n => (inVariable ebar i) ^ n) -
        MvPowerSeries.C c *
          d.prod (fun i n =>
            (linearInVariableStabilization π i) ^ n) =
      c •
        (d.prod (fun i n => (inVariable ebar i) ^ n) -
          d.prod (fun i n =>
            (linearInVariableStabilization π i) ^ n)) by
    rw [MvPowerSeries.smul_eq_C_mul]
    ring]
  exact hprod.trans MvPowerSeries.le_order_smul

theorem coeff_subst_linearInVariableStabilization_monomial
    (q d : σ →₀ ℕ) (c : F.valuationSubring) :
    MvPowerSeries.coeff q
        (MvPowerSeries.subst
          (linearInVariableStabilization (σ := σ) π)
          (MvPowerSeries.monomial d c)) =
      if q = d then π ^ d.degree * c else 0 := by
  have hlinear :
      (Function.const σ π •
          (MvPowerSeries.X :
            σ → MvPowerSeries σ F.valuationSubring)) =
        linearInVariableStabilization (σ := σ) π := by
    funext i
    simp [linearInVariableStabilization, Pi.smul_apply',
      MvPowerSeries.smul_eq_C_mul]
  rw [← hlinear, ← MvPowerSeries.rescale_eq_subst,
    MvPowerSeries.coeff_rescale]
  by_cases hqd : q = d
  · subst q
    rw [MvPowerSeries.coeff_monomial_same, ite_eq_left rfl]
    simp only [Finsupp.prod, Function.const_apply,
      Finset.prod_pow_eq_pow_sum, Finsupp.degree_apply]
  · rw [MvPowerSeries.coeff_monomial_ne hqd, mul_zero,
      ite_eq_right hqd]

theorem coeff_subst_inVariables_monomial_of_degree_le [Finite σ]
    (ebar : LubinTateSeries F π)
    (q d : σ →₀ ℕ) (hq : q.degree ≤ d.degree)
    (c : F.valuationSubring) :
    MvPowerSeries.coeff q
        (MvPowerSeries.subst (fun i : σ => inVariable ebar i)
          (MvPowerSeries.monomial d c)) =
      if q = d then π ^ d.degree * c else 0 := by
  have horder :=
    degree_add_one_le_order_subst_monomial_sub_linear_stabilization
      ebar d c
  have hlt :
      (q.degree : ℕ∞) <
        (MvPowerSeries.subst (fun i : σ => inVariable ebar i)
            (MvPowerSeries.monomial d c) -
          MvPowerSeries.subst
            (linearInVariableStabilization (σ := σ) π)
            (MvPowerSeries.monomial d c)).order :=
    by
      have hqNat : q.degree < d.degree + 1 :=
        Nat.lt_succ_of_le hq
      have hqCast :
          (q.degree : ℕ∞) < ((d.degree + 1 : ℕ) : ℕ∞) := by
        exact_mod_cast hqNat
      exact hqCast.trans_le horder
  have hcoeff :=
    MvPowerSeries.coeff_of_lt_order hlt
  rw [map_sub, sub_eq_zero] at hcoeff
  rw [hcoeff,
    coeff_subst_linearInVariableStabilization_monomial]

theorem coeff_subst_inVariables_add_monomial_of_degree_le [Finite σ]
    (ebar : LubinTateSeries F π)
    (H : MvPowerSeries σ F.valuationSubring)
    (q d : σ →₀ ℕ) (hq : q.degree ≤ d.degree)
    (c : F.valuationSubring) :
    MvPowerSeries.coeff q
        (MvPowerSeries.subst (fun i : σ => inVariable ebar i)
          (H + MvPowerSeries.monomial d c)) =
      MvPowerSeries.coeff q
          (MvPowerSeries.subst (fun i : σ => inVariable ebar i) H) +
        if q = d then π ^ d.degree * c else 0 := by
  rw [
    MvPowerSeries.subst_add (inVariable_hasSubst ebar),
    map_add,
    coeff_subst_inVariables_monomial_of_degree_le ebar q d hq c]

theorem constantCoeff_monomial_eq_zero_stabilization
    {R : Type*} [CommRing R] {τ : Type*}
    {d : τ →₀ ℕ} (hd : d ≠ 0) (c : R) :
    MvPowerSeries.constantCoeff (MvPowerSeries.monomial d c) = 0

theorem coeff_pow_add_monomial_sub_pow_of_degree_le
    {R : Type*} [CommRing R] {τ : Type*}
    {H : MvPowerSeries τ R}
    (hH : MvPowerSeries.constantCoeff H = 0)
    (q d : τ →₀ ℕ) (hq : q.degree ≤ d.degree)
    (hd : 1 ≤ d.degree) (c : R) (n : ℕ) :
    MvPowerSeries.coeff q
        ((H + MvPowerSeries.monomial d c) ^ n - H ^ n) =
      if n = 1 then (if q = d then c else 0) else 0 := by
  classical
  have hd0 : d ≠ 0 := by
    intro h
    subst d
    simp at hd
  by_cases hn : n = 1
  · subst n
    simp [MvPowerSeries.coeff_monomial]
  · rcases n with _ | n
    · simp
    · have hn0 : n ≠ 0 := by
        intro h
        apply hn
        omega
      let M := MvPowerSeries.monomial d c
      let A := H + M
      have hMconstant :
          MvPowerSeries.constantCoeff M = 0 :=
        constantCoeff_monomial_eq_zero_stabilization hd0 c
      have hAconstant :
          MvPowerSeries.constantCoeff A = 0 := by
        simp [A, hH, hMconstant]
      have hHorder : (1 : ℕ∞) ≤ H.order :=
        MvPowerSeries.one_le_order_iff_constCoeff_eq_zero.mpr hH
      have hAorder : (1 : ℕ∞) ≤ A.order :=
        MvPowerSeries.one_le_order_iff_constCoeff_eq_zero.mpr hAconstant
      have hpow :
          M.order + (n : ℕ∞) ≤
            (A ^ (n + 1) - H ^ (n + 1)).order := by
        simpa [A, M, add_sub_cancel_left] using
          order_sub_add_pred_le_order_pow_sub_pow_stabilization
            A H hAorder hHorder (n + 1)
      have hdegree : (d.degree : ℕ∞) ≤ M.order :=
        degree_le_order_monomial_stabilization d c
      have hn' : (1 : ℕ∞) ≤ (n : ℕ∞) := by
        exact_mod_cast Nat.one_le_iff_ne_zero.mpr hn0
      have horder :
          ((d.degree + 1 : ℕ) : ℕ∞) ≤
            (A ^ (n + 1) - H ^ (n + 1)).order := by
        calc
          ((d.degree + 1 : ℕ) : ℕ∞) =
              (d.degree : ℕ∞) + 1 := by norm_cast
          _ ≤ M.order + (n : ℕ∞) :=
            add_le_add hdegree hn'
          _ ≤ (A ^ (n + 1) - H ^ (n + 1)).order :=
            hpow
      have hlt :
          (q.degree : ℕ∞) <
            (A ^ (n + 1) - H ^ (n + 1)).order :=
        by
          have hqNat : q.degree < d.degree + 1 :=
            Nat.lt_succ_of_le hq
          have hqCast :
              (q.degree : ℕ∞) <
                ((d.degree + 1 : ℕ) : ℕ∞) := by
            exact_mod_cast hqNat
          exact hqCast.trans_le horder
      have hzero := MvPowerSeries.coeff_of_lt_order hlt
      simpa [A, M, hn, hn0] using hzero

theorem coeff_pow_add_monomial_of_degree_le
    {R : Type*} [CommRing R] {τ : Type*}
    {H : MvPowerSeries τ R}
    (hH : MvPowerSeries.constantCoeff H = 0)
    (q d : τ →₀ ℕ) (hq : q.degree ≤ d.degree)
    (hd : 1 ≤ d.degree) (c : R) (n : ℕ) :
    MvPowerSeries.coeff q
        ((H + MvPowerSeries.monomial d c) ^ n) =
      MvPowerSeries.coeff q (H ^ n) +
        if n = 1 then (if q = d then c else 0) else 0 := by
  have h :=
    coeff_pow_add_monomial_sub_pow_of_degree_le
      hH q d hq hd c n
  rw [map_sub, sub_eq_iff_eq_add] at h
  simpa [add_comm] using h

theorem coeff_subst_lubinTateSeries_add_monomial_of_degree_le
    (e : LubinTateSeries F π)
    {H : MvPowerSeries σ F.valuationSubring}
    (hH : MvPowerSeries.constantCoeff H = 0)
    (q d : σ →₀ ℕ) (hq : q.degree ≤ d.degree)
    (hd : 1 ≤ d.degree) (c : F.valuationSubring) :
    MvPowerSeries.coeff q
        (PowerSeries.subst
          (H + MvPowerSeries.monomial d c)
          e.toPowerSeries) =
      MvPowerSeries.coeff q
          (PowerSeries.subst H e.toPowerSeries) +
        π * (if q = d then c else 0) := by
  have hd0 : d ≠ 0 := by
    intro h
    subst d
    simp at hd
  have hMconstant :
      MvPowerSeries.constantCoeff
          (MvPowerSeries.monomial d c) = 0 :=
    constantCoeff_monomial_eq_zero_stabilization hd0 c
  have hnewSubst :
      PowerSeries.HasSubst
        (H + MvPowerSeries.monomial d c) :=
    PowerSeries.HasSubst.of_constantCoeff_zero (by
      simp [hH, hMconstant])
  have hHsubst : PowerSeries.HasSubst H :=
    PowerSeries.HasSubst.of_constantCoeff_zero hH
  let oldTerm : ℕ → F.valuationSubring := fun n =>
    PowerSeries.coeff n e.toPowerSeries •
      MvPowerSeries.coeff q (H ^ n)
  let deltaTerm : ℕ → F.valuationSubring := fun n =>
    PowerSeries.coeff n e.toPowerSeries •
      if n = 1 then (if q = d then c else 0) else 0
  have hold : Function.HasFiniteSupport oldTerm := by
    simpa only [oldTerm] using
      PowerSeries.coeff_subst_finite hHsubst e.toPowerSeries q
  have hdelta : Function.HasFiniteSupport deltaTerm := by
    rw [Function.HasFiniteSupport]
    refine (Set.finite_singleton 1).subset ?_
    intro n hn
    simp only [Function.mem_support] at hn
    simp only [Set.mem_singleton_iff]
    by_contra hne
    apply hn
    simp [deltaTerm, hne]
  rw [
    PowerSeries.coeff_subst hnewSubst e.toPowerSeries q,
    PowerSeries.coeff_subst hHsubst e.toPowerSeries q]
  calc
    ∑ᶠ n : ℕ,
        PowerSeries.coeff n e.toPowerSeries •
          MvPowerSeries.coeff q
            ((H + MvPowerSeries.monomial d c) ^ n) =
        (∑ᶠ n : ℕ, (oldTerm n + deltaTerm n)) := by
      apply finsum_congr
      intro n
      rw [coeff_pow_add_monomial_of_degree_le
        hH q d hq hd c n, smul_add]
    _ = (∑ᶠ n : ℕ, oldTerm n) +
        ∑ᶠ n : ℕ, deltaTerm n :=
      finsum_add_distrib hold hdelta
    _ = (∑ᶠ n : ℕ, oldTerm n) +
        PowerSeries.coeff 1 e.toPowerSeries *
          (if q = d then c else 0) := by
      congr 1
      rw [finsum_eq_single _ 1]
      · simp [deltaTerm, smul_eq_mul]
      · intro n hn
        simp [deltaTerm, hn]
    _ = (∑ᶠ n : ℕ, oldTerm n) +
        π * (if q = d then c else 0) := by
      rw [LubinTateSeries.coeff_one_eq_uniformizer]

theorem coeff_defect_add_monomial_eq_of_degree_le_constantCoeff [Finite σ]
    (e ebar : LubinTateSeries F π)
    {H : MvPowerSeries σ F.valuationSubring}
    (hH : MvPowerSeries.constantCoeff H = 0)
    (q d : σ →₀ ℕ) (hq : q.degree ≤ d.degree)
    (hd : 1 ≤ d.degree) (c : F.valuationSubring) :
    MvPowerSeries.coeff q
        (defect e ebar (H + MvPowerSeries.monomial d c)) =
      MvPowerSeries.coeff q (defect e ebar H) +
        if q = d then
          π * ((1 - π ^ (d.degree - 1)) * c)
        else 0 := by
  simp only [
    defect,
    map_sub,
    coeff_subst_lubinTateSeries_add_monomial_of_degree_le
      e hH q d hq hd c,
    coeff_subst_inVariables_add_monomial_of_degree_le
      ebar H q d hq c]
  by_cases hqd : q = d
  · subst q
    simp only [ite_eq_left]
    have hdegree : d.degree = (d.degree - 1) + 1 := by
      omega
    have hpow :
        π ^ d.degree = π * π ^ (d.degree - 1) := by
      calc
        π ^ d.degree =
            π ^ ((d.degree - 1) + 1) :=
          congrArg (fun n : ℕ => π ^ n) hdegree
        _ = π * π ^ (d.degree - 1) := by
          rw [pow_succ, mul_comm]
    rw [hpow]
    ring
  · simp [hqd]

theorem coeff_defect_add_monomial_eq_of_degree_le
    (e ebar : LubinTateSeries F π)
    {H : MvPowerSeries σ F.valuationSubring}
    {L : σ → F.valuationSubring} (hH : HasLinearTerm H L)
    (q d : σ →₀ ℕ) (hq : q.degree ≤ d.degree)
    (hd : 2 ≤ d.degree) (c : F.valuationSubring) :
    MvPowerSeries.coeff q
        (defect e ebar (H + MvPowerSeries.monomial d c)) =
      MvPowerSeries.coeff q (defect e ebar H) +
        if q = d then
          π * ((1 - π ^ (d.degree - 1)) * c)
        else 0 :=
  coeff_defect_add_monomial_eq_of_degree_le_constantCoeff
    e ebar hH.constantCoeff_eq_zero q d hq (by omega) c

theorem linearForm_eq_sum_monomial_stabilization
    (L : σ → F.valuationSubring) :
    linearForm L =
      ∑ i, MvPowerSeries.monomial
        (Finsupp.single i 1) (L i)

theorem coeff_defect_sum_linear_monomials_eq_zero [Finite σ]
    (e ebar : LubinTateSeries F π)
    (L : σ → F.valuationSubring)
    (s : Finset σ) (q : σ →₀ ℕ) (hq : q.degree ≤ 1) :
    MvPowerSeries.coeff q
        (defect e ebar
          (∑ i ∈ s, MvPowerSeries.monomial
            (Finsupp.single i 1) (L i))) = 0

theorem coeff_defect_linearForm_eq_zero_of_degree_le_one
    (e ebar : LubinTateSeries F π)
    (L : σ → F.valuationSubring)
    (q : σ →₀ ℕ) (hq : q.degree ≤ 1) :
    MvPowerSeries.coeff q (defect e ebar (linearForm L)) = 0

theorem two_le_order_defect
    (e ebar : LubinTateSeries F π)
    {H : MvPowerSeries σ F.valuationSubring}
    {L : σ → F.valuationSubring} (hH : HasLinearTerm H L) :
    (2 : ℕ∞) ≤ (defect e ebar H).order