OAI/Analysis/DiamondDistortion/RecursiveModels.lean

GitHub source file

133 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.DiamondDistortion.RecursiveModel.Coord line 19

   Source documentation

   Coordinates on the root-including, countably branching height-h tree.

   abbrev Coord : ℕ → Type
     | 0 => Unit
     | h+1 => Unit ⊕ (ℕ × Coord h)

2. abbrev OAI.DiamondDistortion.RecursiveModel.Vec line 22
3. def OAI.DiamondDistortion.RecursiveModel.rootChildren line 24
4. def OAI.DiamondDistortion.RecursiveModel.finiteLp line 28
5. lemma OAI.DiamondDistortion.RecursiveModel.finiteLp_apply line 30
6. lemma OAI.DiamondDistortion.RecursiveModel.finiteLp_zero line 31
7. lemma OAI.DiamondDistortion.RecursiveModel.finiteLp_add line 32
8. lemma OAI.DiamondDistortion.RecursiveModel.finiteLp_smul line 34
9. def OAI.DiamondDistortion.RecursiveModel.aggregate line 37
10. lemma OAI.DiamondDistortion.RecursiveModel.aggregate_zero line 38
11. lemma OAI.DiamondDistortion.RecursiveModel.aggregate_nonneg line 39
12. lemma OAI.DiamondDistortion.RecursiveModel.aggregate_add line 40
13. lemma OAI.DiamondDistortion.RecursiveModel.aggregate_smul line 42
14. lemma OAI.DiamondDistortion.RecursiveModel.aggregate_mono line 44
15. lemma OAI.DiamondDistortion.RecursiveModel.coordinate_le_aggregate line 49
16. def OAI.DiamondDistortion.RecursiveModel.upper line 55

    Source documentation

    Least nonnegative upper arrays evaluated at the root. P and Q are kept separately; changing their root combination changes the norm.

    def upper (p : ℝ≥0∞) : (h : ℕ) → ZeroHom (Vec h) (ℝ × ℝ)
      | 0 => ⟨fun v => (max (v ()) 0,max (-v ()) 0),by simp only [Finsupp.zero_apply,neg_zero,max_self]; rfl⟩
      | h+1 =>
          let U := upper p h
    …

    Mentions: OAI.DiamondDistortion.RecursiveModel.Vec

17. lemma OAI.DiamondDistortion.RecursiveModel.upper_zero line 67
18. lemma OAI.DiamondDistortion.RecursiveModel.upper_nonneg line 68
19. lemma OAI.DiamondDistortion.RecursiveModel.upper_neg line 74
20. def OAI.DiamondDistortion.RecursiveModel.join line 101

    Source documentation

    A node's two least upper values once its child arrays have norms a,b.

    def join (r a b : ℝ) : ℝ × ℝ := (max a (r+b),max (a-r) b)

21. lemma OAI.DiamondDistortion.RecursiveModel.join_mono line 102
22. lemma OAI.DiamondDistortion.RecursiveModel.join_add line 105
23. lemma OAI.DiamondDistortion.RecursiveModel.join_smul line 116
24. lemma OAI.DiamondDistortion.RecursiveModel.join_root_bound line 121
25. lemma OAI.DiamondDistortion.RecursiveModel.upper_add line 127
26. lemma OAI.DiamondDistortion.RecursiveModel.upper_smul_nonneg line 159
27. lemma OAI.DiamondDistortion.RecursiveModel.upper_child_bound line 184
28. lemma OAI.DiamondDistortion.RecursiveModel.upper_coordinate_bound line 195
29. def OAI.DiamondDistortion.RecursiveModel.nu line 218
30. lemma OAI.DiamondDistortion.RecursiveModel.nu_nonneg line 219
31. lemma OAI.DiamondDistortion.RecursiveModel.nu_zero line 221
32. lemma OAI.DiamondDistortion.RecursiveModel.nu_add line 222
33. lemma OAI.DiamondDistortion.RecursiveModel.nu_neg line 226
34. lemma OAI.DiamondDistortion.RecursiveModel.nu_smul line 228
35. lemma OAI.DiamondDistortion.RecursiveModel.nu_eq_zero line 235
36. def OAI.DiamondDistortion.RecursiveModel.nuSeminorm line 242
37. abbrev OAI.DiamondDistortion.RecursiveModel.ForestCoord line 250

    Source documentation

    Finite disjoint forest, one positive-height rooted tree per component.

    abbrev ForestCoord := Σ h : ℕ,Coord (h+1)

    Mentions: OAI.DiamondDistortion.RecursiveModel.Coord

