LogExpComposition.lean

theorem hasSum_powerSeries_pow_coeff_mul_pow
    [UniformSpace K] [IsUniformAddGroup K] [T3Space K]
    [NonarchimedeanRing K]
    (g : PowerSeries K) (x y : K)
    (hgy : HasSum (fun d : ℕ => PowerSeries.coeff d g * x ^ d) y)
    (q : ℕ) :
    HasSum (fun d : ℕ => PowerSeries.coeff d (g ^ q) * x ^ d) (y ^ q) := by
  induction q with
  | zero =>
      have hsingle :
          HasSum (fun d : ℕ => if d = 0 then (1 : K) else 0) 1 := by
        apply hasSum_single 0
        intro d hd
        simp [hd]
      have hsingle' :
          HasSum (fun d : ℕ => PowerSeries.coeff d (1 : PowerSeries K) * x ^ d) 1 :=
        hsingle.congr_fun fun d => by
          by_cases hd : d = 0
          · subst d
            simp
          · simp [PowerSeries.coeff_one, hd]
      simpa only [pow_zero] using hsingle'
  | succ q ih =>
      have hprod := ih.mul_of_nonarchimedean hgy
      have hsigma :
          HasSum
            (fun nd : Sigma fun d : ℕ => ↑(Finset.antidiagonal d) =>
              (PowerSeries.coeff nd.2.1.1 (g ^ q) * x ^ nd.2.1.1) *
                (PowerSeries.coeff nd.2.1.2 g * x ^ nd.2.1.2))
            (y ^ q * y) := by
        simpa [Function.comp_def] using
          (Finset.HasAntidiagonal.sigmaAntidiagonalEquivProd.hasSum_iff).2 hprod
      have hsumCauchy :
          HasSum
            (fun d : ℕ =>
              ∑ ij : ↑(Finset.antidiagonal d),
                (PowerSeries.coeff ij.1.1 (g ^ q) * x ^ ij.1.1) *
                  (PowerSeries.coeff ij.1.2 g * x ^ ij.1.2))
            (y ^ q * y) :=
        hsigma.sigma fun d => hasSum_fintype _
      rw [show g ^ (q + 1) = g ^ q * g by rw [pow_succ],
        show y ^ (q + 1) = y ^ q * y by rw [pow_succ]]
      refine hsumCauchy.congr_fun ?_
      intro d
      rw [PowerSeries.coeff_mul, Finset.sum_mul]
      rw [← Finset.sum_attach, Finset.attach_eq_univ]
      apply Finset.sum_congr rfl
      intro ij _
      have hijsum : ij.1.1 + ij.1.2 = d :=
        Finset.mem_antidiagonal.mp ij.2
      have hpow : x ^ d = x ^ ij.1.1 * x ^ ij.1.2 := by
        calc
          x ^ d = x ^ (ij.1.1 + ij.1.2) :=
            congrArg (fun n : ℕ => x ^ n) hijsum.symm
          _ = x ^ ij.1.1 * x ^ ij.1.2 := pow_add _ _ _
      rw [hpow]
      ring

theorem valuation_powerSeries_pow_coeff_mul_pow_le
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    (g : PowerSeries K) (x : K) (r : WithZero (Multiplicative ℤ))
    (hcoeff : ∀ d : ℕ, v (PowerSeries.coeff d g * x ^ d) ≤ r)
    (q d : ℕ) :
    v (PowerSeries.coeff d (g ^ q) * x ^ d) ≤ r ^ q

theorem valuation_powerSeries_subst_sigmaTerm_le_outerTerm
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    (f g : PowerSeries K) (x : K)
    (hcoeff : ∀ d : ℕ,
      v (PowerSeries.coeff d g * x ^ d) ≤ v x)
    (q d : ℕ) :
    v (PowerSeries.coeff q f * PowerSeries.coeff d (g ^ q) * x ^ d) ≤
      v (PowerSeries.coeff q f * x ^ q)

