LogConvergence.lean

theorem logOnePlusSeriesField_eq_self_add_tsum_succ_of_summable
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ))) (x : K)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hs :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      Summable (fun n : ℕ => signedLogSeriesTermField x hnK n)) :
    letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
    logOnePlusSeriesFieldOfWithZeroValuation v x hnK =
      x + ∑' n : ℕ, signedLogSeriesTermField x hnK (n + 1) := by
  let : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  have hs' : Summable (fun n : ℕ => signedLogSeriesTermField x hnK n) := hs
  calc
    logOnePlusSeriesFieldOfWithZeroValuation v x hnK =
        ∑' n : ℕ, signedLogSeriesTermField x hnK n := by
      rfl
    _ = signedLogSeriesTermField x hnK 0 +
        ∑' n : ℕ, signedLogSeriesTermField x hnK (n + 1) :=
      hs'.tsum_eq_zero_add
    _ = x + ∑' n : ℕ, signedLogSeriesTermField x hnK (n + 1) := by
      simp

theorem expSeriesField_eq_one_add_tsum_succ_of_summable
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ))) (x : K)
    (hnK : ∀ n : ℕ, (((n.factorial : ℕ) : K) ≠ 0))
    (hs :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      Summable (fun n : ℕ => expSeriesTermField x hnK n)) :
    letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
    expSeriesFieldOfWithZeroValuation v x hnK =
      1 + ∑' n : ℕ, expSeriesTermField x hnK (n + 1) := by
  let : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  have hs' : Summable (fun n : ℕ => expSeriesTermField x hnK n) := hs
  calc
    expSeriesFieldOfWithZeroValuation v x hnK =
        ∑' n : ℕ, expSeriesTermField x hnK n := by
      rfl
    _ = expSeriesTermField x hnK 0 +
        ∑' n : ℕ, expSeriesTermField x hnK (n + 1) :=
      hs'.tsum_eq_zero_add
    _ = 1 + ∑' n : ℕ, expSeriesTermField x hnK (n + 1) := by
      simp

theorem logSeriesTermField_eq_zero_of_eq_zero
    {x : K} (hx : x = 0)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0)) (n : ℕ) :
    logSeriesTermField x hnK n = 0

theorem signedLogSeriesTermField_eq_zero_of_eq_zero
    {x : K} (hx : x = 0)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0)) (n : ℕ) :
    signedLogSeriesTermField x hnK n = 0

theorem logOnePlusSeriesField_zero_ofWithZeroValuation
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0)) :
    logOnePlusSeriesFieldOfWithZeroValuation v 0 hnK = 0

theorem tendsto_zero_logSeriesTermField_ofWithZeroValuation_of_lt_one
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    {p : ℕ} [Fact p.Prime] (x : K)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-(padicValNat p (n + 1) : ℤ)))
    (hvx : v x < (1 : WithZero (Multiplicative ℤ))) :
    letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
    Tendsto (fun n : ℕ => logSeriesTermField x hnK n) atTop
      (𝓝 (0 : K)) := by
  let : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  by_cases hx : x = 0
  · have hconst :
        (fun n : ℕ => logSeriesTermField x hnK n) =
          fun _ : ℕ => (0 : K) := by
      funext n
      exact logSeriesTermField_eq_zero_of_eq_zero hx hnK n
    simp [hconst]
  · have hxpos :
        0 < (ofWithZeroValuation v).val (Units.mk0 x hx) :=
      ofWithZeroValuation_val_mk0_pos_of_lt_one (v := v) hx hvx
    have hunit :=
      tendsto_zero_log_term_ofWithZeroValuation_of_pos
        (v := v) (p := p) (Units.mk0 x hx) hnK hnval hxpos
    simpa [logSeriesTermField, logSeriesTerm] using hunit

theorem tendsto_zero_signedLogSeriesTermField_ofWithZeroValuation_of_lt_one
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    {p : ℕ} [Fact p.Prime] (x : K)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-(padicValNat p (n + 1) : ℤ)))
    (hvx : v x < (1 : WithZero (Multiplicative ℤ))) :
    letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
    Tendsto (fun n : ℕ => signedLogSeriesTermField x hnK n) atTop
      (𝓝 (0 : K)) := by
  let : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  by_cases hx : x = 0
  · have hconst :
        (fun n : ℕ => signedLogSeriesTermField x hnK n) =
          fun _ : ℕ => (0 : K) := by
      funext n
      exact signedLogSeriesTermField_eq_zero_of_eq_zero hx hnK n
    simp [hconst]
  · have hxpos :
        0 < (ofWithZeroValuation v).val (Units.mk0 x hx) :=
      ofWithZeroValuation_val_mk0_pos_of_lt_one (v := v) hx hvx
    have hunit :=
      tendsto_zero_signed_log_term_ofWithZeroValuation_of_pos
        (v := v) (p := p) (Units.mk0 x hx) hnK hnval hxpos
    simpa [signedLogSeriesTermField, logSeriesTermField] using hunit

