feat(algebra/floor): When the floor is strictly positive (#9625)

`⌊a⌋₊` and `⌊a⌋` are strictly positive iff `1 ≤ a`. We use this to slightly golf IMO 2013 P5.

Author: YaelDillies

archive/imo/imo2013_q5.lean

@@ -11,14 +11,14 @@ import data.real.basic
 /-!
 # IMO 2013 Q5
 
-Let ℚ>₀ be the set of positive rational numbers. Let f: ℚ>₀ → ℝ be a function satisfying
+Let `ℚ>₀` be the positive rational numbers. Let `f : ℚ>₀ → ℝ` be a function satisfying
 the conditions
 
-  (1) f(x) * f(y) ≥ f(x * y)
-  (2) f(x + y)    ≥ f(x) + f(y)
+1. `f(x) * f(y) ≥ f(x * y)`
+2. `f(x + y) ≥ f(x) + f(y)`
 
-for all x,y ∈ ℚ>₀. Given that f(a) = a for some rational a > 1, prove that f(x) = x for
-all x ∈ ℚ>₀.
+for all `x, y ∈ ℚ>₀`. Given that `f(a) = a` for some rational `a > 1`, prove that `f(x) = x` for
+all `x ∈ ℚ>₀`.
 
 # Solution
 
@@ -98,54 +98,39 @@ lemma f_pos_of_pos {f : ℚ → ℝ} {q : ℚ} (hq : 0 < q)
   (H4 : ∀ n : ℕ, 0 < n → (n : ℝ) ≤ f n) :
   0 < f q :=
 begin
-  have hfqn := calc f q.num = f (q * q.denom) : by rw ←rat.mul_denom_eq_num
-                        ... ≤ f q * f q.denom : H1 q q.denom hq (nat.cast_pos.mpr q.pos),
-
-  -- Now we just need to show that `f q.num` and `f q.denom` are positive.
-  -- Then nlinarith will be able to close the goal.
-
   have num_pos : 0 < q.num := rat.num_pos_iff_pos.mpr hq,
-  have hqna : (q.num.nat_abs : ℤ) = q.num := int.nat_abs_of_nonneg num_pos.le,
-  have hqfn' :=
-    calc (q.num : ℝ)
-            = ((q.num.nat_abs : ℤ) : ℝ) : congr_arg coe (eq.symm hqna)
-        ... ≤ f q.num.nat_abs           : H4 q.num.nat_abs
-                                            (int.nat_abs_pos_of_ne_zero (ne_of_gt num_pos))
-        ... = f q.num                   : by exact_mod_cast congr_arg f (congr_arg coe hqna),
-
-  have f_num_pos := calc (0 : ℝ) < q.num   : int.cast_pos.mpr num_pos
-                             ... ≤ f q.num : hqfn',
-  have f_denom_pos := calc (0 : ℝ) < q.denom   : nat.cast_pos.mpr q.pos
-                               ... ≤ f q.denom : H4 q.denom q.pos,
-  nlinarith
+  have hmul_pos :=
+    calc (0 : ℝ) < q.num   : int.cast_pos.mpr num_pos
+      ... = ((q.num.nat_abs : ℤ) : ℝ) : congr_arg coe (int.nat_abs_of_nonneg num_pos.le).symm
+      ... ≤ f q.num.nat_abs           : H4 q.num.nat_abs
+                                          (int.nat_abs_pos_of_ne_zero num_pos.ne')
+      ... = f q.num : by { rw ←int.nat_abs_of_nonneg num_pos.le, norm_cast }
+      ... = f (q * q.denom) : by rw ←rat.mul_denom_eq_num
+      ... ≤ f q * f q.denom : H1 q q.denom hq (nat.cast_pos.mpr q.pos),
+  have h_f_denom_pos :=
+    calc (0 : ℝ) < q.denom : nat.cast_pos.mpr q.pos
+      ... ≤ f q.denom : H4 q.denom q.pos,
+  exact pos_of_mul_pos_right hmul_pos h_f_denom_pos.le,
 end
 
 lemma fx_gt_xm1 {f : ℚ → ℝ} {x : ℚ} (hx : 1 ≤ x)
   (H1 : ∀ x y, 0 < x → 0 < y → f (x * y) ≤ f x * f y)
   (H2 : ∀ x y, 0 < x → 0 < y → f x + f y ≤ f (x + y))
   (H4 : ∀ n : ℕ, 0 < n → (n : ℝ) ≤ f n) :
-  ((x - 1 : ℚ) : ℝ) < f x :=
+  (x - 1 : ℝ) < f x :=
 begin
-  have hfe : (⌊x⌋.nat_abs : ℤ) = ⌊x⌋ := int.nat_abs_of_nonneg
-    (floor_nonneg.mpr (zero_le_one.trans hx)),
-  have hfe' : (⌊x⌋.nat_abs : ℚ) = ⌊x⌋, { exact_mod_cast hfe },
-  have h0fx : 0 < ⌊x⌋ := int.cast_pos.mp ((sub_nonneg.mpr hx).trans_lt (sub_one_lt_floor x)),
-  have h_nat_abs_floor_pos : 0 < ⌊x⌋.nat_abs := int.nat_abs_pos_of_ne_zero (ne_of_gt h0fx),
-  have hx0 := calc ((x - 1 : ℚ) : ℝ)
-                     < ⌊x⌋            : by exact_mod_cast sub_one_lt_floor x
-                 ... = ↑⌊x⌋.nat_abs   : by exact_mod_cast hfe.symm
-                 ... ≤ f ⌊x⌋.nat_abs  : H4 ⌊x⌋.nat_abs h_nat_abs_floor_pos
-                 ... = f ⌊x⌋          : by rw hfe',
-
-  obtain (h_eq : (⌊x⌋ : ℚ) = x) | (h_lt : (⌊x⌋ : ℚ) < x) := (floor_le x).eq_or_lt,
+  have hx0 :=
+    calc (x - 1 : ℝ)
+          < ⌊x⌋₊   : by exact_mod_cast sub_one_lt_nat_floor x
+      ... ≤ f ⌊x⌋₊ : H4 _ (nat_floor_pos.2 hx),
+
+  obtain h_eq | h_lt := (nat_floor_le $ zero_le_one.trans hx).eq_or_lt,
   { rwa h_eq at hx0 },
 
-  calc ((x - 1 : ℚ) : ℝ) < f ⌊x⌋               : hx0
-                     ... < f (x - ⌊x⌋) + f ⌊x⌋ : lt_add_of_pos_left (f ↑⌊x⌋)
-                                                   (f_pos_of_pos (sub_pos.mpr h_lt) H1 H4)
-                     ... ≤ f (x - ⌊x⌋ + ⌊x⌋)   : H2 (x - ⌊x⌋) ⌊x⌋ (sub_pos.mpr h_lt)
-                                                    (by exact_mod_cast h0fx)
-                     ... = f x                 : by simp only [sub_add_cancel]
+  calc (x - 1 : ℝ) < f ⌊x⌋₊ : hx0
+    ... < f (x - ⌊x⌋₊) + f ⌊x⌋₊ : lt_add_of_pos_left _ (f_pos_of_pos (sub_pos.mpr h_lt) H1 H4)
+    ... ≤ f (x - ⌊x⌋₊ + ⌊x⌋₊)   : H2 _ _ (sub_pos.mpr h_lt) (nat.cast_pos.2 (nat_floor_pos.2 hx))
+    ... = f x                   : by rw sub_add_cancel
 end
 
 lemma pow_f_le_f_pow {f : ℚ → ℝ} {n : ℕ} (hn : 0 < n) {x : ℚ} (hx : 1 < x)
@@ -223,7 +208,7 @@ begin
   have H3 : ∀ x : ℚ, 0 < x → ∀ n : ℕ, 0 < n → ↑n * f x ≤ f (n * x),
   { intros x hx n hn,
     cases n,
-    { exfalso, exact nat.lt_asymm hn hn },
+    { exact (lt_irrefl 0 hn).elim },
     induction n with pn hpn,
     { simp only [one_mul, nat.cast_one] },
     calc (↑pn + 1 + 1) * f x
@@ -247,7 +232,7 @@ begin
               ... = ↑a * f 1  : by rw hae },
 
     calc (n : ℝ) = (n : ℝ) * 1   : (mul_one _).symm
-             ... ≤ (n : ℝ) * f 1 : (mul_le_mul_left (nat.cast_pos.mpr hn)).mpr hf1
+             ... ≤ (n : ℝ) * f 1 : mul_le_mul_of_nonneg_left hf1 (nat.cast_nonneg _)
              ... ≤ f (n * 1)     : H3 1 zero_lt_one n hn
              ... = f n           : by rw mul_one },
 

src/algebra/floor.lean

@@ -55,7 +55,7 @@ class floor_ring (α) [linear_ordered_ring α] :=
 
 instance : floor_ring ℤ := { floor := id, le_floor := λ _ _, by rw int.cast_id; refl }
 
-variables [linear_ordered_ring α] [floor_ring α]
+variables [linear_ordered_ring α] [floor_ring α] {z : ℤ} {a : α}
 
 /-- `floor x` is the greatest integer `z` such that `z ≤ x`. It is denoted with `⌊x⌋`. -/
 def floor : α → ℤ := floor_ring.floor
@@ -94,6 +94,10 @@ by rw [← int.cast_one, floor_coe]
 @[mono] theorem floor_mono {a b : α} (h : a ≤ b) : ⌊a⌋ ≤ ⌊b⌋ :=
 le_floor.2 (le_trans (floor_le _) h)
 
+lemma floor_pos : 0 < ⌊a⌋ ↔ 1 ≤ a :=
+⟨λ h, le_trans (by rwa [←int.cast_one, int.cast_le, ←zero_add (1 : ℤ), int.add_one_le_iff])
+  (floor_le _), λ h, zero_lt_one.trans_le (le_floor.2 $ by rwa int.cast_one)⟩
+
 @[simp] theorem floor_add_int (x : α) (z : ℤ) : ⌊x + z⌋ = ⌊x⌋ + z :=
 eq_of_forall_le_iff $ λ a, by rw [le_floor,
   ← sub_le_iff_le_add, ← sub_le_iff_le_add, le_floor, int.cast_sub]
@@ -273,7 +277,7 @@ by { rw floor_lt, exact h.trans_le (le_ceil _) }
 /-! ### `nat_floor` and `nat_ceil` -/
 
 section nat
-variables {a : α} {n : ℕ}
+variables {n : ℕ}
 
 /-- `nat_floor x` is the greatest natural `n` that is less than `x`.
 It is equal to `⌊x⌋` when `x ≥ 0`, and is `0` otherwise. It is denoted with `⌊x⌋₊`.-/
@@ -287,12 +291,6 @@ begin
   exact_mod_cast (floor_le a).trans ha,
 end
 
-lemma pos_of_nat_floor_pos (h : 0 < ⌊a⌋₊) : 0 < a :=
-begin
-  refine (le_or_lt a 0).resolve_left (λ ha, lt_irrefl 0 _),
-  rwa nat_floor_of_nonpos ha at h,
-end
-
 lemma nat_floor_le (ha : 0 ≤ a) : ↑⌊a⌋₊ ≤ a :=
 begin
   refine le_trans _ (floor_le _),
@@ -310,6 +308,21 @@ end
 theorem le_nat_floor_iff (ha : 0 ≤ a) : n ≤ ⌊a⌋₊ ↔ ↑n ≤ a :=
 ⟨λ h, (nat.cast_le.2 h).trans (nat_floor_le ha), le_nat_floor_of_le⟩
 
+lemma nat_floor_pos : 0 < ⌊a⌋₊ ↔ 1 ≤ a :=
+begin
+  cases le_total a 0,
+  { rw nat_floor_of_nonpos h,
+    exact iff_of_false (lt_irrefl 0) (λ ha, zero_lt_one.not_le $ ha.trans h) },
+  { rw [←nat.cast_one, ←le_nat_floor_iff h],
+    refl }
+end
+
+lemma pos_of_nat_floor_pos (h : 0 < ⌊a⌋₊) : 0 < a :=
+begin
+  refine (le_or_lt a 0).resolve_left (λ ha, lt_irrefl 0 _),
+  rwa nat_floor_of_nonpos ha at h,
+end
+
 lemma lt_of_lt_nat_floor (h : n < ⌊a⌋₊) : ↑n < a :=
 (nat.cast_lt.2 h).trans_le (nat_floor_le (pos_of_nat_floor_pos ((nat.zero_le n).trans_lt h)).le)
 
@@ -346,6 +359,9 @@ begin
   exact int.le_to_nat _,
 end
 
+lemma sub_one_lt_nat_floor (a : α) : a - 1 < ⌊a⌋₊ :=
+sub_lt_iff_lt_add.2 (lt_nat_floor_add_one a)
+
 lemma nat_floor_eq_zero_iff : ⌊a⌋₊ = 0 ↔ a < 1 :=
 begin
   obtain ha | ha := le_total a 0,