OAI/Geometry/HarmonicGrowth/SpectralSelection.lean

GitHub source file

65 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.HarmonicCounterexample.Construction.charge_distinct line 12
2. lemma OAI.HarmonicCounterexample.Construction.exists_charge_prefix line 22
3. lemma OAI.HarmonicCounterexample.Construction.exists_selected_group line 69
4. lemma OAI.HarmonicCounterexample.Certificate.block0_degrees line 100
5. lemma OAI.HarmonicCounterexample.Certificate.block1_degrees line 103
6. lemma OAI.HarmonicCounterexample.Certificate.block2_degrees line 106
7. lemma OAI.HarmonicCounterexample.Certificate.block3_degrees line 109
8. lemma OAI.HarmonicCounterexample.Certificate.block4_degrees line 112
9. lemma OAI.HarmonicCounterexample.Certificate.block5_degrees line 115
10. lemma OAI.HarmonicCounterexample.Certificate.block6_degrees line 118
11. lemma OAI.HarmonicCounterexample.Certificate.block7_degrees line 121
12. lemma OAI.HarmonicCounterexample.Certificate.block8_degrees line 124
13. lemma OAI.HarmonicCounterexample.Certificate.block9_degrees line 127
14. lemma OAI.HarmonicCounterexample.Certificate.block10_degrees line 130
15. lemma OAI.HarmonicCounterexample.Certificate.block11_degrees line 133
16. lemma OAI.HarmonicCounterexample.Certificate.block12_degrees line 136
17. lemma OAI.HarmonicCounterexample.Certificate.block13_degrees line 139
18. lemma OAI.HarmonicCounterexample.Certificate.block14_degrees line 142
19. lemma OAI.HarmonicCounterexample.Certificate.block15_degrees line 145
20. lemma OAI.HarmonicCounterexample.Certificate.block16_degrees line 148
21. lemma OAI.HarmonicCounterexample.Certificate.block17_degrees line 151
22. lemma OAI.HarmonicCounterexample.Certificate.block18_degrees line 154
23. lemma OAI.HarmonicCounterexample.Certificate.block19_degrees line 157
24. lemma OAI.HarmonicCounterexample.Certificate.block20_degrees line 160
25. lemma OAI.HarmonicCounterexample.Certificate.block21_degrees line 163
26. lemma OAI.HarmonicCounterexample.Certificate.block22_degrees line 166
27. lemma OAI.HarmonicCounterexample.Certificate.block23_degrees line 169
28. lemma OAI.HarmonicCounterexample.Certificate.block24_degrees line 172
29. lemma OAI.HarmonicCounterexample.Certificate.superblock0_degrees line 175
30. lemma OAI.HarmonicCounterexample.Certificate.superblock1_degrees line 182
31. lemma OAI.HarmonicCounterexample.Certificate.superblock2_degrees line 189
32. lemma OAI.HarmonicCounterexample.Certificate.superblock3_degrees line 196
33. lemma OAI.HarmonicCounterexample.Certificate.superblock4_degrees line 203
34. lemma OAI.HarmonicCounterexample.Certificate.selectedGroups_degrees line 210
35. lemma OAI.HarmonicCounterexample.Certificate.selectedGroups_length line 218
36. def OAI.HarmonicCounterexample.Certificate.selectedGroup line 222
37. lemma OAI.HarmonicCounterexample.Certificate.selectedGroup_degree line 225
38. lemma OAI.HarmonicCounterexample.Certificate.list_sum_getElem line 234
39. lemma OAI.HarmonicCounterexample.Certificate.selectedGroup_count_sum line 242
40. abbrev OAI.HarmonicCounterexample.Construction.L line 257
41. def OAI.HarmonicCounterexample.Construction.selectionCountFormula line 259
42. def OAI.HarmonicCounterexample.Construction.selectionCount line 265

    Source documentation

    The same finite count, packaged opaquely by choice to avoid evaluating the 249-entry certificate during kernel conversion of dependent finite sums.

    def selectionCount : Fin L→ℕ :=
    …

    Mentions: OAI.HarmonicCounterexample.Construction.L

43. lemma OAI.HarmonicCounterexample.Construction.selectionCount_eq line 268
44. lemma OAI.HarmonicCounterexample.Construction.exists_selection line 271
45. def OAI.HarmonicCounterexample.Construction.selected line 285
46. lemma OAI.HarmonicCounterexample.Construction.selected_card line 286
47. lemma OAI.HarmonicCounterexample.Construction.selected_mean line 288
48. lemma OAI.HarmonicCounterexample.Construction.selected_nonempty line 290
49. instance OAI.HarmonicCounterexample.Construction.selectionCount_nonzero line 295
50. lemma OAI.HarmonicCounterexample.Construction.dim_exact line 298
51. lemma OAI.HarmonicCounterexample.Construction.low_count_formula line 302
52. lemma OAI.HarmonicCounterexample.Construction.selectionCount_low line 325
53. lemma OAI.HarmonicCounterexample.Construction.selectionCount_high line 329
54. lemma OAI.HarmonicCounterexample.Construction.fin_sum_blocks line 336
55. lemma OAI.HarmonicCounterexample.Construction.large_sum_blocks line 343
56. lemma OAI.HarmonicCounterexample.Construction.large_raw_split line 348
57. lemma OAI.HarmonicCounterexample.Construction.selectionCount_raw_split line 352
58. lemma OAI.HarmonicCounterexample.Construction.selectionCount_low_sum line 356
59. lemma OAI.HarmonicCounterexample.Construction.selectionCount_high_sum line 360
60. lemma OAI.HarmonicCounterexample.Construction.selectionCount_split line 364
61. lemma OAI.HarmonicCounterexample.Construction.selectionCount_sum line 369
62. lemma OAI.HarmonicCounterexample.Construction.euclideanDimension_sixteen line 386
63. lemma OAI.HarmonicCounterexample.Construction.binomRat_add_nat line 393
64. lemma OAI.HarmonicCounterexample.Construction.certificate_transport line 396
65. lemma OAI.HarmonicCounterexample.Construction.selectionCount_surplus line 411