theorem summable_powerSeries_subst_sigma_of_outer_summable
    [Valued K (WithZero (Multiplicative ℤ))] [CompleteSpace K]
    [NonarchimedeanRing K]
    (f g : PowerSeries K) (x y : K)
    (hgy : HasSum (fun d : ℕ => PowerSeries.coeff d g * x ^ d) y)
    (houter : Summable (fun q : ℕ => PowerSeries.coeff q f * x ^ q))
    (hcoeff : ∀ d : ℕ,
      Valued.v (PowerSeries.coeff d g * x ^ d) ≤ Valued.v x) :
    Summable
      (fun qd : Sigma fun _ : ℕ => ℕ =>
        PowerSeries.coeff qd.1 f *
          PowerSeries.coeff qd.2 (g ^ qd.1) * x ^ qd.2) := by
  let term : (Sigma fun _ : ℕ => ℕ) → K := fun qd =>
    PowerSeries.coeff qd.1 f *
      PowerSeries.coeff qd.2 (g ^ qd.1) * x ^ qd.2
  let outerTerm : ℕ → K := fun q => PowerSeries.coeff q f * x ^ q
  change Summable term
  rw [NonarchimedeanAddGroup.summable_iff_tendsto_cofinite_zero]
  rw [tendsto_def]
  intro s hs
  have hrepr := Valued.mem_nhds_zero.mp hs
  let γ := Classical.choose hrepr
  have hγ := Classical.choose_spec hrepr
  have hball :
      {z : K |
        Valued.v z < MonoidWithZeroHom.ValueGroup₀.embedding γ.1} ∈ nhds (0 : K) := by
    apply Valued.mem_nhds_zero.mpr
    exact ⟨γ, by
      intro z hz
      change Valued.v.restrict z < γ.1 at hz
      rw [Valuation.restrict_lt_iff_lt_embedding] at hz
      exact hz⟩
  have houterZero : Tendsto outerTerm cofinite (nhds (0 : K)) := by
    simpa [outerTerm] using houter.tendsto_cofinite_zero
  have houterEventually :
      ∀ᶠ q : ℕ in cofinite,
        Valued.v (outerTerm q) <
          MonoidWithZeroHom.ValueGroup₀.embedding γ.1 :=
    houterZero.eventually hball
  let goodOuter : Set ℕ :=
    {q | Valued.v (outerTerm q) <
      MonoidWithZeroHom.ValueGroup₀.embedding γ.1}
  have hgoodOuter : goodOuter ∈ cofinite := by
    change {q : ℕ |
      Valued.v (outerTerm q) <
        MonoidWithZeroHom.ValueGroup₀.embedding γ.1} ∈ cofinite
    exact houterEventually
  have hbadOuterFinite : goodOuterᶜ.Finite :=
    Filter.mem_cofinite.mp hgoodOuter
  let Q : Finset ℕ := hbadOuterFinite.toFinset
  have hpower : ∀ q : ℕ,
      HasSum
        (fun d : ℕ => PowerSeries.coeff d (g ^ q) * x ^ d)
        (y ^ q) :=
    fun q => hasSum_powerSeries_pow_coeff_mul_pow g x y hgy q
  have hfiber : ∀ q : ℕ,
      HasSum (fun d : ℕ => term ⟨q, d⟩)
        (PowerSeries.coeff q f * y ^ q) := by
    intro q
    simpa [term, mul_assoc] using
      (hpower q).mul_left (PowerSeries.coeff q f)
  let badFiber : ℕ → Set ℕ := fun q => {d | term ⟨q, d⟩ ∉ s}
  have hbadFiberFinite : ∀ q : ℕ, (badFiber q).Finite := by
    intro q
    have hevent := (hfiber q).summable.tendsto_cofinite_zero.eventually hs
    apply (Filter.mem_cofinite.mp hevent).subset
    intro d hd
    exact hd
  let D : ℕ → Finset ℕ := fun q => (hbadFiberFinite q).toFinset
  let E : Finset (Sigma fun _ : ℕ => ℕ) := Q.sigma D
  apply Filter.mem_cofinite.mpr
  apply E.finite_toSet.subset
  intro qd hbad
  by_contra hnotE
  have hgood : term qd ∈ s := by
    by_cases hq : qd.1 ∈ Q
    · have hdnot : qd.2 ∉ D qd.1 := by
        intro hd
        apply hnotE
        exact Finset.mem_sigma.mpr ⟨hq, hd⟩
      by_contra hterm
      apply hdnot
      simp [D, badFiber, hterm]
    · have houterGood :
          Valued.v (outerTerm qd.1) <
            MonoidWithZeroHom.ValueGroup₀.embedding γ.1 := by
        have hgoodMem : qd.1 ∈ goodOuter := by
          by_contra hnotGood
          apply hq
          simpa [Q] using hnotGood
        exact hgoodMem
      apply hγ
      change Valued.v.restrict (term qd) < γ.1
      rw [Valuation.restrict_lt_iff_lt_embedding]
      have hbound :=
        valuation_powerSeries_subst_sigmaTerm_le_outerTerm
          Valued.v f g x hcoeff qd.1 qd.2
      exact lt_of_le_of_lt (by simpa [term, outerTerm] using hbound) houterGood
  exact hbad hgood

