feat(algebra/floor): notation for nat_floor and nat_ceil (#8526)

We introduce the notations ` ⌊a⌋₊` for `nat_floor a` and `⌈a⌉₊` for `nat_ceil a`, mimicking the existing notations for `floor` and `ceil` (with the `+` corresponding to the recent notation for `nnnorm`).

src/algebra/archimedean.lean

@@ -261,7 +261,7 @@ theorem archimedean_iff_rat_lt :
 ⟨@exists_rat_gt α _,
   λ H, archimedean_iff_nat_lt.2 $ λ x,
   let ⟨q, h⟩ := H x in
-  ⟨nat_ceil q, lt_of_lt_of_le h $
+  ⟨⌈q⌉₊, lt_of_lt_of_le h $
     by simpa only [rat.cast_coe_nat] using (@rat.cast_le α _ _ _).2 (le_nat_ceil _)⟩⟩
 
 theorem archimedean_iff_rat_le :

src/algebra/floor.lean

@@ -28,6 +28,11 @@ We define `floor`, `ceil`, `nat_floor`and `nat_ceil` functions on linear ordered
 
 - `⌊x⌋` is `floor x`.
 - `⌈x⌉` is `ceil x`.
+- `⌊x⌋₊` is `nat_floor x`.
+- `⌈x⌉₊` is `nat_ceil x`.
+
+The index `₊` in the notations for `nat_floor` and `nat_ceil` is used in analogy to the notation
+for `nnnorm`.
 
 ## Tags
 
@@ -52,7 +57,7 @@ instance : floor_ring ℤ := { floor := id, le_floor := λ _ _, by rw int.cast_i
 
 variables [linear_ordered_ring α] [floor_ring α]
 
-/-- `floor x` is the greatest integer `z` such that `z ≤ x` -/
+/-- `floor x` is the greatest integer `z` such that `z ≤ x`. It is denoted with `⌊x⌋`. -/
 def floor : α → ℤ := floor_ring.floor
 
 notation `⌊` x `⌋` := floor x
@@ -132,10 +137,10 @@ begin
   exact ⟨floor_le v, lt_floor_add_one v⟩
 end
 
-lemma floor_eq_on_Ico (n : ℤ) : ∀ x ∈ (set.Ico n (n+1) : set α), floor x = n :=
+lemma floor_eq_on_Ico (n : ℤ) : ∀ x ∈ (set.Ico n (n+1) : set α), ⌊x⌋ = n :=
 λ x ⟨h₀, h₁⟩, floor_eq_iff.mpr ⟨h₀, h₁⟩
 
-lemma floor_eq_on_Ico' (n : ℤ) : ∀ x ∈ (set.Ico n (n+1) : set α), (floor x : α) = n :=
+lemma floor_eq_on_Ico' (n : ℤ) : ∀ x ∈ (set.Ico n (n+1) : set α), (⌊x⌋ : α) = n :=
 λ x hx, by exact_mod_cast floor_eq_on_Ico n x hx
 
 /-- The fractional part fract r of r is just r - ⌊r⌋ -/
@@ -207,7 +212,7 @@ begin
   abel
 end
 
-/-- `ceil x` is the smallest integer `z` such that `x ≤ z` -/
+/-- `ceil x` is the smallest integer `z` such that `x ≤ z`. It is denoted with `⌈x⌉`. -/
 def ceil (x : α) : ℤ := -⌊-x⌋
 
 notation `⌈` x `⌉` := ceil x
@@ -256,10 +261,10 @@ lemma ceil_eq_iff {r : α} {z : ℤ} :
 by rw [←ceil_le, ←int.cast_one, ←int.cast_sub, ←lt_ceil,
 int.sub_one_lt_iff, le_antisymm_iff, and.comm]
 
-lemma ceil_eq_on_Ioc (n : ℤ) : ∀ x ∈ (set.Ioc (n-1) n : set α), ceil x = n :=
+lemma ceil_eq_on_Ioc (n : ℤ) : ∀ x ∈ (set.Ioc (n-1) n : set α), ⌈x⌉ = n :=
 λ x ⟨h₀, h₁⟩, ceil_eq_iff.mpr ⟨h₀, h₁⟩
 
-lemma ceil_eq_on_Ioc' (n : ℤ) : ∀ x ∈ (set.Ioc (n-1) n : set α), (ceil x : α) = n :=
+lemma ceil_eq_on_Ioc' (n : ℤ) : ∀ x ∈ (set.Ioc (n-1) n : set α), (⌈x⌉ : α) = n :=
 λ x hx, by exact_mod_cast ceil_eq_on_Ioc n x hx
 
 /-! ### `nat_floor` and `nat_ceil` -/
@@ -268,102 +273,106 @@ section nat
 variables {a : α} {n : ℕ}
 
 /-- `nat_floor x` is the greatest natural `n` that is less than `x`.
-It is equal to `⌊q⌋` when `q ≥ 0`, and is `0` otherwise. -/
+It is equal to `⌊x⌋` when `x ≥ 0`, and is `0` otherwise. It is denoted with `⌊x⌋₊`.-/
 def nat_floor (a : α) : ℕ := int.to_nat ⌊a⌋
 
-lemma nat_floor_of_nonpos (ha : a ≤ 0) : nat_floor a = 0 :=
+notation `⌊` x `⌋₊` := nat_floor x
+
+lemma nat_floor_of_nonpos (ha : a ≤ 0) : ⌊a⌋₊ = 0 :=
 begin
   apply int.to_nat_of_nonpos,
   exact_mod_cast (floor_le a).trans ha,
 end
 
-lemma pos_of_nat_floor_pos (h : 0 < nat_floor a) : 0 < a :=
+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) : ↑(nat_floor a) ≤ a :=
+lemma nat_floor_le (ha : 0 ≤ a) : ↑⌊a⌋₊ ≤ a :=
 begin
   refine le_trans _ (floor_le _),
   norm_cast,
   exact (int.to_nat_of_nonneg (floor_nonneg.2 ha)).le,
 end
 
-lemma le_nat_floor_of_le (h : ↑n ≤ a) : n ≤ nat_floor a :=
+lemma le_nat_floor_of_le (h : ↑n ≤ a) : n ≤ ⌊a⌋₊ :=
 begin
   have hn := int.le_to_nat n,
   norm_cast at hn,
   exact hn.trans (int.to_nat_le_to_nat (le_floor.2 h)),
 end
 
-theorem le_nat_floor_iff (ha : 0 ≤ a) : n ≤ nat_floor a ↔ ↑n ≤ a :=
+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 lt_of_lt_nat_floor (h : n < nat_floor a) : ↑n < a :=
+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)
 
