Unmeasurable set (incomplete).

unmeasurable.lean

import data.real.basic data.real.cardinality data.set.disjointed
-- https://gist.github.com/pedrominicz/f03f3b5b405a08e2ba2c30529d5c2337
import .quotient_group_cardinality

-- https://www.youtube.com/watch?v=llnNaRzuvd4

open_locale big_operators

--def upper (f : ℕ → ennreal) : set ennreal :=
--  {a | ∀ n, ∑ (i : fin n), f i ≤ a}

def upper (f : ℕ → ennreal) : set ennreal :=
  {a | ∀ n : ℕ, ∑ i in finset.range n, f i ≤ a}

def limit (f : ℕ → ennreal) (l : ennreal) : Prop :=
  l ∈ upper f ∧ ∀ a ∈ upper f, l ≤ a

class is_measure (μ : set ℝ → ennreal) :=
(measure_Icc (a b : ℝ) : μ (set.Icc a b) = ennreal.of_real (abs (a - b)))
(measure_shift (a : ℝ) (s : set ℝ) : μ {r | r + a ∈ s} = μ s)
(measure_Union {f : ℕ → set ℝ} {a : ennreal} :
  pairwise (disjoint on f) → (limit (μ ∘ f) a ↔ μ (⋃i, f i) = a))

open is_measure

def Q : set ℝ := λ r, ∃ k : ℚ, ↑k = r

instance : is_add_subgroup Q :=
{ zero_mem := ⟨0, by push_cast; linarith⟩,
  add_mem := λ _ _ ⟨a, _⟩ ⟨b, _⟩, ⟨a + b, by push_cast; linarith⟩,
  neg_mem := λ _ ⟨a, _⟩, ⟨-a, by push_cast; linarith⟩ }

def RQ : Type := quotient_add_group.quotient Q
notation `ℝ/ℚ` := RQ

def RQ.mk : ℝ → ℝ/ℚ := quotient_add_group.mk

instance : has_coe ℝ ℝ/ℚ := ⟨RQ.mk⟩

namespace cardinal

noncomputable def aux (q : ℚ) : Q := ⟨↑q, ⟨q, rfl⟩⟩

lemma aux_injective : function.injective aux := λ _ _, by simp [aux]

lemma aux_surjective : function.surjective aux := λ ⟨_, _, rfl⟩, ⟨_, rfl⟩

lemma mk_rat_eq_mk_Q : mk ℚ = mk Q :=
begin
  apply le_antisymm,
  { exact mk_le_of_injective aux_injective },
  { exact mk_le_of_surjective aux_surjective }
end

lemma mk_real_eq_mk_RQ : mk ℝ = mk ℝ/ℚ :=
begin
  apply mk_quotient_add_group,
  { rw mk_real, apply le_of_lt, apply cantor },
  { rw [←mk_rat_eq_mk_Q, mk_rat, mk_real], apply cantor }
end

lemma mk_RQ : mk ℝ/ℚ = 2 ^ omega.{0} := by rw [←mk_real_eq_mk_RQ, mk_real]

lemma not_countable_RQ : ¬ set.countable (set.univ : set ℝ/ℚ) :=
begin
  rw [countable_iff, mk_univ, mk_RQ],
  exact (and_not_self _).mp ∘ lt_of_lt_of_le (cantor _)
end

end cardinal

def omega : set ℝ := {r | ∃ r' : ℝ/ℚ, r = fract (quot.out r')}
notation `Ω` := omega

lemma fract_eq_RQ (r : ℝ) : ((fract r : ℝ) : ℝ/ℚ) = r :=
quot.sound ⟨⌊r⌋, by simp [fract]; ring⟩

example (q : ℚ) (r : ℝ) : (r : ℝ/ℚ) = ↑(r + q) :=
quot.sound ⟨q, by linarith⟩