theorem summable_logSeriesTermField_ofWithZeroValuation_of_lt_one
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    {p : ℕ} [Fact p.Prime] (x : K)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-(padicValNat p (n + 1) : ℤ)))
    (hvx : v x < (1 : WithZero (Multiplicative ℤ)))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
    Summable (fun n : ℕ => logSeriesTermField x hnK n) := by
  let : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  let : CompleteSpace K := hcomplete
  have : NonarchimedeanRing K := nonarchimedeanRing_ofWithZeroValuation v
  have hzero :
      Tendsto (fun n : ℕ => logSeriesTermField x hnK n) atTop
        (𝓝 (0 : K)) :=
    tendsto_zero_logSeriesTermField_ofWithZeroValuation_of_lt_one
      (v := v) (p := p) x hnK hnval hvx
  have hcofinite :
      Tendsto (fun n : ℕ => logSeriesTermField x hnK n) cofinite
        (𝓝 (0 : K)) := by
    simpa [Nat.cofinite_eq_atTop] using hzero
  rw [NonarchimedeanAddGroup.summable_iff_tendsto_cofinite_zero]
  exact hcofinite

theorem summable_signedLogSeriesTermField_ofWithZeroValuation_of_lt_one
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    {p : ℕ} [Fact p.Prime] (x : K)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-(padicValNat p (n + 1) : ℤ)))
    (hvx : v x < (1 : WithZero (Multiplicative ℤ)))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
    Summable (fun n : ℕ => signedLogSeriesTermField x hnK n) := by
  let : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  let : CompleteSpace K := hcomplete
  have : NonarchimedeanRing K := nonarchimedeanRing_ofWithZeroValuation v
  have hzero :
      Tendsto (fun n : ℕ => signedLogSeriesTermField x hnK n) atTop
        (𝓝 (0 : K)) :=
    tendsto_zero_signedLogSeriesTermField_ofWithZeroValuation_of_lt_one
      (v := v) (p := p) x hnK hnval hvx
  have hcofinite :
      Tendsto (fun n : ℕ => signedLogSeriesTermField x hnK n) cofinite
        (𝓝 (0 : K)) := by
    simpa [Nat.cofinite_eq_atTop] using hzero
  rw [NonarchimedeanAddGroup.summable_iff_tendsto_cofinite_zero]
  exact hcofinite

theorem hasSum_signedLogSeriesTermField_logOnePlusSeriesField_ofWithZeroValuation_of_lt_one
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    {p : ℕ} [Fact p.Prime] (x : K)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-(padicValNat p (n + 1) : ℤ)))
    (hvx : v x < (1 : WithZero (Multiplicative ℤ)))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
    HasSum (fun n : ℕ => signedLogSeriesTermField x hnK n)
      (logOnePlusSeriesFieldOfWithZeroValuation v x hnK) := by
  let : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  have hs :
      Summable (fun n : ℕ => signedLogSeriesTermField x hnK n) :=
    summable_signedLogSeriesTermField_ofWithZeroValuation_of_lt_one
      (v := v) (p := p) x hnK hnval hvx hcomplete
  simpa [logOnePlusSeriesFieldOfWithZeroValuation] using hs.hasSum

theorem hasSum_powerSeries_log_eval_logOnePlusSeriesField
    [Algebra ℚ K]
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    {p : ℕ} [Fact p.Prime] (x : K)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-(padicValNat p (n + 1) : ℤ)))
    (hvx : v x < (1 : WithZero (Multiplicative ℤ)))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
    HasSum
      (fun n : ℕ =>
        PowerSeries.coeff (n + 1) (PowerSeries.log K) *
          x ^ (n + 1))
      (logOnePlusSeriesFieldOfWithZeroValuation v x hnK) := by
  let : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  have hsum :=
    hasSum_signedLogSeriesTermField_logOnePlusSeriesField_ofWithZeroValuation_of_lt_one
      (v := v) (p := p) x hnK hnval hvx hcomplete
  exact hsum.congr_fun fun n =>
    powerSeries_log_coeff_mul_pow_eq_signedLogSeriesTermField
      (K := K) x hnK n

theorem hasSum_powerSeries_log_eval_nat_logOnePlusSeriesField
    [Algebra ℚ K]
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    {p : ℕ} [Fact p.Prime] (x : K)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-(padicValNat p (n + 1) : ℤ)))
    (hvx : v x < (1 : WithZero (Multiplicative ℤ)))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
    HasSum
      (fun n : ℕ =>
        PowerSeries.coeff n (PowerSeries.log K) * x ^ n)
      (logOnePlusSeriesFieldOfWithZeroValuation v x hnK) := by
  let : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  let f : ℕ → K := fun n =>
    PowerSeries.coeff n (PowerSeries.log K) * x ^ n
  have htail :
      HasSum (fun n : ℕ => f (n + 1))
        (logOnePlusSeriesFieldOfWithZeroValuation v x hnK) := by
    simpa only [f] using
      hasSum_powerSeries_log_eval_logOnePlusSeriesField
        (v := v) (p := p) x hnK hnval hvx hcomplete
  have hfull :=
    (hasSum_nat_add_iff
      (f := f)
      (g := logOnePlusSeriesFieldOfWithZeroValuation v x hnK) 1).1 htail
  simpa [f, PowerSeries.coeff_log] using hfull

