quasi-borel-spaces/QuasiBorelSpaces/Nat.lean at main · YellPika/quasi-borel-spaces · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
import QuasiBorelSpaces.Prod
import QuasiBorelSpaces.Prop

namespace QuasiBorelSpace.Nat

example : DiscreteQuasiBorelSpace ℕ := inferInstance

variable
  {A : Type*} [QuasiBorelSpace A]
  {B : Type*} [QuasiBorelSpace B]
  {C : Type*} [QuasiBorelSpace C]

@[fun_prop]
lemma isHom_rec
    {f : A → B} (hf : IsHom f)
    {g : A → ℕ → B → B} (hg : IsHom fun (x, y, z) ↦ g x y z)
    {h : A → ℕ} (hh : IsHom h)
    : IsHom (fun x ↦ (Nat.rec (f x) (g x) (h x) : B)) := by
  apply isHom_cases (ix := h) (f := fun n x ↦ (Nat.rec (f x) (g x) n : B))
  · exact hh
  · intro n
    induction n with
    | zero =>
      simp only [Nat.rec_zero]
      fun_prop
    | succ n ih =>
      simp only
      fun_prop

@[simp, local fun_prop]
lemma isHom_lt : IsHom (fun x : ℕ × ℕ ↦ x.1 < x.2) := by
  simp only [isHom_of_discrete_countable]

@[fun_prop]
lemma isHom_lt'
    {f : A → ℕ} (hf : IsHom f)
    {g : A → ℕ} (hg : IsHom g)
    : IsHom (fun x ↦ f x < g x) := by
  fun_prop

@[simp, local fun_prop]
lemma isHom_add : IsHom (fun x : ℕ × ℕ ↦ x.1 + x.2) := by
  simp only [isHom_of_discrete_countable]

@[fun_prop]
lemma isHom_add'
    {f : A → ℕ} (hf : IsHom f)
    {g : A → ℕ} (hg : IsHom g)
    : IsHom (fun x ↦ f x + g x) := by
  fun_prop

@[fun_prop]
lemma isHom_find
    {p : A → ℕ → Prop}
    [∀ x, DecidablePred (p x)]
    {q : ∀ x, ∃ n, p x n}
    (hp : ∀ n, IsHom (p · n))
    : IsHom fun x ↦ Nat.find (q x) := by
  rw [isHom_def,]
  intro φ hφ
  simp only [isHom_ofMeasurableSpace]
  intro X hX
  have : (fun r ↦ Nat.find (q (φ r))) ⁻¹' X
       = {r | ∃n ∈ X, p (φ r) n ∧ ∀{m}, m < n → ¬p (φ r) m} := by
    ext r
    simp only [Set.mem_preimage, Set.mem_setOf_eq]
    apply Iff.intro
    · intro h
      use Nat.find (q (φ r))
      use h
      use Nat.find_spec (q (φ r))
      use Nat.find_min (q (φ r))
    · rintro ⟨n, hn₁, hn₂, hn₃⟩
      suffices Nat.find (q (φ r)) = n by simp_all only [MeasurableSpace.measurableSet_top]
      rw [Nat.find_eq_iff]
      grind
  rw [this, measurableSet_setOf, ←isHom_iff_measurable]
  apply Prop.isHom_exists fun n ↦ Prop.isHom_and ?_ (Prop.isHom_and ?_ ?_)
  · simp only [isHom_const']
  · fun_prop
  · apply Prop.isHom_forall fun m ↦ ?_
    apply Prop.isHom_forall fun hmn ↦ ?_
    fun_prop

end QuasiBorelSpace.Nat

namespace QuasiBorelSpace.Fin

@[simps!]
instance {n} : QuasiBorelSpace (Fin n) := ofMeasurableSpace

example {n} : DiscreteQuasiBorelSpace (Fin n) := inferInstance

end QuasiBorelSpace.Fin