theorem hasSum_powerSeries_subst_sigma
    [Valued K (WithZero (Multiplicative ℤ))] [CompleteSpace K]
    [NonarchimedeanRing K]
    (f g : PowerSeries K) (x y z : K)
    (hgy : HasSum (fun d : ℕ => PowerSeries.coeff d g * x ^ d) y)
    (houterX : Summable
      (fun q : ℕ => PowerSeries.coeff q f * x ^ q))
    (houterY : HasSum
      (fun q : ℕ => PowerSeries.coeff q f * y ^ q) z)
    (hcoeff : ∀ d : ℕ,
      Valued.v (PowerSeries.coeff d g * x ^ d) ≤ Valued.v x) :
    HasSum
      (fun qd : Sigma fun _ : ℕ => ℕ =>
        PowerSeries.coeff qd.1 f *
          PowerSeries.coeff qd.2 (g ^ qd.1) * x ^ qd.2)
      z := by
  have hsigma :=
    summable_powerSeries_subst_sigma_of_outer_summable
      f g x y hgy houterX hcoeff
  have hinner : ∀ q : ℕ,
      HasSum
        (fun d : ℕ =>
          PowerSeries.coeff q f * PowerSeries.coeff d (g ^ q) * x ^ d)
        (PowerSeries.coeff q f * y ^ q) := by
    intro q
    simpa [mul_assoc] using
      (hasSum_powerSeries_pow_coeff_mul_pow g x y hgy q).mul_left
        (PowerSeries.coeff q f)
  exact HasSum.sigma_of_hasSum houterY hinner hsigma