lemma eq_of_real_add_rat_eq_fract {q : ℚ} {r : ℝ} {a : ℝ/ℚ} (h : r + q = fract a.out') :
  a = r :=
begin
  rw ←a.out_eq',
  apply quot.sound,
  unfold fract at h,
  exact ⟨-q - ↑⌊a.out'⌋, by push_cast; linarith⟩
end

def omega_add (a : ℚ) : set ℝ := {r | r + a ∈ Ω}
prefix `Ω+`:max := omega_add

lemma pairwise_disjoint_on_omega_add_aux (a b : ℚ) : Ω+a = Ω+b ∨ disjoint Ω+a Ω+b :=
begin
  by_cases h : a = b,
  { left, rw h },
  { right,
    rintros x ⟨⟨a', ha⟩, ⟨b', hb⟩⟩,
    apply h, clear h,
    have h : (a : ℝ) - b = fract (quot.out a') - fract (quot.out b'), by linarith,
    have ha := eq_of_real_add_rat_eq_fract ha,
    have hb := eq_of_real_add_rat_eq_fract hb,
    rw [ha, hb, sub_self, sub_eq_zero] at h,
    exact rat.cast_inj.mp h }
end

#check function.injective

def r : ℝ → ℝ → Prop := @setoid.r _ (quotient_add_group.left_rel Q)
local infix ` ~ ` := r

lemma rel_of_fract_rel_fract {a b : ℝ} (h : fract a ~ fract b) : a ~ b :=
begin
  cases h with q h,
  unfold fract at h,
  exact ⟨q + ⌊b⌋ - ⌊a⌋, by push_cast; linarith⟩
end

lemma rel_of_eq {a b : ℝ} (h : a = b) : a ~ b :=
⟨0, by push_cast; linarith⟩

lemma rel_of_add_rat_rel {a b : ℝ} {q : ℚ} : a + q ~ b → a ~ b :=
λ ⟨q', _⟩, ⟨q + q', by push_cast; linarith⟩

lemma rel_symm {a b : ℝ} : a ~ b → b ~ a :=
λ ⟨q, _⟩, ⟨-q, by push_cast; linarith⟩

lemma pairwise_disjoint_on_omega_add :
  pairwise (disjoint on omega_add) :=
begin
  intros i j hij,
  cases pairwise_disjoint_on_omega_add_aux i j with h h, swap, exact h,
  exfalso, apply hij,
  rw set.ext_iff at h,
  let r : ℝ := fract (quot.out (RQ.mk 0)),
  specialize h (r - i),
  cases h with h,
  have : r ∈ Ω := ⟨(0 : ℝ), rfl⟩,
  have : r - i ∈ Ω+i, by simpa [omega_add],
  cases h this with x hx,
  cases this with y h,
  suffices : y = x,
  { rw [this, ←hx, add_right_inj] at h,
    norm_cast at h },
  have : @setoid.r _ (quotient_add_group.left_rel Q) (quot.out y) (quot.out x),
  { have : r = fract (quot.out x) - j + i, by linarith,
    have : fract (quot.out x) + ↑(- j + i) = fract (quot.out y),
    { push_cast, linarith },
    exact rel_symm (rel_of_fract_rel_fract (rel_of_add_rat_rel (rel_of_eq this))), },
  have := quotient.sound' this,
  unfold quotient.mk' at this,
  rwa [←quot.out_eq x, ←quot.out_eq y]
end

lemma ennreal.le_add : ∀ a b : ennreal, a ≤ a + b :=
begin
  rintros ⟨_ | a⟩ ⟨_ | _⟩ ⟨_, _⟩ h; try { simpa },
  use a,
  simp only [option.mem_def, ennreal.some_eq_coe] at h,
  norm_cast at h,
  simp [h.symm]
end

section

parameters {μ : set ℝ → ennreal} [is_measure μ] {s t : set ℝ}

lemma measure_omega_eq_measure_omega_add {a : ℚ} : μ Ω = μ Ω+a :=
by simp [omega_add, @measure_shift μ (by apply_instance) a Ω]

lemma limit_eq_zero_iff {f : ℕ → ennreal}: limit f 0 ↔ ∀ n, f n = 0 :=
begin
  split; intro h,
  { suffices : ∀ n x, x < n → f x = 0,
    { intro n,
      exact this (n + 1) n (lt_add_one n) },
    simp [limit, upper] at h, exact h },
  { suffices : ∀ n x, x < n → f x = 0,
      simpa [limit, upper],
    intros _ _ _, apply h }
end

@[simp] def const_set (s : set ℝ) (n : ℕ) : set ℝ :=
  if 0 = n then s else ∅

lemma pairwise_disjoint_on_const_set (s : set ℝ) :
  pairwise (disjoint on const_set s) :=
begin
  rintros ⟨_ | _⟩ ⟨_ | _⟩ h;
    change disjoint _ _;
    rw disjoint_iff,
  { exfalso, apply h, refl },
  { ext, simp only [if_true, const_set, eq_self_iff_true],
    rw if_neg, swap, exact h,
    change _ ∧ false ↔ false, cc },
  { ext, simp only [if_true, const_set, eq_self_iff_true],
    rw if_neg, swap, exact h.symm,
    change false ∧ _ ↔ false, cc },
  { ext, simp only [const_set],
    rw if_neg, swap, exact of_to_bool_ff rfl,
    change false ∧ _ ↔ false, cc }
end

lemma ennreal.eq_zero_of_add_finite_le {a b : ennreal} (hb : b < ⊤) (h : a + b ≤ b) :
  a = 0 :=
begin
  cases b, exfalso, simp at hb, exact hb, clear hb,
  cases a, exfalso, simp at h, exact h,
  simp only [ennreal.coe_eq_zero, ennreal.some_eq_coe] at *,
  cases a with a ha, cases b with b hb,
  norm_cast at h,
  have : a + b ≤ b, from h,
  congr, linarith
end

lemma measure_empty_eq_zero : μ ∅ = 0 :=
begin
  let s : set ℝ := set.Icc 0 1,
  have hs : μ s = 1, from (measure_Icc 0 1).trans (by simp),
  have : s = ⋃i, const_set s i,
  { ext, rw set.mem_Union, split,
    { rintro ⟨h₁, h₂⟩, use 0, simp [h₁, h₂] },
    { rintro ⟨_ | _, hi⟩,
      { exact hi },
      { exfalso, exact hi } } },
  rw [this, ←measure_Union (pairwise_disjoint_on_const_set s)] at hs,
  swap, apply_instance,
  simp only [limit, upper, function.comp_app, set.mem_set_of_eq] at hs,
  cases hs with h,
  specialize h 2,
  rw finset.sum_range_succ at h,
  simp [show μ s = 1, from (measure_Icc 0 1).trans (by simp)] at h,
  exact ennreal.eq_zero_of_add_finite_le ennreal.coe_lt_top h
end

def f (n : ℕ) : set ℝ :=
  if 0 = n then s else if 1 = n then t \ s else ∅

lemma f_eq_empty : ∀ n ≥ 2, f n = ∅ :=
λ _ _, by simp only [f]; rw [if_neg, if_neg]; linarith

lemma pairwise_disjoint_on_f : pairwise (disjoint on f) :=
begin
  intros i j h,
  change disjoint _ _,
  rw disjoint_iff,
  simp only [f],
  rcases i with _|_|_,
  { rw if_pos, swap, refl,
    rw if_neg, swap, exact h,
    split_ifs; ext,
    { change _ ∧ _ ∧ _ ↔ false, tauto },
    { change _ ∧ false ↔ false, tauto } },
  { rw if_neg, swap, exact zero_ne_one,
    rw if_pos, swap, refl,
    split_ifs; ext,
    { change (_ ∧ _) ∧ _ ↔ false, tauto },
    { change _ ∧ false ↔ false, tauto } },
  { rw if_neg, swap, exact of_to_bool_ff rfl,
    rw if_neg, swap, exact of_to_bool_ff rfl,
    ext, change false ∧ _ ↔ false, tauto }
end

lemma eq_Union_f (hst : s ⊆ t) : t = ⋃i, f i :=
begin
  ext,
  simp only [f, set.mem_Union],
  split,
  { intro ht,
    classical, by_cases hs : x ∈ s,
    { use 0, simpa },
    { use 1, simp, tauto } },
  { rintro ⟨_|_|_, h⟩,
    { rw if_pos at h, swap, refl,
      exact hst h },
    { rw if_neg at h, swap, exact zero_ne_one,
      rw if_pos at h, swap, refl,
      exact h.1 },
    { rw if_neg at h, swap, exact of_to_bool_ff rfl,
      rw if_neg at h, swap, exact of_to_bool_ff rfl,
      exfalso, exact h } }
end

lemma measure_f_eq_zero {n : ℕ} (h : 2 ≤ n) : μ (f n) = 0 :=
begin
  rcases n with _|_|_, linarith, linarith,
  simp only [f],
  rw [if_neg, if_neg, measure_empty_eq_zero]; exact of_to_bool_ff rfl
end

noncomputable def g (n : ℕ) : ennreal :=
  if 0 = n then 0 else if 1 = n then μ (f 0) else μ (f 0) + μ (f 1)

lemma g_eq_limit {n : ℕ} (h : 2 ≤ n) : g n = μ (f 0) + μ (f 1) :=
begin
  rcases n with _|_|_, linarith, linarith,
  simp only [g],
  rw [if_neg, if_neg]; exact of_to_bool_ff rfl
end

lemma limit_measure_f : limit (μ ∘ f) (μ (f 0) + μ (f 1)) :=
begin
  split,
  { intros n a ha,
    change _ = _ at ha,
    cases h₀ : μ (f 0) with b₀; rw h₀ at ha, simp at ha, exfalso, exact ha,
    cases h₁ : μ (f 1) with b₁; rw h₁ at ha, simp at ha, exfalso, exact ha,
    rcases n with _|_|_,
    { exact ⟨0, by simp⟩ },
    { exact ⟨b₀, by simp [h₀, (option.some_inj.mp ha).symm]⟩, },
    { use a,
      split, swap, refl,
      simp only [option.mem_def],
      have : some a = g n.succ.succ,
      { simp only [g],
        rw [if_neg, if_neg, ←ha, ←h₀, ←h₁]; exact of_to_bool_ff rfl },
      rw this,
      apply finset.sum_range_induction, simp [g],
      intro n, rcases n with _|_|n, simp [g],
      { simp only [g], rw [if_neg, if_neg, if_neg, if_pos]; linarith },
      { rw [g_eq_limit, g_eq_limit, @measure_f_eq_zero n.succ.succ, add_zero];
        exact inf_eq_left.mp rfl } } },
  { intros a h,
    specialize h 2,
    have : finset.range 2 = {0, 1}, by refl,
    simp [this] at h, exact h }
end

lemma measure_le_measure (hst : s ⊆ t) : μ s ≤ μ t :=
begin
  have := (measure_Union pairwise_disjoint_on_f).mp limit_measure_f,
  rw [eq_Union_f hst, this],
  simp only [f],
  rw if_pos, swap, refl,
  rw if_neg, swap, exact zero_ne_one,
  rw if_pos, swap, refl,
  apply ennreal.le_add
end

end

section

parameters {μ : set ℝ → ennreal} [is_measure μ]

lemma omega_subset_unit_interval : Ω ⊆ set.Icc 0 1 :=
begin
  rintros _ ⟨r, rfl⟩, split,
  { exact fract_nonneg (quot.out r) },
  { exact le_of_lt (fract_lt_one (quot.out r)) }
end

lemma measure_omega_le_measure_unit_interval : μ Ω ≤ μ (set.Icc 0 1) :=
begin
  apply measure_le_measure,
  apply omega_subset_unit_interval
end

def s : set ℝ := ⋃q : set.Icc (-1 : ℚ) 1, Ω+q

lemma measure_s_le_three : μ s ≤ 3 :=
begin
  have : μ (set.Icc (-1) 2) = 3,
  { have h := (@measure_Icc μ (by apply_instance) (-1) 2),
    norm_num at h,
    have : (3 : ℝ) > 0, by linarith,
    have : abs (3 : ℝ) = 3, from abs_of_pos this,
    rw this at h,
    have : ennreal.of_real 3 = 3,
    { simp only [ennreal.of_real, nnreal.of_real],
      norm_num, refl },
    rwa this at h },
  rw ←this,
  apply measure_le_measure,
  rintros x h,
  simp [s, omega_add] at h,
  rcases h with ⟨q, ⟨hq₁, hq₂⟩, h⟩,
  cases omega_subset_unit_interval h with h₁ h₂,
  split,
  { rw ←zero_add (-1 : ℝ),
    apply add_le_of_le_sub_right,
    rw sub_neg_eq_add,
    transitivity, exact h₁,
    rw add_le_add_iff_left,
    norm_cast,
    exact hq₂ },
  { rw ←le_sub_iff_add_le at h₂,
    transitivity, exact h₂,
    suffices : -(q : ℝ) ≤ 2 - 1,
    { linarith },
    norm_num, norm_cast,
    rw ←neg_neg (1 : ℚ),
    exact neg_le_neg hq₁ }
end

example : μ Ω = 0 :=
sorry

end