lemmas about powers of elements (#1688)

* feat(algebra/archimedean): add alternative version of exists_int_pow_near

- also add docstrings

* feat(analysis/normed_space/basic): additional inequality lemmas

- that there exists elements with large and small norms in a nondiscrete normed field.

* doc(algebra/archimedean): edit docstrings

* Apply suggestions from code review

Co-Authored-By: Chris Hughes <33847686+ChrisHughes24@users.noreply.github.com>

Author: 2 people

src/algebra/archimedean.lean

@@ -32,6 +32,8 @@ let ⟨n, h⟩ := archimedean.arch x hy0 in
        ... < 1 + n • (y - 1) : by rw add_comm; exact lt_add_one _
        ... ≤ y ^ n           : one_add_sub_mul_le_pow (le_of_lt hy1) _⟩
 
+/-- Every x greater than 1 is between two successive natural-number
+powers of another y greater than one. -/
 lemma exists_nat_pow_near {x : α} {y : α} (hx : 1 < x) (hy : 1 < y) :
   ∃ n : ℕ, y ^ n ≤ x ∧ x < y ^ (n + 1) :=
 have h : ∃ n : ℕ, x < y ^ n, from pow_unbounded_of_one_lt _ hy,
@@ -67,6 +69,9 @@ end linear_ordered_ring
 
 section linear_ordered_field
 
+/-- Every positive x is between two successive integer powers of
+another y greater than one. This is the same as `exists_int_pow_near'`,
+but with ≤ and < the other way around. -/
 lemma exists_int_pow_near [discrete_linear_ordered_field α] [archimedean α]
   {x : α} {y : α} (hx : 0 < x) (hy : 1 < y) :
   ∃ n : ℤ, y ^ n ≤ x ∧ x < y ^ (n + 1) :=
@@ -82,6 +87,19 @@ let ⟨M, hM⟩ := pow_unbounded_of_one_lt x hy in
 let ⟨n, hn₁, hn₂⟩ := int.exists_greatest_of_bdd hb he in
   ⟨n, hn₁, lt_of_not_ge (λ hge, not_le_of_gt (int.lt_succ _) (hn₂ _ hge))⟩
 
+/-- Every positive x is between two successive integer powers of
+another y greater than one. This is the same as `exists_int_pow_near`,
+but with ≤ and < the other way around. -/
+lemma exists_int_pow_near' [discrete_linear_ordered_field α] [archimedean α]
+  {x : α} {y : α} (hx : 0 < x) (hy : 1 < y) :
+  ∃ n : ℤ, y ^ n < x ∧ x ≤ y ^ (n + 1) :=
+let ⟨m, hle, hlt⟩ := exists_int_pow_near (inv_pos hx) hy in
+have hyp : 0 < y, from lt_trans (discrete_linear_ordered_field.zero_lt_one α) hy,
+⟨-(m+1),
+by rwa [fpow_neg, one_div_eq_inv, inv_lt (fpow_pos_of_pos hyp _) hx],
+by rwa [neg_add, neg_add_cancel_right, fpow_neg, one_div_eq_inv,
+        le_inv hx (fpow_pos_of_pos hyp _)]⟩
+
 variables [linear_ordered_field α] [floor_ring α]
 
 lemma sub_floor_div_mul_nonneg (x : α) {y : α} (hy : 0 < y) :

src/analysis/normed_space/basic.lean

@@ -398,6 +398,20 @@ begin
   { simp [inv_lt_one hy] }
 end
 
+lemma exists_lt_norm (α : Type*) [nondiscrete_normed_field α]
+  (r : ℝ) : ∃ x : α, r < ∥x∥ :=
+let ⟨w, hw⟩ := exists_one_lt_norm α in
+let ⟨n, hn⟩ := pow_unbounded_of_one_lt r hw in
+⟨w^n, by rwa norm_pow⟩
+
+lemma exists_norm_lt (α : Type*) [nondiscrete_normed_field α]
+  {r : ℝ} (hr : 0 < r) : ∃ x : α, 0 < ∥x∥ ∧ ∥x∥ < r :=
+let ⟨w, hw⟩ := exists_one_lt_norm α in
+let ⟨n, hle, hlt⟩ := exists_int_pow_near' hr hw in
+⟨w^n, by { rw norm_fpow; exact fpow_pos_of_pos (lt_trans zero_lt_one hw) _},
+by rwa norm_fpow⟩
+
+
 instance : normed_field ℝ :=
 { norm := λ x, abs x,
   dist_eq := assume x y, rfl,