AbsoluteValues.lean

def absoluteValueDist {K : Type*} [Field K] (v : AbsoluteValue K ℝ) (x y : K) : ℝ

theorem absoluteValueDist_nonneg
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ) (x y : K) :
    0 ≤ absoluteValueDist v x y

theorem absoluteValueDist_eq_zero_iff
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ) (x y : K) :
    absoluteValueDist v x y = 0 ↔ x = y

theorem absoluteValueDist_self
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ) (x : K) :
    absoluteValueDist v x x = 0

theorem absoluteValueDist_comm
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ) (x y : K) :
    absoluteValueDist v x y = absoluteValueDist v y x

theorem absoluteValueDist_triangle
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ) (x y z : K) :
    absoluteValueDist v x z ≤
      absoluteValueDist v x y + absoluteValueDist v y z

theorem absoluteValueUniformity_basis
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ) :
    (@uniformity K v.uniformSpace).HasBasis ((0 : ℝ) < ·)
      (fun ε => {p : K × K | absoluteValueDist v p.2 p.1 < ε}) := by
  simpa [absoluteValueDist] using
    (AbsoluteValue.hasBasis_uniformity (abv := v))

def TrivialAbsoluteValue {K : Type*} [Field K] (v : AbsoluteValue K ℝ) : Prop

theorem not_trivialAbsoluteValue_iff_exists_ne_one
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ) :
    ¬ TrivialAbsoluteValue v ↔ ∃ x : K, x ≠ 0 ∧ v x ≠ 1

theorem not_trivialAbsoluteValue_iff_isNontrivial
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ) :
    ¬ TrivialAbsoluteValue v ↔ v.IsNontrivial

theorem absoluteValue_axioms
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ) :
    (∀ x : K, 0 ≤ v x ∧ (v x = 0 ↔ x = 0)) ∧
      (∀ x y : K, v (x * y) = v x * v y) ∧
        ∀ x y : K, v (x + y) ≤ v x + v y

theorem absoluteValue_finset_sum_le
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ)
    {ι : Type*} (s : Finset ι) (f : ι → K) :
    v (s.sum f) ≤ s.sum (fun i => v (f i)) := by
  classical
  refine Finset.induction_on s ?empty ?insert
  · simp
  · intro i s his ih
    rw [Finset.sum_insert his, Finset.sum_insert his]
    exact (v.add_le (f i) (s.sum f)).trans
      (by
        simpa [add_comm, add_left_comm, add_assoc] using
          add_le_add_left ih (v (f i)))

def EquivalentAbsoluteValues {K : Type*} [Field K]
    (v w : AbsoluteValue K ℝ) : Prop

theorem equivalentAbsoluteValues_iff_isEquiv
    {K : Type*} [Field K] (v w : AbsoluteValue K ℝ) :
    EquivalentAbsoluteValues v w ↔ v.IsEquiv w

theorem equivalentAbsoluteValues_of_isEquiv
    {K : Type*} [Field K] {v w : AbsoluteValue K ℝ}
    (h : v.IsEquiv w) :
    EquivalentAbsoluteValues v w

theorem isEquiv_of_equivalentAbsoluteValues
    {K : Type*} [Field K] {v w : AbsoluteValue K ℝ}
    (h : EquivalentAbsoluteValues v w) :
    v.IsEquiv w

theorem equivalentAbsoluteValues_refl
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ) :
    EquivalentAbsoluteValues v v

theorem equivalentAbsoluteValues_symm
    {K : Type*} [Field K] {v w : AbsoluteValue K ℝ}
    (h : EquivalentAbsoluteValues v w) :
    EquivalentAbsoluteValues w v

theorem equivalentAbsoluteValues_trans
    {K : Type*} [Field K] {v₁ v₂ v₃ : AbsoluteValue K ℝ}
    (h₁₂ : EquivalentAbsoluteValues v₁ v₂)
    (h₂₃ : EquivalentAbsoluteValues v₂ v₃) :
    EquivalentAbsoluteValues v₁ v₃

theorem equivalentAbsoluteValues_iff_exists_rpow_eq
    {K : Type*} [Field K] (v w : AbsoluteValue K ℝ) :
    EquivalentAbsoluteValues v w ↔ ∃ s : ℝ, 0 < s ∧ (v · ^ s) = w

