IntertwinerConstruction.lean

structure PadicChangedUniformizerApproximation
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) where
  series : PowerSeries (padicCompletedUnramifiedWittRing p)
  constantCoeff_eq_zero :
    PowerSeries.constantCoeff series = 0
  coeff_one_eq :
    PowerSeries.coeff 1 series =
      (padicChangedUniformizerLinearCoefficient p u :
        padicCompletedUnramifiedWittRing p)

def padicChangedUniformizerApproximation
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) :
    ℕ → PadicChangedUniformizerApproximation p u
  | 0 =>
      { series :=
          PowerSeries.monomial 1
            (padicChangedUniformizerLinearCoefficient p u :
              padicCompletedUnramifiedWittRing p)
        constantCoeff_eq_zero := by
          rw [← PowerSeries.coeff_zero_eq_constantCoeff,
            PowerSeries.coeff_monomial]
          simp
        coeff_one_eq := by simp }
  | n + 1 =>
      let A := padicChangedUniformizerApproximation p u n
      let m := n + 2
      let c :=
        padicChangedUniformizerCorrectionCoefficient
          p u A.series A.constantCoeff_eq_zero m (by omega)
      { series := A.series + PowerSeries.monomial m c
        constantCoeff_eq_zero := by
          rw [map_add, A.constantCoeff_eq_zero,
            ← PowerSeries.coeff_zero_eq_constantCoeff,
            PowerSeries.coeff_monomial]
          simp [m]
        coeff_one_eq := by
          rw [map_add, A.coeff_one_eq,
            PowerSeries.coeff_monomial]
          simp [m] }

theorem padicChangedUniformizerApproximation_succ
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ)
    (n : ℕ) :
    (padicChangedUniformizerApproximation p u (n + 1)).series =
      (padicChangedUniformizerApproximation p u n).series +
        PowerSeries.monomial (n + 2)
          (padicChangedUniformizerCorrectionCoefficient p u
            (padicChangedUniformizerApproximation p u n).series
            (padicChangedUniformizerApproximation p u n).constantCoeff_eq_zero
            (n + 2) (by omega)) :=
  rfl

theorem
    padicChangedUniformizerApproximation_coeff_succ_eq_of_lt
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ)
    (n q : ℕ) (hq : q < n + 2) :
    PowerSeries.coeff q
        (padicChangedUniformizerApproximation p u (n + 1)).series =
      PowerSeries.coeff q
        (padicChangedUniformizerApproximation p u n).series

theorem padicChangedUniformizerApproximation_coeff_eq_of_le
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ)
    (q : ℕ) {a b : ℕ} (hab : a ≤ b)
    (hq : q < a + 2) :
    PowerSeries.coeff q
        (padicChangedUniformizerApproximation p u b).series =
      PowerSeries.coeff q
        (padicChangedUniformizerApproximation p u a).series

theorem
    padicChangedUniformizerApproximation_succ_defect_coeff
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ)
    (n : ℕ) :
    PowerSeries.coeff (n + 2)
        (padicChangedUniformizerDefect p u
          (padicChangedUniformizerApproximation p u (n + 1)).series) =
      0

def padicChangedUniformizerIntertwiner
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) :
    PowerSeries (padicCompletedUnramifiedWittRing p)

theorem padicChangedUniformizerIntertwiner_coeff
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ)
    (m : ℕ) :
    PowerSeries.coeff m
        (padicChangedUniformizerIntertwiner p u) =
      PowerSeries.coeff m
        (padicChangedUniformizerApproximation p u m).series

theorem padicChangedUniformizerIntertwiner_constantCoeff
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) :
    PowerSeries.constantCoeff
        (padicChangedUniformizerIntertwiner p u) = 0

theorem padicChangedUniformizerIntertwiner_coeff_one
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) :
    PowerSeries.coeff 1
        (padicChangedUniformizerIntertwiner p u) =
      (padicChangedUniformizerLinearCoefficient p u :
        padicCompletedUnramifiedWittRing p)

theorem padicChangedUniformizerIntertwiner_hasSubst
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) :
    PowerSeries.HasSubst
      (padicChangedUniformizerIntertwiner p u)

theorem padicChangedUniformizerIntertwiner_coeff_eq_approximation
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ)
    (q a : ℕ) (hq : q < a + 2) :
    PowerSeries.coeff q
        (padicChangedUniformizerIntertwiner p u) =
      PowerSeries.coeff q
        (padicChangedUniformizerApproximation p u a).series

theorem padicChangedUniformizerDefect_coeff_zero
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) :
    PowerSeries.coeff 0
        (padicChangedUniformizerDefect p u
          (padicChangedUniformizerIntertwiner p u)) = 0

theorem padicChangedUniformizerDefect_coeff_one
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) :
    PowerSeries.coeff 1
        (padicChangedUniformizerDefect p u
          (padicChangedUniformizerIntertwiner p u)) = 0

theorem padicChangedUniformizerDefect_coeff_succ_succ
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ)
    (n : ℕ) :
    PowerSeries.coeff (n + 2)
        (padicChangedUniformizerDefect p u
          (padicChangedUniformizerIntertwiner p u)) = 0

theorem padicChangedUniformizerIntertwiner_functionalEquation
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ) :
    PowerSeries.subst
        (padicChangedUniformizerIntertwiner p u)
        (PowerSeries.map
          (padicValuationSubringToCompletedUnramifiedWittRing p)
          (standardLubinTateSeries
            (standardLubinTateChangedUniformizer_isUniformizer
              (padicMultiplicativeLubinTateSeries_isUniformizer p) u)).toPowerSeries) =
      PowerSeries.subst
        (PowerSeries.map
          (padicValuationSubringToCompletedUnramifiedWittRing p)
          (padicMultiplicativeLubinTateSeries p).toPowerSeries)
        (PowerSeries.map WittVector.frobenius
          (padicChangedUniformizerIntertwiner p u))

theorem padicChangedUniformizerIntertwiner_unique
    (p : ℕ) [Fact p.Prime]
    (u : (padicLocalField p).valuationSubringˣ)
    {H H' : PowerSeries (padicCompletedUnramifiedWittRing p)}
    (hHconstant : PowerSeries.constantCoeff H = 0)
    (hH'constant : PowerSeries.constantCoeff H' = 0)
    (hlinear :
      PowerSeries.coeff 1 H = PowerSeries.coeff 1 H')
    (hH :
      PowerSeries.subst H
          (padicCompletedChangedStandardSeries p u) =
        PowerSeries.subst
          (padicCompletedMultiplicativeSeries p)
          (PowerSeries.map WittVector.frobenius H))
    (hH' :
      PowerSeries.subst H'
          (padicCompletedChangedStandardSeries p u) =
        PowerSeries.subst
          (padicCompletedMultiplicativeSeries p)
          (PowerSeries.map WittVector.frobenius H')) :
    H = H'