-theorem nat_floor_lt_iff (ha : 0 ≤ a) : nat_floor a < n ↔ a < ↑n :=
+theorem nat_floor_lt_iff (ha : 0 ≤ a) : ⌊a⌋₊ < n ↔ a < ↑n :=
 le_iff_le_iff_lt_iff_lt.1 (le_nat_floor_iff ha)
 
-theorem nat_floor_mono {a₁ a₂ : α} (h : a₁ ≤ a₂) : nat_floor a₁ ≤ nat_floor a₂ :=
+theorem nat_floor_mono {a₁ a₂ : α} (h : a₁ ≤ a₂) : ⌊a₁⌋₊ ≤ ⌊a₂⌋₊ :=
 begin
   obtain ha | ha := le_total a₁ 0,
   { rw nat_floor_of_nonpos ha,
     exact nat.zero_le _ },
   exact le_nat_floor_of_le ((nat_floor_le ha).trans h),
 end
 
-@[simp] theorem nat_floor_coe (n : ℕ) : nat_floor (n : α) = n :=
+@[simp] theorem nat_floor_coe (n : ℕ) : ⌊(n : α)⌋₊ = n :=
 begin
   rw nat_floor,
   convert int.to_nat_coe_nat n,
   exact floor_coe n,
 end
 
-@[simp] theorem nat_floor_zero : nat_floor (0 : α) = 0 := nat_floor_coe 0
+@[simp] theorem nat_floor_zero : ⌊(0 : α)⌋₊ = 0 := nat_floor_coe 0
 
-theorem nat_floor_add_nat (ha : 0 ≤ a) (n : ℕ) : nat_floor (a + n) = nat_floor a + n :=
+theorem nat_floor_add_nat (ha : 0 ≤ a) (n : ℕ) : ⌊a + n⌋₊ = ⌊a⌋₊ + n :=
 begin
   change int.to_nat ⌊a + (n : ℤ)⌋ = int.to_nat ⌊a⌋ + n,
   rw [floor_add_int, int.to_nat_add_nat (le_floor.2 ha)],
 end
 
