feat(measure_theory): int.floor etc are measurable (#10265)

## API changes

### `algebra/order/archimedean`

* rename `rat.cast_floor` to `rat.floor_cast` to reflect the order of operations;
* same for `rat.cast_ceil` and `rat.cast_round`;
* add `rat.cast_fract`.

### `algebra/order/floor`

* add `@[simp]` to `nat.floor_eq_zero`;
* add `nat.floor_eq_iff'`, `nat.preimage_floor_zero`, and `nat.preimage_floor_of_ne_zero`;
* add `nat.ceil_eq_iff`, `nat.preimage_ceil_zero`, and `nat.preimage_ceil_of_ne_zero`;
* add `int.preimage_floor_singleton`;
* add `int.self_sub_floor`, `int.fract_int_add`, `int.preimage_fract`, `int.image_fract`;
* add `int.preimage_ceil_singleton`.

### `measure_theory/function/floor`

New file. Prove that the functions defined in `algebra.order.floor` are measurable.

src/algebra/continued_fractions/computation/terminates_iff_rat.lean

@@ -166,7 +166,7 @@ namespace int_fract_pair
 
 lemma coe_of_rat_eq :
   ((int_fract_pair.of q).mapFr coe : int_fract_pair K) = int_fract_pair.of v :=
-by simp [int_fract_pair.of, v_eq_q, int.fract]
+by simp [int_fract_pair.of, v_eq_q]
 
 lemma coe_stream_nth_rat_eq :
     ((int_fract_pair.stream q n).map (mapFr coe) : option $ int_fract_pair K)

src/algebra/order/archimedean.lean

@@ -345,15 +345,18 @@ begin
   split; linarith
 end
 
-@[simp, norm_cast] theorem rat.cast_floor (x : ℚ) : ⌊(x:α)⌋ = ⌊x⌋ :=
+@[simp, norm_cast] theorem rat.floor_cast (x : ℚ) : ⌊(x:α)⌋ = ⌊x⌋ :=
 floor_eq_iff.2 (by exact_mod_cast floor_eq_iff.1 (eq.refl ⌊x⌋))
 
-@[simp, norm_cast] theorem rat.cast_ceil (x : ℚ) : ⌈(x:α)⌉ = ⌈x⌉ :=
-by rw [←neg_inj, ←floor_neg, ←floor_neg, ← rat.cast_neg, rat.cast_floor]
+@[simp, norm_cast] theorem rat.ceil_cast (x : ℚ) : ⌈(x:α)⌉ = ⌈x⌉ :=
+by rw [←neg_inj, ←floor_neg, ←floor_neg, ← rat.cast_neg, rat.floor_cast]
 
-@[simp, norm_cast] theorem rat.cast_round (x : ℚ) : round (x:α) = round x :=
+@[simp, norm_cast] theorem rat.round_cast (x : ℚ) : round (x:α) = round x :=
 have ((x + 1 / 2 : ℚ) : α) = x + 1 / 2, by simp,
-by rw [round, round, ← this, rat.cast_floor]
+by rw [round, round, ← this, rat.floor_cast]
+
+@[simp, norm_cast] theorem rat.cast_fract (x : ℚ) : (↑(fract x) : α) = fract x :=
+by { simp only [fract, rat.cast_sub], simp }
 
 end
 

src/algebra/order/floor.lean

@@ -46,6 +46,7 @@ many lemmas.
 rounding, floor, ceil
 -/
 
+open set
 variables {α : Type*}
 
 /-! ### Floor semiring -/
@@ -130,19 +131,29 @@ lemma pos_of_floor_pos (h : 0 < ⌊a⌋₊) : 0 < a :=
 lemma lt_of_lt_floor (h : n < ⌊a⌋₊) : ↑n < a :=
 (nat.cast_lt.2 h).trans_le $ floor_le (pos_of_floor_pos $ (nat.zero_le n).trans_lt h).le
 
-lemma floor_eq_zero : ⌊a⌋₊ = 0 ↔ a < 1 :=
+@[simp] lemma floor_eq_zero : ⌊a⌋₊ = 0 ↔ a < 1 :=
 by { rw [←lt_one_iff, ←@cast_one α], exact floor_lt' nat.one_ne_zero }
 
 lemma floor_eq_iff (ha : 0 ≤ a) : ⌊a⌋₊ = n ↔ ↑n ≤ a ∧ a < ↑n + 1 :=
 by rw [←le_floor_iff ha, ←nat.cast_one, ←nat.cast_add, ←floor_lt ha, nat.lt_add_one_iff,
   le_antisymm_iff, and.comm]
 
+lemma floor_eq_iff' (hn : n ≠ 0) : ⌊a⌋₊ = n ↔ ↑n ≤ a ∧ a < ↑n + 1 :=
+by rw [← le_floor_iff' hn, ← nat.cast_one, ← nat.cast_add, ← floor_lt' (nat.add_one_ne_zero n),
+  nat.lt_add_one_iff, le_antisymm_iff, and.comm]
+
 lemma floor_eq_on_Ico (n : ℕ) : ∀ a ∈ (set.Ico n (n+1) : set α), ⌊a⌋₊ = n :=
 λ a ⟨h₀, h₁⟩, (floor_eq_iff $ n.cast_nonneg.trans h₀).mpr ⟨h₀, h₁⟩
 
 lemma floor_eq_on_Ico' (n : ℕ) : ∀ a ∈ (set.Ico n (n+1) : set α), (⌊a⌋₊ : α) = n :=
 λ x hx, by exact_mod_cast floor_eq_on_Ico n x hx
 
+@[simp] lemma preimage_floor_zero : (floor : α → ℕ) ⁻¹' {0} = Iio 1 :=
+ext $ λ a, floor_eq_zero
+
+lemma preimage_floor_of_ne_zero {n : ℕ} (hn : n ≠ 0) : (floor : α → ℕ) ⁻¹' {n} = Ico n (n + 1) :=
+ext $ λ a, floor_eq_iff' hn
+
 /-! #### Ceil -/
 
 lemma gc_ceil_coe : galois_connection (ceil : α → ℕ) coe := floor_semiring.gc_ceil
@@ -173,6 +184,17 @@ begin
   { rwa [floor_of_nonpos ha.le, lt_ceil] }
 end
 
+lemma ceil_eq_iff (hn : n ≠ 0) : ⌈a⌉₊ = n ↔ ↑(n - 1) < a ∧ a ≤ n :=
+by rw [← ceil_le, ← not_le, ← ceil_le, not_le,
+  tsub_lt_iff_right (nat.add_one_le_iff.2 (pos_iff_ne_zero.2 hn)), nat.lt_add_one_iff,
+  le_antisymm_iff, and.comm]
+
+@[simp] lemma preimage_ceil_zero : (nat.ceil : α → ℕ) ⁻¹' {0} = Iic 0 :=
+ext $ λ x, ceil_eq_zero
+
+lemma preimage_ceil_of_ne_zero (hn : n ≠ 0) : (nat.ceil : α → ℕ) ⁻¹' {n} = Ioc ↑(n - 1) n :=
+ext $ λ x, ceil_eq_iff hn
+
 end linear_ordered_semiring
 
 section linear_ordered_ring
@@ -358,15 +380,25 @@ lemma floor_eq_on_Ico (n : ℤ) : ∀ a ∈ set.Ico (n : α) (n + 1), ⌊a⌋ =
 lemma floor_eq_on_Ico' (n : ℤ) : ∀ a ∈ set.Ico (n : α) (n + 1), (⌊a⌋ : α) = n :=
 λ a ha, congr_arg _ $ floor_eq_on_Ico n a ha
 
+@[simp] lemma preimage_floor_singleton (m : ℤ) : (floor : α → ℤ) ⁻¹' {m} = Ico m (m + 1) :=
+ext $ λ x, floor_eq_iff
+
 /-! #### Fractional part -/
 
+@[simp] lemma self_sub_floor (a : α) : a - ⌊a⌋ = fract a := rfl
+
 @[simp] lemma floor_add_fract (a : α) : (⌊a⌋ : α) + fract a = a := add_sub_cancel'_right _ _
 
 @[simp] lemma fract_add_floor (a : α) : fract a + ⌊a⌋ = a := sub_add_cancel _ _
 
-@[simp] lemma fract_add_int (a : α) (m : ℤ) : fract (a + m) = fract a := by simp [fract]
+@[simp] lemma fract_add_int (a : α) (m : ℤ) : fract (a + m) = fract a :=
+by { rw fract, simp }
 
-@[simp] lemma fract_sub_int (a : α) (m : ℤ) : fract (a - m) = fract a := by simp [fract]
+@[simp] lemma fract_sub_int (a : α) (m : ℤ) : fract (a - m) = fract a :=
+by { rw fract, simp }
+
+@[simp] lemma fract_int_add (m : ℤ) (a : α) : fract (↑m + a) = fract a :=
+by rw [add_comm, fract_add_int]
 
 @[simp] lemma self_sub_fract (a : α) : a - fract a = ⌊a⌋ := sub_sub_cancel _ _
 
@@ -427,6 +459,27 @@ begin
   abel
 end
 
+lemma preimage_fract (s : set α) : fract ⁻¹' s = ⋃ m : ℤ, (λ x, x - m) ⁻¹' (s ∩ Ico (0 : α) 1) :=
+begin
+  ext x,
+  simp only [mem_preimage, mem_Union, mem_inter_eq],
+  refine ⟨λ h, ⟨⌊x⌋, h, fract_nonneg x, fract_lt_one x⟩, _⟩,
+  rintro ⟨m, hms, hm0, hm1⟩,
+  obtain rfl : ⌊x⌋ = m, from floor_eq_iff.2 ⟨sub_nonneg.1 hm0, sub_lt_iff_lt_add'.1 hm1⟩,
+  exact hms
+end
+
+lemma image_fract (s : set α) : fract '' s = ⋃ m : ℤ, (λ x, x - m) '' s ∩ Ico 0 1 :=
+begin
+  ext x,
+  simp only [mem_image, mem_inter_eq, mem_Union], split,
+  { rintro ⟨y, hy, rfl⟩,
+    exact ⟨⌊y⌋, ⟨y, hy, rfl⟩, fract_nonneg y, fract_lt_one y⟩ },
+  { rintro ⟨m, ⟨y, hys, rfl⟩, h0, h1⟩,
+    obtain rfl : ⌊y⌋ = m, from floor_eq_iff.2 ⟨sub_nonneg.1 h0, sub_lt_iff_lt_add'.1 h1⟩,
+    exact ⟨y, hys, rfl⟩ }
+end
+
 /-! #### Ceil -/
 
 lemma gc_ceil_coe : galois_connection ceil (coe : ℤ → α) := floor_ring.gc_ceil_coe
@@ -486,6 +539,9 @@ lemma ceil_eq_on_Ioc' (z : ℤ) : ∀ a ∈ set.Ioc (z - 1 : α) z, (⌈a⌉ : 
 lemma floor_lt_ceil_of_lt {a b : α} (h : a < b) : ⌊a⌋ < ⌈b⌉ :=
 cast_lt.1 $ (floor_le a).trans_lt $ h.trans_le $ le_ceil b
 
+@[simp] lemma preimage_ceil_singleton (m : ℤ) : (ceil : α → ℤ) ⁻¹' {m} = Ioc (m - 1) m :=
+ext $ λ x, ceil_eq_iff
+
 /-! #### A floor ring as a floor semiring -/
 
 @[priority 100] -- see Note [lower instance priority]

src/measure_theory/function/floor.lean

@@ -0,0 +1,78 @@
+/-
+Copyright (c) 2021 Yury G. Kudryashov. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yury G. Kudryashov
+-/
+import measure_theory.constructions.borel_space
+
+/-!
+# Measurability of `⌊x⌋` etc
+
+In this file we prove that `int.floor`, `int.ceil`, `int.fract`, `nat.floor`, and `nat.ceil` are
+measurable under some assumptions on the (semi)ring.
+-/
+
+open set
+
+section floor_ring
+
+variables {α R : Type*} [measurable_space α] [linear_ordered_ring R] [floor_ring R]
+  [topological_space R] [order_topology R] [measurable_space R]
+
+lemma int.measurable_floor [opens_measurable_space R] :
+  measurable (int.floor : R → ℤ) :=
+measurable_to_encodable $ λ x, by simpa only [int.preimage_floor_singleton]
+  using measurable_set_Ico
+
+@[measurability] lemma measurable.floor [opens_measurable_space R]
+  {f : α → R} (hf : measurable f) : measurable (λ x, ⌊f x⌋) :=
+int.measurable_floor.comp hf
+
+lemma int.measurable_ceil [opens_measurable_space R] :
+  measurable (int.ceil : R → ℤ) :=
+measurable_to_encodable $ λ x,
+  by simpa only [int.preimage_ceil_singleton] using measurable_set_Ioc
+
+@[measurability] lemma measurable.ceil [opens_measurable_space R]
+  {f : α → R} (hf : measurable f) : measurable (λ x, ⌈f x⌉) :=
+int.measurable_ceil.comp hf
+
+lemma measurable_fract [borel_space R] : measurable (int.fract : R → R) :=
+begin
+  intros s hs,
+  rw int.preimage_fract,
+  exact measurable_set.Union (λ z, measurable_id.sub_const _ (hs.inter measurable_set_Ico))
+end
+
+@[measurability] lemma measurable.fract [borel_space R]
+  {f : α → R} (hf : measurable f) : measurable (λ x, int.fract (f x)) :=
+measurable_fract.comp hf
+
+lemma measurable_set.image_fract [borel_space R] {s : set R} (hs : measurable_set s) :
+  measurable_set (int.fract '' s) :=
+begin
+  simp only [int.image_fract, sub_eq_add_neg, image_add_right'],
+  exact measurable_set.Union (λ m, (measurable_add_const _ hs).inter measurable_set_Ico)
+end
+
+end floor_ring
+
+section floor_semiring
+
+variables {α R : Type*} [measurable_space α] [linear_ordered_semiring R] [floor_semiring R]
+  [topological_space R] [order_topology R] [measurable_space R] [opens_measurable_space R]
+  {f : α → R}
+
+lemma nat.measurable_floor : measurable (nat.floor : R → ℕ) :=
+measurable_to_encodable $ λ n, by cases eq_or_ne ⌊n⌋₊ 0; simp [*, nat.preimage_floor_of_ne_zero]
+
+@[measurability] lemma measurable.nat_floor (hf : measurable f) : measurable (λ x, ⌊f x⌋₊) :=
+nat.measurable_floor.comp hf
+
+lemma nat.measurable_ceil : measurable (nat.ceil : R → ℕ) :=
+measurable_to_encodable $ λ n, by cases eq_or_ne ⌈n⌉₊ 0; simp [*, nat.preimage_ceil_of_ne_zero]
+
+@[measurability] lemma measurable.nat_ceil (hf : measurable f) : measurable (λ x, ⌈f x⌉₊) :=
+nat.measurable_ceil.comp hf
+
+end floor_semiring

src/number_theory/zsqrtd/gaussian_int.lean

@@ -118,12 +118,12 @@ lemma div_def (x y : ℤ[i]) : x / y = ⟨round ((x * conj y).re / norm y : ℚ)
 show zsqrtd.mk _ _ = _, by simp [rat.of_int_eq_mk, rat.mk_eq_div, div_eq_mul_inv]
 
 lemma to_complex_div_re (x y : ℤ[i]) : ((x / y : ℤ[i]) : ℂ).re = round ((x / y : ℂ).re) :=
-by rw [div_def, ← @rat.cast_round ℝ _ _];
-  simp [-rat.cast_round, mul_assoc, div_eq_mul_inv, mul_add, add_mul]
+by rw [div_def, ← @rat.round_cast ℝ _ _];
+  simp [-rat.round_cast, mul_assoc, div_eq_mul_inv, mul_add, add_mul]
 
 lemma to_complex_div_im (x y : ℤ[i]) : ((x / y : ℤ[i]) : ℂ).im = round ((x / y : ℂ).im) :=
-by rw [div_def, ← @rat.cast_round ℝ _ _, ← @rat.cast_round ℝ _ _];
-  simp [-rat.cast_round, mul_assoc, div_eq_mul_inv, mul_add, add_mul]
+by rw [div_def, ← @rat.round_cast ℝ _ _, ← @rat.round_cast ℝ _ _];
+  simp [-rat.round_cast, mul_assoc, div_eq_mul_inv, mul_add, add_mul]
 
 lemma norm_sq_le_norm_sq_of_re_le_of_im_le {x y : ℂ} (hre : |x.re| ≤ |y.re|)
   (him : |x.im| ≤ |y.im|) : x.norm_sq ≤ y.norm_sq :=