theorem hasSum_formalLogOnePlusLeftVariableLogSubst_monomialValue_pair
    [Algebra ℚ K]
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    {p : ℕ} [Fact p.Prime] (x y : K)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-(padicValNat p (n + 1) : ℤ)))
    (hvx : v x < (1 : WithZero (Multiplicative ℤ)))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
    HasSum
      (fun d : Fin 2 →₀ ℕ =>
        MvPowerSeries.coeff d (formalLogOnePlusLeftVariableLogSubst K) *
          mvPowerSeriesMonomialValue
            (fun i : Fin 2 => if i = 0 then x else y) d)
      (logOnePlusSeriesFieldOfWithZeroValuation v x hnK) := by
  let : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  let term : (Fin 2 →₀ ℕ) → K := fun d =>
    MvPowerSeries.coeff d (formalLogOnePlusLeftVariableLogSubst K) *
      mvPowerSeriesMonomialValue
        (fun i : Fin 2 => if i = 0 then x else y) d
  let axis : ℕ → (Fin 2 →₀ ℕ) := fun n => Finsupp.single (0 : Fin 2) n
  have haxis_inj : Function.Injective axis := by
    intro m n h
    have hcoord := congrArg (fun d : Fin 2 →₀ ℕ => d (0 : Fin 2)) h
    simpa [axis] using hcoord
  have haxis :
      HasSum (term ∘ axis)
        (logOnePlusSeriesFieldOfWithZeroValuation v x hnK) := by
    refine
      (hasSum_powerSeries_log_eval_nat_logOnePlusSeriesField
        (v := v) (p := p) x hnK hnval hvx hcomplete).congr_fun ?_
    intro n
    simp [term, axis, formalLogOnePlusLeftVariableLogSubst_coeff_single,
      mvPowerSeriesMonomialValue]
  have hout : ∀ d, d ∉ Set.range axis → term d = 0 := by
    intro d hd
    have hne : ∀ n : ℕ, d ≠ Finsupp.single (0 : Fin 2) n := by
      intro n h
      exact hd ⟨n, by simpa [axis] using h.symm⟩
    simp [term, formalLogOnePlusLeftVariableLogSubst_coeff_of_ne_axis K d hne]
  exact (haxis_inj.hasSum_iff (f := term) hout).1 haxis

theorem hasSum_formalLogOnePlusRightVariableLogSubst_monomialValue_pair
    [Algebra ℚ K]
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    {p : ℕ} [Fact p.Prime] (x y : K)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-(padicValNat p (n + 1) : ℤ)))
    (hvy : v y < (1 : WithZero (Multiplicative ℤ)))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
    HasSum
      (fun d : Fin 2 →₀ ℕ =>
        MvPowerSeries.coeff d (formalLogOnePlusRightVariableLogSubst K) *
          mvPowerSeriesMonomialValue
            (fun i : Fin 2 => if i = 0 then x else y) d)
      (logOnePlusSeriesFieldOfWithZeroValuation v y hnK) := by
  let : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  let term : (Fin 2 →₀ ℕ) → K := fun d =>
    MvPowerSeries.coeff d (formalLogOnePlusRightVariableLogSubst K) *
      mvPowerSeriesMonomialValue
        (fun i : Fin 2 => if i = 0 then x else y) d
  let axis : ℕ → (Fin 2 →₀ ℕ) := fun n => Finsupp.single (1 : Fin 2) n
  have haxis_inj : Function.Injective axis := by
    intro m n h
    have hcoord := congrArg (fun d : Fin 2 →₀ ℕ => d (1 : Fin 2)) h
    simpa [axis] using hcoord
  have haxis :
      HasSum (term ∘ axis)
        (logOnePlusSeriesFieldOfWithZeroValuation v y hnK) := by
    refine
      (hasSum_powerSeries_log_eval_nat_logOnePlusSeriesField
        (v := v) (p := p) y hnK hnval hvy hcomplete).congr_fun ?_
    intro n
    simp [term, axis, formalLogOnePlusRightVariableLogSubst_coeff_single,
      mvPowerSeriesMonomialValue]
  have hout : ∀ d, d ∉ Set.range axis → term d = 0 := by
    intro d hd
    have hne : ∀ n : ℕ, d ≠ Finsupp.single (1 : Fin 2) n := by
      intro n h
      exact hd ⟨n, by simpa [axis] using h.symm⟩
    simp [term, formalLogOnePlusRightVariableLogSubst_coeff_of_ne_axis K d hne]
  exact (haxis_inj.hasSum_iff (f := term) hout).1 haxis

