New planet Cartan to introduce Filter

[WenrongZou]

Description of planet design:

• Level 01: Introduce filters as generalized points. The three filter axioms are only mentioned:

  1. the whole set is large: Set.univ ∈ f;
  2. any superset of a large set is large: if s ∈ f and s ⊆ t, then t ∈ f;
  3. the intersection of two large sets is large: if s ∈ f and t ∈ f, then s ∩ t ∈ f.

  The main example is the neighborhood filter 𝓝 a, and the exercise verifies the third axiom for it:

  Statement {a : ℝ} {s t : Set ℝ} (hs : s ∈ 𝓝 a) (ht : t ∈ 𝓝 a) : s ∩ t ∈ 𝓝 a

• Level 02: Characterize membership in 𝓝 a for open sets, introducing IsOpen:

  Statement : Ioo (-1) 1 ∈ 𝓝 0

• Level 03: Introduce Filter.atTop as the generalized point "at infinity": its members are the sets containing every sufficiently large number. Prove that the open ray beyond b is a neighborhood of +∞, using Filter.mem_atTop and the second axiom:

  Statement {b : ℝ} : {x : ℝ | b < x} ∈ atTop

• Level 04: Introduce the principal filter 𝓟 and the order on filters (Filter.le_def, reverse of set inclusion), and prove principal_singleton_le_nhds : 𝓟 {a} ≤ 𝓝 a.

• Level 05: Introduce 𝓝[>] a (defined as 𝓝 a ⊓ 𝓟 (Set.Ioi a)) together with the intervals Set.Ioo/Set.Iio/Set.Ioi, and prove Set.Ioo (0 : ℝ) 1 ∈ 𝓝[>] (0 : ℝ) via Filter.mem_inf_iff_superset.

• Level 06: Introduce Filter.Eventually. Goal: {a : ℝ} (hab : a < 0) : ∀ᶠ x in 𝓝 a, x < 0.

• Level 07: Introduce EventuallyEq and tactic filter_upwards. Goal:

  Statement {f g : ℝ → ℝ} {a : ℝ} (ha : a < 0) (h : ∀ x < 0, f x = g x) :
      f =ᶠ[𝓝 a] g

• Level 08: An exercise about EventuallyEq and filter_upwards, using IsOpen.eventually_mem:

  Statement {f g : ℝ → ℝ} {a b c : ℝ} (ha : a ∈ Ioo b c)
      (h : ∀ x ∈ Ioo b c, f x = g x) : f =ᶠ[𝓝 a] g

• Levels 09–11: Three levels about the eventual behavior of 1/x along different filters, showing how the same predicate behaves at different generalized points:

  • Level 09: ∀ᶠ x in 𝓝[>] (0 : ℝ), 1/x > 5 — from the right of 0, 1/x is eventually large.
  • Level 10: ¬ (∀ᶠ x in 𝓝[≠] (0 : ℝ), 1/x > 5) — but not on the punctured neighborhood, since every punctured neighborhood of 0 contains negative numbers.
  • Level 11: ∀ᶠ x in atTop, 1/x < 1/5 — at infinity, 1/x is eventually small.

• Level 12: Transitivity of EventuallyEq, using filter_upwards. (This step will be used in the Boss level.)

• Level 13: Introduce IsLocallyConstant and prove the theorem IsLocallyConstant.eventually_eq, namely

  Statement IsLocallyConstant.eventually_eq {f : ℝ → ℝ} {x : ℝ}
      (hf : IsLocallyConstant f) : ∀ᶠ y in 𝓝 x, f y = f x

• Level 14: (Boss Level) Two locally constant functions that agree at a point agree in a neighbourhood of that point.

[TentativeConvert]

I'm not particularly happy with the proof I provided here. Two alternatives below. Note that you again have infima of suprema showing up in the infoview after the first step, in both of these proofs. In the second step, the second proof uses a more specialized theorem, than the first, but it's shorter and uses filter_upwards. So I would tend towards the second alternative.

  rw [nhdsWithin]
  rw [eventually_inf]
  let s := Set.Ioo (-1:ℝ) (1/5)
  have hs : s ∈ 𝓝 0 := by 
    rw [IsOpen.mem_nhds_iff,]
    simp_log [s]
    apply isOpen_Ioo
  let I := Ioi (0 : ℝ)
  have hI : I ∈ 𝓟 (Ioi 0):= by 
    simp_log [I]
  use s, hs, I, hI
  intro x hx
  have : 0 < x ∧ x < 1/5 := by grind
  simp_log
  rw [lt_inv_comm₀]
  grind
  grind
  grind

  rw [nhdsWithin]
  rw [eventually_inf_principal]
  have hx :  ∀ᶠ (x : ℝ) in 𝓝 0, x < 1 / 5 := by
    apply eventually_lt_nhds
    grind
  filter_upwards [hx]
  intro a h₁ h₂
  simp_log
  rw [lt_inv_comm₀]
  grind
  grind
  grind

[WenrongZou]

This is one reason for me to introduce infimum. When user unfold nhdsWithin, they will come across infimum. Previously, I think if we want introduce infimum, we should also supremum, because of symmetry. So I add two levels to do this in the early version.

[WenrongZou]

I think we should try to avoid unfolding nhdsWithin. We already have some theorems in mathlib to transform the goals contained nhdsWithin (see above example). Then it is unnecessary to introduce infimum of filter.

[TentativeConvert]

… continuing from comment above: So this is really the only explanation I'd put in this level. (Scribble will say: "Yes, you could show this from first principals, but actually it’s quicker if you realise this is a filter, and everybody knows it's a filter, so you can quote one of the filter axioms instead". Don't write this here – this kind of text will go in the translation files. I just want to convey what I imagine the game to look like in the end.