diff --git a/Carleson/DiscreteCarleson.lean b/Carleson/DiscreteCarleson.lean index 87de41d8..b18d1bda 100644 --- a/Carleson/DiscreteCarleson.lean +++ b/Carleson/DiscreteCarleson.lean @@ -1,5 +1,6 @@ import Carleson.Forest import Carleson.HardyLittlewood +import Carleson.MinLayer open MeasureTheory Measure NNReal Metric Complex Set Function BigOperators Bornology open scoped ENNReal @@ -77,77 +78,13 @@ def 𝔏₀ (k n : β„•) : Set (𝔓 X) := /-- `𝔏₁(k, n, j, l)` consists of the minimal elements in `ℭ₁(k, n, j)` not in `𝔏₁(k, n, j, l')` for some `l' < l`. Defined near (5.1.11). -/ def 𝔏₁ (k n j l : β„•) : Set (𝔓 X) := - minimals (·≀·) (ℭ₁ k n j \ ⋃ (l' < l), 𝔏₁ k n j l') - -lemma 𝔏₁_disjoint {k n j l l' : β„•} (h : l β‰  l') : Disjoint (𝔏₁ (X := X) k n j l) (𝔏₁ k n j l') := by - wlog hl : l < l'; Β· exact (this h.symm (by omega)).symm - rw [disjoint_right]; intro p hp - rw [𝔏₁, mem_minimals_iff, mem_diff] at hp; replace hp := hp.1.2; contrapose! hp - refine mem_iUnionβ‚‚_of_mem hl hp - -lemma exists_le_of_mem_𝔏₁ {k n j l : β„•} {p : 𝔓 X} (hp : p ∈ 𝔏₁ k n j l) : - βˆƒ p' ∈ ℭ₁ k n j, p' ≀ p ∧ 𝔰 p' + l ≀ 𝔰 p := by - induction l generalizing p with - | zero => - rw [𝔏₁] at hp; simp_rw [not_lt_zero', iUnion_of_empty, iUnion_empty, diff_empty] at hp - use p, hp.1; simp - | succ l ih => - have np : p βˆ‰ 𝔏₁ k n j l := disjoint_right.mp (𝔏₁_disjoint (by omega)) hp - rw [𝔏₁, mem_minimals_iff] at hp np - have rl : p ∈ ℭ₁ k n j \ ⋃ (l' < l), 𝔏₁ k n j l' := by - refine mem_of_mem_of_subset hp.1 (diff_subset_diff_right ?_) - refine biUnion_subset_biUnion_left fun k hk ↦ ?_ - rw [mem_def, Nat.le_eq] at hk ⊒; omega - simp_rw [rl, true_and] at np; push_neg at np; obtain ⟨p', hp', lp⟩ := np - have mp' : p' ∈ 𝔏₁ k n j l := by - by_contra h - have cp : p' ∈ ℭ₁ k n j \ ⋃ (l' < l + 1), 𝔏₁ k n j l' := by - have : βˆ€ l', l' < l + 1 ↔ l' < l ∨ l' = l := by omega - simp_rw [this, iUnion_or, iUnion_union_distrib] - simp only [iUnion_iUnion_eq_left, mem_diff, mem_union, mem_iUnion, exists_prop, not_or, - not_exists, not_and] at hp' ⊒ - tauto - exact absurd (hp.2 cp lp.1) (ne_eq _ _ β–Έ lp.2) - obtain ⟨d, md, ld, sd⟩ := ih mp'; use d, md, (ld.trans lp.1) - rw [Nat.cast_add, Nat.cast_one, ← add_assoc] - have π“˜lt : π“˜ p' < π“˜ p := by - refine lt_of_le_of_ne lp.1.1 (not_lt_of_π“˜_eq_π“˜.mt ?_) - rw [not_not]; exact lt_of_le_of_ne lp.1 lp.2.symm - have 𝔰lt : 𝔰 p' < 𝔰 p := by rw [Grid.lt_def] at π“˜lt; exact π“˜lt.2 - omega + (ℭ₁ k n j).minLayer l /-- The subset `β„­β‚‚(k, n, j)` of `ℭ₁(k, n, j)`, given in (5.1.13). -/ 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 - -lemma exists_le_of_mem_β„­β‚‚ {k n j : β„•} {p : 𝔓 X} (hp : p ∈ β„­β‚‚ k n j) : - βˆƒ p' ∈ ℭ₁ k n j, p' ≀ p ∧ 𝔰 p' + (Z * (n + 1) : β„•) ≀ 𝔰 p := by - have mp : p ∈ ℭ₁ k n j \ ⋃ (l' < Z * (n + 1)), 𝔏₁ k n j l' := by - refine mem_of_mem_of_subset hp (diff_subset_diff_right ?_) - refine biUnion_subset_biUnion_left fun k hk ↦ ?_ - rw [mem_def, Nat.le_eq] at hk ⊒; omega - let C : Finset (𝔓 X) := - ((ℭ₁ k n j).toFinset \ (Finset.range (Z * (n + 1))).biUnion fun l' ↦ - (𝔏₁ k n j l').toFinset).filter (Β· ≀ p) - have Cn : C.Nonempty := by - use p - simp_rw [C, Finset.mem_filter, le_rfl, and_true, Finset.mem_sdiff, - Finset.mem_biUnion, Finset.mem_range, not_exists, not_and, mem_toFinset] - simp_rw [mem_diff, mem_iUnion, exists_prop, not_exists, not_and] at mp - exact mp - obtain ⟨p', mp', maxp'⟩ := C.exists_minimal Cn - simp_rw [C, Finset.mem_filter, Finset.mem_sdiff, Finset.mem_biUnion, Finset.mem_range, not_exists, - not_and, mem_toFinset] at mp' maxp' - conv at maxp' => enter [x]; rw [and_imp] - have mp'₁ : p' ∈ 𝔏₁ k n j (Z * (n + 1)) := by - rw [𝔏₁, mem_minimals_iff] - simp_rw [mem_diff, mem_iUnion, exists_prop, not_exists, not_and] - exact ⟨mp'.1, fun y hy ly ↦ (eq_of_le_of_not_lt ly (maxp' y hy (ly.trans mp'.2))).symm⟩ - obtain ⟨po, mpo, lpo, spo⟩ := exists_le_of_mem_𝔏₁ mp'₁ - use po, mpo, lpo.trans mp'.2, spo.trans mp'.2.1.2 + (ℭ₁ k n j).layersAbove (Z * (n + 1)) + +lemma β„­β‚‚_subset_ℭ₁ {k n j : β„•} : β„­β‚‚ k n j βŠ† ℭ₁ (X := X) k n j := layersAbove_subset /-- The subset `π”˜β‚(k, n, j)` of `ℭ₁(k, n, j)`, given in (5.1.14). -/ def π”˜β‚ (k n j : β„•) : Set (𝔓 X) := @@ -163,25 +100,29 @@ def 𝔏₂ (k n j : β„•) : Set (𝔓 X) := def ℭ₃ (k n j : β„•) : Set (𝔓 X) := β„­β‚‚ k n j \ 𝔏₂ k n j +lemma ℭ₃_def {k n j : β„•} {p : 𝔓 X} : + p ∈ ℭ₃ k n j ↔ p ∈ β„­β‚‚ k n j ∧ βˆƒ u ∈ π”˜β‚ k n j, π“˜ p β‰  π“˜ u ∧ smul 2 p ≀ smul 1 u := by + rw [ℭ₃, mem_diff, 𝔏₂, mem_setOf, not_and, and_congr_right_iff]; intro h + simp_rw [h, true_implies, not_not] + 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) := - maximals (·≀·) (ℭ₃ k n j \ ⋃ (l' < l), 𝔏₃ k n j l') + (ℭ₃ k n j).maxLayer l /-- The subset `β„­β‚„(k, n, j)` of `ℭ₃(k, n, j)`, given in (5.1.19). -/ def β„­β‚„ (k n j : β„•) : Set (𝔓 X) := - ℭ₃ k n j \ ⋃ (l ≀ Z * (n + 1)), 𝔏₃ k n j l + (ℭ₃ k n j).layersBelow (Z * (n + 1)) -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 +lemma β„­β‚„_subset_ℭ₃ {k n j : β„•} : β„­β‚„ k n j βŠ† ℭ₃ (X := X) k n j := layersBelow_subset /-- 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) := - { i : Grid X | i ≀ π“˜ u ∧ s i + Z * (n + 1) + 1 = 𝔰 u ∧ Β¬ ball (c i) (8 * D ^ s i) βŠ† π“˜ u } + { i : Grid X | i ≀ π“˜ u ∧ s i + (Z * (n + 1) : β„•) + 1 = 𝔰 u ∧ Β¬ ball (c i) (8 * D ^ s i) βŠ† π“˜ u } /-- The subset `𝔏₄(k, n, j)` of `β„­β‚„(k, n, j)`, given near (5.1.22). Todo: we may need to change the definition to say that `p` @@ -193,6 +134,11 @@ def 𝔏₄ (k n j : β„•) : Set (𝔓 X) := def β„­β‚… (k n j : β„•) : Set (𝔓 X) := β„­β‚„ k n j \ 𝔏₄ k n j +lemma β„­β‚…_def {k n j : β„•} {p : 𝔓 X} : + p ∈ β„­β‚… k n j ↔ p ∈ β„­β‚„ k n j ∧ βˆ€ u ∈ π”˜β‚ k n j, Β¬(π“˜ p : Set X) βŠ† ⋃ (i ∈ 𝓛 (X := X) n u), i := by + rw [β„­β‚…, mem_diff, 𝔏₄, mem_setOf, not_and, and_congr_right_iff]; intro h + simp_rw [h, true_implies]; push_neg; rfl + 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 @@ -960,9 +906,9 @@ lemma ordConnected_C2 : OrdConnected (β„­β‚‚ k n j : Set (𝔓 X)) := by 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] + simp_rw [β„­β‚‚, layersAbove, 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 + rw [minLayer, 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 @@ -975,9 +921,8 @@ lemma ordConnected_C3 : OrdConnected (ℭ₃ k n j : Set (𝔓 X)) := by 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 + rw [ℭ₃_def] at mp'' ⊒ + obtain ⟨-, u, mu, π“˜nu, su⟩ := mp''; refine ⟨mp'₁, ⟨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⟩ @@ -988,9 +933,9 @@ lemma ordConnected_C4 : OrdConnected (β„­β‚„ k n j : Set (𝔓 X)) := by 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] + simp_rw [β„­β‚„, layersBelow, mem_diff, mp'₁, true_and] by_contra h; simp_rw [mem_iUnion] at h; obtain ⟨l', hl', p'm⟩ := h - rw [𝔏₃, mem_maximals_iff] at p'm; simp_rw [mem_diff] at p'm + rw [maxLayer_def, 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'' refine mem_of_mem_of_subset mp'' <| iUnionβ‚‚_mono' fun i hi ↦ ⟨i, hi.le.trans hl', subset_rfl⟩ @@ -1048,6 +993,9 @@ In lemmas, we will assume `u ∈ π”˜β‚ k n l` -/ def 𝔗₁ (k n j : β„•) (u : 𝔓 X) : Set (𝔓 X) := { p ∈ ℭ₁ k n j | π“˜ p β‰  π“˜ u ∧ smul 2 p ≀ smul 1 u } +lemma π“˜_lt_of_mem_𝔗₁ (h : p ∈ 𝔗₁ k n j p') : π“˜ p < π“˜ p' := by + rw [𝔗₁, mem_setOf] at h; exact lt_of_le_of_ne h.2.2.1 h.2.1 + /-- The subset `π”˜β‚‚(k, n, j)` of `π”˜β‚(k, n, j)`, given in (5.4.2). -/ def π”˜β‚‚ (k n j : β„•) : Set (𝔓 X) := { u ∈ π”˜β‚ k n j | Β¬ Disjoint (𝔗₁ k n j u) (ℭ₆ k n j) } @@ -1258,7 +1206,7 @@ lemma forest_separation (hu : u ∈ π”˜β‚ƒ k n j) (hu' : u' ∈ π”˜β‚ƒ k n j) (hp : p ∈ 𝔗₂ k n j u') (h : π“˜ p ≀ π“˜ u) : 2 ^ (Z * (n + 1)) < dist_(p) (𝒬 p) (𝒬 u) := by simp_rw [𝔗₂, mem_inter_iff, mem_iUnionβ‚‚, mem_iUnion] at hp obtain ⟨mp₆, v, mv, rv, ⟨-, np, sl⟩⟩ := hp - obtain ⟨p', mp', lp', sp'⟩ := exists_le_of_mem_β„­β‚‚ <| + obtain ⟨p', mp', lp', sp'⟩ := exists_scale_add_le_of_mem_layersAbove <| (ℭ₆_subset_β„­β‚… |>.trans β„­β‚…_subset_β„­β‚„ |>.trans β„­β‚„_subset_ℭ₃ |>.trans ℭ₃_subset_β„­β‚‚) mp₆ have np'u : Β¬URel k n j v u := by by_contra h; apply absurd (Eq.symm _) huu' @@ -1267,7 +1215,7 @@ lemma forest_separation (hu : u ∈ π”˜β‚ƒ k n j) (hu' : u' ∈ π”˜β‚ƒ k n j) have vnu : v β‰  u := by by_contra h; subst h; exact absurd URel.rfl np'u simp_rw [URel, vnu, false_or, not_exists, not_and] at np'u have mpt : p' ∈ 𝔗₁ k n j v := by - refine ⟨mp', ?_, ?_⟩ + refine ⟨minLayer_subset mp', ?_, ?_⟩ Β· exact (lp'.1.trans_lt (lt_of_le_of_ne sl.1 np)).ne Β· exact (wiggle_order_11_10 lp' (C5_3_3_le (X := X).trans (by norm_num))).trans sl specialize np'u p' mpt @@ -1311,9 +1259,76 @@ lemma forest_separation (hu : u ∈ π”˜β‚ƒ k n j) (hu' : u' ∈ π”˜β‚ƒ k n j) one_mul] /-- Lemma 5.4.8, verifying (2.0.37) -/ -lemma forest_inner (hu : u ∈ π”˜β‚ƒ k n j) (hp : p ∈ 𝔗₂ k n j u') : +lemma forest_inner (hu : u ∈ π”˜β‚ƒ k n j) (hp : p ∈ 𝔗₂ k n j u) : ball (𝔠 p) (8 * D ^ 𝔰 p) βŠ† π“˜ u := by - sorry + let C : Set (𝔓 X) := + {q ∈ ℭ₃ k n j ∩ ⋃ (u' ∈ π”˜β‚‚ k n j) (_ : URel k n j u u'), (𝔗₁ k n j u') | p ≀ q} + have pβ‚„ := (𝔗₂_subset_ℭ₆.trans ℭ₆_subset_β„­β‚… |>.trans β„­β‚…_subset_β„­β‚„) hp + have p₁ := (β„­β‚„_subset_ℭ₃.trans ℭ₃_subset_β„­β‚‚ |>.trans β„­β‚‚_subset_ℭ₁) pβ‚„ + have mpC : p ∈ C := by + simp_rw [C, mem_setOf]; simp_rw [𝔗₂, mem_inter_iff] at hp ⊒ + simp_rw [hp.2, le_rfl]; simpa using β„­β‚„_subset_ℭ₃ pβ‚„ + obtain ⟨q, mq, maxq⟩ := Finset.exists_maximal _ (toFinset_nonempty.mpr ⟨_, mpC⟩) + simp only [mem_toFinset] at mq maxq + have lq : p ≀ q := mq.2 + have q_max_ℭ₃ : q ∈ (ℭ₃ k n j).maxLayer 0 := by + rw [maxLayer_zero, mem_maximals_iff] + refine ⟨mq.1.1, fun q' mq' lq' ↦ eq_of_le_of_not_lt lq' (maxq q' ?_)⟩ + have z : p ≀ q' := lq.trans lq' + obtain ⟨-, u'', mu'', nu'', sl⟩ := ℭ₃_def.mp mq' + replace nu'' : π“˜ q' < π“˜ u'' := lt_of_le_of_ne sl.1 nu'' + have s2 : smul 2 p ≀ smul 2 q' := wiggle_order_11_10 z (C5_3_3_le (X := X).trans (by norm_num)) + have s2' : smul 2 p ≀ smul 1 u'' := s2.trans sl + have s10 : smul 10 p ≀ smul 1 u'' := smul_mono s2' le_rfl (by norm_num) + simp_rw [𝔗₂, mem_inter_iff, mem_iUnionβ‚‚, mem_iUnion] at hp + obtain ⟨p₆, u', mu', ru', pu'⟩ := hp + have ur : URel k n j u' u'' := Or.inr ⟨p, pu', s10⟩ + have hu'' : u'' ∈ π”˜β‚‚ k n j := by + rw [π”˜β‚‚, mem_setOf, not_disjoint_iff] + refine ⟨mu'', ⟨p, ?_, pβ‚†βŸ©βŸ© + simpa [𝔗₁, p₁, s2'] using (z.1.trans_lt nu'').ne + have ru'' : URel k n j u u'' := equivalenceOn_urel.trans (π”˜β‚ƒ_subset_π”˜β‚‚ hu) mu' hu'' ru' ur + simp_rw [C, mem_setOf, mem_inter_iff, mq', z, mem_iUnionβ‚‚, mem_iUnion, true_and, and_true] + use u'', hu'', ru''; exact ⟨(ℭ₃_subset_β„­β‚‚.trans β„­β‚‚_subset_ℭ₁) mq', nu''.ne, sl⟩ + -- ... + -- obtain ⟨r, r_max_ℭ₃, lr, sr⟩ := exists_le_add_scale_of_mem_layersBelow pβ‚„ + have sq : 𝔰 p + (Z * (n + 1) : β„•) ≀ 𝔰 q := sorry + -- ... + simp_rw [C, mem_inter_iff, mem_iUnionβ‚‚, mem_iUnion] at mq + obtain ⟨-, u', mu', ru', mq'⟩ := mq.1 + have qlu : π“˜ q < π“˜ u := URel.eq (π”˜β‚ƒ_subset_π”˜β‚‚ hu) mu' ru' β–Έ π“˜_lt_of_mem_𝔗₁ mq' + have squ : 𝔰 q < 𝔰 u := (Grid.lt_def.mp qlu).2 + have spu : 𝔰 p ≀ 𝔰 u - (Z * (n + 1) : β„•) - 1 := by omega -- ... + have : βˆƒ I, s I = 𝔰 u - (Z * (n + 1) : β„•) - 1 ∧ π“˜ p ≀ I ∧ I ≀ π“˜ u := by + apply Grid.exists_sandwiched (lq.1.trans qlu.le) (𝔰 u - (Z * (n + 1) : β„•) - 1) + refine ⟨spu, ?_⟩; change _ ≀ 𝔰 u; suffices 0 ≀ Z * (n + 1) by omega + exact Nat.zero_le _ + obtain ⟨I, sI, plI, Ilu⟩ := this + have bI : I βˆ‰ 𝓛 n u := by + have pβ‚… := (𝔗₂_subset_ℭ₆.trans ℭ₆_subset_β„­β‚…) hp + rw [β„­β‚…_def] at pβ‚…; replace pβ‚… := pβ‚….2; contrapose! pβ‚… + use u, (π”˜β‚ƒ_subset_π”˜β‚‚.trans π”˜β‚‚_subset_π”˜β‚) hu, plI.1.trans (subset_biUnion_of_mem pβ‚…) + rw [𝓛, mem_setOf, not_and] at bI; specialize bI Ilu + rw [not_and, not_not] at bI; specialize bI (by omega); rw [← sI] at spu + rcases spu.eq_or_lt with h | h + Β· have : π“˜ p = I := by + apply eq_of_le_of_not_lt plI; rw [Grid.lt_def, not_and_or, not_lt]; exact Or.inr h.symm.le + rwa [← this] at bI + Β· apply subset_trans (ball_subset_ball' _) bI + have ds : c (π“˜ p) ∈ ball (c I) (4 * D ^ s I) := (plI.1.trans Grid_subset_ball) Grid.c_mem_Grid + rw [mem_ball] at ds + calc + _ ≀ 4 * D * (D : ℝ) ^ 𝔰 p + 4 * D ^ s I := by + gcongr + Β· linarith [four_le_realD X] + Β· exact ds.le + _ = 4 * D ^ (𝔰 p + 1) + 4 * D ^ s I := by + rw [mul_assoc]; congr; rw [mul_comm, ← zpow_add_oneβ‚€ (defaultD_pos _).ne'] + _ ≀ 4 * D ^ s I + 4 * D ^ s I := by + gcongr + Β· exact one_le_D + Β· omega + _ = _ := by ring def C5_4_8 (n : β„•) : β„• := (4 * n + 12) * 2 ^ n diff --git a/Carleson/MinLayer.lean b/Carleson/MinLayer.lean new file mode 100644 index 00000000..2d4dfe5b --- /dev/null +++ b/Carleson/MinLayer.lean @@ -0,0 +1,163 @@ +import Carleson.TileStructure + +namespace Set + +variable {Ξ± : Type*} [PartialOrder Ξ±] + +/-- The `n`th minimal layer of `A`. -/ +def minLayer (A : Set Ξ±) (n : β„•) : Set Ξ± := + minimals (Β· ≀ Β·) (A \ ⋃ (k < n), A.minLayer k) + +/-- The `n`th maximal layer of `A`. -/ +def maxLayer (A : Set Ξ±) (n : β„•) : Set Ξ± := + A.minLayer (Ξ± := Ξ±α΅’α΅ˆ) n + +/-- The elements above `A`'s `n` minimal layers. -/ +def layersAbove (A : Set Ξ±) (n : β„•) : Set Ξ± := + A \ ⋃ (k ≀ n), A.minLayer k + +/-- The elements below `A`'s `n` maximal layers. -/ +def layersBelow (A : Set Ξ±) (n : β„•) : Set Ξ± := + A \ ⋃ (k ≀ n), A.maxLayer k + +variable {A : Set Ξ±} {m n : β„•} {a : Ξ±} + +lemma maxLayer_def : A.maxLayer n = maximals (Β· ≀ Β·) (A \ ⋃ (k < n), A.maxLayer k) := by + rw [maxLayer, minLayer]; rfl + +lemma minLayer_subset : A.minLayer n βŠ† A := + calc + _ βŠ† A \ ⋃ (k < n), A.minLayer k := by rw [minLayer]; exact minimals_subset .. + _ βŠ† A := diff_subset + +lemma maxLayer_subset : A.maxLayer n βŠ† A := minLayer_subset + +lemma layersAbove_subset : A.layersAbove n βŠ† A := diff_subset + +lemma layersBelow_subset : A.layersBelow n βŠ† A := diff_subset + +lemma minLayer_zero : A.minLayer 0 = minimals (Β· ≀ Β·) A := by rw [minLayer]; simp + +lemma maxLayer_zero : A.maxLayer 0 = maximals (Β· ≀ Β·) A := by rw [maxLayer_def]; simp + +lemma disjoint_minLayer_of_ne (h : m β‰  n) : Disjoint (A.minLayer m) (A.minLayer n) := by + wlog hl : m < n generalizing m n; Β· exact (this h.symm (by omega)).symm + rw [disjoint_right]; intro p hp + rw [minLayer, mem_minimals_iff, mem_diff] at hp; replace hp := hp.1.2; contrapose! hp + exact mem_iUnionβ‚‚_of_mem hl hp + +lemma disjoint_maxLayer_of_ne (h : m β‰  n) : Disjoint (A.maxLayer m) (A.maxLayer n) := + disjoint_minLayer_of_ne h + +lemma pairwiseDisjoint_minLayer : univ.PairwiseDisjoint A.minLayer := fun _ _ _ _ ↦ + disjoint_minLayer_of_ne + +lemma pairwiseDisjoint_maxLayer : univ.PairwiseDisjoint A.maxLayer := fun _ _ _ _ ↦ + disjoint_minLayer_of_ne + +lemma exists_le_in_minLayer_of_le (ha : a ∈ A.minLayer n) (hm : m ≀ n) : + βˆƒ c ∈ A.minLayer m, c ≀ a := by + induction n, hm using Nat.le_induction generalizing a with + | base => use a + | succ n _ ih => + have nma : a βˆ‰ A.minLayer n := + disjoint_right.mp (disjoint_minLayer_of_ne (by omega)) ha + rw [minLayer, mem_minimals_iff] at ha nma + have al : a ∈ A \ ⋃ (l < n), A.minLayer l := by + refine mem_of_mem_of_subset ha.1 (diff_subset_diff_right ?_) + refine biUnion_subset_biUnion_left fun k hk ↦ ?_ + rw [mem_def, Nat.le_eq] at hk ⊒; omega + simp_rw [al, true_and] at nma; push_neg at nma; obtain ⟨a', ha', la⟩ := nma + have ma' : a' ∈ A.minLayer n := by + by_contra h + have a'l : a' ∈ A \ ⋃ (l < n + 1), A.minLayer l := by + have : βˆ€ l, l < n + 1 ↔ l < n ∨ l = n := by omega + simp_rw [this, iUnion_or, iUnion_union_distrib] + simp only [iUnion_iUnion_eq_left, mem_diff, mem_union, mem_iUnion, exists_prop, not_or, + not_exists, not_and] at ha' ⊒ + tauto + exact absurd (ha.2 a'l la.1) (ne_eq _ _ β–Έ la.2) + obtain ⟨c, mc, lc⟩ := ih ma'; use c, mc, lc.trans la.1 + +lemma exists_le_in_maxLayer_of_le (ha : a ∈ A.maxLayer n) (hm : m ≀ n) : + βˆƒ c ∈ A.maxLayer m, a ≀ c := exists_le_in_minLayer_of_le (Ξ± := Ξ±α΅’α΅ˆ) ha hm + +open Classical + +variable [Fintype Ξ±] + +lemma exists_le_in_layersAbove_of_le (ha : a ∈ A.layersAbove n) (hm : m ≀ n) : + βˆƒ c ∈ A.minLayer m, c ≀ a := by + have ma : a ∈ A \ ⋃ (l' < n), A.minLayer l' := by + refine mem_of_mem_of_subset ha (diff_subset_diff_right ?_) + refine biUnion_subset_biUnion_left fun k hk ↦ ?_ + rw [mem_def, Nat.le_eq] at hk ⊒; omega + let C : Finset Ξ± := + (A.toFinset \ (Finset.range n).biUnion fun l ↦ (A.minLayer l).toFinset).filter (Β· ≀ a) + have Cn : C.Nonempty := by + use a + simp_rw [C, Finset.mem_filter, le_rfl, and_true, Finset.mem_sdiff, + Finset.mem_biUnion, Finset.mem_range, not_exists, not_and, mem_toFinset] + simp_rw [mem_diff, mem_iUnion, exists_prop, not_exists, not_and] at ma + exact ma + obtain ⟨a', ma', mina'⟩ := C.exists_minimal Cn + simp_rw [C, Finset.mem_filter, Finset.mem_sdiff, Finset.mem_biUnion, Finset.mem_range, not_exists, + not_and, mem_toFinset] at ma' mina' + conv at mina' => enter [x]; rw [and_imp] + have ma'₁ : a' ∈ A.minLayer n := by + rw [minLayer, mem_minimals_iff] + simp_rw [mem_diff, mem_iUnion, exists_prop, not_exists, not_and] + exact ⟨ma'.1, fun y hy ly ↦ (eq_of_le_of_not_lt ly (mina' y hy (ly.trans ma'.2))).symm⟩ + obtain ⟨c, mc, lc⟩ := exists_le_in_minLayer_of_le ma'₁ hm + use c, mc, lc.trans ma'.2 + +lemma exists_le_in_layersBelow_of_le (ha : a ∈ A.layersBelow n) (hm : m ≀ n) : + βˆƒ c ∈ A.maxLayer m, a ≀ c := exists_le_in_layersAbove_of_le (Ξ± := Ξ±α΅’α΅ˆ) ha hm + +end Set + +noncomputable section + +open Set +open scoped ShortVariables +variable {X : Type*} [PseudoMetricSpace X] {a : β„•} {q : ℝ} {K : X β†’ X β†’ β„‚} + {σ₁ Οƒβ‚‚ : X β†’ β„€} {F G : Set X} [ProofData a q K σ₁ Οƒβ‚‚ F G] [TileStructure Q D ΞΊ S o] +variable {A : Set (𝔓 X)} {p : 𝔓 X} {n : β„•} + +lemma exists_scale_add_le_of_mem_minLayer (hp : p ∈ A.minLayer n) : + βˆƒ p' ∈ A.minLayer 0, p' ≀ p ∧ 𝔰 p' + n ≀ 𝔰 p := by + induction n generalizing p with + | zero => use p, hp, le_rfl, by omega + | succ n ih => + obtain ⟨p', mp', lp'⟩ := exists_le_in_minLayer_of_le hp (show n ≀ n + 1 by omega) + obtain ⟨q, mq, lq, _⟩ := ih mp'; use q, mq, lq.trans lp'; suffices 𝔰 p' < 𝔰 p by omega + have l : π“˜ p' < π“˜ p := by + refine lt_of_le_of_ne lp'.1 (not_lt_of_π“˜_eq_π“˜.mt ?_); rw [not_not] + exact lt_of_le_of_ne lp' <| (disjoint_minLayer_of_ne (by omega)).ne_of_mem mp' hp + rw [Grid.lt_def] at l; exact l.2 + +lemma exists_le_add_scale_of_mem_maxLayer (hp : p ∈ A.maxLayer n) : + βˆƒ p' ∈ A.maxLayer 0, p ≀ p' ∧ 𝔰 p + n ≀ 𝔰 p' := by + induction n generalizing p with + | zero => use p, hp, le_rfl, by omega + | succ n ih => + obtain ⟨p', mp', lp'⟩ := exists_le_in_maxLayer_of_le hp (show n ≀ n + 1 by omega) + obtain ⟨q, mq, lq, _⟩ := ih mp'; use q, mq, lp'.trans lq; suffices 𝔰 p < 𝔰 p' by omega + have l : π“˜ p < π“˜ p' := by + refine lt_of_le_of_ne lp'.1 (not_lt_of_π“˜_eq_π“˜.mt ?_); rw [not_not] + exact lt_of_le_of_ne lp' <| (disjoint_maxLayer_of_ne (by omega)).ne_of_mem hp mp' + rw [Grid.lt_def] at l; exact l.2 + +lemma exists_scale_add_le_of_mem_layersAbove (hp : p ∈ A.layersAbove n) : + βˆƒ p' ∈ A.minLayer 0, p' ≀ p ∧ 𝔰 p' + n ≀ 𝔰 p := by + obtain ⟨p', mp', lp'⟩ := exists_le_in_layersAbove_of_le hp le_rfl + obtain ⟨q, mq, lq, sq⟩ := exists_scale_add_le_of_mem_minLayer mp' + use q, mq, lq.trans lp', sq.trans lp'.1.2 + +lemma exists_le_add_scale_of_mem_layersBelow (hp : p ∈ A.layersBelow n) : + βˆƒ p' ∈ A.maxLayer 0, p ≀ p' ∧ 𝔰 p + n ≀ 𝔰 p' := by + obtain ⟨p', mp', lp'⟩ := exists_le_in_layersBelow_of_le hp le_rfl + obtain ⟨q, mq, lq, sq⟩ := exists_le_add_scale_of_mem_maxLayer mp' + use q, mq, lp'.trans lq, (add_le_add_right lp'.1.2 _).trans sq + +end diff --git a/blueprint/src/chapter/main.tex b/blueprint/src/chapter/main.tex index dc23f7a6..090eca58 100644 --- a/blueprint/src/chapter/main.tex +++ b/blueprint/src/chapter/main.tex @@ -2239,6 +2239,7 @@ \section{Proof of the Exceptional Sets Lemma} \end{lemma} \begin{proof} +\leanok Let $x\in X$. For each $\fu\in \fU_1(k,n,j)$ with $x\in \scI(\fu)$, as $\fu \in \fC_1(k,n,j)$, there are at least $2^{j}$ elements $\mathfrak{m}\in \mathfrak{M}(k,n)$