Construction.lean`

61 declarations, 0 contain sorry, 0 declared as axioms

Recurrent scales and orthogonal displacement sheets in real Hilbert space.

abbrev OAI.DoublingHilbert.Base line 14
abbrev OAI.DoublingHilbert.Tuple line 15
def OAI.DoublingHilbert.scale line 18
Source documentation
The scale at index j has exponent j + 1.
```
def scale (j : ℕ) : ℝ := (1000 : ℝ)⁻¹ ^ (j + 1)
```
def OAI.DoublingHilbert.colors line 20
def OAI.DoublingHilbert.widthFactor line 22
theorem OAI.DoublingHilbert.colors_pos line 24
theorem OAI.DoublingHilbert.widthFactor_pos line 26
theorem OAI.DoublingHilbert.recurrent_parameters line 28
theorem OAI.DoublingHilbert.scale_pos line 34
theorem OAI.DoublingHilbert.scale_succ line 36
def OAI.DoublingHilbert.inColoredStrip line 39
def OAI.DoublingHilbert.allowed line 43
def OAI.DoublingHilbert.admissible line 48
Source documentation
Value zero means no displacement; a nonzero tuple entry i+1 means color i.
```
def admissible (p : Base) (w : Tuple) : Prop :=
…
```
Mentions: OAI.DoublingHilbert.Base, OAI.DoublingHilbert.Tuple
def OAI.DoublingHilbert.sheetDomain line 51
def OAI.DoublingHilbert.coordinate line 53
def OAI.DoublingHilbert.levelVector line 55
def OAI.DoublingHilbert.tupleVector line 58
def OAI.DoublingHilbert.baseVector line 61
def OAI.DoublingHilbert.point line 64
def OAI.DoublingHilbert.constructedSet line 68
Source documentation
The fixed subset defined by finite-support displacements and open-strip conditions.
```
def constructedSet : Set RealL2 := {z | ∃ p w, admissible p w ∧ z = point p w}
```
Mentions: OAI.DoublingHilbert.RealL2, OAI.DoublingHilbert.admissible, OAI.DoublingHilbert.point
theorem OAI.DoublingHilbert.isOpen_inColoredStrip line 70
theorem OAI.DoublingHilbert.isOpen_allowed line 80
theorem OAI.DoublingHilbert.isOpen_sheetDomain line 84
theorem OAI.DoublingHilbert.admissible_zero line 100
theorem OAI.DoublingHilbert.tupleVector_zero line 102
theorem OAI.DoublingHilbert.point_zero line 104
theorem OAI.DoublingHilbert.point_mem line 106
theorem OAI.DoublingHilbert.coordinate_injective line 109
theorem OAI.DoublingHilbert.coordinate_ne_zero line 114
theorem OAI.DoublingHilbert.coordinate_ne_one line 117
theorem OAI.DoublingHilbert.norm_levelVector line 120
theorem OAI.DoublingHilbert.inner_levelVector line 124
theorem OAI.DoublingHilbert.norm_levelVector_sub_sq line 139
theorem OAI.DoublingHilbert.baseVector_sub line 145
theorem OAI.DoublingHilbert.baseVector_norm_sq line 150
theorem OAI.DoublingHilbert.point_dist_sameTuple_sq line 154
theorem OAI.DoublingHilbert.tupleVector_update line 160
theorem OAI.DoublingHilbert.point_update line 173
theorem OAI.DoublingHilbert.admissible_update_iff line 177
def OAI.DoublingHilbert.entryVector line 202
Source documentation
The complete level coordinate, including zero.
```
def entryVector (w : Tuple) (j : ℕ) : RealL2 :=
…
```
Mentions: OAI.DoublingHilbert.Tuple, OAI.DoublingHilbert.RealL2
theorem OAI.DoublingHilbert.entryVector_eq_zero line 205
theorem OAI.DoublingHilbert.entryVector_of_ne_zero line 208
theorem OAI.DoublingHilbert.tupleVector_sum_on line 211
theorem OAI.DoublingHilbert.inner_entryVector_entryVector line 227
theorem OAI.DoublingHilbert.inner_baseVector_levelVector line 233
theorem OAI.DoublingHilbert.inner_baseVector_entryVector line 238

theorem OAI.DoublingHilbert.norm_sum_sq_of_inner_eq_zero line 245

Source documentation

Finite Pythagoras for pairwise orthogonal vectors.

theorem norm_sum_sq_of_inner_eq_zero {ι E : Type*} [NormedAddCommGroup E]
    [InnerProductSpace ℝ E] (s : Finset ι) (v : ι → E)
    (hv : ∀ i ∈ s, ∀ j ∈ s, i ≠ j → inner ℝ (v i) (v j) = 0) :
    ‖∑ i ∈ s, v i‖ ^ 2 = ∑ i ∈ s, ‖v i‖ ^ 2 := by
…

theorem OAI.DoublingHilbert.point_dist_sq line 261

Source documentation

Exact orthogonal decomposition of source distances.

theorem point_dist_sq (p q : Base) (w w' : Tuple) (s : Finset ℕ)
    (hw : w.support ⊆ s) (hw' : w'.support ⊆ s) :
    dist (point p w) (point q w') ^ 2 = (p.1 - q.1) ^ 2 + (p.2 - q.2) ^ 2 +
      ∑ j ∈ s, ‖entryVector w j - entryVector w' j‖ ^ 2 := by
…

Mentions: OAI.DoublingHilbert.Base, OAI.DoublingHilbert.Tuple, OAI.DoublingHilbert.point, OAI.DoublingHilbert.entryVector

theorem OAI.DoublingHilbert.scale_le_norm_entryVector_sub line 283
Source documentation
Distinct choices at one level are at least one scale apart.
```
theorem scale_le_norm_entryVector_sub {w w' : Tuple} {j : ℕ} (hne : w j ≠ w' j) :
    scale j ≤ ‖entryVector w j - entryVector w' j‖ := by