theorem equivalentAbsoluteValues_iff_lt_one
    {K : Type*} [Field K] (v w : AbsoluteValue K ℝ) :
    EquivalentAbsoluteValues v w ↔ ∀ x : K, v x < 1 ↔ w x < 1

theorem absoluteValueApproximation_exists_separating_element
    {K : Type*} [Field K] {ι : Type*} [Finite ι]
    (v : ι → AbsoluteValue K ℝ)
    (hnontrivial : ∀ i, ¬ TrivialAbsoluteValue (v i))
    (hinequiv : Pairwise fun i j => ¬ EquivalentAbsoluteValues (v i) (v j)) :
    ∀ i, ∃ z : K, 1 < v i z ∧ ∀ j, j ≠ i → v j z < 1 := by
  apply AbsoluteValue.exists_one_lt_lt_one_pi_of_not_isEquiv
  · intro i
    exact (not_trivialAbsoluteValue_iff_isNontrivial (v i)).mp (hnontrivial i)
  · intro i j hij hIsEquiv
    exact
      (hinequiv hij)
        ((equivalentAbsoluteValues_iff_isEquiv (v i) (v j)).mpr hIsEquiv)

theorem absoluteValueApproximation_exists_bump_element
    {K : Type*} [Field K] {ι : Type*} [Finite ι]
    (v : ι → AbsoluteValue K ℝ) {i : ι} {z : K}
    (hlarge : 1 < v i z)
    (hsmall : ∀ j, j ≠ i → v j z < 1)
    {ε : ℝ} (hε : 0 < ε) :
    ∃ e : K, v i (e - 1) < ε ∧ ∀ j, j ≠ i → v j e < ε

theorem absoluteValueApproximation_exists_bump_family
    {K : Type*} [Field K] {ι : Type*} [Finite ι]
    (v : ι → AbsoluteValue K ℝ)
    (hnontrivial : ∀ i, ¬ TrivialAbsoluteValue (v i))
    (hinequiv : Pairwise fun i j => ¬ EquivalentAbsoluteValues (v i) (v j))
    {ε : ℝ} (hε : 0 < ε) :
    ∃ e : ι → K,
      ∀ i, v i (e i - 1) < ε ∧ ∀ j, j ≠ i → v j (e i) < ε := by
  classical
  have hsep :=
    absoluteValueApproximation_exists_separating_element
      (v := v) hnontrivial hinequiv
  choose z hz using hsep
  have hbump :
      ∀ i, ∃ e : K,
        v i (e - 1) < ε ∧ ∀ j, j ≠ i → v j e < ε := by
    intro i
    exact absoluteValueApproximation_exists_bump_element
      (v := v) (i := i) (z := z i) (hz i).1 (hz i).2 hε
  choose e he using hbump
  exact ⟨e, he⟩

theorem absoluteValueApproximation_sum_sub
    {K : Type*} [Field K] {ι : Type*} [Fintype ι] [DecidableEq ι]
    (a e : ι → K) (i : ι) :
    (∑ j, a j * e j) - a i =
      ∑ j, if j = i then a j * (e j - 1) else a j * e j := by
  classical
  have hsingle : (∑ j : ι, if j = i then a j else 0) = a i := by
    simp
  calc
    (∑ j, a j * e j) - a i
        = (∑ j, a j * e j) - ∑ j, (if j = i then a j else 0) := by
            rw [hsingle]
    _ = ∑ j, (a j * e j - if j = i then a j else 0) := by
            rw [Finset.sum_sub_distrib]
    _ = ∑ j, if j = i then a j * (e j - 1) else a j * e j := by
            refine Finset.sum_congr rfl ?_
            intro j _
            by_cases hji : j = i
            · simp [hji, mul_sub]
            · simp [hji]

theorem absoluteValueApproximation_from_weighted_bump_family
    {K : Type*} [Field K] {ι : Type*} [Fintype ι]
    (v : ι → AbsoluteValue K ℝ) (a e : ι → K) {ε δ : ℝ}
    (hεδ : (Fintype.card ι : ℝ) * δ < ε)
    (hdiag : ∀ i, v i (a i) * v i (e i - 1) < δ)
    (hoff : ∀ i j, j ≠ i → v i (a j) * v i (e j) < δ) :
    ∃ x : K, ∀ i, v i (x - a i) < ε

