Place_mk_taylorCoeff_aeval.lean

theorem coeff_evalEval_C_add_X_congr {K : Type*} [CommRing K] (G : Polynomial (Polynomial K)) (a :
  K)
    (m : ℕ) (Y Y' : PowerSeries K)
    (h : ∀ r, r < m → PowerSeries.coeff r Y = PowerSeries.coeff r Y') :
    ∀ r, r < m →
      PowerSeries.coeff r ((G.map (mapRingHom (algebraMap K (PowerSeries K)))).evalEval
          (PowerSeries.C a + PowerSeries.X) Y)
        = PowerSeries.coeff r ((G.map (mapRingHom (algebraMap K (PowerSeries K)))).evalEval
          (PowerSeries.C a + PowerSeries.X) Y')

theorem taylorCoeff_evalEval_eq_coeff {K F : Type*} [Field K] [Field F] [Algebra K F]
    (v : Place K F) (hv : v.IsRational) {z y : F}
    (hz : z ∈ v.toValuationSubring) (hy : y ∈ v.toValuationSubring)
    (ht : v.ord (z - algebraMap K F (v.evalAt z)) = 1)
    (p : Polynomial (Polynomial K)) (r : ℕ) :
    taylorCoeff v (z - algebraMap K F (v.evalAt z)) r
        ((p.map (mapRingHom (algebraMap K F))).evalEval z y)
      = PowerSeries.coeff r ((p.map (mapRingHom (algebraMap K (PowerSeries K)))).evalEval
          (PowerSeries.C (v.evalAt z) + PowerSeries.X)
          (PowerSeries.mk fun n => taylorCoeff v (z - algebraMap K F (v.evalAt z)) n y)) := by
  have h := mk_taylorCoeff_evalEval v hv ht hz hy p
  rw [mk_taylorCoeff_eq_C_add_X v hv hz ht] at h
  have h2 := congrArg (PowerSeries.coeff r) h
  rwa [PowerSeries.coeff_mk] at h2

theorem inv_mem_of_evalAt_ne_zero {K F : Type*} [Field K] [Field F] [Algebra K F]
    (v : Place K F) (hv : v.IsRational) {s : F} (hs : s ∈ v.toValuationSubring)
    (hs0 : v.evalAt s ≠ 0) : s⁻¹ ∈ v.toValuationSubring

theorem eq_taylorCoeff_inv {K F : Type*} [Field K] [Field F] [Algebra K F]
    (v : Place K F) (hv : v.IsRational) {t : F} (ht : v.ord t = 1)
    {s : F} (hs : s ∈ v.toValuationSubring) (hs0 : v.evalAt s ≠ 0)
    (m : ℕ) (σ : ℕ → K)
    (hσ : ∀ r, r < m →
      ∑ x ∈ Finset.HasAntidiagonal.antidiagonal r, σ x.1 * taylorCoeff v t x.2 s = if r = 0 then 1
        else 0) :
    ∀ r, r < m → σ r = taylorCoeff v t r s⁻¹ := by
  have hsinv : s⁻¹ ∈ v.toValuationSubring := inv_mem_of_evalAt_ne_zero v hv hs hs0
  have hs' : s ≠ 0 := by
    intro h0; apply hs0; rw [h0]
    have := taylorCoeff_algebraMap v t (0 : K) 0
    rw [map_zero] at this
    simpa using this
  have hτ : ∀ r, ∑ x ∈ Finset.HasAntidiagonal.antidiagonal r, taylorCoeff v t x.1 s⁻¹ * taylorCoeff
    v t x.2 s
      = if r = 0 then 1 else 0 := by
    intro r
    rw [← taylorCoeff_mul v hv ht hsinv hs r, inv_mul_cancel₀ hs',
      show (1 : F) = algebraMap K F 1 from (map_one _).symm, taylorCoeff_algebraMap]
  have ha0 : taylorCoeff v t 0 s ≠ 0 := by rwa [taylorCoeff_zero]
  intro r
  induction r using Nat.strong_induction_on with
  | _ r ih =>
    intro hr
    have e1 := hσ r hr
    have e2 := hτ r
    rw [Finset.Nat.sum_antidiagonal_eq_sum_range_succ_mk, Finset.sum_range_succ, Nat.sub_self]
      at e1 e2
    have hsum : ∑ k ∈ Finset.range r, σ k * taylorCoeff v t (r - k) s
        = ∑ k ∈ Finset.range r, taylorCoeff v t k s⁻¹ * taylorCoeff v t (r - k) s :=
      Finset.sum_congr rfl fun k hk =>
        by rw [ih k (Finset.mem_range.mp hk) (by have := Finset.mem_range.mp hk; omega)]
    rw [hsum] at e1
    have e3 : σ r * taylorCoeff v t 0 s = taylorCoeff v t r s⁻¹ * taylorCoeff v t 0 s := by
      have := e1.trans e2.symm
      exact add_left_cancel this
    exact mul_right_cancel₀ ha0 e3

theorem eq_taylorCoeff_of_forall_coeff_evalEval_eq_zero {K F : Type*} [Field K] [Field F] [Algebra
  K F]
    (v : Place K F) (hv : v.IsRational) {z y : F}
    (hz : z ∈ v.toValuationSubring) (hy : y ∈ v.toValuationSubring)
    (ht : v.ord (z - algebraMap K F (v.evalAt z)) = 1)
    (G : Polynomial (Polynomial K))
    (hG : (G.map (Polynomial.mapRingHom (algebraMap K F))).evalEval z y = 0)
    (hsep : (Polynomial.derivative G).evalEval (v.evalAt z) (v.evalAt y) ≠ 0)
    (m : ℕ) (w : ℕ → K) (hw0 : w 0 = v.evalAt y)
    (hw : ∀ r, r < m → PowerSeries.coeff r
        ((G.map (Polynomial.mapRingHom (algebraMap K (PowerSeries K)))).evalEval
          (PowerSeries.C (v.evalAt z) + PowerSeries.X) (PowerSeries.mk w)) = 0) :
    ∀ r, r < m → w r = taylorCoeff v (z - algebraMap K F (v.evalAt z)) r y

theorem coeff_eq_of_forall_coeff_eval_eq_zero {K : Type*} [CommRing K] (f : Polynomial (PowerSeries
  K))
    (a Y : PowerSeries K) (ha : f.eval a = 0)
    (hunit : IsUnit (PowerSeries.constantCoeff (f.derivative.eval a)))
    (h0 : PowerSeries.constantCoeff Y = PowerSeries.constantCoeff a) (m : ℕ)
    (hY : ∀ r, r < m → PowerSeries.coeff r (f.eval Y) = 0) :
    ∀ r, r < m → PowerSeries.coeff r Y = PowerSeries.coeff r a

theorem mk_taylorCoeff_add (v : Place K F) (hv : v.IsRational) {t : F} (ht : v.ord t = 1)
    {f g : F} (hf : f ∈ v.toValuationSubring) (hg : g ∈ v.toValuationSubring) :
    (PowerSeries.mk fun n => taylorCoeff v t n (f + g))
      = (PowerSeries.mk fun n => taylorCoeff v t n f) + (PowerSeries.mk fun n => taylorCoeff v t n
        g) := by
  ext n
  rw [map_add, PowerSeries.coeff_mk, PowerSeries.coeff_mk, PowerSeries.coeff_mk,
    taylorCoeff_add v hv ht hf hg]

theorem mk_taylorCoeff_mul (v : Place K F) (hv : v.IsRational) {t : F} (ht : v.ord t = 1)
    {f g : F} (hf : f ∈ v.toValuationSubring) (hg : g ∈ v.toValuationSubring) :
    (PowerSeries.mk fun n => taylorCoeff v t n (f * g))
      = (PowerSeries.mk fun n => taylorCoeff v t n f) * (PowerSeries.mk fun n => taylorCoeff v t n
        g) := by
  ext n
  rw [PowerSeries.coeff_mk, PowerSeries.coeff_mul, taylorCoeff_mul v hv ht hf hg n]
  exact Finset.sum_congr rfl fun x _ => by rw [PowerSeries.coeff_mk, PowerSeries.coeff_mk]

theorem mk_taylorCoeff_algebraMap (v : Place K F) (t : F) (c : K) :
    (PowerSeries.mk fun n => taylorCoeff v t n (algebraMap K F c)) = PowerSeries.C c := by
  ext n
  rw [PowerSeries.coeff_mk, taylorCoeff_algebraMap, PowerSeries.coeff_C]

theorem aeval_mem_toValuationSubring (v : Place K F) {σ : Type*} (f : σ → F)
    (hf : ∀ s, f s ∈ v.toValuationSubring) (H : MvPolynomial σ K) :
    MvPolynomial.aeval f H ∈ v.toValuationSubring

theorem mk_taylorCoeff_aeval (v : Place K F) (hv : v.IsRational) {t : F} (ht : v.ord t = 1)
    {σ : Type*} (f : σ → F) (hf : ∀ s, f s ∈ v.toValuationSubring) (H : MvPolynomial σ K) :
    (PowerSeries.mk fun n => taylorCoeff v t n (MvPolynomial.aeval f H))
      = MvPolynomial.aeval (fun s => PowerSeries.mk fun n => taylorCoeff v t n (f s)) H := by
  induction H using MvPolynomial.induction_on with
  | C c =>
    rw [MvPolynomial.aeval_C, MvPolynomial.aeval_C, mk_taylorCoeff_algebraMap]
    exact PowerSeries.C_eq_algebraMap (R := K) ▸ rfl
  | add p q hp hq =>
    rw [map_add, map_add, mk_taylorCoeff_add v hv ht (aeval_mem_toValuationSubring v f hf p)
      (aeval_mem_toValuationSubring v f hf q), hp, hq]
  | mul_X p s hp =>
    rw [map_mul, map_mul, MvPolynomial.aeval_X, MvPolynomial.aeval_X,
      mk_taylorCoeff_mul v hv ht (aeval_mem_toValuationSubring v f hf p) (hf s), hp]

theorem coeff_evalEval_sum_monomial_eq {K : Type*} [Field K] (G : Polynomial (Polynomial K)) (a : K)
    {m : ℕ} (w : Fin m → K) (Y : PowerSeries K) (hY : ∀ i : Fin m, PowerSeries.coeff (i : ℕ) Y = w
      i)
    (i : Fin m) :
    ((G.map (mapRingHom (C : K →+* Polynomial K))).evalEval (C a + X)
        (∑ j : Fin m, monomial (j : ℕ) (w j))).coeff i
      = PowerSeries.coeff (i : ℕ) ((G.map (mapRingHom (algebraMap K (PowerSeries K)))).evalEval
          (PowerSeries.C a + PowerSeries.X) Y)

theorem _root_.AlgebraicCurve.Place.mk_taylorCoeff_aeval {K F : Type*} [Field K] [Field F] [Algebra
  K F]
    (v : Place K F) (hv : v.IsRational) {t : F} (ht : v.ord t = 1)
    {σ : Type*} (f : σ → F) (hf : ∀ s, f s ∈ v.toValuationSubring) (H : MvPolynomial σ K) :
    (PowerSeries.mk fun n => taylorCoeff v t n (MvPolynomial.aeval f H))
      = MvPolynomial.aeval (fun s => PowerSeries.mk fun n => taylorCoeff v t n (f s)) H :=
  JetBridge.mk_taylorCoeff_aeval v hv ht f hf H