…
```
Mentions: OAI.DoublingHilbert.Tuple, OAI.DoublingHilbert.scale, OAI.DoublingHilbert.entryVector
theorem OAI.DoublingHilbert.norm_entryVector_sub_sq_le line 295
theorem OAI.DoublingHilbert.norm_entryVector_sub_le_dist line 312
Source documentation
Every individual level distance is no larger than the whole source distance.
```
theorem norm_entryVector_sub_le_dist (p q : Base) (w w' : Tuple) (j : ℕ) :
    ‖entryVector w j - entryVector w' j‖ ≤ dist (point p w) (point q w') := by
…
```
Mentions: OAI.DoublingHilbert.Base, OAI.DoublingHilbert.Tuple, OAI.DoublingHilbert.entryVector, OAI.DoublingHilbert.point
theorem OAI.DoublingHilbert.abs_fst_sub_le_dist line 323
theorem OAI.DoublingHilbert.abs_snd_sub_le_dist line 333
theorem OAI.DoublingHilbert.coarse_coordinate_eq line 343
theorem OAI.DoublingHilbert.point_dist_sameTuple_le line 349
theorem OAI.DoublingHilbert.scale_antitone line 358
theorem OAI.DoublingHilbert.scale_le_div_of_lt line 362
theorem OAI.DoublingHilbert.intermediate_unique line 366
theorem OAI.DoublingHilbert.scale_add line 377
theorem OAI.DoublingHilbert.sum_scale_sq_le line 382
Source documentation
A deliberately coarse geometric-tail bound, adequate for the covering constant.
```
theorem sum_scale_sq_le {s : Finset ℕ} {R : ℝ} (hR : 0 ≤ R)
    (hs : ∀ j ∈ s, scale j ≤ R) : ∑ j ∈ s, (scale j) ^ 2 ≤ 2 * R ^ 2 := by
…
```
Mentions: OAI.DoublingHilbert.scale
theorem OAI.DoublingHilbert.fine_tail_le line 420
Source documentation
A uniform squared-distance bound for the finite-coordinate fine tail.
```
theorem fine_tail_le (w w' : Tuple) (s : Finset ℕ) {t : ℝ} (ht : 0 < t)
    (hs : ∀ j ∈ s, scale j ≤ t / 64) :
    ∑ j ∈ s, ‖entryVector w j - entryVector w' j‖ ^ 2 ≤ t ^ 2 / 1024 := by
…
```
Mentions: OAI.DoublingHilbert.Tuple, OAI.DoublingHilbert.scale, OAI.DoublingHilbert.entryVector