theorem hasSum_formalLogOnePlusProductRightSide_monomialValue_pair
    [Algebra ℚ K]
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    {p : ℕ} [Fact p.Prime] (x y : K)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-(padicValNat p (n + 1) : ℤ)))
    (hvx : v x < (1 : WithZero (Multiplicative ℤ)))
    (hvy : v y < (1 : WithZero (Multiplicative ℤ)))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
    HasSum
      (fun d : Fin 2 →₀ ℕ =>
        MvPowerSeries.coeff d (formalLogOnePlusProductRightSide K) *
          mvPowerSeriesMonomialValue
            (fun i : Fin 2 => if i = 0 then x else y) d)
      (logOnePlusSeriesFieldOfWithZeroValuation v x hnK +
        logOnePlusSeriesFieldOfWithZeroValuation v y hnK) := by
  let : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  have hleft :=
    hasSum_formalLogOnePlusLeftVariableLogSubst_monomialValue_pair
      (v := v) (p := p) x y hnK hnval hvx hcomplete
  have hright :=
    hasSum_formalLogOnePlusRightVariableLogSubst_monomialValue_pair
      (v := v) (p := p) x y hnK hnval hvy hcomplete
  refine (hleft.add hright).congr_fun ?_
  intro d
  rw [formalLogOnePlusProductRightSide_coeff]
  ring

theorem tendsto_logOnePlusPartialSumField_ofWithZeroValuation_of_lt_one
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    {p : ℕ} [Fact p.Prime] (x : K)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-(padicValNat p (n + 1) : ℤ)))
    (hvx : v x < (1 : WithZero (Multiplicative ℤ)))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
    Tendsto (fun N : ℕ => logOnePlusPartialSumField x hnK N) atTop
      (𝓝 (logOnePlusSeriesFieldOfWithZeroValuation v x hnK)) := by
  let : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  have hsum :=
    hasSum_signedLogSeriesTermField_logOnePlusSeriesField_ofWithZeroValuation_of_lt_one
      (v := v) (p := p) x hnK hnval hvx hcomplete
  simpa [logOnePlusPartialSumField] using hsum.tendsto_sum_nat

theorem tendsto_zero_signedLogSeriesTermField_ofWithZeroValuation_scaled_of_lt_one
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    {p : ℕ} [Fact p.Prime] (e : ℕ) (x : K)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-((e : ℤ) * (padicValNat p (n + 1) : ℤ))))
    (hvx : v x < (1 : WithZero (Multiplicative ℤ))) :
    letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
    Tendsto (fun n : ℕ => signedLogSeriesTermField x hnK n) atTop
      (𝓝 (0 : K)) := by
  let : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  by_cases hx : x = 0
  · have hconst :
        (fun n : ℕ => signedLogSeriesTermField x hnK n) =
          fun _ : ℕ => (0 : K) := by
      funext n
      exact signedLogSeriesTermField_eq_zero_of_eq_zero hx hnK n
    simp [hconst]
  · have hxpos :
        0 < (ofWithZeroValuation v).val (Units.mk0 x hx) :=
      ofWithZeroValuation_val_mk0_pos_of_lt_one (v := v) hx hvx
    have hunit :=
      tendsto_zero_signed_log_term_ofWithZeroValuation_scaled_of_pos
        (v := v) (p := p) e (Units.mk0 x hx) hnK hnval hxpos
    simpa [signedLogSeriesTermField, logSeriesTermField] using hunit

theorem summable_signedLogSeriesTermField_ofWithZeroValuation_scaled_of_lt_one
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    {p : ℕ} [Fact p.Prime] (e : ℕ) (x : K)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-((e : ℤ) * (padicValNat p (n + 1) : ℤ))))
    (hvx : v x < (1 : WithZero (Multiplicative ℤ)))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
    Summable (fun n : ℕ => signedLogSeriesTermField x hnK n) := by
  let : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  let : CompleteSpace K := hcomplete
  have : NonarchimedeanRing K := nonarchimedeanRing_ofWithZeroValuation v
  have hzero :
      Tendsto (fun n : ℕ => signedLogSeriesTermField x hnK n) atTop
        (𝓝 (0 : K)) :=
    tendsto_zero_signedLogSeriesTermField_ofWithZeroValuation_scaled_of_lt_one
      (v := v) (p := p) e x hnK hnval hvx
  have hcofinite :
      Tendsto (fun n : ℕ => signedLogSeriesTermField x hnK n) cofinite
        (𝓝 (0 : K)) := by
    simpa [Nat.cofinite_eq_atTop] using hzero
  rw [NonarchimedeanAddGroup.summable_iff_tendsto_cofinite_zero]
  exact hcofinite

theorem hasSum_signedLogSeriesTermField_logOnePlusSeriesField_ofWithZeroValuation_scaled_of_lt_one
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    {p : ℕ} [Fact p.Prime] (e : ℕ) (x : K)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-((e : ℤ) * (padicValNat p (n + 1) : ℤ))))
    (hvx : v x < (1 : WithZero (Multiplicative ℤ)))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
    HasSum (fun n : ℕ => signedLogSeriesTermField x hnK n)
      (logOnePlusSeriesFieldOfWithZeroValuation v x hnK) := by
  let : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  have hs :
      Summable (fun n : ℕ => signedLogSeriesTermField x hnK n) :=
    summable_signedLogSeriesTermField_ofWithZeroValuation_scaled_of_lt_one
      (v := v) (p := p) e x hnK hnval hvx hcomplete
  simpa [logOnePlusSeriesFieldOfWithZeroValuation] using hs.hasSum

