From ae2a7e77ca46df6c288de521e2f5681d164a083d Mon Sep 17 00:00:00 2001 From: Jeremy Tan Jie Rui Date: Sat, 13 Jul 2024 02:56:44 +0800 Subject: [PATCH] Convexity lemmas (5.3.5 to 5.3.12) (#71) --- Carleson/DiscreteCarleson.lean | 129 +++++++++++++++++++++++++++++---- blueprint/src/chapter/main.tex | 32 ++++++-- 2 files changed, 141 insertions(+), 20 deletions(-) diff --git a/Carleson/DiscreteCarleson.lean b/Carleson/DiscreteCarleson.lean index 0f97b244..adc2a4d1 100644 --- a/Carleson/DiscreteCarleson.lean +++ b/Carleson/DiscreteCarleson.lean @@ -33,14 +33,20 @@ def 𝔐 (k n : β„•) : Set (𝔓 X) := maximals (·≀·) (aux𝔐 k n) def dens' (k : β„•) (P' : Set (𝔓 X)) : ℝβ‰₯0∞ := ⨆ p' ∈ P', ⨆ (l : ℝβ‰₯0), ⨆ (_hl : 2 ≀ l), ⨆ (p : 𝔓 X) (_h1p : p ∈ TilesAt k) (_h2p : smul l p' ≀ smul l p), - l ^ (- (a : β„€)) * volume (Eβ‚‚ l p) / volume (π“˜ p : Set X) + l ^ (-a : β„€) * volume (Eβ‚‚ l p) / volume (π“˜ p : Set X) + +lemma dens'_iSup {k : β„•} {P : Set (𝔓 X)} : dens' k P = ⨆ p ∈ P, dens' k {p} := by + simp_rw [dens', mem_singleton_iff, iSup_iSup_eq_left] def auxβ„­ (k n : β„•) : Set (𝔓 X) := { p ∈ TilesAt k | 2 ^ (4 * a - n) < dens' k {p} } /-- The partition `β„­(k, n)` of `𝔓(k)` by density, given in (5.1.7). -/ def β„­ (k n : β„•) : Set (𝔓 X) := - { p ∈ TilesAt k | dens' k {p} ∈ Ioc (2 ^ (4 * a - n)) (2 ^ (4 * a - (n + 1))) } + { p ∈ TilesAt k | dens' k {p} ∈ Ioc (2 ^ (4 * a - n)) (2 ^ (4 * a - n + 1)) } + +lemma β„­_subset_TilesAt {k n : β„•} : β„­ k n βŠ† TilesAt (X := X) k := fun t mt ↦ by + rw [β„­, mem_setOf] at mt; exact mt.1 /-- The subset `𝔅(p)` of `𝔐(k, n)`, given in (5.1.8). -/ def 𝔅 (k n : β„•) (p : 𝔓 X) : Set (𝔓 X) := @@ -54,6 +60,9 @@ Together with `𝔏₀(k, n)` this forms a partition. -/ def ℭ₁ (k n j : β„•) : Set (𝔓 X) := preℭ₁ k n j \ preℭ₁ k n (j + 1) +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 + /-- The subset `𝔏₀(k, n, j)` of `β„­(k, n)`, given in (5.1.10). -/ def 𝔏₀ (k n : β„•) : Set (𝔓 X) := { p ∈ β„­ k n | 𝔅 k n p = βˆ… } @@ -69,6 +78,9 @@ otherwise we need to add an upper bound. -/ def β„­β‚‚ (k n j : β„•) : Set (𝔓 X) := ℭ₁ k n j \ ⋃ (l ≀ Z * (n + 1)), 𝔏₁ k n j l +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 + /-- The subset `π”˜β‚(k, n, j)` of `ℭ₁(k, n, j)`, given in (5.1.14). -/ def π”˜β‚ (k n j : β„•) : Set (𝔓 X) := { u ∈ ℭ₁ k n j | βˆ€ p ∈ ℭ₁ k n j, π“˜ u < π“˜ p β†’ Disjoint (ball_(u) (𝒬 u) 100) (ball_(p) (𝒬 p) 100) } @@ -81,6 +93,9 @@ def 𝔏₂ (k n j : β„•) : Set (𝔓 X) := def ℭ₃ (k n j : β„•) : Set (𝔓 X) := β„­β‚‚ k n j \ 𝔏₂ k n j +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 + /-- `𝔏₃(k, n, j, l)` consists of the maximal elements in `ℭ₃(k, n, j)` not in `𝔏₃(k, n, j, l')` for some `l' < l`. Defined near (5.1.17). -/ def 𝔏₃ (k n j l : β„•) : Set (𝔓 X) := @@ -92,6 +107,9 @@ otherwise we need to add an upper bound. -/ def β„­β‚„ (k n j : β„•) : Set (𝔓 X) := ℭ₃ k n j \ ⋃ (l : β„•), 𝔏₃ k n j l +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 + /-- The subset `𝓛(u)` of `Grid X`, given near (5.1.20). Note: It seems to also depend on `n`. -/ def 𝓛 (n : β„•) (u : 𝔓 X) : Set (Grid X) := @@ -107,6 +125,9 @@ def 𝔏₄ (k n j : β„•) : Set (𝔓 X) := def β„­β‚… (k n j : β„•) : Set (𝔓 X) := β„­β‚„ k n j \ 𝔏₄ k n j +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 + /-- 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} } @@ -406,7 +427,7 @@ def secondExceptionSupportEquiv : simp only [Subtype.mk.injEq]; omega /-- Lemma 5.2.6 -/ -lemma second_exception : volume (Gβ‚‚ (X := X)) ≀ 2 ^ (-4 : β„€) * volume G := by +lemma second_exception : volume (Gβ‚‚ (X := X)) ≀ 2 ^ (-4 : β„€) * volume G := calc _ ≀ βˆ‘' (n : β„•), volume (⋃ (k < n), setA (X := X) (2 * n + 6) k n) := measure_iUnion_le _ _ = βˆ‘' (n : β„•), volume (⋃ (k : β„•), if k < n then setA (X := X) (2 * n + 6) k n else βˆ…) := by @@ -459,7 +480,7 @@ def C5_2_9 [ProofData a q K σ₁ Οƒβ‚‚ F G] (n : β„•) : ℝβ‰₯0 := D ^ (1 - ΞΊ /-- Lemma 5.2.9 -/ lemma boundary_exception {u : 𝔓 X} (hu : u ∈ π”˜β‚ k n l) : - volume (⋃ i ∈ 𝓛 (X := X) n u, (i : Set X)) ≀ C5_2_9 X n * volume (π“˜ u : Set X) := by + volume (⋃ i ∈ 𝓛 (X := X) n u, (i : Set X)) ≀ C5_2_9 X n * volume (π“˜ u : Set X) := by sorry /-- Lemma 5.2.10 -/ @@ -486,36 +507,114 @@ lemma ordConnected_tilesAt : OrdConnected (TilesAt k : Set (𝔓 X)) := by /-- Lemma 5.3.5 -/ lemma ordConnected_C : OrdConnected (β„­ k n : Set (𝔓 X)) := by - sorry + rw [ordConnected_def]; intro p mp p'' mp'' p' mp' + rw [β„­, mem_setOf] at mp mp'' ⊒ + have z := mem_of_mem_of_subset mp' (ordConnected_tilesAt.out mp.1 mp''.1) + refine ⟨z, ?_⟩ + have : βˆ€ q' ∈ TilesAt (X := X) k, βˆ€ q ≀ q', dens' k {q'} ≀ dens' k {q} := fun q' _ q hq ↦ by + simp_rw [dens', mem_singleton_iff, iSup_iSup_eq_left]; gcongr with l hl a _ + exact iSup_const_mono fun h ↦ + wiggle_order_11_10 hq (C5_3_3_le (X := X).trans (by norm_num) |>.trans hl) |>.trans h + exact ⟨mp''.2.1.trans_le (this _ mp''.1 _ mp'.2), (this _ z _ mp'.1).trans mp.2.2⟩ /-- Lemma 5.3.6 -/ lemma ordConnected_C1 : OrdConnected (ℭ₁ k n j : Set (𝔓 X)) := by - sorry + rw [ordConnected_def]; intro p mp p'' mp'' p' mp' + have mp'₁ : p' ∈ β„­ (X := X) k n := mem_of_mem_of_subset mp' + (ordConnected_C.out (mem_of_mem_of_subset mp ℭ₁_subset_β„­) + (mem_of_mem_of_subset mp'' ℭ₁_subset_β„­)) + simp_rw [ℭ₁, mem_diff, preℭ₁, mem_setOf, not_and, not_le] at mp mp'' ⊒ + simp_rw [mp.1.1, true_and, true_implies] at mp + simp_rw [mp'₁, true_and, true_implies] + simp_rw [mp''.1.1, true_and, true_implies] at mp'' + constructor + Β· refine mp''.1.trans (Finset.card_le_card fun b mb ↦ ?_) + simp_rw [Finset.mem_filter, Finset.mem_univ, true_and, 𝔅, mem_setOf] at mb ⊒ + have := wiggle_order_11_10 (n := 100) mp'.2 (C5_3_3_le (X := X).trans (by norm_num)) + exact ⟨mb.1, this.trans mb.2⟩ + Β· refine (Finset.card_le_card fun b mb ↦ ?_).trans_lt mp.2 + simp_rw [Finset.mem_filter, Finset.mem_univ, true_and, 𝔅, mem_setOf] at mb ⊒ + have := wiggle_order_11_10 (n := 100) mp'.1 (C5_3_3_le (X := X).trans (by norm_num)) + exact ⟨mb.1, this.trans mb.2⟩ /-- Lemma 5.3.7 -/ lemma ordConnected_C2 : OrdConnected (β„­β‚‚ k n j : Set (𝔓 X)) := by - sorry + rw [ordConnected_def]; intro p mp p'' mp'' p' mp' + have mp₁ := mem_of_mem_of_subset mp β„­β‚‚_subset_ℭ₁ + have mp'₁ : p' ∈ ℭ₁ (X := X) k n j := mem_of_mem_of_subset mp' + (ordConnected_C1.out mp₁ (mem_of_mem_of_subset mp'' β„­β‚‚_subset_ℭ₁)) + by_cases e : p = p'; Β· rwa [e] at mp + simp_rw [β„­β‚‚, mem_diff, mp'₁, true_and] + by_contra h; rw [mem_iUnionβ‚‚] at h; obtain ⟨l', bl', p'm⟩ := h + rw [𝔏₁, mem_minimals_iff] at p'm + have pnm : p βˆ‰ ⋃ l'', ⋃ (_ : l'' < l'), 𝔏₁ k n j l'' := by + replace mp := mp.2; contrapose! mp + exact mem_of_mem_of_subset mp + (iUnion_mono'' fun i ↦ iUnion_subset_iUnion_const fun hi ↦ (hi.trans_le bl').le) + exact absurd (p'm.2 ⟨mp.1, pnm⟩ mp'.1).symm e /-- Lemma 5.3.8 -/ lemma ordConnected_C3 : OrdConnected (ℭ₃ k n j : Set (𝔓 X)) := by - sorry + rw [ordConnected_def]; intro p mp p'' mp'' p' mp' + have mp₁ := mem_of_mem_of_subset mp ℭ₃_subset_β„­β‚‚ + have mp''₁ := mem_of_mem_of_subset mp'' ℭ₃_subset_β„­β‚‚ + have mp'₁ : p' ∈ β„­β‚‚ (X := X) k n j := mem_of_mem_of_subset mp' (ordConnected_C2.out mp₁ mp''₁) + simp_rw [ℭ₃, mem_diff, mp''₁, mp'₁, true_and, 𝔏₂, mem_setOf, + mp''₁, mp'₁, true_and, not_not] at mp'' ⊒ + obtain ⟨u, mu, π“˜nu, su⟩ := mp''; use u, mu + exact ⟨(mp'.2.1.trans_lt (lt_of_le_of_ne su.1 π“˜nu)).ne, + (wiggle_order_11_10 mp'.2 (C5_3_3_le (X := X).trans (by norm_num))).trans su⟩ /-- Lemma 5.3.9 -/ lemma ordConnected_C4 : OrdConnected (β„­β‚„ k n j : Set (𝔓 X)) := by - sorry + rw [ordConnected_def]; intro p mp p'' mp'' p' mp' + have mp''₁ := mem_of_mem_of_subset mp'' β„­β‚„_subset_ℭ₃ + have mp'₁ : p' ∈ ℭ₃ (X := X) k n j := mem_of_mem_of_subset mp' + (ordConnected_C3.out (mem_of_mem_of_subset mp β„­β‚„_subset_ℭ₃) mp''₁) + by_cases e : p' = p''; Β· rwa [← e] at mp'' + simp_rw [β„­β‚„, mem_diff, mp'₁, true_and] + by_contra h; rw [mem_iUnion] at h; obtain ⟨l', p'm⟩ := h + rw [𝔏₃, mem_maximals_iff] at p'm; simp_rw [mem_diff] at p'm + have p''nm : p'' βˆ‰ ⋃ l'', ⋃ (_ : l'' < l'), 𝔏₃ k n j l'' := by + replace mp'' := mp''.2; contrapose! mp'' + exact mem_of_mem_of_subset mp'' (iUnionβ‚‚_subset_iUnion ..) + exact absurd (p'm.2 ⟨mp''₁, p''nm⟩ mp'.2) e /-- Lemma 5.3.10 -/ lemma ordConnected_C5 : OrdConnected (β„­β‚… k n j : Set (𝔓 X)) := by - sorry + rw [ordConnected_def]; intro p mp p'' mp'' p' mp' + have mp₁ := mem_of_mem_of_subset mp β„­β‚…_subset_β„­β‚„ + have mp'₁ : p' ∈ β„­β‚„ (X := X) k n j := mem_of_mem_of_subset mp' + (ordConnected_C4.out mp₁ (mem_of_mem_of_subset mp'' β„­β‚…_subset_β„­β‚„)) + simp_rw [β„­β‚…, mem_diff, mp₁, mp'₁, true_and, 𝔏₄, mem_setOf, + mp₁, mp'₁, true_and] at mp ⊒ + contrapose! mp; obtain ⟨u, mu, sπ“˜u⟩ := mp; use u, mu, mp'.1.1.1.trans sπ“˜u /-- Lemma 5.3.11 -/ -lemma dens1_le_dens' {P : Set (𝔓 X)} (hP : P βŠ† TilesAt k) : - dens₁ P ≀ dens' k P := by - sorry +lemma dens1_le_dens' {P : Set (𝔓 X)} (hP : P βŠ† TilesAt k) : dens₁ P ≀ dens' k P := by + rw [dens₁, dens']; gcongr with p' mp' l hl + simp_rw [ENNReal.mul_iSup, iSup_le_iff, mul_div_assoc]; intro p mp sl + suffices p ∈ TilesAt k by + exact le_iSup_of_le p (le_iSupβ‚‚_of_le this sl (mul_le_mul' (by norm_cast) le_rfl)) + simp_rw [TilesAt, mem_preimage, 𝓒, mem_diff, aux𝓒, mem_setOf] + constructor + Β· rw [mem_lowerClosure] at mp; obtain ⟨p'', mp'', lp''⟩ := mp + have := mem_of_mem_of_subset mp'' hP + simp_rw [TilesAt, mem_preimage, 𝓒, mem_diff, aux𝓒, mem_setOf] at this + obtain ⟨J, lJ, vJ⟩ := this.1; use J, lp''.1.trans lJ + Β· by_contra h; obtain ⟨J, lJ, vJ⟩ := h + have := mem_of_mem_of_subset mp' hP + simp_rw [TilesAt, mem_preimage, 𝓒, mem_diff, aux𝓒, mem_setOf] at this + apply absurd _ this.2; use J, sl.1.trans lJ /-- Lemma 5.3.12 -/ -lemma dens1_le {A : Set (𝔓 X)} (hA : A βŠ† β„­ k n) : dens₁ A ≀ 2 ^ (4 * a - n + 1) := by - sorry +lemma dens1_le {A : Set (𝔓 X)} (hA : A βŠ† β„­ k n) : dens₁ A ≀ 2 ^ (4 * a - n + 1) := + calc + _ ≀ dens' k A := dens1_le_dens' (hA.trans β„­_subset_TilesAt) + _ ≀ dens' k (β„­ (X := X) k n) := iSup_le_iSup_of_subset hA + _ ≀ _ := by + rw [dens'_iSup, iSupβ‚‚_le_iff]; intro p mp + rw [β„­, mem_setOf] at mp; exact mp.2.2 /-! ## Section 5.4 and Lemma 5.1.2 -/ diff --git a/blueprint/src/chapter/main.tex b/blueprint/src/chapter/main.tex index 814afb02..1938086e 100644 --- a/blueprint/src/chapter/main.tex +++ b/blueprint/src/chapter/main.tex @@ -1057,6 +1057,7 @@ \chapter{Proof of Finitary Carleson} \end{equation} \end{lemma} \begin{proof} + \leanok Fix $x\in G\setminus G'$. Sorting the tiles $\fp$ on the left-hand-side of \eqref{eq-sump} by the value $\ps(\fp)\in [-S,S]$, it suffices to prove for every $-S\le s\le S$ that @@ -2519,6 +2520,7 @@ \section{Auxiliary lemmas} \end{lemma} \begin{proof} + \leanok Let $\fp \le \fp' \le \fp''$ with $\fp, \fp'' \in \fC(k,n)$. Then, in particular, $\fp, \fp'' \in \fP(k)$, so, by \Cref{P-convex}, $\fp' \in \fP(k)$. Next, we show that if $\fq \le \fq' \in \fP(k)$ then $\dens'_k(\{\fq\}) \ge \dens_k'(\{\fq'\})$. If $\fp \in \fP(k)$ and $\lambda \ge 2$ with $\lambda \fq' \lesssim \lambda \fp$, then it follows from $\fq \le \fq'$, \eqref{eq-sc1} of \Cref{wiggle-order-3} and transitivity of $\lesssim$ that $\lambda \fq \lesssim \lambda \fp$. Thus the supremum in the definition \eqref{eq-densdef} of $\dens_k'(\{\fq\})$ is over a superset of the set the supremum in the definition of $\dens_k'(\{\fq'\})$ is taken over, which shows $\dens'_k(\{\fq\}) \ge \dens_k'(\{\fq'\})$. From $\fp' \le \fp''$, $\fp'' \in \fC(k,n)$ and \eqref{def-cnk} it then follows that $$ 2^{4a}2^{-n} < \dens_k'(\{\fp''\}) \le \dens_k'(\{\fp'\})\,. @@ -2539,6 +2541,7 @@ \section{Auxiliary lemmas} \end{lemma} \begin{proof} + \leanok Let $\fp\le\fp'\le\fp''$ with $\fp, \fp'' \in \fC_1(k,n,j)$. By \Cref{C-convex} and the inclusion $\fC_1(k,n,j) \subset \fC(k,n)$, which holds by definition \eqref{defcnkj}, we have $\fp' \in \fC(k,n)$. By \eqref{eq-sc1} and transitivity of $\lesssim$ we have that $\fq \le \fq'$ and $100 \fq' \lesssim \mathfrak{m}$ imply $100 \fq \lesssim \mathfrak{m}$. So, by \eqref{defbfp}, $\mathfrak{B}(\fp'') \subset \mathfrak{B}(\fp') \subset \mathfrak{B}(\fp)$. Consequently, by \eqref{defcnkj} $$ 2^j \le |\mathfrak{B}(\fp'')|\le |\mathfrak{B}(\fp')| \le |\mathfrak{B}(\fp)| < 2^{j+1}\,, @@ -2555,10 +2558,16 @@ \section{Auxiliary lemmas} \end{lemma} \begin{proof} + \leanok Let $\fp \le \fp' \le \fp''$ with $\fp, \fp'' \in \fC_2(k,n,j)$. By \eqref{eq-C2-def}, we have \begin{equation*} \fC_2(k,n,j) \subset \fC_1(k,n,j)\ . - \end{equation*} Combined with \Cref{C1-convex}, it follows that $\fp' \in \fC_1(k,n,j)$. Suppose that $\fp' \notin \fC_2(k,n,j)$. By \eqref{eq-C2-def}, this implies that there exists $0 \le l' \le Z(n+1)$ with $\fp' \in \fL_1(k,n,j,l')$. By the definition \eqref{eq-L1-def} of $\fL_1(k,n,j,l')$, this implies that $\fp$ is minimal with respect to $\le$ in $\fC_1(k,n,j) \setminus \bigcup_{l < l'} \fL_1(k,n,j,l)$. Since $\fp \in \fC_2(k,n,j)$ we must have $\fp \ne \fp'$. Thus $\fp \le \fp'$ and $\fp \ne \fp'$. By minimality of $\fp'$ it follows that $\fp \notin \fC_1(k,n,j) \setminus \bigcup_{l < l'} \fL_1(k,n,j,l)$. But by \eqref{eq-C2-def} this implies $\fp \notin \fC_2(k,n,j)$, a contradiction. + \end{equation*} Combined with \Cref{C1-convex}, it follows that $\fp' \in \fC_1(k,n,j)$. + If $\fp=\fp'$ the statement is trivially true, otherwise suppose that $\fp' \notin \fC_2(k,n,j)$. + By \eqref{eq-C2-def}, this implies that there exists $0 \le l' \le Z(n+1)$ with $\fp' \in \fL_1(k,n,j,l')$. + By the definition \eqref{eq-L1-def} of $\fL_1(k,n,j,l')$, this implies that $\fp'$ is minimal + with respect to $\le$ in $\fC_1(k,n,j) \setminus \bigcup_{l < l'} \fL_1(k,n,j,l)$. + Since $\fp\le\fp'$ and $\fp\in\fC_2(k,n,j)$, $\fp=\fp'$, a contradiction. \end{proof} \begin{lemma}[C3 convex] @@ -2570,7 +2579,13 @@ \section{Auxiliary lemmas} \end{lemma} \begin{proof} - Let $\fp \le \fp' \le \fp''$ with $\fp, \fp'' \in \fC_3(k,n,j)$. By \eqref{eq-C3-def} and \Cref{C2-convex} it follows that $\fp' \in \fC_2(k,n,j)$. Suppose that $\fp' \notin \fC_3(k,n,j)$. Then, by \eqref{eq-C3-def} and \eqref{eq-L2-def}, there exists $\fu \in \fU_1(k,n,j)$ with $2\fp' \lesssim \fu$ and $\scI(\fp') \ne \scI(\fu)$. Together this gives $\scI(\fp') \subsetneq \scI(\fu)$. From $\fp' \le \fp$, \eqref{eq-sc1} and transitivity of $\lesssim$ we then have $2\fp \lesssim \fu$. Also, $\scI(\fp) \subset \scI(\fp') \subsetneq \scI(\fu)$, so $\scI(\fp) \ne \scI(\fu)$. But then $\fp \in \fL_2(k,n,j)$, contradicting by \eqref{eq-C3-def} the assumption $\fp \in \fC_3(k,n,j)$. + \leanok + Let $\fp \le \fp' \le \fp''$ with $\fp, \fp'' \in \fC_3(k,n,j)$. + By \eqref{eq-C3-def} and \Cref{C2-convex} it follows that $\fp' \in \fC_2(k,n,j)$. + By \eqref{eq-C3-def} and \eqref{eq-L2-def}, there exists $\fu \in \fU_1(k,n,j)$ with + $2\fp'' \lesssim \fu$ and $\scI(\fp'') \subsetneq \scI(\fu)$. From $\fp' \le \fp''$, + \eqref{eq-sc1} and transitivity of $\lesssim$ we then have + $2\fp' \lesssim \fu$ and $\scI(\fp') \subsetneq \scI(\fu)$, so $\fp' \in \fC_3(k,n,j)$. \end{proof} \begin{lemma}[C4 convex] @@ -2582,7 +2597,9 @@ \section{Auxiliary lemmas} \end{lemma} \begin{proof} - Let $\fp \le \fp' \le\fp''$ with $\fp, \fp'' \in \fC_4(k,n,j)$. As before we obtain from the inclusion $\fC_4(k,n,j) \subset \fC_3(k,n,j)$ and \Cref{C3-convex} that $\fp' \in \fC_3(k,n,j)$. Thus, if $\fp' \notin \fC_4(k,n,j)$ then by \eqref{eq-L3-def} there exists $l$ such that $\fp' \in \fL_3(k,n,j,l)$. Thus $\fp'$ is maximal with respect to $\le$ in $\fC_3(k,n,j) \setminus \bigcup_{0 \le l' < l} \fL_3(k,n,j,l')$. Since $\fp'' \in \fC_4(k,n,j)$ we must have $\fp' \ne \fp''$. Thus $\fp' \le \fp''$ and $\fp'\ne \fp''$. By minimality of $\fp'$ it follows that $\fp'' \notin \fC_3(k,n,j) \setminus \bigcup_{l < l'} \fL_3(k,n,j,l)$. But by \eqref{eq-C4-def} this implies $\fp'' \notin \fC_4(k,n,j)$, a contradiction. + \leanok + The proof is entirely analogous to \Cref{C2-convex}, substituting $\fC_4$ for $\fC_2$, + $\fC_3$ for $\fC_1$ and $\fp'\le\fp''$ for $\fp\le\fp'$. \end{proof} \begin{lemma}[C5 convex] @@ -2594,8 +2611,11 @@ \section{Auxiliary lemmas} \end{lemma} \begin{proof} - Let $\fp \le \fp' \le\fp''$ with $\fp, \fp'' \in \fC_5(k,n,j)$. Then $\fp, \fp'' \in \fC_4(k,n,j)$ by \eqref{defc5}, and thus by \Cref{C4-convex} also $\fp' \in \fC_4(k,n,j)$. Suppose that $\fp' \notin \fC_5(k,n,j)$. By \eqref{defc5}, it follows that $\fp' \in \fL_4(k,n,j)$. - By \eqref{eq-L4-def}, there exists $\fu \in \fU_1(k,n,j)$ with $\scI(\fp') \subset \bigcup \mathcal{L}(\fu)$. Then also $\scI(\fp) \subset \bigcup \mathcal{L}(\fu)$, a contradiction. + \leanok + Let $\fp \le \fp' \le\fp''$ with $\fp, \fp'' \in \fC_5(k,n,j)$. + Then $\fp, \fp'' \in \fC_4(k,n,j)$ by \eqref{defc5}, and thus by \Cref{C4-convex} $\fp' \in \fC_4(k,n,j)$. + It suffices to show that if $\fp' \in \fL_4(k,n,j)$ then $\fp \in \fL_4(k,n,j)$ by contraposition; + this is true by \eqref{eq-L4-def} and $\fp\le\fp'$. \end{proof} \begin{lemma}[dens compare] @@ -2608,6 +2628,7 @@ \section{Auxiliary lemmas} \end{equation} \end{lemma} \begin{proof} +\leanok It suffices to show that for all $\fp'\in \fP'$ and $\lambda\ge 2$ and $\fp\in \fP(\fP')$ with $\lambda \fp' \lesssim \lambda \fp$ we have \begin{equation} @@ -2655,6 +2676,7 @@ \section{Auxiliary lemmas} \end{lemma} \begin{proof} + \leanok We have by \Cref{dens-compare} that $\dens_1(\mathfrak{A}) \le \dens_k'(\mathfrak{A})$. Since $\mathfrak{A} \subset \fC(k,n)$, it follows from monotonicity of suprema and the definition \eqref{eq-densdef} that $