Lemma 5.5.1, for real (#122)

Carleson/Discrete/Defs.lean

@@ -21,6 +21,16 @@ def 𝓒 (k : ℕ) : Set (Grid X) :=
 /-- The definition `𝔓(k)` given in (5.1.3). -/
 def TilesAt (k : ℕ) : Set (𝔓 X) := 𝓘 ⁻¹' 𝓒 k
 
+lemma disjoint_TilesAt_of_ne {m n : ℕ} (h : m ≠ n) : Disjoint (TilesAt (X := X) m) (TilesAt n) := by
+  wlog hl : m < n generalizing m n; · exact (this h.symm (by omega)).symm
+  by_contra! h; rw [not_disjoint_iff] at h; obtain ⟨p, mp₁, mp₂⟩ := h
+  simp_rw [TilesAt, mem_preimage, 𝓒, mem_diff, aux𝓒, mem_setOf] at mp₁ mp₂
+  apply absurd _ mp₂.2; obtain ⟨j, lj, vj⟩ := mp₁.1; use j, lj; apply lt_of_le_of_lt _ vj
+  exact mul_le_mul_right' (ENNReal.zpow_le_of_le one_le_two (by omega)) _
+
+lemma pairwiseDisjoint_TilesAt : univ.PairwiseDisjoint (TilesAt (X := X)) := fun _ _ _ _ ↦
+  disjoint_TilesAt_of_ne
+
 def aux𝔐 (k n : ℕ) : Set (𝔓 X) :=
   {p ∈ TilesAt k | 2 ^ (-n : ℤ) * volume (𝓘 p : Set X) < volume (E₁ p) }
 
@@ -46,6 +56,21 @@ def ℭ (k n : ℕ) : Set (𝔓 X) :=
 lemma ℭ_subset_TilesAt {k n : ℕ} : ℭ k n ⊆ TilesAt (X := X) k := fun t mt ↦ by
   rw [ℭ, mem_setOf] at mt; exact mt.1
 
+lemma disjoint_ℭ_of_ne {k m n : ℕ} (h : m ≠ n) : Disjoint (ℭ (X := X) k m) (ℭ k n) := by
+  wlog hl : m < n generalizing m n; · exact (this h.symm (by omega)).symm
+  by_contra! h; rw [not_disjoint_iff] at h; obtain ⟨p, mp₁, mp₂⟩ := h
+  apply absurd _ (not_disjoint_iff.mpr ⟨_, mp₁.2, mp₂.2⟩)
+  rw [Ioc_disjoint_Ioc, le_max_iff]; left; rw [min_le_iff]; right
+  exact ENNReal.zpow_le_of_le one_le_two (by omega)
+
+lemma pairwiseDisjoint_ℭ :
+    (univ : Set (ℕ × ℕ)).PairwiseDisjoint (fun kn ↦ ℭ (X := X) kn.1 kn.2) :=
+  fun ⟨k₁, n₁⟩ _ ⟨k₂, n₂⟩ _ hn ↦ by
+    change Disjoint (ℭ k₁ n₁) (ℭ k₂ n₂)
+    by_cases hk : k₁ = k₂
+    · rw [ne_eq, Prod.mk.injEq, not_and] at hn; exact hk ▸ disjoint_ℭ_of_ne (hn hk)
+    · exact disjoint_of_subset ℭ_subset_TilesAt ℭ_subset_TilesAt (disjoint_TilesAt_of_ne hk)
+
 /-- The subset `𝔅(p)` of `𝔐(k, n)`, given in (5.1.8). -/
 def 𝔅 (k n : ℕ) (p : 𝔓 X) : Set (𝔓 X) :=
   { m ∈ 𝔐 k n | smul 100 p ≤ smul 1 m }
@@ -61,6 +86,16 @@ def ℭ₁ (k n j : ℕ) : Set (𝔓 X) :=
 lemma ℭ₁_subset_ℭ {k n j : ℕ} : ℭ₁ k n j ⊆ ℭ (X := X) k n := fun t mt ↦ by
   rw [ℭ₁, preℭ₁, mem_diff, mem_setOf] at mt; exact mt.1.1
 
+lemma disjoint_ℭ₁_of_ne {k n j l : ℕ} (h : j ≠ l) : Disjoint (ℭ₁ (X := X) k n j) (ℭ₁ k n l) := by
+  wlog hl : j < l generalizing j l; · exact (this h.symm (by omega)).symm
+  by_contra! h; rw [not_disjoint_iff] at h; obtain ⟨p, mp₁, mp₂⟩ := h
+  simp_rw [ℭ₁, mem_diff, preℭ₁, mem_setOf, mp₁.1.1, true_and, not_le] at mp₁ mp₂
+  have := mp₂.1.trans_lt mp₁.2
+  rw [pow_lt_pow_iff_right one_lt_two] at this; omega
+
+lemma pairwiseDisjoint_ℭ₁ {k n : ℕ} : univ.PairwiseDisjoint (ℭ₁ (X := X) k n) := fun _ _ _ _ ↦
+  disjoint_ℭ₁_of_ne
+
 lemma card_𝔅_of_mem_ℭ₁ {k n j : ℕ} {p : 𝔓 X} (hp : p ∈ ℭ₁ k n j) :
     (𝔅 k n p).toFinset.card ∈ Ico (2 ^ j) (2 ^ (j + 1)) := by
   simp_rw [ℭ₁, mem_diff, preℭ₁, mem_setOf, hp.1.1, true_and, not_le] at hp
@@ -130,6 +165,8 @@ is at most the least upper bound of `𝓛 n u` in `Grid X`. -/
 def 𝔏₄ (k n j : ℕ) : Set (𝔓 X) :=
   { p ∈ ℭ₄ k n j | ∃ u ∈ 𝔘₁ k n j, (𝓘 p : Set X) ⊆ ⋃ (i ∈ 𝓛 (X := X) n u), i }
 
+lemma 𝔏₄_subset_ℭ₄ {k n j : ℕ} : 𝔏₄ k n j ⊆ ℭ₄ (X := X) k n j := fun _ mu ↦ mu.1
+
 /-- The subset `ℭ₅(k, n, j)` of `ℭ₄(k, n, j)`, given in (5.1.23). -/
 def ℭ₅ (k n j : ℕ) : Set (𝔓 X) :=
   ℭ₄ k n j \ 𝔏₄ k n j
@@ -142,6 +179,37 @@ lemma ℭ₅_def {k n j : ℕ} {p : 𝔓 X} :
 lemma ℭ₅_subset_ℭ₄ {k n j : ℕ} : ℭ₅ k n j ⊆ ℭ₄ (X := X) k n j := fun t mt ↦ by
   rw [ℭ₅, mem_diff] at mt; exact mt.1
 
+-- These inclusion and disjointness lemmas are only used in `antichain_decomposition`
+section AntichainDecomp
+
+variable {k n j l : ℕ}
+
+lemma 𝔏₀_subset_ℭ : 𝔏₀ (X := X) k n ⊆ ℭ k n := fun _ mu ↦ mu.1
+lemma 𝔏₀_disjoint_ℭ₁ : Disjoint (𝔏₀ (X := X) k n) (ℭ₁ k n j) := by
+  by_contra h; rw [not_disjoint_iff] at h; obtain ⟨p, ⟨_, b0⟩, ⟨⟨_, bp⟩ , _⟩⟩ := h
+  simp [filter_mem_univ_eq_toFinset, b0] at bp
+
+lemma 𝔏₁_subset_ℭ₁ : 𝔏₁ (X := X) k n j l ⊆ ℭ₁ k n j := minLayer_subset
+lemma 𝔏₁_subset_ℭ : 𝔏₁ (X := X) k n j l ⊆ ℭ k n := minLayer_subset.trans ℭ₁_subset_ℭ
+
+lemma 𝔏₂_subset_ℭ₁ : 𝔏₂ k n j ⊆ ℭ₁ (X := X) k n j := 𝔏₂_subset_ℭ₂.trans ℭ₂_subset_ℭ₁
+lemma 𝔏₂_subset_ℭ : 𝔏₂ k n j ⊆ ℭ (X := X) k n := 𝔏₂_subset_ℭ₁.trans ℭ₁_subset_ℭ
+lemma 𝔏₂_disjoint_ℭ₃ : Disjoint (𝔏₂ (X := X) k n j) (ℭ₃ k n j) := disjoint_sdiff_right
+
+lemma 𝔏₃_subset_ℭ₁ : 𝔏₃ k n j l ⊆ ℭ₁ (X := X) k n j :=
+  maxLayer_subset.trans ℭ₃_subset_ℭ₂ |>.trans ℭ₂_subset_ℭ₁
+lemma 𝔏₃_subset_ℭ : 𝔏₃ k n j l ⊆ ℭ (X := X) k n := 𝔏₃_subset_ℭ₁.trans ℭ₁_subset_ℭ
+
+lemma 𝔏₄_subset_ℭ₁ : 𝔏₄ k n j ⊆ ℭ₁ (X := X) k n j :=
+  𝔏₄_subset_ℭ₄.trans ℭ₄_subset_ℭ₃ |>.trans ℭ₃_subset_ℭ₂ |>.trans ℭ₂_subset_ℭ₁
+lemma 𝔏₄_subset_ℭ : 𝔏₄ k n j ⊆ ℭ (X := X) k n := 𝔏₄_subset_ℭ₁.trans ℭ₁_subset_ℭ
+
+lemma ℭ₅_subset_ℭ₁ : ℭ₅ k n j ⊆ ℭ₁ (X := X) k n j :=
+  ℭ₅_subset_ℭ₄.trans ℭ₄_subset_ℭ₃ |>.trans ℭ₃_subset_ℭ₂ |>.trans ℭ₂_subset_ℭ₁
+lemma ℭ₅_subset_ℭ : ℭ₅ k n j ⊆ ℭ (X := X) k n := ℭ₅_subset_ℭ₁.trans ℭ₁_subset_ℭ
+
+end AntichainDecomp
+
 /-- The set $\mathcal{P}_{F,G}$, defined in (5.1.24). -/
 def highDensityTiles : Set (𝔓 X) :=
   { p : 𝔓 X | 2 ^ (2 * a + 5) * volume F / volume G < dens₂ {p} }

Carleson/Discrete/Forests.lean

@@ -143,9 +143,7 @@ def ℭ₆ (k n j : ℕ) : Set (𝔓 X) :=
   { p ∈ ℭ₅ k n j | ¬ (𝓘 p : Set X) ⊆ G' }
 
 lemma ℭ₆_subset_ℭ₅ : ℭ₆ (X := X) k n j ⊆ ℭ₅ k n j := sep_subset ..
-lemma ℭ₆_subset_ℭ : ℭ₆ (X := X) k n j ⊆ ℭ k n :=
-  ℭ₆_subset_ℭ₅ |>.trans ℭ₅_subset_ℭ₄ |>.trans ℭ₄_subset_ℭ₃ |>.trans ℭ₃_subset_ℭ₂ |>.trans
-    ℭ₂_subset_ℭ₁ |>.trans ℭ₁_subset_ℭ
+lemma ℭ₆_subset_ℭ : ℭ₆ (X := X) k n j ⊆ ℭ k n := ℭ₆_subset_ℭ₅.trans ℭ₅_subset_ℭ
 
 /-- The subset `𝔗₁(u)` of `ℭ₁(k, n, j)`, given in (5.4.1).
 In lemmas, we will assume `u ∈ 𝔘₁ k n l` -/
@@ -775,35 +773,83 @@ def ℜ₂ : Set (𝔓 X) := 𝔓pos ∩ ⋃ (n : ℕ) (k ≤ n) (j ≤ 2 * n +
 /-- The union occurring in the statement of Lemma 5.5.1 containing 𝔏₃ -/
 def ℜ₃ : Set (𝔓 X) := 𝔓pos ∩ ⋃ (n : ℕ) (k ≤ n) (j ≤ 2 * n + 3) (l ≤ Z * (n + 1)), 𝔏₃ k n j l
 
+/-- Lemma allowing to peel `⋃ (n : ℕ) (k ≤ n)` from unions in the proof of Lemma 5.5.1. -/
+lemma mem_iUnion_iff_mem_of_mem_ℭ {f : ℕ → ℕ → Set (𝔓 X)} (hp : p ∈ ℭ k n ∧ k ≤ n)
+    (hf : ∀ k n, f k n ⊆ ℭ k n) : p ∈ ⋃ (n : ℕ) (k ≤ n), f k n ↔ p ∈ f k n := by
+  simp_rw [mem_iUnion]; constructor <;> intro h
+  · obtain ⟨n', k', _, mp⟩ := h
+    have e := pairwiseDisjoint_ℭ (X := X).elim (mem_univ (k, n)) (mem_univ (k', n'))
+      (not_disjoint_iff.mpr ⟨p, hp.1, hf k' n' mp⟩)
+    rw [Prod.mk.inj_iff] at e
+    exact e.1 ▸ e.2 ▸ mp
+  · use n, k, hp.2
+
+/-- Lemma allowing to peel `⋃ (j ≤ 2 * n + 3)` from unions in the proof of Lemma 5.5.1. -/
+lemma mem_iUnion_iff_mem_of_mem_ℭ₁ {f : ℕ → Set (𝔓 X)} (hp : p ∈ ℭ₁ k n j ∧ j ≤ 2 * n + 3)
+    (hf : ∀ j, f j ⊆ ℭ₁ k n j) : p ∈ ⋃ (j ≤ 2 * n + 3), f j ↔ p ∈ f j := by
+  simp_rw [mem_iUnion]; constructor <;> intro h
+  · obtain ⟨j', _, mp⟩ := h
+    have e := pairwiseDisjoint_ℭ₁ (X := X).elim (mem_univ j) (mem_univ j')
+      (not_disjoint_iff.mpr ⟨p, hp.1, hf j' mp⟩)
+    exact e ▸ mp
+  · use j, hp.2
+
 /-- Lemma 5.5.1 -/
-lemma antichain_decomposition : 𝔓pos (X := X) ∩ 𝔓₁ᶜ ⊆ ℜ₀ ∪ ℜ₁ ∪ ℜ₂ ∪ ℜ₃ := by
-  unfold ℜ₀ ℜ₁ ℜ₂ ℜ₃; simp_rw [← inter_union_distrib_left]; intro p ⟨h, mp'⟩
-  refine ⟨h, ?_⟩; simp_rw [mem_union, mem_iUnion, or_assoc]
+lemma antichain_decomposition : 𝔓pos (X := X) ∩ 𝔓₁ᶜ = ℜ₀ ∪ ℜ₁ ∪ ℜ₂ ∪ ℜ₃ := by
+  unfold ℜ₀ ℜ₁ ℜ₂ ℜ₃ 𝔓₁; simp_rw [← inter_union_distrib_left]; ext p
+  simp_rw [mem_inter_iff, and_congr_right_iff, mem_compl_iff, mem_union]; intro h
+  obtain ⟨k, n, hkn, split⟩ := exists_k_n_j_of_mem_𝔓pos h
+  have pc : p ∈ ℭ k n := by
+    rcases split with ml0 | ⟨_, _, mc1⟩
+    · exact 𝔏₀_subset_ℭ ml0
+    · exact ℭ₁_subset_ℭ mc1
+  iterate 5 rw [mem_iUnion_iff_mem_of_mem_ℭ ⟨pc, hkn⟩]
+  pick_goal 5; · exact fun _ _ ↦ 𝔏₀_subset_ℭ
+  pick_goal 4; · exact fun _ _ ↦ iUnion₂_subset fun _ _ ↦ iUnion₂_subset fun _ _ ↦ 𝔏₁_subset_ℭ
+  pick_goal 3; · exact fun _ _ ↦ iUnion₂_subset fun _ _ ↦ 𝔏₂_subset_ℭ
+  pick_goal 2; · exact fun _ _ ↦ iUnion₂_subset fun _ _ ↦ iUnion₂_subset fun _ _ ↦ 𝔏₃_subset_ℭ
+  pick_goal -1; · exact fun _ _ ↦ iUnion₂_subset fun _ _ ↦ ℭ₅_subset_ℭ
+  by_cases ml0 : p ∈ 𝔏₀ k n
+  · simp_rw [ml0, true_or, iff_true, mem_iUnion₂]; push_neg; intros
+    exact fun a ↦ disjoint_left.mp 𝔏₀_disjoint_ℭ₁ ml0 (ℭ₅_subset_ℭ₁ a)
+  simp_rw [ml0, false_or] at split ⊢
+  obtain ⟨j, hj, mc1⟩ := split
+  iterate 4 rw [mem_iUnion_iff_mem_of_mem_ℭ₁ ⟨mc1, hj⟩]
+  pick_goal 4; · exact fun _ ↦ iUnion₂_subset fun _ _ ↦ 𝔏₁_subset_ℭ₁
+  pick_goal 3; · exact fun _ ↦ 𝔏₂_subset_ℭ₁
+  pick_goal 2; · exact fun _ ↦ iUnion₂_subset fun _ _ ↦ 𝔏₃_subset_ℭ₁
+  pick_goal -1; · exact fun _ ↦ ℭ₅_subset_ℭ₁
+  by_cases mc2 : p ∉ ℭ₂ k n j
+  all_goals
+    have mc2' := mc2
+    simp_rw [ℭ₂, layersAbove, mem_diff, not_and, mc1, true_implies, not_not_mem] at mc2'
+  · change p ∈ ⋃ (l ≤ Z * (n + 1)), 𝔏₁ k n j l at mc2'
+    simp_rw [mc2', true_or, iff_true]; contrapose! mc2
+    exact ℭ₅_subset_ℭ₄.trans ℭ₄_subset_ℭ₃ |>.trans ℭ₃_subset_ℭ₂ mc2
+  change p ∉ ⋃ (l ≤ Z * (n + 1)), 𝔏₁ k n j l at mc2'; simp_rw [mc2', false_or]
+  rw [not_not_mem] at mc2; by_cases ml2 : p ∈ 𝔏₂ k n j
+  · simp_rw [ml2, true_or, iff_true]
+    exact fun a ↦ disjoint_left.mp 𝔏₂_disjoint_ℭ₃ ml2 (ℭ₅_subset_ℭ₄.trans ℭ₄_subset_ℭ₃ a)
+  simp_rw [ml2, false_or]
+  have mc3 : p ∈ ℭ₃ k n j := ⟨mc2, ml2⟩
+  by_cases mc4 : p ∉ ℭ₄ k n j
+  all_goals
+    have mc4' := mc4
+    simp_rw [ℭ₄, layersBelow, mem_diff, not_and, mc3, true_implies, not_not_mem] at mc4'
+  · change p ∈ ⋃ (l ≤ Z * (n + 1)), 𝔏₃ k n j l at mc4'
+    simp_rw [mc4', iff_true]; contrapose! mc4
+    exact ℭ₅_subset_ℭ₄ mc4
+  change p ∉ ⋃ (l ≤ Z * (n + 1)), 𝔏₃ k n j l at mc4'
+  simp_rw [mc4', iff_false, ℭ₅]; rw [not_not_mem] at mc4 ⊢; simp_rw [mem_diff, mc4, true_and]
   have nG₃ : ¬(𝓘 p : Set X) ⊆ G₃ := by
     suffices ¬(𝓘 p : Set X) ⊆ G' by contrapose! this; exact subset_union_of_subset_right this _
     by_contra hv
     rw [𝔓pos, mem_setOf, inter_comm _ G'ᶜ, ← inter_assoc, ← diff_eq_compl_inter,
       diff_eq_empty.mpr hv] at h
     simp at h
-  obtain ⟨k, n, hkn, mp⟩ := exists_k_n_j_of_mem_𝔓pos h
-  rcases mp with ml0 | ⟨j, hj, mc1⟩
-  · exact Or.inl ⟨n, k, hkn, ml0⟩
-  · right; by_cases mc2 : p ∉ ℭ₂ k n j
-    · simp_rw [ℭ₂, layersAbove, mem_diff, not_and, mc1, true_implies, not_not_mem] at mc2
-      simp_rw [mem_iUnion] at mc2; obtain ⟨l, hl, f⟩ := mc2
-      exact Or.inl ⟨n, k, hkn, j, hj, l, hl, f⟩
-    · right; rw [not_not_mem] at mc2; by_cases ml2 : p ∈ 𝔏₂ k n j
-      · exact Or.inl ⟨n, k, hkn, j, hj, ml2⟩
-      · have mc3 : p ∈ ℭ₃ k n j := ⟨mc2, ml2⟩
-        right; by_cases mc4 : p ∉ ℭ₄ k n j
-        · simp_rw [ℭ₄, layersBelow, mem_diff, not_and, mc3, true_implies, not_not_mem] at mc4
-          simp_rw [mem_iUnion] at mc4; obtain ⟨l, hl, f⟩ := mc4
-          exact ⟨n, k, hkn, j, hj, l, hl, f⟩
-        · apply absurd mp'; simp_rw [mem_compl_iff, not_not_mem, 𝔓₁, mem_iUnion]
-          refine ⟨n, k, hkn, j, hj, not_not_mem.mp mc4, ?_⟩
-          contrapose! nG₃
-          exact le_iSup₂_of_le n k <| le_iSup₂_of_le hkn j <| le_iSup₂_of_le hj p <|
-            le_iSup_of_le nG₃ subset_rfl
+  contrapose! nG₃
+  exact le_iSup₂_of_le n k <| le_iSup₂_of_le hkn j <|
+    le_iSup₂_of_le hj p <| le_iSup_of_le nG₃ subset_rfl
 
 /-- The subset `𝔏₀(k, n, l)` of `𝔏₀(k, n)`, given in Lemma 5.5.3.
   We use the name `𝔏₀'` in Lean. The indexing is off-by-one w.r.t. the blueprint -/

blueprint/src/chapter/main.tex

@@ -3073,7 +3073,7 @@ \section{Proof of the Forest Complement Lemma}
     \begin{align}
         \label{eq-fp'-decomposition}
         &\quad \fP_2 \cap \fP_{G \setminus G'}\\
-        &\subset \bigcup_{k \ge 0} \bigcup_{n \ge k} \fL_0(k,n) \cap \fP_{G \setminus G'} \\
+        &= \bigcup_{k \ge 0} \bigcup_{n \ge k} \fL_0(k,n) \cap \fP_{G \setminus G'} \\
         &\quad\cup \bigcup_{k \ge 0} \bigcup_{n \ge k}\bigcup_{0 \le j \le 2n+3} \fL_2(k,n,j) \cap \fP_{G \setminus G'}\\
         &\quad\cup \bigcup_{k \ge 0} \bigcup_{n \ge k}\bigcup_{0 \le j \le 2n+3} \bigcup_{0 \le l \le Z(n+1)} \fL_1(k,n,j,l) \cap \fP_{G \setminus G'}\\
         &\quad\cup \bigcup_{k \ge 0} \bigcup_{n \ge k}\bigcup_{0 \le j \le 2n+3} \bigcup_{0 \le l \le Z(n+1)} \fL_3(k,n,j,l)\cap \fP_{G \setminus G'}\,.
@@ -3086,7 +3086,7 @@ \section{Proof of the Forest Complement Lemma}
 
     Next, since $E_2(\lambda, \fp') \subset \scI(\fp')\cap G$ for every $\lambda \ge 2$ and every tile $\fp' \in \fP(k)$ with $\lambda\fp \lesssim \lambda \fp'$, it follows from \eqref{muhj2} that $\mu(E_2(\lambda, \fp')) \le 2^{-k} \mu(\scI(\fp'))$ for every such $\fp'$, so $\dens_k'(\{\fp\}) \le 2^{-k}$. Combining this with $a \ge 0$, it follows from \eqref{def-cnk} that there exists $n\ge k$ with $\fp \in \fC(k,n)$.
 
-    Since $\fp \in \fP_{G \setminus G'}$, we have in particular $\scI(\fp) \not \subset A(2n + 6, k, n)$, so there exist at most $1 + (4n + 12)2^n < 2^{2n+4}$ tiles $\mathfrak{m} \in \mathfrak{M}(k,n)$ with $\fp \le \mathfrak{m}$. It follows that $\fp \in \fL_0(k,n)$ or $\fp \in \fC_1(k,n,j)$ for some $1 \le j \le 2n + 3$. In the former case we are done, in the latter case the inclusion to be shown follows immediately from the definitions of the collections $\fC_i$ and $\fL_i$.
+    Since $\fp \in \fP_{G \setminus G'}$, we have in particular $\scI(\fp) \not \subset A(2n + 6, k, n)$, so there exist at most $1 + (4n + 12)2^n < 2^{2n+4}$ tiles $\mathfrak{m} \in \mathfrak{M}(k,n)$ with $\fp \le \mathfrak{m}$. It follows that $\fp \in \fL_0(k,n)$ or $\fp \in \fC_1(k,n,j)$ for some $1 \le j \le 2n + 3$. In the former case we are done, in the latter case the equality to be shown follows from the definitions of the collections $\fC_i$ and $\fL_i$.
 \end{proof}
 
 \begin{lemma}[L0 antichain]