theorem hasSum_powerSeries_subst_coeff_mul_pow_of_sigma
    [Valued K (WithZero (Multiplicative ℤ))]
    (f g : PowerSeries K) (x z : K)
    (hg0 : PowerSeries.constantCoeff g = 0)
    (hsigma :
      HasSum
        (fun qd : Sigma fun _ : ℕ => ℕ =>
          PowerSeries.coeff qd.1 f *
            PowerSeries.coeff qd.2 (g ^ qd.1) * x ^ qd.2)
        z) :
    HasSum
      (fun d : ℕ =>
        PowerSeries.coeff d (PowerSeries.subst g f) * x ^ d)
      z := by
  have hg : PowerSeries.HasSubst g :=
    PowerSeries.HasSubst.of_constantCoeff_zero' hg0
  let sigmaTerm : (Sigma fun _ : ℕ => ℕ) → K := fun qd =>
    PowerSeries.coeff qd.1 f *
      PowerSeries.coeff qd.2 (g ^ qd.1) * x ^ qd.2
  have hsigma' : HasSum sigmaTerm z := by
    simpa [sigmaTerm] using hsigma
  let swap :
      (Sigma fun _ : ℕ => ℕ) ≃ (Sigma fun _ : ℕ => ℕ) :=
    { toFun := fun dq => ⟨dq.2, dq.1⟩
      invFun := fun qd => ⟨qd.2, qd.1⟩
      left_inv := by intro dq; cases dq; rfl
      right_inv := by intro qd; cases qd; rfl }
  have hswapped : HasSum (sigmaTerm ∘ swap) z :=
    (swap.hasSum_iff).2 hsigma'
  have hfiber : ∀ d : ℕ,
      HasSum
        (fun q : ℕ => (sigmaTerm ∘ swap) ⟨d, q⟩)
        (PowerSeries.coeff d (PowerSeries.subst g f) * x ^ d) := by
    intro d
    let base : ℕ → K := fun q =>
      PowerSeries.coeff q f • PowerSeries.coeff d (g ^ q)
    let fiberTerm : ℕ → K := fun q => base q * x ^ d
    have hsupport : base.support.Finite := by
      rw [← Function.HasFiniteSupport]
      simpa only [base] using PowerSeries.coeff_subst_finite' hg f d
    let S : Finset ℕ := hsupport.toFinset
    have hfinite :
        HasSum fiberTerm (∑ q ∈ S, fiberTerm q) := by
      apply hasSum_sum_of_ne_finset_zero
      intro q hq
      have hbase : base q = 0 := by
        by_contra hne
        apply hq
        simp [S, hne]
      simp [fiberTerm, hbase]
    have hsum :
        (∑ q ∈ S, fiberTerm q) =
          PowerSeries.coeff d (PowerSeries.subst g f) * x ^ d := by
      rw [PowerSeries.coeff_subst' hg f d]
      rw [finsum_eq_sum _ hsupport]
      rw [Finset.sum_mul]
    rw [hsum] at hfinite
    simpa [fiberTerm, base, sigmaTerm, swap, Function.comp_def,
      smul_eq_mul, mul_assoc] using hfinite
  exact hswapped.sigma hfiber

theorem hasSum_powerSeries_subst_coeff_mul_pow
    [Valued K (WithZero (Multiplicative ℤ))] [CompleteSpace K]
    [NonarchimedeanRing K]
    (f g : PowerSeries K) (x y z : K)
    (hg0 : PowerSeries.constantCoeff g = 0)
    (hgy : HasSum (fun d : ℕ => PowerSeries.coeff d g * x ^ d) y)
    (houterX : Summable
      (fun q : ℕ => PowerSeries.coeff q f * x ^ q))
    (houterY : HasSum
      (fun q : ℕ => PowerSeries.coeff q f * y ^ q) z)
    (hcoeff : ∀ d : ℕ,
      Valued.v (PowerSeries.coeff d g * x ^ d) ≤ Valued.v x) :
    HasSum
      (fun d : ℕ =>
        PowerSeries.coeff d (PowerSeries.subst g f) * x ^ d)
      z := by
  apply hasSum_powerSeries_subst_coeff_mul_pow_of_sigma f g x z hg0
  exact hasSum_powerSeries_subst_sigma
    f g x y z hgy houterX houterY hcoeff

theorem hasSum_formalExpPowerSeries_eval_expSeriesField_ofWithZeroValuation_scaled
    [Algebra ℚ K]
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    {p : ℕ} [Fact p.Prime] (e : ℕ) (x : K)
    (hnK : ∀ n : ℕ, (((n.factorial : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n.factorial : ℕ) : K)) =
        WithZero.exp (-((e : ℤ) * (padicValNat p n.factorial : ℤ))))
    (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) :
    letI : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
    HasSum
      (fun n : ℕ =>
        PowerSeries.coeff n (PowerSeries.exp K) * x ^ n)
      (expSeriesFieldOfWithZeroValuation v x hnK) := by
  let : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  have hsum :=
    hasSum_expSeriesTermField_expSeriesField_ofWithZeroValuation_scaled_of_threshold
      (v := v) (p := p) e x hnK hnval hthreshold hcomplete
  exact hsum.congr_fun fun n =>
    formalExpPowerSeries_coeff_mul_pow_eq_expSeriesTermField
      (K := K) x hnK n

theorem hasSum_powerSeries_sub_one_coeff_mul_pow
    [Valued K (WithZero (Multiplicative ℤ))]
    (f : PowerSeries K) (x z : K)
    (hf : HasSum (fun d : ℕ => PowerSeries.coeff d f * x ^ d) z) :
    HasSum
      (fun d : ℕ => PowerSeries.coeff d (f - 1) * x ^ d)
      (z - 1) := by
  have hsingle :
      HasSum (fun d : ℕ => if d = 0 then (1 : K) else 0) 1 := by
    apply hasSum_single 0
    intro d hd
    simp [hd]
  have hone :
      HasSum
        (fun d : ℕ => PowerSeries.coeff d (1 : PowerSeries K) * x ^ d)
        1 :=
    hsingle.congr_fun fun d => by
      by_cases hd : d = 0
      · subst d
        simp
      · simp [PowerSeries.coeff_one, hd]
  refine (hf.sub hone).congr_fun ?_
  intro d
  rw [map_sub]
  ring

theorem valuation_lt_one_ofWithZeroValuation_scaled_threshold_real
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    {p : ℕ} [Fact p.Prime] (e : ℕ) {x : K}
    (hthreshold : ∀ hx : x ≠ 0,
      (e : ℝ) / ((p : ℝ) - 1) <
        ((ofWithZeroValuation v).val (Units.mk0 x hx) : ℝ)) :
    v x < (1 : WithZero (Multiplicative ℤ))

theorem valuation_powerSeries_log_coeff_mul_pow_le_self_scaled
    [Algebra ℚ K]
    (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) : ℤ))))
    (hthreshold : ∀ hx : x ≠ 0,
      (e : ℝ) / ((p : ℝ) - 1) <
        ((ofWithZeroValuation v).val (Units.mk0 x hx) : ℝ))
    (d : ℕ) :
    v (PowerSeries.coeff d (PowerSeries.log K) * x ^ d) ≤
      v x

