Skip to content

Commit

Permalink
Lemma 5.4.8
Browse files Browse the repository at this point in the history
  • Loading branch information
@Parcly-Taxel
Parcly-Taxel committed Jul 26, 2024
1 parent b6db988 commit 24ce5fb
Show file tree
Hide file tree
Showing 3 changed files with 263 additions and 84 deletions.
183 changes: 99 additions & 84 deletions Carleson/DiscreteCarleson.lean
View file
Original file line number Diff line number Diff line change
@@ -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
Expand Down Expand Up @@ -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) :=
Expand All @@ -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`
Expand All @@ -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

Expand Down Expand Up @@ -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
Expand All @@ -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⟩

Expand All @@ -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⟩
Expand Down Expand Up @@ -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) }
Expand Down Expand Up @@ -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'
Expand All @@ -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
Expand Down Expand Up @@ -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

Expand Down
Loading

0 comments on commit 24ce5fb

Please sign in to comment.