theorem tendsto_logOnePlusPartialSumField_ofWithZeroValuation_scaled_of_lt_one
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    {p : ℕ} [Fact p.Prime] (e : ℕ) (x : K)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-((e : ℤ) * (padicValNat p (n + 1) : ℤ))))
    (hvx : v x < (1 : WithZero (Multiplicative ℤ)))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
    Tendsto (fun N : ℕ => logOnePlusPartialSumField x hnK N) atTop
      (𝓝 (logOnePlusSeriesFieldOfWithZeroValuation v x hnK)) := by
  let : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  have hsum :=
    hasSum_signedLogSeriesTermField_logOnePlusSeriesField_ofWithZeroValuation_scaled_of_lt_one
      (v := v) (p := p) e x hnK hnval hvx hcomplete
  simpa [logOnePlusPartialSumField] using hsum.tendsto_sum_nat

theorem hasSum_signedLogSeriesTermField_add_logOnePlusSeriesField
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    {p : ℕ} [Fact p.Prime] (x y : K)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-(padicValNat p (n + 1) : ℤ)))
    (hvx : v x < (1 : WithZero (Multiplicative ℤ)))
    (hvy : v y < (1 : WithZero (Multiplicative ℤ)))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
    HasSum
      (fun n : ℕ =>
        signedLogSeriesTermField x hnK n +
          signedLogSeriesTermField y hnK n)
      (logOnePlusSeriesFieldOfWithZeroValuation v x hnK +
        logOnePlusSeriesFieldOfWithZeroValuation v y hnK) := by
  let : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  exact
    (hasSum_signedLogSeriesTermField_logOnePlusSeriesField_ofWithZeroValuation_of_lt_one
      (v := v) (p := p) x hnK hnval hvx hcomplete).add
      (hasSum_signedLogSeriesTermField_logOnePlusSeriesField_ofWithZeroValuation_of_lt_one
        (v := v) (p := p) y hnK hnval hvy hcomplete)

theorem logOnePlusPartialSumField_add_eq_sum_add_terms
    (x y : K)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0)) (N : ℕ) :
    logOnePlusPartialSumField x hnK N +
        logOnePlusPartialSumField y hnK N =
      ∑ n ∈ Finset.range N,
        (signedLogSeriesTermField x hnK n +
          signedLogSeriesTermField y hnK n)

theorem tendsto_logOnePlusPartialSumField_add
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    {p : ℕ} [Fact p.Prime] (x y : K)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-(padicValNat p (n + 1) : ℤ)))
    (hvx : v x < (1 : WithZero (Multiplicative ℤ)))
    (hvy : v y < (1 : WithZero (Multiplicative ℤ)))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
    Tendsto
      (fun N : ℕ =>
        logOnePlusPartialSumField x hnK N +
          logOnePlusPartialSumField y hnK N)
      atTop
      (𝓝 (logOnePlusSeriesFieldOfWithZeroValuation v x hnK +
        logOnePlusSeriesFieldOfWithZeroValuation v y hnK)) := by
  let : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  have hx :=
    tendsto_logOnePlusPartialSumField_ofWithZeroValuation_of_lt_one
      (v := v) (p := p) x hnK hnval hvx hcomplete
  have hy :=
    tendsto_logOnePlusPartialSumField_ofWithZeroValuation_of_lt_one
      (v := v) (p := p) y hnK hnval hvy hcomplete
  exact hx.add hy

theorem logOnePlusSeriesField_eq_self_add_tsum_succ_ofWithZeroValuation_of_lt_one
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    {p : ℕ} [Fact p.Prime] (x : K)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-(padicValNat p (n + 1) : ℤ)))
    (hvx : v x < (1 : WithZero (Multiplicative ℤ)))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
    logOnePlusSeriesFieldOfWithZeroValuation v x hnK =
      x + ∑' n : ℕ, signedLogSeriesTermField x hnK (n + 1) := by
  let : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  exact
    logOnePlusSeriesField_eq_self_add_tsum_succ_of_summable v x hnK
      (summable_signedLogSeriesTermField_ofWithZeroValuation_of_lt_one
        (v := v) (p := p) x hnK hnval hvx hcomplete)

theorem logSeriesTermField_ne_zero_of_ne_zero
    {x : K} (hx : x ≠ 0)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0)) (n : ℕ) :
    logSeriesTermField x hnK n ≠ 0

theorem valuation_logSeriesTermField_lt_self_of_inv_sub_one_lt
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    {p : ℕ} [Fact p.Prime] {x : K} (hx : x ≠ 0)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-(padicValNat p (n + 1) : ℤ)))
    (hthreshold :
      1 / ((p : ℚ) - 1) <
        ((ofWithZeroValuation v).val (Units.mk0 x hx) : ℚ))
    {n : ℕ} (hn : n ≠ 0) :
    v (logSeriesTermField x hnK n) < v x