38. abbrev OAI.DiamondDistortion.RecursiveModel.ForestVec line 251
39. def OAI.DiamondDistortion.RecursiveModel.components line 252
40. lemma OAI.DiamondDistortion.RecursiveModel.components_apply line 253
41. def OAI.DiamondDistortion.RecursiveModel.componentValues line 255
42. lemma OAI.DiamondDistortion.RecursiveModel.componentValues_apply line 257
43. lemma OAI.DiamondDistortion.RecursiveModel.componentValues_zero line 259
44. def OAI.DiamondDistortion.RecursiveModel.exponent line 261
45. instance OAI.DiamondDistortion.RecursiveModel.exponent_ge_one line 262
46. def OAI.DiamondDistortion.RecursiveModel.nuMap line 263
47. def OAI.DiamondDistortion.RecursiveModel.vectorNormValues line 264
48. lemma OAI.DiamondDistortion.RecursiveModel.vectorNormValues_apply line 265
49. lemma OAI.DiamondDistortion.RecursiveModel.vectorNormValues_zero line 266
50. lemma OAI.DiamondDistortion.RecursiveModel.vectorNormValues_nonneg line 267
51. lemma OAI.DiamondDistortion.RecursiveModel.vectorNormValues_add line 268
52. lemma OAI.DiamondDistortion.RecursiveModel.vectorNormValues_neg line 271
53. lemma OAI.DiamondDistortion.RecursiveModel.vectorNormValues_smul line 275
54. def OAI.DiamondDistortion.RecursiveModel.vectorNorm line 281

    Source documentation

    Exactly the outer Hilbert sum of the root-sum ν_h norms with p_h=1+1/h.

    def vectorNorm (v : ForestVec) : ℝ := aggregate 2 (vectorNormValues v)

    Mentions: OAI.DiamondDistortion.RecursiveModel.ForestVec, OAI.DiamondDistortion.RecursiveModel.aggregate, OAI.DiamondDistortion.RecursiveModel.vectorNormValues

55. lemma OAI.DiamondDistortion.RecursiveModel.vectorNorm_zero line 282
56. lemma OAI.DiamondDistortion.RecursiveModel.vectorNorm_add line 283
57. lemma OAI.DiamondDistortion.RecursiveModel.vectorNorm_neg line 285
58. lemma OAI.DiamondDistortion.RecursiveModel.vectorNorm_smul line 286
59. lemma OAI.DiamondDistortion.RecursiveModel.vectorNorm_coordinate line 288
60. def OAI.DiamondDistortion.RecursiveModel.vectorSeminorm line 292
61. def OAI.DiamondDistortion.RecursiveModel.rootP line 300

    Source documentation

    Separate Euclidean root arrays for the joined (p=2) models.

    def rootP (h : ℕ) : ZeroHom (Vec (h+1)) ℝ :=
    …

    Mentions: OAI.DiamondDistortion.RecursiveModel.Vec

62. def OAI.DiamondDistortion.RecursiveModel.rootQ line 302
63. def OAI.DiamondDistortion.RecursiveModel.forestP line 304
64. def OAI.DiamondDistortion.RecursiveModel.forestQ line 305
65. lemma OAI.DiamondDistortion.RecursiveModel.forestP_zero line 306
66. lemma OAI.DiamondDistortion.RecursiveModel.forestQ_zero line 307
67. lemma OAI.DiamondDistortion.RecursiveModel.forestP_nonneg line 308
68. lemma OAI.DiamondDistortion.RecursiveModel.forestQ_nonneg line 309
69. lemma OAI.DiamondDistortion.RecursiveModel.forestP_add line 310
70. lemma OAI.DiamondDistortion.RecursiveModel.forestQ_add line 317
71. lemma OAI.DiamondDistortion.RecursiveModel.forestP_neg line 324
72. lemma OAI.DiamondDistortion.RecursiveModel.forestQ_neg line 330
73. lemma OAI.DiamondDistortion.RecursiveModel.forestP_smul line 332
74. lemma OAI.DiamondDistortion.RecursiveModel.forestQ_smul line 338
75. lemma OAI.DiamondDistortion.RecursiveModel.forest_coordinate line 340
76. def OAI.DiamondDistortion.RecursiveModel.zeroNorm line 349

    Source documentation

    Root-zero common-root norm. The new root coordinate is absent, not free.

    def zeroNorm (v : ForestVec) : ℝ := max (forestP v) (forestQ v)

    Mentions: OAI.DiamondDistortion.RecursiveModel.ForestVec, OAI.DiamondDistortion.RecursiveModel.forestP, OAI.DiamondDistortion.RecursiveModel.forestQ

