RecursiveCorrection.lean

def monomialCorrection
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (e ebar : LubinTateSeries F π)
    {H : MvPowerSeries σ F.valuationSubring}
    {L : σ → F.valuationSubring} (hH : HasLinearTerm H L)
    (d : σ →₀ ℕ) (hd : 2 ≤ d.degree) :
    MvPowerSeries σ F.valuationSubring

def correctedIntertwiner
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (e ebar : LubinTateSeries F π)
    {H : MvPowerSeries σ F.valuationSubring}
    {L : σ → F.valuationSubring} (hH : HasLinearTerm H L)
    (d : σ →₀ ℕ) (hd : 2 ≤ d.degree) :
    MvPowerSeries σ F.valuationSubring

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

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

theorem le_order_finset_sum
    {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
    {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
    {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
    {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 linearInVariable
    (π : F.valuationSubring) (i : σ) :
    MvPowerSeries σ F.valuationSubring

theorem linearInVariable_constantCoeff
    (π : F.valuationSubring) (i : σ) :
    MvPowerSeries.constantCoeff (linearInVariable π i) = 0

theorem linearInVariable_hasSubst [Finite σ]
    (π : F.valuationSubring) :
    MvPowerSeries.HasSubst (linearInVariable (σ := σ) π)

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

theorem one_le_order_linearInVariable
    (π : F.valuationSubring) (i : σ) :
    (1 : ℕ∞) ≤ (linearInVariable π i).order

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

theorem degree_add_one_le_order_subst_monomial_sub_linear [Finite σ]
    (ebar : LubinTateSeries F π)
    (d : σ →₀ ℕ) (c : F.valuationSubring) :
    ((d.degree + 1 : ℕ) : ℕ∞) ≤
      (MvPowerSeries.subst (fun i : σ => inVariable ebar i)
          (MvPowerSeries.monomial d c) -
        MvPowerSeries.subst (linearInVariable (σ := σ) π)
          (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 => (linearInVariable π i) ^ n)).order := by
    simpa only [Finsupp.prod, Finsupp.degree_apply] using
      natCast_sum_add_one_le_order_prod_pow_sub_prod_pow
        (s := d.support)
        (fun i : σ => inVariable ebar i)
        (linearInVariable (σ := σ) π)
        (fun i => d i)
        (fun i hi => Finsupp.mem_support_iff.mp hi)
        (fun i _ => one_le_order_inVariable ebar i)
        (fun i _ => one_le_order_linearInVariable π i)
        (fun i _ =>
          two_le_order_inVariable_sub_linearInVariable ebar i)
  rw [
    MvPowerSeries.subst_monomial
      (inVariable_hasSubst ebar) d c,
    MvPowerSeries.subst_monomial
      (linearInVariable_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 => (linearInVariable π i) ^ n) =
      c •
        (d.prod (fun i n => (inVariable ebar i) ^ n) -
          d.prod (fun i n => (linearInVariable π i) ^ n)) by
    rw [MvPowerSeries.smul_eq_C_mul]
    ring]
  exact hprod.trans MvPowerSeries.le_order_smul

theorem coeff_subst_linearInVariable_monomial
    (d : σ →₀ ℕ) (c : F.valuationSubring) :
    MvPowerSeries.coeff d
        (MvPowerSeries.subst (linearInVariable (σ := σ) π)
          (MvPowerSeries.monomial d c)) =
      π ^ d.degree * c

theorem coeff_subst_inVariables_monomial [Finite σ]
    (ebar : LubinTateSeries F π)
    (d : σ →₀ ℕ) (c : F.valuationSubring) :
    MvPowerSeries.coeff d
        (MvPowerSeries.subst (fun i : σ => inVariable ebar i)
          (MvPowerSeries.monomial d c)) =
      π ^ d.degree * c := by
  have horder :=
    degree_add_one_le_order_subst_monomial_sub_linear ebar d c
  have hlt :
      (d.degree : ℕ∞) <
        (MvPowerSeries.subst (fun i : σ => inVariable ebar i)
            (MvPowerSeries.monomial d c) -
          MvPowerSeries.subst (linearInVariable (σ := σ) π)
            (MvPowerSeries.monomial d c)).order :=
    by
      have hdegree_lt :
          (d.degree : ℕ∞) < ((d.degree + 1 : ℕ) : ℕ∞) := by
        exact_mod_cast Nat.lt_succ_self d.degree
      exact hdegree_lt.trans_le horder
  have hcoeff :=
    MvPowerSeries.coeff_of_lt_order hlt
  rw [map_sub, sub_eq_zero] at hcoeff
  rw [hcoeff, coeff_subst_linearInVariable_monomial]

theorem coeff_subst_inVariables_add_monomial [Finite σ]
    (ebar : LubinTateSeries F π)
    (H : MvPowerSeries σ F.valuationSubring)
    (d : σ →₀ ℕ) (c : F.valuationSubring) :
    MvPowerSeries.coeff d
        (MvPowerSeries.subst (fun i : σ ↦ inVariable ebar i)
          (H + MvPowerSeries.monomial d c)) =
      MvPowerSeries.coeff d
          (MvPowerSeries.subst (fun i : σ ↦ inVariable ebar i) H) +
        π ^ d.degree * c := by
  rw [
    MvPowerSeries.subst_add (inVariable_hasSubst ebar),
    map_add,
    coeff_subst_inVariables_monomial]

theorem constantCoeff_monomial_eq_zero
    {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
    {R : Type*} [CommRing R] {τ : Type*}
    {H : MvPowerSeries τ R}
    (hH : MvPowerSeries.constantCoeff H = 0)
    (d : τ →₀ ℕ) (hd : 2 ≤ d.degree) (c : R) (n : ℕ) :
    MvPowerSeries.coeff d
        ((H + MvPowerSeries.monomial d c) ^ n - H ^ n) =
      if n = 1 then c 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_same]
  · 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 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
            A H hAorder hHorder (n + 1)
      have hdegree : (d.degree : ℕ∞) ≤ M.order :=
        degree_le_order_monomial 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 :
          (d.degree : ℕ∞) <
            (A ^ (n + 1) - H ^ (n + 1)).order :=
        by
          have hdegree_lt :
              (d.degree : ℕ∞) < ((d.degree + 1 : ℕ) : ℕ∞) := by
            exact_mod_cast Nat.lt_succ_self d.degree
          exact hdegree_lt.trans_le horder
      have hzero := MvPowerSeries.coeff_of_lt_order hlt
      simpa [A, M, hn0] using hzero

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

theorem coeff_subst_lubinTateSeries_add_monomial
    (e : LubinTateSeries F π)
    {H : MvPowerSeries σ F.valuationSubring}
    {L : σ → F.valuationSubring} (hH : HasLinearTerm H L)
    (d : σ →₀ ℕ) (hd : 2 ≤ d.degree)
    (c : F.valuationSubring) :
    MvPowerSeries.coeff d
        (PowerSeries.subst
          (H + MvPowerSeries.monomial d c)
          e.toPowerSeries) =
      MvPowerSeries.coeff d
          (PowerSeries.subst H e.toPowerSeries) +
        π * c

theorem coeff_defect_add_monomial
    (e ebar : LubinTateSeries F π)
    {H : MvPowerSeries σ F.valuationSubring}
    {L : σ → F.valuationSubring} (hH : HasLinearTerm H L)
    (d : σ →₀ ℕ) (hd : 2 ≤ d.degree)
    (c : F.valuationSubring) :
    MvPowerSeries.coeff d
        (defect e ebar (H + MvPowerSeries.monomial d c)) =
      MvPowerSeries.coeff d (defect e ebar H) +
        π * ((1 - π ^ (d.degree - 1)) * c)

theorem correctedIntertwiner_hasLinearTerm
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (e ebar : LubinTateSeries F π)
    {H : MvPowerSeries σ F.valuationSubring}
    {L : σ → F.valuationSubring} (hH : HasLinearTerm H L)
    (d : σ →₀ ℕ) (hd : 2 ≤ d.degree) :
    HasLinearTerm (correctedIntertwiner hπ e ebar hH d hd) L

theorem coeff_defect_correctedIntertwiner_eq_zero
    (hπ : F.toCompleteDVF.valuation.IsUniformizer (π : K))
    (e ebar : LubinTateSeries F π)
    {H : MvPowerSeries σ F.valuationSubring}
    {L : σ → F.valuationSubring} (hH : HasLinearTerm H L)
    (d : σ →₀ ℕ) (hd : 2 ≤ d.degree) :
    MvPowerSeries.coeff d
        (defect e ebar
          (correctedIntertwiner hπ e ebar hH d hd)) = 0