theorem valuation_signedLogSeriesTermField_lt_self_of_inv_sub_one_lt
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    {p : ℕ} [Fact p.Prime] {x : K} (hx : x ≠ 0)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-(padicValNat p (n + 1) : ℤ)))
    (hthreshold :
      1 / ((p : ℚ) - 1) <
        ((ofWithZeroValuation v).val (Units.mk0 x hx) : ℚ))
    {n : ℕ} (hn : n ≠ 0) :
    v (signedLogSeriesTermField x hnK n) < v x

theorem valuation_logHigherTailPartialSumField_lt_self_of_inv_sub_one_lt
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    {p : ℕ} [Fact p.Prime] {x : K} (hx : x ≠ 0)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-(padicValNat p (n + 1) : ℤ)))
    (hthreshold :
      1 / ((p : ℚ) - 1) <
        ((ofWithZeroValuation v).val (Units.mk0 x hx) : ℚ))
    (N : ℕ) :
    v (∑ n ∈ Finset.range N, signedLogSeriesTermField x hnK (n + 1)) <
      v x

theorem tendsto_logHigherTailPartialSumField_ofWithZeroValuation_of_lt_one
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    {p : ℕ} [Fact p.Prime] (x : K)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-(padicValNat p (n + 1) : ℤ)))
    (hvx : v x < (1 : WithZero (Multiplicative ℤ)))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
    Tendsto
      (fun N : ℕ =>
        ∑ n ∈ Finset.range N, signedLogSeriesTermField x hnK (n + 1))
      atTop
      (𝓝 (logOnePlusSeriesFieldOfWithZeroValuation v x hnK - x)) := by
  let : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  have hfull :
      Tendsto
        (fun N : ℕ => logOnePlusPartialSumField x hnK (N + 1))
        atTop (𝓝 (logOnePlusSeriesFieldOfWithZeroValuation v x hnK)) := by
    exact
      (tendsto_logOnePlusPartialSumField_ofWithZeroValuation_of_lt_one
        (v := v) (p := p) x hnK hnval hvx hcomplete).comp
          (tendsto_add_atTop_nat 1)
  have hsub :
      Tendsto
        (fun N : ℕ => logOnePlusPartialSumField x hnK (N + 1) - x)
        atTop
        (𝓝 (logOnePlusSeriesFieldOfWithZeroValuation v x hnK - x)) :=
    hfull.sub tendsto_const_nhds
  have htail :
      (fun N : ℕ => logOnePlusPartialSumField x hnK (N + 1) - x) =
      fun N : ℕ =>
        ∑ n ∈ Finset.range N, signedLogSeriesTermField x hnK (n + 1) := by
    funext N
    rw [logOnePlusPartialSumField, Finset.sum_range_succ']
    simp
  simpa [htail] using hsub

theorem valuation_logHigherTailField_lt_self_of_inv_sub_one_lt
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    {p : ℕ} [Fact p.Prime] {x : K} (hx : x ≠ 0)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-(padicValNat p (n + 1) : ℤ)))
    (hvx : v x < (1 : WithZero (Multiplicative ℤ)))
    (hthreshold :
      1 / ((p : ℚ) - 1) <
        ((ofWithZeroValuation v).val (Units.mk0 x hx) : ℚ))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    v (logOnePlusSeriesFieldOfWithZeroValuation v x hnK - x) <
      v x := by
  exact
    valuation_limit_lt_of_tendsto_of_eventually_lt
      (v := v) (γ := v x) ((_root_.Valuation.ne_zero_iff v).2 hx)
      (tendsto_logHigherTailPartialSumField_ofWithZeroValuation_of_lt_one
        (v := v) (p := p) x hnK hnval hvx hcomplete)
      (Eventually.of_forall fun N =>
        valuation_logHigherTailPartialSumField_lt_self_of_inv_sub_one_lt
          (v := v) (p := p) (x := x) hx hnK hnval hthreshold N)

theorem valuation_logOnePlusSeriesField_eq_self_of_inv_sub_one_lt
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    {p : ℕ} [Fact p.Prime] {x : K} (hx : x ≠ 0)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-(padicValNat p (n + 1) : ℤ)))
    (hvx : v x < (1 : WithZero (Multiplicative ℤ)))
    (hthreshold :
      1 / ((p : ℚ) - 1) <
        ((ofWithZeroValuation v).val (Units.mk0 x hx) : ℚ))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    v (logOnePlusSeriesFieldOfWithZeroValuation v x hnK) = v x := by
  have htail :
      v (logOnePlusSeriesFieldOfWithZeroValuation v x hnK - x) <
        v x :=
    valuation_logHigherTailField_lt_self_of_inv_sub_one_lt
      (v := v) (p := p) (x := x) hx hnK hnval hvx hthreshold hcomplete
  have hsplit :
      logOnePlusSeriesFieldOfWithZeroValuation v x hnK =
        x + (logOnePlusSeriesFieldOfWithZeroValuation v x hnK - x) := by
    abel
  rw [hsplit]
  exact v.map_add_eq_of_lt_left htail