77. lemma OAI.DiamondDistortion.RecursiveModel.zeroNorm_zero line 350
78. lemma OAI.DiamondDistortion.RecursiveModel.zeroNorm_add line 351
79. lemma OAI.DiamondDistortion.RecursiveModel.zeroNorm_neg line 355
80. lemma OAI.DiamondDistortion.RecursiveModel.zeroNorm_smul line 356
81. lemma OAI.DiamondDistortion.RecursiveModel.zeroNorm_coordinate line 362
82. def OAI.DiamondDistortion.RecursiveModel.zeroSeminorm line 366
83. abbrev OAI.DiamondDistortion.RecursiveModel.JoinedCoord line 373
84. abbrev OAI.DiamondDistortion.RecursiveModel.JoinedVec line 374
85. def OAI.DiamondDistortion.RecursiveModel.joinedChildren line 375
86. def OAI.DiamondDistortion.RecursiveModel.joinedUpper line 378
87. def OAI.DiamondDistortion.RecursiveModel.joinedNorm line 381

    Source documentation

    Free new-root sum, which is genuinely twice the common-root norm on root zero.

    def joinedNorm (v : JoinedVec) : ℝ := (joinedUpper v).1+(joinedUpper v).2

    Mentions: OAI.DiamondDistortion.RecursiveModel.JoinedVec, OAI.DiamondDistortion.RecursiveModel.joinedUpper

88. lemma OAI.DiamondDistortion.RecursiveModel.joinedNorm_zero line 382
89. lemma OAI.DiamondDistortion.RecursiveModel.joinedNorm_add line 383
90. lemma OAI.DiamondDistortion.RecursiveModel.joinedNorm_neg line 391
91. lemma OAI.DiamondDistortion.RecursiveModel.joinedNorm_smul_nonneg line 394
92. lemma OAI.DiamondDistortion.RecursiveModel.joinedNorm_smul line 396
93. lemma OAI.DiamondDistortion.RecursiveModel.joinedNorm_coordinate line 401
94. lemma OAI.DiamondDistortion.RecursiveModel.joinedNorm_root_zero line 410
95. def OAI.DiamondDistortion.RecursiveModel.joinedSeminorm line 414
96. def OAI.DiamondDistortion.RecursiveModel.ancestors line 422

    Source documentation

    Prefix ancestors, including both the root and the coordinate itself.

    def ancestors : (h : ℕ) → Coord h → Finset (Coord h)
      | 0,_ => {()}
      | _+1,.inl _ => {.inl ()}
      | h+1,.inr (i,s) => insert (.inl ()) ((ancestors h s).image (fun t => .inr (i,t)))

    Mentions: OAI.DiamondDistortion.RecursiveModel.Coord