theorem absoluteValueApproximation_exists_coefficient_precision
    {K : Type*} [Field K] {ι : Type*} [Finite ι]
    (v : ι → AbsoluteValue K ℝ) (a : ι → K) {δ : ℝ} (hδ : 0 < δ) :
    ∃ η : ℝ, 0 < η ∧ ∀ i j, v i (a j) * η < δ

theorem absoluteValueApproximation
    {K : Type*} [Field K] {ι : Type*} [Finite ι]
    (v : ι → AbsoluteValue K ℝ)
    (hnontrivial : ∀ i, ¬ TrivialAbsoluteValue (v i))
    (hinequiv : Pairwise fun i j => ¬ EquivalentAbsoluteValues (v i) (v j))
    (a : ι → K) {ε : ℝ} (hε : 0 < ε) :
    ∃ x : K, ∀ i, v i (x - a i) < ε := by
  classical
  let : Fintype ι := Fintype.ofFinite ι
  let δ : ℝ := ε / ((Fintype.card ι : ℝ) + 1)
  have hcard_add_pos : 0 < (Fintype.card ι : ℝ) + 1 := by positivity
  have hδ_pos : 0 < δ := by
    dsimp [δ]
    exact div_pos hε hcard_add_pos
  have hεδ : (Fintype.card ι : ℝ) * δ < ε := by
    have hcard_div_lt_one :
        (Fintype.card ι : ℝ) / ((Fintype.card ι : ℝ) + 1) < 1 := by
      exact (div_lt_one hcard_add_pos).mpr (by linarith)
    calc
      (Fintype.card ι : ℝ) * δ =
          ε * ((Fintype.card ι : ℝ) / ((Fintype.card ι : ℝ) + 1)) := by
        dsimp [δ]
        ring
      _ < ε * 1 := mul_lt_mul_of_pos_left hcard_div_lt_one hε
      _ = ε := by ring
  obtain ⟨η, hη_pos, hη⟩ :=
    absoluteValueApproximation_exists_coefficient_precision (v := v) (a := a) hδ_pos
  obtain ⟨e, he⟩ :=
    absoluteValueApproximation_exists_bump_family
      (v := v) hnontrivial hinequiv (ε := η) hη_pos
  exact
    absoluteValueApproximation_from_weighted_bump_family
      (v := v) (a := a) (e := e) hεδ
      (fun i => by
        have hmul_le :
            v i (a i) * v i (e i - 1) ≤ v i (a i) * η :=
          mul_le_mul_of_nonneg_left (le_of_lt (he i).1) ((v i).nonneg (a i))
        exact lt_of_le_of_lt hmul_le (hη i i))
      (fun i j hji => by
        have hsmall : v i (e j) < η := (he j).2 i (Ne.symm hji)
        have hmul_le :
            v i (a j) * v i (e j) ≤ v i (a j) * η :=
          mul_le_mul_of_nonneg_left (le_of_lt hsmall) ((v i).nonneg (a j))
        exact lt_of_le_of_lt hmul_le (hη i j))

def NonarchimedeanAbsoluteValue {K : Type*} [Field K]
    (v : AbsoluteValue K ℝ) : Prop

def ArchimedeanAbsoluteValue {K : Type*} [Field K]
    (v : AbsoluteValue K ℝ) : Prop

def StrongTriangle {K : Type*} [Field K] (v : AbsoluteValue K ℝ) : Prop

theorem nonarchimedean_iff_bounded_nat
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ) :
    NonarchimedeanAbsoluteValue v ↔ ∃ C : ℝ, ∀ n : ℕ, v (n : K) ≤ C

theorem archimedean_iff_not_nonarchimedean
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ) :
    ArchimedeanAbsoluteValue v ↔ ¬ NonarchimedeanAbsoluteValue v

theorem strong_triangle_iff_isNonarchimedean
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ) :
    StrongTriangle v ↔ IsNonarchimedean (v : K → ℝ)

theorem nat_le_one_of_strong_triangle
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ)
    (hstrong : StrongTriangle v) (n : ℕ) :
    v (n : K) ≤ 1

theorem nonarchimedean_of_strong_triangle
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ)
    (hstrong : StrongTriangle v) :
    NonarchimedeanAbsoluteValue v

theorem nat_bound_ge_one
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ) {C : ℝ}
    (hC : ∀ n : ℕ, v (n : K) ≤ C) :
    1 ≤ C