theorem valuation_formalExp_sub_one_coeff_mul_pow_le_self_scaled
    [Algebra ℚ K]
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    {p : ℕ} [Fact p.Prime] (e : ℕ) {x : K}
    (hnK : ∀ n : ℕ, (((n.factorial : ℕ) : K) ≠ 0))
    (hnval : ∀ n : ℕ,
      v (((n.factorial : ℕ) : K)) =
        WithZero.exp (-((e : ℤ) * (padicValNat p n.factorial : ℤ))))
    (hthreshold : ∀ hx : x ≠ 0,
      (e : ℝ) / ((p : ℝ) - 1) <
        ((ofWithZeroValuation v).val (Units.mk0 x hx) : ℝ))
    (d : ℕ) :
    v (PowerSeries.coeff d ((PowerSeries.exp K) - 1) * x ^ d) ≤ v x

theorem hasSum_powerSeries_X_coeff_mul_pow
    [Valued K (WithZero (Multiplicative ℤ))] (x : K) :
    HasSum
      (fun d : ℕ => PowerSeries.coeff d (PowerSeries.X : PowerSeries K) * x ^ d)
      x := by
  have hsingle :
      HasSum (fun d : ℕ => if d = 1 then x else 0) x := by
    apply hasSum_single 1
    intro d hd
    simp [hd]
  exact hsingle.congr_fun fun d => by
    by_cases hd : d = 1
    · subst d
      simp [PowerSeries.coeff_X]
    · simp [PowerSeries.coeff_X, hd]

