Skip to content

Commit

Permalink
Convexity lemmas (5.3.5 to 5.3.12) (#71)
Browse files Browse the repository at this point in the history
  • Loading branch information
@Parcly-Taxel
Parcly-Taxel authored Jul 12, 2024
1 parent 5a83b4a commit ae2a7e7
Show file tree
Hide file tree
Showing 2 changed files with 141 additions and 20 deletions.
129 changes: 114 additions & 15 deletions Carleson/DiscreteCarleson.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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) :=
Expand All @@ -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 = ∅ }
Expand All @@ -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) }
Expand All @@ -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) :=
Expand All @@ -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) :=
Expand All @@ -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} }
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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 -/
Expand All @@ -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 -/

Expand Down
32 changes: 27 additions & 5 deletions blueprint/src/chapter/main.tex
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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'\})\,.
Expand All @@ -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}\,,
Expand All @@ -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]
Expand All @@ -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]
Expand All @@ -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]
Expand All @@ -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]
Expand All @@ -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}
Expand Down Expand Up @@ -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
$
Expand Down

0 comments on commit ae2a7e7

Please sign in to comment.