Valued_multipliable_one_add_of_tendsto_cofinite_zero.lean

theorem valuation_prod_one_add_sub_one_lt {Γ : Type*} [LinearOrderedCommGroupWithZero Γ] (w
  : Valuation K Γ)
    {ι : Type*} (f : ι → K) (u : Finset ι) {g : Γ} (hg : 0 < g)
    (h1 : ∀ i ∈ u, w (f i) < 1) (hgu : ∀ i ∈ u, w (f i) < g) :
    w (∏ i ∈ u, (1 + f i) - 1) < g

theorem valuation_prod_one_add_le {Γ : Type*} [LinearOrderedCommGroupWithZero Γ] (w :
  Valuation K Γ)
    {ι : Type*} (f : ι → K) (S₀ : Finset ι) (hS₀ : ∀ i, i ∉ S₀ → w (f i) < 1) (s :
      Finset ι) :
    w (∏ i ∈ s, (1 + f i)) ≤ ∏ i ∈ S₀, max 1 (w (1 + f i))

theorem multipliable_aux [CompleteSpace K] {ι : Type*} (f : ι → K)
    (hf : Tendsto f cofinite (𝓝 0)) : Multipliable (fun i => 1 + f i) := by
  classical
  set w : Valuation K hv.v.ValueGroup₀ := (hv.v).restrict with hw
  have hC : CauchySeq (fun s : Finset ι => ∏ i ∈ s, (1 + f i)) := by
    rw [(Valued.hasBasis_uniformity K Γ₀).cauchySeq_iff]
    intro γ _
    have h1mem : {x : K | w x < 1} ∈ 𝓝 (0 : K) :=
      (Valued.hasBasis_nhds_zero K Γ₀).mem_of_mem (i := 1) trivial
    have hS₀fin : (f ⁻¹' {x : K | w x < 1})ᶜ.Finite := by
      have := hf h1mem
      rwa [mem_map, mem_cofinite] at this
    set S₀ : Finset ι := hS₀fin.toFinset with hS₀
    have hS₀' : ∀ i, i ∉ S₀ → w (f i) < 1 := by
      intro i hi
      by_contra h
      exact hi (hS₀fin.mem_toFinset.mpr h)
    set M := ∏ i ∈ S₀, max 1 (w (1 + f i)) with hM
    have hM1 : 1 ≤ M := Finset.one_le_prod fun i _ => le_max_left _ _
    have hM0 : M ≠ 0 := ne_of_gt (lt_of_lt_of_le zero_lt_one hM1)
    set δ := γ * (Units.mk0 M hM0)⁻¹ with hδ
    have hδmem : {x : K | w x < δ.1} ∈ 𝓝 (0 : K) :=
      (Valued.hasBasis_nhds_zero K Γ₀).mem_of_mem (i := δ) trivial
    have hTfin : (f ⁻¹' {x : K | w x < δ.1})ᶜ.Finite := by
      have := hf hδmem
      rwa [mem_map, mem_cofinite] at this
    set N : Finset ι := S₀ ∪ hTfin.toFinset with hN
    have hoff : ∀ i, i ∉ N → w (f i) < 1 ∧ w (f i) < δ.1 := by
      intro i hi
      rw [hN, Finset.mem_union, not_or] at hi
      refine ⟨hS₀' i hi.1, ?_⟩
      by_contra h
      exact hi.2 (hTfin.mem_toFinset.mpr h)
    have hdist : ∀ m : Finset ι, N ≤ m → w (∏ i ∈ m, (1 + f i) - ∏ i ∈ N, (1 + f i)) < γ.1 := by
      intro m hm
      have e : ∏ i ∈ m, (1 + f i) - ∏ i ∈ N, (1 + f i) =
          (∏ i ∈ N, (1 + f i)) * (∏ i ∈ m \ N, (1 + f i) - 1) := by
        rw [mul_sub, mul_one, mul_comm, Finset.prod_sdiff hm]
      rw [e, Valuation.map_mul]
      have hA : w (∏ i ∈ N, (1 + f i)) ≤ M := valuation_prod_one_add_le w f S₀ hS₀' N
      have hB : w (∏ i ∈ m \ N, (1 + f i) - 1) < δ.1 :=
        valuation_prod_one_add_sub_one_lt w f (m \ N) δ.zero_lt
          (fun i hi => (hoff i (Finset.mem_sdiff.mp hi).2).1) (fun i hi => (hoff i
            (Finset.mem_sdiff.mp hi).2).2)
      calc w (∏ i ∈ N, (1 + f i)) * w (∏ i ∈ m \ N, (1 + f i) - 1)
          ≤ M * w (∏ i ∈ m \ N, (1 + f i) - 1) := by gcongr
        _ < M * δ.1 := mul_lt_mul_of_pos_left hB (lt_of_lt_of_le zero_lt_one hM1)
        _ = γ.1 := by
          rw [hδ, Units.val_mul, Units.val_inv_eq_inv_val, Units.val_mk0, mul_comm (γ.1),
            mul_inv_cancel_left₀ hM0]
    refine ⟨N, fun m hm n hn => ?_⟩
    change w ((∏ i ∈ n, (1 + f i)) - ∏ i ∈ m, (1 + f i)) < γ.1
    have e : (∏ i ∈ n, (1 + f i)) - ∏ i ∈ m, (1 + f i) =
        ((∏ i ∈ n, (1 + f i)) - ∏ i ∈ N, (1 + f i)) - ((∏ i ∈ m, (1 + f i)) - ∏ i ∈ N, (1 + f i))
          := by ring
    rw [e]
    exact w.map_sub_lt (hdist n hn) (hdist m hm)
  obtain ⟨a, ha⟩ := cauchySeq_tendsto_of_complete hC
  exact ⟨a, ha⟩

theorem _root_.Valued.multipliable_one_add_of_tendsto_cofinite_zero
    {K : Type*} [Field K] {Γ₀ : Type*} [LinearOrderedCommGroupWithZero Γ₀] [Valued K Γ₀]
      [CompleteSpace K]
    {ι : Type*} (f : ι → K) (hf : Tendsto f cofinite (𝓝 0)) :
    Multipliable (fun i => 1 + f i) :=
  ValuedProdAux.multipliable_aux f hf