transfinite induction

Stream: general

[Kenny Lau]

Just for curiosity, is this a thing in Lean?

[Patrick Massot]

https://gitter.im/leanprover_public/Lobby?at=5a4a3b7a232e79134db2c204

[Sebastien Gouezel]

I would like to make a transfinite induction on a type, with respect to a minimal well-order (for which the initial segments are shorter than the whole type). So, I would need something like the next lemma.

lemma exists_small_well_order (α : Type u) : ∃ (r : rel α α), is_well_order α r ∧ (∀ (x : α),
  #{y // r y x} < #α) := sorry

What we have on ordinals and cardinals contains this and much more, for sure, but I found the API hard to work with, and I could not locate this specific lemma (or a suitable variant). @Mario Carneiro , do you have a hint on where I should look?

[Mario Carneiro]

That is the defining property of ord

[Mario Carneiro]

docs#cardinal.ord

[Mario Carneiro]

especially see docs#cardinal.card_typein_lt

[Sebastien Gouezel]

That's what I am trying to play with, but as far as I can tell these functions don't give me an order on my original type (only on (cardinal.ord (#α)).out.α), so I would need to transport my order through some equiv, but I don't find the lemmas saying that the image of a well-order under an equiv is a well-order.

[Johan Commelin]

@Aaron Anderson has done a lot of thing with well-orders recently. Maybe he can help.

[Mario Carneiro]

The reason for the equality hypothesis in card_typein_lt is exactly so that you can use your original type alpha instead of the out type

[Sebastien Gouezel]

Sure, this lemma is perfect once I know how to construct my well-order on α with the right ordinal type, and this is what I can't see how to do with the current API.

[Mario Carneiro]

docs#ord_eq?

[Sebastien Gouezel]

Thanks!

[Sebastien Gouezel]

I struggled to get this one (this is so much harder to use a part of the library one doesn't know), but in the end it comes out pretty cleanly. Did you know that, assuming the continuum hypothesis, you can find a subset of $\mathbb{R}^2$ which is very large if you see it through vertical lines (i.e., along each vertical line, it misses only a countable set), but it is very small if you see it through horizontal lines (i.e., along each horizontal line, it is countable)? This may seem to contradict Fubini (the set has full measure when integrated in one direction, zero measure in the other direction), but of course it is non-measurable.

import analysis.normed_space.hahn_banach
import set_theory.cardinal_ordinal

universe u
variables {α : Type u}
open set cardinal
open_locale cardinal

lemma countable_iff_lt_aleph_one {α : Type*} (s : set α) : countable s ↔ #s < aleph 1 :=
begin
  have : aleph 1 = (aleph 0).succ, by simp only [← aleph_succ, ordinal.succ_zero],
  rw [countable_iff, ← aleph_zero, this, lt_succ],
end

theorem sierpinski_pathological_family (Hcont : #ℝ = aleph 1) :
  ∃ (f : ℝ → set ℝ), (∀ x, countable (univ \ f x)) ∧ (∀ y, countable {x | y ∈ f x}) :=
begin
  rcases ord_eq ℝ with ⟨r, hr, H⟩,
  resetI,
  refine ⟨λ x, {y | r x y}, λ x, _, _⟩,
  { have : univ \ {y | r x y} = {y | r y x} ∪ {x},
    { ext y,
      simp only [true_and, mem_univ, mem_set_of_eq, mem_insert_iff, union_singleton, mem_diff],
      rcases trichotomous_of r x y with h|rfl|h,
      { simp only [h, not_or_distrib, false_iff, not_true],
        split,
        { rintros rfl, exact irrefl_of r y h },
        { exact asymm h } },
      { simp only [true_or, eq_self_iff_true, iff_true], exact irrefl x },
      { simp only [h, iff_true, or_true], exact asymm h } },
    rw this,
    apply countable.union _ (countable_singleton _),
    rw [countable_iff_lt_aleph_one, ← Hcont],
    exact card_typein_lt r x H },
  { assume y,
    rw [countable_iff_lt_aleph_one, ← Hcont],
    exact card_typein_lt r y H }
end

The part using well-orders can certainly be golfed a lot (why isn't linarith able to close this right away?), but the cardinal API is perfect here.

[David Wärn]

This is a nice example! FWIW, a while ago I thought a little about creating an API for transfinite recursion, to show things like "there's a function $\mathbb R \to \mathbb R$ which is locally surjective", where the end-user wouldn't have to think about recursion. For countable recursion, the Rasiowa-Sikorski lemma provides this sort of API, and I used it in order/countable_dense_linear_order to do the back-and-forth method without mentioning recursion. But the story with general transfinite recursion is a little more complicated. Returning to the local surjection example, you can imagine a partial order P of "states" for the recursion, where an element of P is a partial function R -> R defined on less than continuum many points. Then you have continuum many "desired properties", of the form "some element in (a,b) should map to x". Crucially these are all individually "easy to satisfy", in the sense that they determine dense subsets of P. But you also need to able to take upper bounds of certain chains in P. Here you need to be careful: it's true that a countable chain in P has an upper bound, but it's possible that a chain of size $\kappa < 2^{\aleph_0}$ has no upper bound. One way of rescuing this is to note that P has a sort of 'rank' function, sending a partial function to the cardinality of its domain. Then you can say that each "desired property" can be satisfied without increasing the rank, and you can take upper bounds of chains given some condition on the ranks (and you get some condition on the rank of the upper bound)

[Mario Carneiro]

You don't really need the continuum hypothesis for this, you could just prove it on any set of cardinality aleph 1

[Sebastien Gouezel]

Mario Carneiro said:

You don't really need the continuum hypothesis for this, you could just prove it on any set of cardinality aleph 1

Sure. But the goal is to use this in another proof, and that's the form I need.

[Kevin Buzzard]

Martin's axiom is designed to solve this kind of problem

[Kevin Buzzard]

Unfortunately, it's an axiom as opposed to a theorem