theorem add_pow_le_of_bounded_nat
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ) {C : ℝ}
    (hC : ∀ n : ℕ, v (n : K) ≤ C) (x y : K) (n : ℕ) :
    v ((x + y) ^ n) ≤
      ((n + 1 : ℕ) : ℝ) * C * (max (v x) (v y)) ^ n

theorem tendsto_linear_bound_rpow_inv
    {C : ℝ} (hC : 0 < C) :
    Tendsto
      (fun n : ℕ => ((((n + 1 : ℕ) : ℝ) * C) ^ ((n : ℝ)⁻¹)))
      atTop (𝓝 1) := by
  have hCroot :
      Tendsto (fun n : ℕ => C ^ ((n : ℝ)⁻¹)) atTop (𝓝 1) := by
    have hcont : ContinuousAt (fun t : ℝ => C ^ t) 0 :=
      Real.continuousAt_const_rpow hC.ne'
    have hzero : Tendsto (fun n : ℕ => (n : ℝ)⁻¹) atTop (𝓝 0) :=
      tendsto_inv_atTop_zero.comp tendsto_natCast_atTop_atTop
    change Tendsto
      ((fun t : ℝ => C ^ t) ∘ fun n : ℕ => (n : ℝ)⁻¹) atTop (𝓝 1)
    simpa only [Real.rpow_zero] using hcont.tendsto.comp hzero
  have hshiftReal :
      Tendsto (fun x : ℝ => x ^ ((1 : ℝ) / (1 * x + (-1)))) atTop (𝓝 1) :=
    tendsto_rpow_div_mul_add 1 1 (-1) zero_ne_one
  have hshiftNat :
      Tendsto (fun n : ℕ => (((n + 1 : ℕ) : ℝ) ^ ((n : ℝ)⁻¹)))
        atTop (𝓝 1) := by
    have hnatshift : Tendsto (fun n : ℕ => (n : ℝ) + 1) atTop atTop :=
      tendsto_atTop_add_const_right atTop 1 tendsto_natCast_atTop_atTop
    refine (hshiftReal.comp hnatshift).congr' ?_
    exact Eventually.of_forall fun n => by
      simp [Nat.cast_add, Nat.cast_one, one_div, add_assoc]
  have htarget :
      Tendsto
        (fun n : ℕ => ((((n + 1 : ℕ) : ℝ) * C) ^ ((n : ℝ)⁻¹)))
        atTop (𝓝 (1 * 1)) := by
    refine (hshiftNat.mul hCroot).congr' ?_
    exact Eventually.of_forall fun n => by
      have hn_nonneg : 0 ≤ ((n + 1 : ℕ) : ℝ) := by positivity
      have hmul :=
        (Real.mul_rpow (z := ((n : ℝ)⁻¹)) hn_nonneg (le_of_lt hC)).symm
      simpa [mul_comm, mul_left_comm, mul_assoc] using hmul
  simpa using htarget

theorem add_le_root_bound_of_bounded_nat
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ) {C : ℝ}
    (hC : ∀ n : ℕ, v (n : K) ≤ C) (x y : K)
    {n : ℕ} (hn : n ≠ 0) :
    v (x + y) ≤
      ((((n + 1 : ℕ) : ℝ) * C) ^ ((n : ℝ)⁻¹)) *
        max (v x) (v y)

theorem strong_triangle_of_nonarchimedean
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ)
    (hnonarch : NonarchimedeanAbsoluteValue v) :
    StrongTriangle v

theorem nonarchimedean_iff_strong_triangle
    {K : Type*} [Field K] (v : AbsoluteValue K ℝ) :
    NonarchimedeanAbsoluteValue v ↔ StrongTriangle v

theorem strong_triangle_eq_max_of_ne
    {K : Type*} [Field K] {v : AbsoluteValue K ℝ}
    (hstrong : StrongTriangle v)
    {x y : K} (hxy : v x ≠ v y) :
    v (x + y) = max (v x) (v y)

theorem rat_equivalent_real_or_padic
    (v : AbsoluteValue ℚ ℝ) (hnontrivial : ¬ TrivialAbsoluteValue v) :
    EquivalentAbsoluteValues v Rat.AbsoluteValue.real ∨
      ∃! p : ℕ, ∃ (_ : Fact p.Prime),
        EquivalentAbsoluteValues v (Rat.AbsoluteValue.padic p)