DyadicBernsteinCertificate.lean

1 import KomorebiLSM.TensorBernsteinCertificate
2 
3 /-! Complete dyadic subdivision attains every prescribed positive cell size. -/
4 set_option autoImplicit false
5 namespace Komorebi.LSM.TensorBernsteinCertificate
6 noncomputable section
7 
8 /-- One dyadic bisection, with both branches represented explicitly. -/
9 def Rectangle.half (R : Rectangle) (axis : Fin 2) (upper : Bool) : Rectangle :=
10   if upper then R.upper axis else R.lower axis
11 
12 theorem Rectangle.half_domain_subset (R : Rectangle) (axis : Fin 2) (upper : Bool) :
13     (R.half axis upper).domain⊆R.domain := by
14   intro x hx i
15   cases upper
16   · have h := hx i
17     constructor
18     · exact h.1
19     · by_cases he : i=axis
20       · subst i
21         simp [Rectangle.half,Rectangle.lower] at h
22         have hp : (R.lo axis : ℝ)<R.hi axis := by exact_mod_cast R.proper axis
23         linarith
24       · simpa [Rectangle.half,Rectangle.lower,he] using h.2
25   · have h := hx i
26     constructor
27     · by_cases he : i=axis
28       · subst i
29         simp [Rectangle.half,Rectangle.upper] at h
30         have hp : (R.lo axis : ℝ)<R.hi axis := by exact_mod_cast R.proper axis
31         linarith
32       · simpa [Rectangle.half,Rectangle.upper,he] using h.1
33     · exact h.2
34 
35 def Rectangle.quarter (R : Rectangle) (upperX upperY : Bool) : Rectangle :=
36   (R.half 0 upperX).half 1 upperY
37 
38 theorem Rectangle.quarter_domain_subset (R : Rectangle) (upperX upperY : Bool) :
39     (R.quarter upperX upperY).domain⊆R.domain :=
40   (Rectangle.half_domain_subset _ _ _).trans (Rectangle.half_domain_subset _ _ _)
41 
42 theorem Rectangle.quarter_width (R : Rectangle) (upperX upperY : Bool) (i : Fin 2) :
43     (R.quarter upperX upperY).width i=R.width i/2 := by
44   fin_cases i <;> cases upperX <;> cases upperY <;>
45     simp [Rectangle.quarter,Rectangle.half,Rectangle.lower,Rectangle.upper,Rectangle.width] <;> ring
46 
47 /-- A complete four-child round is a complete binary split at each of its two axes. -/
48 def SubdivisionWitness.of_quarters {p : Polynomial₂} {R : Rectangle}
49     (w : ∀ upperX upperY,SubdivisionWitness p (R.quarter upperX upperY)) : SubdivisionWitness p R :=
50   .split 0 (.split 1 (w false false) (w false true))
51     (.split 1 (w true false) (w true true))
52 
53 /-- At depth `N` each coordinate has been halved `N` times. -/
54 theorem witness_of_scale {p : Polynomial₂} {root : Rectangle} {delta epsilon : ℝ}
55     (hepsilon : epsilon<delta)
56     (hcert : ∀ R : Rectangle,R.domain⊆root.domain →
57       (∀ i,(R.width i : ℝ)<delta) → Nonempty (LocalCertificate p R))
58     (N : ℕ) (R : Rectangle) (hsub : R.domain⊆root.domain)
59     (hwidth : ∀ i,(R.width i : ℝ)≤(2 : ℝ)^N*epsilon) :
60     Nonempty (SubdivisionWitness p R) := by
61   induction N generalizing R with
62   | zero =>
63     have hw0 (i : Fin 2) : (R.width i : ℝ)≤epsilon := by simpa using hwidth i
64     exact ⟨.leaf (hcert R hsub (fun i => (hw0 i).trans_lt hepsilon)).some⟩
65   | succ N ih =>
66     have hw (upperX upperY : Bool) (i : Fin 2) :
67         ((R.quarter upperX upperY).width i : ℝ)≤(2 : ℝ)^N*epsilon := by
68       rw [Rectangle.quarter_width]
69       push_cast
70       have hi := hwidth i
71       rw [pow_succ] at hi
72       linarith
73     have hh (upperX upperY : Bool) : Nonempty (SubdivisionWitness p (R.quarter upperX upperY)) :=
74       ih _ ((R.quarter_domain_subset upperX upperY).trans hsub) (hw upperX upperY)
75     exact ⟨.of_quarters (fun upperX upperY => (hh upperX upperY).some)⟩
76 
77 /-- No coverage oracle is supplied: a finite complete dyadic tree reaches any uniform cell size. -/
78 theorem witness_of_uniform_small {p : Polynomial₂} (delta : ℝ) (hdelta : 0<delta)
79     (hcert : ∀ R : Rectangle,R.domain⊆square.domain →
80       (∀ i,(R.width i : ℝ)<delta) → Nonempty (LocalCertificate p R)) :
81     Nonempty (SubdivisionWitness p square) := by
82   let epsilon : ℝ := delta/2
83   have he0 : 0<epsilon := by dsimp [epsilon]; positivity
84   have hed : epsilon<delta := by dsimp [epsilon]; linarith
85   obtain ⟨N,hN⟩ := exists_nat_gt (2/epsilon)
86   have hn : (N : ℝ)<(2 : ℝ)^N := by exact_mod_cast N.lt_two_pow_self
87   have hw : (2 : ℝ)≤(2 : ℝ)^N*epsilon := by
88     have hg : 2<(N : ℝ)*epsilon := (div_lt_iff₀ he0).mp hN
89     nlinarith
90   apply witness_of_scale hed hcert N square (Set.Subset.refl _)
91   intro i
92   have hs : (square.width i : ℝ)=2 := by norm_num [Rectangle.width,square]
93   rw [hs]
94   exact hw
95 
96 /-- A literal complete grid: each round bisects both axes in all four children. -/
97 def UniformCertificate (p : Polynomial₂) (R : Rectangle) : ℕ → Type
98   | 0 => LocalCertificate p R
99   | N+1 => ∀ upperX upperY,UniformCertificate p (R.quarter upperX upperY) N
100 
101 def UniformCertificate.toSubdivision {p : Polynomial₂} {R : Rectangle} :
102     {N : ℕ} → UniformCertificate p R N → SubdivisionWitness p R
103   | 0,c => .leaf c
104   | _+1,c => .of_quarters (fun a b => (c a b).toSubdivision)
105 
106 theorem UniformCertificate.sound {p : Polynomial₂} {R : Rectangle} {N : ℕ}
107     (cert : UniformCertificate p R N) {x : Fin 2 → ℝ} (hx : x∈R.domain) : 0≤value p x :=
108   cert.toSubdivision.sound hx
109 
110 theorem uniform_of_scale {p : Polynomial₂} {root : Rectangle} {delta epsilon : ℝ}
111     (hepsilon : epsilon<delta)
112     (hcert : ∀ R : Rectangle,R.domain⊆root.domain →
113       (∀ i,(R.width i : ℝ)<delta) → Nonempty (LocalCertificate p R))
114     (N : ℕ) (R : Rectangle) (hsub : R.domain⊆root.domain)
115     (hwidth : ∀ i,(R.width i : ℝ)≤(2 : ℝ)^N*epsilon) :
116     Nonempty (UniformCertificate p R N) := by
117   induction N generalizing R with
118   | zero =>
119     have hw0 (i : Fin 2) : (R.width i : ℝ)≤epsilon := by simpa using hwidth i
120     exact hcert R hsub (fun i => (hw0 i).trans_lt hepsilon)
121   | succ N ih =>
122     have hw (upperX upperY : Bool) (i : Fin 2) :
123         ((R.quarter upperX upperY).width i : ℝ)≤(2 : ℝ)^N*epsilon := by
124       rw [Rectangle.quarter_width]
125       push_cast
126       have hi := hwidth i
127       rw [pow_succ] at hi
128       linarith
129     exact ⟨fun a b => (ih _ ((R.quarter_domain_subset a b).trans hsub) (hw a b)).some⟩
130 
131 /-- Every sufficiently fine full dyadic subdivision succeeds once a uniform small-cell bound holds. -/
132 theorem eventually_uniform_dyadic {p : Polynomial₂} (delta : ℝ) (hdelta : 0<delta)
133     (hcert : ∀ R : Rectangle,R.domain⊆square.domain →
134       (∀ i,(R.width i : ℝ)<delta) → Nonempty (LocalCertificate p R)) :
135     ∃ N : ℕ,∀ M : ℕ,N≤M → Nonempty (UniformCertificate p square M) := by
136   let epsilon : ℝ := delta/2
137   have he0 : 0<epsilon := by dsimp [epsilon]; positivity
138   have hed : epsilon<delta := by dsimp [epsilon]; linarith
139   obtain ⟨N,hN⟩ := exists_nat_gt (2/epsilon)
140   have hn : (N : ℝ)<(2 : ℝ)^N := by exact_mod_cast N.lt_two_pow_self
141   have hw : (2 : ℝ)≤(2 : ℝ)^N*epsilon := by
142     have hg : 2<(N : ℝ)*epsilon := (div_lt_iff₀ he0).mp hN
143     nlinarith
144   refine ⟨N,fun M hNM => ?_⟩
145   apply uniform_of_scale hed hcert M square (Set.Subset.refl _)
146   intro i
147   have hp : (2 : ℝ)^N≤(2 : ℝ)^M := pow_le_pow_right₀ (by norm_num) hNM
148   have hm := hw.trans (mul_le_mul_of_nonneg_right hp he0.le)
149   have hs : (square.width i : ℝ)=2 := by norm_num [Rectangle.width,square]
150   rw [hs]
151   exact hm
152 
153 end
154 end Komorebi.LSM.TensorBernsteinCertificate

Back to source controls