theorem hasSum_powerSeries_one_add_X_coeff_mul_pow
    [Valued K (WithZero (Multiplicative ℤ))] (x : K) :
    HasSum
      (fun d : ℕ =>
        PowerSeries.coeff d (1 + PowerSeries.X : PowerSeries K) * x ^ d)
      (1 + x) := by
  have hsingle :
      HasSum (fun d : ℕ => if d = 0 then (1 : K) else 0) 1 := by
    apply hasSum_single 0
    intro d hd
    simp [hd]
  have hone :
      HasSum
        (fun d : ℕ => PowerSeries.coeff d (1 : PowerSeries K) * x ^ d)
        1 :=
    hsingle.congr_fun fun d => by
      by_cases hd : d = 0
      · subst d
        simp
      · simp [PowerSeries.coeff_one, hd]
  have hx := hasSum_powerSeries_X_coeff_mul_pow (K := K) x
  refine (hone.add hx).congr_fun ?_
  intro d
  rw [map_add]
  ring

theorem expSeries_logOnePlusSeries_eq_one_add_ofWithZeroValuation_scaled_of_threshold
    [Algebra ℚ K]
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    {p : ℕ} [Fact p.Prime] (e : ℕ) (x : K)
    (hnKlog : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnvalLog : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-((e : ℤ) * (padicValNat p (n + 1) : ℤ))))
    (hnKexp : ∀ n : ℕ, (((n.factorial : ℕ) : K) ≠ 0))
    (hnvalExp : ∀ n : ℕ,
      v (((n.factorial : ℕ) : K)) =
        WithZero.exp (-((e : ℤ) * (padicValNat p n.factorial : ℤ))))
    (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) :
    expSeriesFieldOfWithZeroValuation v
        (logOnePlusSeriesFieldOfWithZeroValuation v x hnKlog) hnKexp =
      1 + x := by
  let : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  let : CompleteSpace K := hcomplete
  have : NonarchimedeanRing K := nonarchimedeanRing_ofWithZeroValuation v
  let : IsAddTorsionFree K := IsAddTorsionFree.of_module_rat K
  by_cases hx : x = 0
  · subst x
    simp
  · let y : K := logOnePlusSeriesFieldOfWithZeroValuation v x hnKlog
    have hvx_lt_one : v x < (1 : WithZero (Multiplicative ℤ)) :=
      valuation_lt_one_ofWithZeroValuation_scaled_threshold_real
        (v := v) (p := p) e hthreshold
    have hthresholdRat :
        (e : ℚ) / ((p : ℚ) - 1) <
          ((ofWithZeroValuation v).val (Units.mk0 x hx) : ℚ) := by
      exact_mod_cast hthreshold hx
    have hvy_eq : v y = v x := by
      simpa [y] using
        valuation_logOnePlusSeriesField_eq_self_of_scaled_inv_sub_one_lt
          (v := v) (p := p) e (x := x) hx hnKlog hnvalLog hvx_lt_one
          hthresholdRat hcomplete
    have hy : y ≠ 0 := by
      intro hy0
      have hzero : v y = 0 := by simp [hy0]
      have hxzero : v x = 0 := by simpa [hvy_eq] using hzero
      exact ((_root_.Valuation.ne_zero_iff v).2 hx) hxzero
    have hyval_eq :
        (ofWithZeroValuation v).val (Units.mk0 y hy) =
          (ofWithZeroValuation v).val (Units.mk0 x hx) :=
      ofWithZeroValuation_val_eq_of_valuation_eq v hvy_eq
    have hythreshold : ∀ hy' : y ≠ 0,
        (e : ℝ) / ((p : ℝ) - 1) <
          ((ofWithZeroValuation v).val (Units.mk0 y hy') : ℝ) := by
      intro hy'
      have hyproof : Units.mk0 y hy' = Units.mk0 y hy := by
        ext
        rfl
      rw [hyproof, hyval_eq]
      exact hthreshold hx
    have hinner :
        HasSum
          (fun d : ℕ =>
            PowerSeries.coeff d (PowerSeries.log K) * x ^ d)
          y := by
      simpa [y] using
        hasSum_powerSeries_log_eval_nat_logOnePlusSeriesField_ofWithZeroValuation_scaled
          (v := v) (p := p) e x hnKlog hnvalLog hvx_lt_one hcomplete
    have houterX :
        HasSum
          (fun q : ℕ => PowerSeries.coeff q (PowerSeries.exp K) * x ^ q)
          (expSeriesFieldOfWithZeroValuation v x hnKexp) :=
      hasSum_formalExpPowerSeries_eval_expSeriesField_ofWithZeroValuation_scaled
        (v := v) (p := p) e x hnKexp hnvalExp hthreshold hcomplete
    have houterY :
        HasSum
          (fun q : ℕ => PowerSeries.coeff q (PowerSeries.exp K) * y ^ q)
          (expSeriesFieldOfWithZeroValuation v y hnKexp) :=
      hasSum_formalExpPowerSeries_eval_expSeriesField_ofWithZeroValuation_scaled
        (v := v) (p := p) e y hnKexp hnvalExp hythreshold hcomplete
    have hcoeff : ∀ d : ℕ,
        v (PowerSeries.coeff d (PowerSeries.log K) * x ^ d) ≤ v x :=
      valuation_powerSeries_log_coeff_mul_pow_le_self_scaled
        (v := v) (p := p) e hnKlog hnvalLog hthreshold
    have hcomp :
        HasSum
          (fun d : ℕ =>
            PowerSeries.coeff d
                (PowerSeries.subst (PowerSeries.log K)
                  (PowerSeries.exp K)) * x ^ d)
          (expSeriesFieldOfWithZeroValuation v y hnKexp) :=
      hasSum_powerSeries_subst_coeff_mul_pow
        (PowerSeries.exp K) (PowerSeries.log K) x y
          (expSeriesFieldOfWithZeroValuation v y hnKexp)
          PowerSeries.constantCoeff_log hinner
          houterX.summable houterY hcoeff
    rw [PowerSeries.exp_subst_log_eq_one_add_X K] at hcomp
    exact hcomp.unique (hasSum_powerSeries_one_add_X_coeff_mul_pow (K := K) x)

theorem logOnePlusSeries_expSeries_sub_one_eq_self_ofWithZeroValuation_scaled_of_threshold
    [Algebra ℚ K]
    (v : _root_.Valuation K (WithZero (Multiplicative ℤ)))
    {p : ℕ} [Fact p.Prime] (e : ℕ) (x : K)
    (hnKexp : ∀ n : ℕ, (((n.factorial : ℕ) : K) ≠ 0))
    (hnvalExp : ∀ n : ℕ,
      v (((n.factorial : ℕ) : K)) =
        WithZero.exp (-((e : ℤ) * (padicValNat p n.factorial : ℤ))))
    (hnKlog : ∀ n : ℕ, (((n + 1 : ℕ) : K) ≠ 0))
    (hnvalLog : ∀ n : ℕ,
      v (((n + 1 : ℕ) : K)) =
        WithZero.exp (-((e : ℤ) * (padicValNat p (n + 1) : ℤ))))
    (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
        (expSeriesFieldOfWithZeroValuation v x hnKexp - 1) hnKlog =
      x := by
  let : Valued K (WithZero (Multiplicative ℤ)) := Valued.mk' v
  let : CompleteSpace K := hcomplete
  have : NonarchimedeanRing K := nonarchimedeanRing_ofWithZeroValuation v
  let : IsAddTorsionFree K := IsAddTorsionFree.of_module_rat K
  by_cases hx : x = 0
  · subst x
    simp
  · let y : K := expSeriesFieldOfWithZeroValuation v x hnKexp - 1
    have hvx_lt_one : v x < (1 : WithZero (Multiplicative ℤ)) :=
      valuation_lt_one_ofWithZeroValuation_scaled_threshold_real
        (v := v) (p := p) e hthreshold
    have hthresholdRat :
        (e : ℚ) / ((p : ℚ) - 1) <
          ((ofWithZeroValuation v).val (Units.mk0 x hx) : ℚ) := by
      exact_mod_cast hthreshold hx
    have hvy_eq : v y = v x := by
      simpa [y] using
        valuation_expSeriesField_sub_one_eq_self_ofWithZeroValuation_scaled_of_threshold
          (v := v) (p := p) e (x := x) hx hnKexp hnvalExp
          hthresholdRat hcomplete
    have hvy_lt_one : v y < (1 : WithZero (Multiplicative ℤ)) := by
      simpa [hvy_eq] using hvx_lt_one
    have hexp :
        HasSum
          (fun d : ℕ => PowerSeries.coeff d (PowerSeries.exp K) * x ^ d)
          (expSeriesFieldOfWithZeroValuation v x hnKexp) :=
      hasSum_formalExpPowerSeries_eval_expSeriesField_ofWithZeroValuation_scaled
        (v := v) (p := p) e x hnKexp hnvalExp hthreshold hcomplete
    have hinner :
        HasSum
          (fun d : ℕ =>
            PowerSeries.coeff d ((PowerSeries.exp K) - 1) * x ^ d)
          y := by
      simpa [y] using
        hasSum_powerSeries_sub_one_coeff_mul_pow
          (PowerSeries.exp K) x
            (expSeriesFieldOfWithZeroValuation v x hnKexp) hexp
    have houterX :
        HasSum
          (fun q : ℕ =>
            PowerSeries.coeff q (PowerSeries.log K) * x ^ q)
          (logOnePlusSeriesFieldOfWithZeroValuation v x hnKlog) :=
      hasSum_powerSeries_log_eval_nat_logOnePlusSeriesField_ofWithZeroValuation_scaled
        (v := v) (p := p) e x hnKlog hnvalLog hvx_lt_one hcomplete
    have houterY :
        HasSum
          (fun q : ℕ =>
            PowerSeries.coeff q (PowerSeries.log K) * y ^ q)
          (logOnePlusSeriesFieldOfWithZeroValuation v y hnKlog) :=
      hasSum_powerSeries_log_eval_nat_logOnePlusSeriesField_ofWithZeroValuation_scaled
        (v := v) (p := p) e y hnKlog hnvalLog hvy_lt_one hcomplete
    have hcoeff : ∀ d : ℕ,
        v (PowerSeries.coeff d ((PowerSeries.exp K) - 1) * x ^ d) ≤ v x :=
      valuation_formalExp_sub_one_coeff_mul_pow_le_self_scaled
        (v := v) (p := p) e hnKexp hnvalExp hthreshold
    have hg0 :
        PowerSeries.constantCoeff ((PowerSeries.exp K) - 1) = 0 := by
      simp
    have hcomp :
        HasSum
          (fun d : ℕ =>
            PowerSeries.coeff d
                (PowerSeries.subst ((PowerSeries.exp K) - 1)
                  (PowerSeries.log K)) * x ^ d)
          (logOnePlusSeriesFieldOfWithZeroValuation v y hnKlog) :=
      hasSum_powerSeries_subst_coeff_mul_pow
        (PowerSeries.log K) ((PowerSeries.exp K) - 1) x y
          (logOnePlusSeriesFieldOfWithZeroValuation v y hnKlog)
          hg0 hinner houterX.summable houterY hcoeff
    rw [PowerSeries.log_subst_exp_sub_one_eq_X K] at hcomp
    exact hcomp.unique (hasSum_powerSeries_X_coeff_mul_pow (K := K) x)