-lemma lt_nat_floor_add_one (a : α) : a < nat_floor a + 1 :=
+lemma lt_nat_floor_add_one (a : α) : a < ⌊a⌋₊ + 1 :=
 begin
   refine (lt_floor_add_one a).trans_le (add_le_add_right _ 1),
   norm_cast,
   exact int.le_to_nat _,
 end
 
-lemma nat_floor_eq_zero_iff : nat_floor a = 0 ↔ a < 1 :=
+lemma nat_floor_eq_zero_iff : ⌊a⌋₊ = 0 ↔ a < 1 :=
 begin
   obtain ha | ha := le_total a 0,
   { exact iff_of_true (nat_floor_of_nonpos ha) (ha.trans_lt zero_lt_one) },
   rw [←nat.cast_one, ←nat_floor_lt_iff ha, nat.lt_add_one_iff, nat.le_zero_iff],
 end
 
 /-- `nat_ceil x` is the least natural `n` that is greater than `x`.
-It is equal to `⌈q⌉` when `q ≥ 0`, and is `0` otherwise. -/
+It is equal to `⌈x⌉` when `x ≥ 0`, and is `0` otherwise. It is denoted with `⌈x⌉₊`. -/
 def nat_ceil (a : α) : ℕ := int.to_nat ⌈a⌉
 
-theorem nat_ceil_le : nat_ceil a ≤ n ↔ a ≤ n :=
+notation `⌈` x `⌉₊` := nat_ceil x
+
+theorem nat_ceil_le : ⌈a⌉₊ ≤ n ↔ a ≤ n :=
 by rw [nat_ceil, int.to_nat_le, ceil_le]; refl
 
-theorem lt_nat_ceil : n < nat_ceil a ↔ (n : α) < a :=
+theorem lt_nat_ceil : n < ⌈a⌉₊ ↔ (n : α) < a :=
 not_iff_not.1 $ by rw [not_lt, not_lt, nat_ceil_le]
 
-theorem le_nat_ceil (a : α) : a ≤ nat_ceil a := nat_ceil_le.1 (le_refl _)
+theorem le_nat_ceil (a : α) : a ≤ ⌈a⌉₊ := nat_ceil_le.1 (le_refl _)
 
-theorem nat_ceil_mono {a₁ a₂ : α} (h : a₁ ≤ a₂) : nat_ceil a₁ ≤ nat_ceil a₂ :=
+theorem nat_ceil_mono {a₁ a₂ : α} (h : a₁ ≤ a₂) : ⌈a₁⌉₊ ≤ ⌈a₂⌉₊ :=
 nat_ceil_le.2 (le_trans h (le_nat_ceil _))
 
-@[simp] theorem nat_ceil_coe (n : ℕ) : nat_ceil (n : α) = n :=
+@[simp] theorem nat_ceil_coe (n : ℕ) : ⌈(n : α)⌉₊ = n :=
 show (⌈((n : ℤ) : α)⌉).to_nat = n, by rw [ceil_coe]; refl
 
-@[simp] theorem nat_ceil_zero : nat_ceil (0 : α) = 0 := nat_ceil_coe 0
+@[simp] theorem nat_ceil_zero : ⌈(0 : α)⌉₊ = 0 := nat_ceil_coe 0
 
-theorem nat_ceil_add_nat {a : α} (a_nonneg : 0 ≤ a) (n : ℕ) : nat_ceil (a + n) = nat_ceil a + n :=
+theorem nat_ceil_add_nat {a : α} (a_nonneg : 0 ≤ a) (n : ℕ) : ⌈a + n⌉₊ = ⌈a⌉₊ + n :=
 begin
   change int.to_nat (⌈a + (n:ℤ)⌉) = int.to_nat ⌈a⌉ + n,
   rw [ceil_add_int],
@@ -373,48 +382,47 @@ begin
   refl
 end
 
-theorem nat_ceil_lt_add_one {a : α} (a_nonneg : 0 ≤ a) :
-  (nat_ceil a : α) < a + 1 :=
+theorem nat_ceil_lt_add_one {a : α} (a_nonneg : 0 ≤ a) : (⌈a⌉₊ : α) < a + 1 :=
 lt_nat_ceil.1 $ by rw (
-  show nat_ceil (a + 1) = nat_ceil a + 1, by exact_mod_cast (nat_ceil_add_nat a_nonneg 1));
+  show ⌈a + 1⌉₊ = ⌈a⌉₊ + 1, by exact_mod_cast (nat_ceil_add_nat a_nonneg 1));
   apply nat.lt_succ_self
 