theorem logOnePlusSeriesField_ne_zero_of_inv_sub_one_lt
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    {p : ℕ} [Fact p.Prime] {x : K} (hx : x ≠ 0)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-(padicValNat p (n + 1) : ℤ)))
    (hvx : v x < (1 : WithZero (Multiplicative ℤ)))
    (hthreshold :
      1 / ((p : ℚ) - 1) <
        ((ofWithZeroValuation v).val (Units.mk0 x hx) : ℚ))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    logOnePlusSeriesFieldOfWithZeroValuation v x hnK ≠ 0 := by
  intro hzero
  have hv :
      v (logOnePlusSeriesFieldOfWithZeroValuation v x hnK) = v x :=
    valuation_logOnePlusSeriesField_eq_self_of_inv_sub_one_lt
      (v := v) (p := p) (x := x) hx hnK hnval hvx hthreshold hcomplete
  rw [hzero, map_zero] at hv
  exact ((_root_.Valuation.ne_zero_iff v).2 hx) hv.symm

theorem logOnePlusSeriesField_eq_zero_iff_of_inv_sub_one_lt
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    {p : ℕ} [Fact p.Prime] {x : K}
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-(padicValNat p (n + 1) : ℤ)))
    (hvx : v x < (1 : WithZero (Multiplicative ℤ)))
    (hthreshold : ∀ hx : x ≠ 0,
      1 / ((p : ℚ) - 1) <
        ((ofWithZeroValuation v).val (Units.mk0 x hx) : ℚ))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    logOnePlusSeriesFieldOfWithZeroValuation v x hnK = 0 ↔ x = 0 := by
  constructor
  · intro hlog
    by_contra hx
    exact
      (logOnePlusSeriesField_ne_zero_of_inv_sub_one_lt
        (v := v) (p := p) (x := x) hx hnK hnval hvx (hthreshold hx)
        hcomplete) hlog
  · intro hx
    subst x
    simp

theorem valuation_logSeriesTermField_lt_self_of_scaled_inv_sub_one_lt
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    {p : ℕ} [Fact p.Prime] (e : ℕ) {x : K} (hx : x ≠ 0)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-((e : ℤ) * (padicValNat p (n + 1) : ℤ))))
    (hthreshold :
      (e : ℚ) / ((p : ℚ) - 1) <
        ((ofWithZeroValuation v).val (Units.mk0 x hx) : ℚ))
    {n : ℕ} (hn : n ≠ 0) :
    v (logSeriesTermField x hnK n) < v x

theorem valuation_signedLogSeriesTermField_lt_self_of_scaled_inv_sub_one_lt
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    {p : ℕ} [Fact p.Prime] (e : ℕ) {x : K} (hx : x ≠ 0)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-((e : ℤ) * (padicValNat p (n + 1) : ℤ))))
    (hthreshold :
      (e : ℚ) / ((p : ℚ) - 1) <
        ((ofWithZeroValuation v).val (Units.mk0 x hx) : ℚ))
    {n : ℕ} (hn : n ≠ 0) :
    v (signedLogSeriesTermField x hnK n) < v x

theorem valuation_logHigherTailPartialSumField_lt_self_of_scaled_inv_sub_one_lt
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    {p : ℕ} [Fact p.Prime] (e : ℕ) {x : K} (hx : x ≠ 0)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-((e : ℤ) * (padicValNat p (n + 1) : ℤ))))
    (hthreshold :
      (e : ℚ) / ((p : ℚ) - 1) <
        ((ofWithZeroValuation v).val (Units.mk0 x hx) : ℚ))
    (N : ℕ) :
    v (∑ n ∈ Finset.range N, signedLogSeriesTermField x hnK (n + 1)) <
      v x

