Nonarchimedean property of padic

Stream: new members

[Sophia Rodriguez]

Hi there!

I want to show something like $||\sum_{i \in s}x_i||_p \leq max{||x_i||_p}$ where s is a Finset of Nat and $x_i \in \mathbb{Q}_p$. (that is, the Finset.sum version of padicNormE.nonarchimedean').

I found this IsNonarchimedean.finset_image_add_of_nonempty, but I can not fill in the parameters.

[Sophia Rodriguez]

To illustrate the issue better, here is my code

variable {p : ℕ} [Fact p.Prime]
variable (f : ℕ → ℚ_[p])

open Topology Filter

local notation "partial_sum" => fun s ↦ ∑ b : Finset.range s, f b

lemma padic_Nonarch : IsNonarchimedean (norm (E := ℚ_[p])) :=
  IsUltrametricDist.isNonarchimedean_norm

lemma tends_to (h : (Tendsto f atTop (𝓝 0))) : IsCauSeq norm partial_sum := by
  delta IsCauSeq
  intro ε hε
  simp only [ge_iff_le, Finset.univ_eq_attach]
  apply Metric.tendsto_atTop.1 at h
  obtain ⟨N, hN⟩ := h ε hε
  use N
  intro j hj
  have conv1 : ∑ b ∈ (Finset.range j).attach, f ↑b = ∑ b ∈ (Finset.range j), f b :=
    Finset.sum_attach (Finset.range j) f
  have conv2 : ∑ b ∈ (Finset.range N).attach, f ↑b = ∑ b ∈ (Finset.range N), f b :=
    Finset.sum_attach (Finset.range N) f
  rw [conv1, conv2]
  rw [Finset.sum_range_sub_sum_range hj]
  simp only [gt_iff_lt]
  have := IsNonarchimedean.finset_image_add_of_nonempty padic_Nonarch f (t := Finset.filter (fun k ↦ N ≤ k) (Finset.range j)) (by sorry)

[David Loeffler]

I think you may be looking for docs#IsUltrametricDist.exists_norm_finset_sum_le_of_nonempty (or one of the other variants in the same file).

[Sophia Rodriguez]

exactly! thanks