-lemma lt_of_nat_ceil_lt {x : α} {n : ℕ} (h : nat_ceil x < n) : x < n :=
+lemma lt_of_nat_ceil_lt {x : α} {n : ℕ} (h : ⌈x⌉₊ < n) : x < n :=
 lt_of_le_of_lt (le_nat_ceil x) (by exact_mod_cast h)
 
-lemma le_of_nat_ceil_le {x : α} {n : ℕ} (h : nat_ceil x ≤ n) : x ≤ n :=
+lemma le_of_nat_ceil_le {x : α} {n : ℕ} (h : ⌈x⌉₊ ≤ n) : x ≤ n :=
 le_trans (le_nat_ceil x) (by exact_mod_cast h)
 
 end nat
 
 namespace int
 
 @[simp] lemma preimage_Ioo {x y : α} :
-  ((coe : ℤ → α) ⁻¹' (set.Ioo x y)) = set.Ioo (floor x) (ceil y) :=
+  ((coe : ℤ → α) ⁻¹' (set.Ioo x y)) = set.Ioo ⌊x⌋ ⌈y⌉ :=
 by { ext, simp [floor_lt, lt_ceil] }
 
 @[simp] lemma preimage_Ico {x y : α} :
-  ((coe : ℤ → α) ⁻¹' (set.Ico x y)) = set.Ico (ceil x) (ceil y) :=
+  ((coe : ℤ → α) ⁻¹' (set.Ico x y)) = set.Ico ⌈x⌉ ⌈y⌉ :=
 by { ext, simp [ceil_le, lt_ceil] }
 
 @[simp] lemma preimage_Ioc {x y : α} :
-  ((coe : ℤ → α) ⁻¹' (set.Ioc x y)) = set.Ioc (floor x) (floor y) :=
+  ((coe : ℤ → α) ⁻¹' (set.Ioc x y)) = set.Ioc ⌊x⌋ ⌊y⌋ :=
 by { ext, simp [floor_lt, le_floor] }
 
 @[simp] lemma preimage_Icc {x y : α} :
-  ((coe : ℤ → α) ⁻¹' (set.Icc x y)) = set.Icc (ceil x) (floor y) :=
+  ((coe : ℤ → α) ⁻¹' (set.Icc x y)) = set.Icc ⌈x⌉ ⌊y⌋ :=
 by { ext, simp [ceil_le, le_floor] }
 
-@[simp] lemma preimage_Ioi {x : α} : ((coe : ℤ → α) ⁻¹' (set.Ioi x)) = set.Ioi (floor x) :=
+@[simp] lemma preimage_Ioi {x : α} : ((coe : ℤ → α) ⁻¹' (set.Ioi x)) = set.Ioi ⌊x⌋ :=
 by { ext, simp [floor_lt] }
 
-@[simp] lemma preimage_Ici {x : α} : ((coe : ℤ → α) ⁻¹' (set.Ici x)) = set.Ici (ceil x) :=
+@[simp] lemma preimage_Ici {x : α} : ((coe : ℤ → α) ⁻¹' (set.Ici x)) = set.Ici ⌈x⌉ :=
 by { ext, simp [ceil_le] }
 
-@[simp] lemma preimage_Iio {x : α} : ((coe : ℤ → α) ⁻¹' (set.Iio x)) = set.Iio (ceil x) :=
+@[simp] lemma preimage_Iio {x : α} : ((coe : ℤ → α) ⁻¹' (set.Iio x)) = set.Iio ⌈x⌉ :=
 by { ext, simp [lt_ceil] }
 
-@[simp] lemma preimage_Iic {x : α} : ((coe : ℤ → α) ⁻¹' (set.Iic x)) = set.Iic (floor x) :=
+@[simp] lemma preimage_Iic {x : α} : ((coe : ℤ → α) ⁻¹' (set.Iic x)) = set.Iic ⌊x⌋ :=
 by { ext, simp [le_floor] }
 
 end int

src/analysis/special_functions/exp_log.lean

@@ -709,8 +709,8 @@ begin
   refine ⟨N, trivial, λ x hx, _⟩, rw mem_Ioi at hx,
   have hx₀ : 0 < x, from N.cast_nonneg.trans_lt hx,
   rw [mem_Ici, le_div_iff (pow_pos hx₀ _), ← le_div_iff' hC₀],
-  calc x ^ n ≤ (nat_ceil x) ^ n : pow_le_pow_of_le_left hx₀.le (le_nat_ceil _) _
-  ... ≤ exp (nat_ceil x) / (exp 1 * C) : (hN _ (lt_nat_ceil.2 hx).le).le
+  calc x ^ n ≤ ⌈x⌉₊ ^ n : pow_le_pow_of_le_left hx₀.le (le_nat_ceil _) _
+  ... ≤ exp ⌈x⌉₊ / (exp 1 * C) : (hN _ (lt_nat_ceil.2 hx).le).le
   ... ≤ exp (x + 1) / (exp 1 * C) : div_le_div_of_le (mul_pos (exp_pos _) hC₀).le
     (exp_le_exp.2 $ (nat_ceil_lt_add_one hx₀.le).le)
   ... = exp x / C : by rw [add_comm, exp_add, mul_div_mul_left _ _ (exp_pos _).ne']

src/data/real/basic.lean

@@ -366,7 +366,7 @@ begin
     exact ne_of_gt (nat.cast_pos.2 n0) },
   have hg : is_cau_seq abs (λ n, f n / n : ℕ → ℚ),
   { intros ε ε0,
-    suffices : ∀ j k ≥ nat_ceil ε⁻¹, (f j / j - f k / k : ℚ) < ε,
+    suffices : ∀ j k ≥ ⌈ε⁻¹⌉₊, (f j / j - f k / k : ℚ) < ε,
     { refine ⟨_, λ j ij, abs_lt.2 ⟨_, this _ _ ij (le_refl _)⟩⟩,
       rw [neg_lt, neg_sub], exact this _ _ (le_refl _) ij },
     intros j k ij ik,

src/data/real/pi.lean

@@ -301,13 +301,13 @@ begin
       by { rw div_eq_iff (integral_sin_pow_pos (2 * n + 1)).ne',
            convert integral_sin_pow (2 * n + 1), simp with field_simps, norm_cast } },
   refine tendsto_of_tendsto_of_tendsto_of_le_of_le _ _ (λ n, (h₄ n).le) (λ n, (h₃ n)),
-  { refine metric.tendsto_at_top.mpr (λ ε hε, ⟨nat_ceil (1 / ε), λ n hn, _⟩),
+  { refine metric.tendsto_at_top.mpr (λ ε hε, ⟨⌈1 / ε⌉₊, λ n hn, _⟩),
     have h : (2:ℝ) * n / (2 * n + 1) - 1 = -1 / (2 * n + 1),
     { conv_lhs { congr, skip, rw ← @div_self _ _ ((2:ℝ) * n + 1) (by { norm_cast, linarith }), },
       rw [← sub_div, ← sub_sub, sub_self, zero_sub] },
     have hpos : (0:ℝ) < 2 * n + 1, { norm_cast, norm_num },
     rw [dist_eq, h, abs_div, abs_neg, abs_one, abs_of_pos hpos, one_div_lt hpos hε],
-    calc 1 / ε ≤ nat_ceil (1 / ε) : le_nat_ceil _
+    calc 1 / ε ≤ ⌈1 / ε⌉₊ : le_nat_ceil _
           ... ≤ n : by exact_mod_cast hn.le
           ... < 2 * n + 1 : by { norm_cast, linarith } },
   { exact tendsto_const_nhds },

src/measure_theory/borel_space.lean

@@ -1104,7 +1104,7 @@ def finite_spanning_sets_in_Ioo_rat (μ : measure ℝ) [locally_finite_measure 
     calc μ (Ioo _ _) ≤ μ (Icc _ _) : μ.mono Ioo_subset_Icc_self
                  ... < ∞           : is_compact_Icc.finite_measure,
   spanning := Union_eq_univ_iff.2 $ λ x,
-    ⟨nat_floor (abs x), neg_lt.1 ((neg_le_abs_self x).trans_lt (lt_nat_floor_add_one _)),
+    ⟨⌊abs x⌋₊, neg_lt.1 ((neg_le_abs_self x).trans_lt (lt_nat_floor_add_one _)),
       (le_abs_self x).trans_lt (lt_nat_floor_add_one _)⟩ }
 
 lemma measure_ext_Ioo_rat {μ ν : measure ℝ} [locally_finite_measure μ]