97. lemma OAI.DiamondDistortion.RecursiveModel.self_mem_ancestors line 426
98. lemma OAI.DiamondDistortion.RecursiveModel.ancestor_trans line 433
99. def OAI.DiamondDistortion.RecursiveModel.forestAncestors line 455
100. lemma OAI.DiamondDistortion.RecursiveModel.forest_self_mem line 457
101. lemma OAI.DiamondDistortion.RecursiveModel.forest_ancestor_trans line 459
102. def OAI.DiamondDistortion.RecursiveModel.ForestHead line 467

     Source documentation

     Finite heads are componentwise ancestor closed; a used component includes its original root. There is no joined free root in this index type.

     def ForestHead := {H : Finset ForestCoord // ∀ i ∈ H,forestAncestors i ⊆ H}

     Mentions: OAI.DiamondDistortion.RecursiveModel.ForestCoord, OAI.DiamondDistortion.RecursiveModel.forestAncestors

103. def OAI.DiamondDistortion.RecursiveModel.forestHead line 468
104. lemma OAI.DiamondDistortion.RecursiveModel.forestHead_contains line 473
105. def OAI.DiamondDistortion.RecursiveModel.joinedAncestors line 477
106. lemma OAI.DiamondDistortion.RecursiveModel.joined_self_mem line 480
107. lemma OAI.DiamondDistortion.RecursiveModel.joined_ancestor_trans line 484
108. def OAI.DiamondDistortion.RecursiveModel.JoinedHead line 503

     Source documentation

     The joined root belongs to every allowed head, including otherwise empty heads.

     def JoinedHead := {H : Finset JoinedCoord // Sum.inl () ∈ H ∧ ∀ i ∈ H,joinedAncestors i ⊆ H}

     Mentions: OAI.DiamondDistortion.RecursiveModel.JoinedCoord, OAI.DiamondDistortion.RecursiveModel.joinedAncestors

109. def OAI.DiamondDistortion.RecursiveModel.joinedHead line 504
110. lemma OAI.DiamondDistortion.RecursiveModel.joinedHead_contains line 513
111. def OAI.DiamondDistortion.RecursiveModel.vectorData line 519

     Source documentation

     The dense-coordinate presentations of the three distinct recursive Banach spaces. Each space is the completion for its displayed, exact finite norm.

     def vectorData : CoordinateCompletion.Data ForestCoord where
     …

     Mentions: OAI.DiamondDistortion.CoordinateCompletion.Data, OAI.DiamondDistortion.RecursiveModel.ForestCoord

112. def OAI.DiamondDistortion.RecursiveModel.zeroData line 522
113. def OAI.DiamondDistortion.RecursiveModel.joinedData line 525
114. abbrev OAI.DiamondDistortion.RecursiveModel.VectorSpace line 528
115. abbrev OAI.DiamondDistortion.RecursiveModel.ZeroRootSpace line 529
116. abbrev OAI.DiamondDistortion.RecursiveModel.FreeRootSpace line 530
117. def OAI.DiamondDistortion.RecursiveModel.vectorHeads line 532
118. def OAI.DiamondDistortion.RecursiveModel.zeroHeads line 534
119. def OAI.DiamondDistortion.RecursiveModel.freeHeads line 536
120. lemma OAI.DiamondDistortion.RecursiveModel.vectorHeads_commutes line 538
121. lemma OAI.DiamondDistortion.RecursiveModel.zeroHeads_commutes line 539
122. lemma OAI.DiamondDistortion.RecursiveModel.freeHeads_commutes line 540
123. lemma OAI.DiamondDistortion.RecursiveModel.vector_norm_embedding line 542
124. lemma OAI.DiamondDistortion.RecursiveModel.zero_norm_embedding line 544
125. lemma OAI.DiamondDistortion.RecursiveModel.free_norm_embedding line 546
126. lemma OAI.DiamondDistortion.RecursiveModel.pure_tail_new_root line 550

     Source documentation

     The new-root coordinate vanishes on every pure tail for an allowed joined head.

     lemma pure_tail_new_root (H : JoinedHead) {y : FreeRootSpace}
         (hy : freeHeads.projection H y=0) : joinedData.coordinate (Sum.inl ()) y=0 := by
     …

     Mentions: OAI.DiamondDistortion.RecursiveModel.JoinedHead, OAI.DiamondDistortion.RecursiveModel.FreeRootSpace

127. lemma OAI.DiamondDistortion.RecursiveModel.free_root_zero_norm line 558

     Source documentation

     Root-zero identification retains the factor two; the root-max and root-sum models are not silently normalized into one another.

     lemma free_root_zero_norm (v : JoinedVec) (hv : (joinedChildren v).1=0) :
         ‖joinedData.embedding v‖=2*‖zeroData.embedding (joinedChildren v).2‖ := by
     …

     Mentions: OAI.DiamondDistortion.RecursiveModel.JoinedVec, OAI.DiamondDistortion.RecursiveModel.joinedChildren

128. theorem OAI.DiamondDistortion.RecursiveModel.sixth_graph line 567
129. theorem OAI.DiamondDistortion.RecursiveModel.cubic_graph line 571
130. theorem OAI.DiamondDistortion.RecursiveModel.cubic_weak line 575
131. theorem OAI.DiamondDistortion.RecursiveModel.free_lens line 580
132. theorem OAI.DiamondDistortion.RecursiveModel.free_graph line 587
133. theorem OAI.DiamondDistortion.RecursiveModel.zero_graph line 591