theorem tendsto_logHigherTailPartialSumField_ofWithZeroValuation_scaled_of_lt_one
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    {p : ℕ} [Fact p.Prime] (e : ℕ) (x : K)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-((e : ℤ) * (padicValNat p (n + 1) : ℤ))))
    (hvx : v x < (1 : WithZero (Multiplicative ℤ)))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
    Tendsto
      (fun N : ℕ =>
        ∑ n ∈ Finset.range N, signedLogSeriesTermField x hnK (n + 1))
      atTop
      (𝓝 (logOnePlusSeriesFieldOfWithZeroValuation v x hnK - x)) := by
  let : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  have hfull :
      Tendsto
        (fun N : ℕ => logOnePlusPartialSumField x hnK (N + 1))
        atTop (𝓝 (logOnePlusSeriesFieldOfWithZeroValuation v x hnK)) := by
    exact
      (tendsto_logOnePlusPartialSumField_ofWithZeroValuation_scaled_of_lt_one
        (v := v) (p := p) e x hnK hnval hvx hcomplete).comp
          (tendsto_add_atTop_nat 1)
  have hsub :
      Tendsto
        (fun N : ℕ => logOnePlusPartialSumField x hnK (N + 1) - x)
        atTop
        (𝓝 (logOnePlusSeriesFieldOfWithZeroValuation v x hnK - x)) :=
    hfull.sub tendsto_const_nhds
  have htail :
      (fun N : ℕ => logOnePlusPartialSumField x hnK (N + 1) - x) =
      fun N : ℕ =>
        ∑ n ∈ Finset.range N, signedLogSeriesTermField x hnK (n + 1) := by
    funext N
    rw [logOnePlusPartialSumField, Finset.sum_range_succ']
    simp
  simpa [htail] using hsub

theorem valuation_logHigherTailField_lt_self_of_scaled_inv_sub_one_lt
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    {p : ℕ} [Fact p.Prime] (e : ℕ) {x : K} (hx : x ≠ 0)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-((e : ℤ) * (padicValNat p (n + 1) : ℤ))))
    (hvx : v x < (1 : WithZero (Multiplicative ℤ)))
    (hthreshold :
      (e : ℚ) / ((p : ℚ) - 1) <
        ((ofWithZeroValuation v).val (Units.mk0 x hx) : ℚ))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    v (logOnePlusSeriesFieldOfWithZeroValuation v x hnK - x) <
      v x := by
  exact
    valuation_limit_lt_of_tendsto_of_eventually_lt
      (v := v) (γ := v x) ((_root_.Valuation.ne_zero_iff v).2 hx)
      (tendsto_logHigherTailPartialSumField_ofWithZeroValuation_scaled_of_lt_one
        (v := v) (p := p) e x hnK hnval hvx hcomplete)
      (Eventually.of_forall fun N =>
        valuation_logHigherTailPartialSumField_lt_self_of_scaled_inv_sub_one_lt
          (v := v) (p := p) e (x := x) hx hnK hnval hthreshold N)

theorem valuation_logOnePlusSeriesField_eq_self_of_scaled_inv_sub_one_lt
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    {p : ℕ} [Fact p.Prime] (e : ℕ) {x : K} (hx : x ≠ 0)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-((e : ℤ) * (padicValNat p (n + 1) : ℤ))))
    (hvx : v x < (1 : WithZero (Multiplicative ℤ)))
    (hthreshold :
      (e : ℚ) / ((p : ℚ) - 1) <
        ((ofWithZeroValuation v).val (Units.mk0 x hx) : ℚ))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    v (logOnePlusSeriesFieldOfWithZeroValuation v x hnK) = v x := by
  have htail :
      v (logOnePlusSeriesFieldOfWithZeroValuation v x hnK - x) <
        v x :=
    valuation_logHigherTailField_lt_self_of_scaled_inv_sub_one_lt
      (v := v) (p := p) e (x := x) hx hnK hnval hvx hthreshold hcomplete
  have hsplit :
      logOnePlusSeriesFieldOfWithZeroValuation v x hnK =
        x + (logOnePlusSeriesFieldOfWithZeroValuation v x hnK - x) := by
    abel
  rw [hsplit]
  exact v.map_add_eq_of_lt_left htail

theorem logOnePlusSeriesField_ne_zero_of_scaled_inv_sub_one_lt
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    {p : ℕ} [Fact p.Prime] (e : ℕ) {x : K} (hx : x ≠ 0)
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-((e : ℤ) * (padicValNat p (n + 1) : ℤ))))
    (hvx : v x < (1 : WithZero (Multiplicative ℤ)))
    (hthreshold :
      (e : ℚ) / ((p : ℚ) - 1) <
        ((ofWithZeroValuation v).val (Units.mk0 x hx) : ℚ))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    logOnePlusSeriesFieldOfWithZeroValuation v x hnK ≠ 0 := by
  intro hzero
  have hv :
      v (logOnePlusSeriesFieldOfWithZeroValuation v x hnK) = v x :=
    valuation_logOnePlusSeriesField_eq_self_of_scaled_inv_sub_one_lt
      (v := v) (p := p) e (x := x) hx hnK hnval hvx hthreshold hcomplete
  rw [hzero, map_zero] at hv
  exact ((_root_.Valuation.ne_zero_iff v).2 hx) hv.symm

theorem logOnePlusSeriesField_eq_zero_iff_of_scaled_inv_sub_one_lt
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    {p : ℕ} [Fact p.Prime] (e : ℕ) {x : K}
    (hnK : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-((e : ℤ) * (padicValNat p (n + 1) : ℤ))))
    (hvx : v x < (1 : WithZero (Multiplicative ℤ)))
    (hthreshold : ∀ hx : x ≠ 0,
      (e : ℚ) / ((p : ℚ) - 1) <
        ((ofWithZeroValuation v).val (Units.mk0 x hx) : ℚ))
    (hcomplete :
      letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
      CompleteSpace K) :
    logOnePlusSeriesFieldOfWithZeroValuation v x hnK = 0 ↔ x = 0 := by
  constructor
  · intro hlog
    by_contra hx
    exact
      (logOnePlusSeriesField_ne_zero_of_scaled_inv_sub_one_lt
        (v := v) (p := p) e (x := x) hx hnK hnval hvx (hthreshold hx)
        hcomplete) hlog
  · intro hx
    subst x
    simp