OAI/Analysis/RecursivePotentials/ChallengeDefinitions.lean

GitHub source file

159 declarations, 0 contain sorry, 0 declared as axioms

The final claim constructs the spaces and states all eleven original results. Analysis.RecursivePotentials.Challenge.main_iff_original verifies statement preservation.

  1. def OAI.RecursivePotentials.leastPair line 18

    Also declared: ComparatorChallenges/RecursivePotentials.lean:18 (same declaration text).

  2. structure OAI.RecursivePotentials.FiniteRootedTree line 20

    Also declared: ComparatorChallenges/RecursivePotentials.lean:20 (same declaration text).

  3. def OAI.RecursivePotentials.FiniteRootedTree.children line 35

    Also declared: ComparatorChallenges/RecursivePotentials.lean:35 (same declaration text).

  4. def OAI.RecursivePotentials.FiniteRootedTree.maxDepth line 38

    Also declared: ComparatorChallenges/RecursivePotentials.lean:38 (same declaration text).

  5. def OAI.RecursivePotentials.FiniteRootedTree.fields line 40

    Also declared: ComparatorChallenges/RecursivePotentials.lean:40 (same declaration text).

  6. def OAI.RecursivePotentials.FiniteRootedTree.Initial line 53

    Also declared: ComparatorChallenges/RecursivePotentials.lean:53 (same declaration text).

  7. def OAI.RecursivePotentials.FiniteRootedTree.ancestors line 59

    Also declared: ComparatorChallenges/RecursivePotentials.lean:59 (same declaration text).

  8. def OAI.RecursivePotentials.FiniteRootedTree.ancestorClosure line 64

    Also declared: ComparatorChallenges/RecursivePotentials.lean:64 (same declaration text).

  9. def OAI.RecursivePotentials.FiniteRootedTree.restrict line 67

    Also declared: ComparatorChallenges/RecursivePotentials.lean:67 (same declaration text).

  10. def OAI.RecursivePotentials.FiniteRootedTree.extend line 75

    Also declared: ComparatorChallenges/RecursivePotentials.lean:75 (same declaration text).

  11. def OAI.RecursivePotentials.FiniteRootedTree.head line 79

    Also declared: ComparatorChallenges/RecursivePotentials.lean:79 (same declaration text).

  12. def OAI.RecursivePotentials.FiniteRootedTree.projectHead line 81

    Also declared: ComparatorChallenges/RecursivePotentials.lean:81 (same declaration text).

  13. structure OAI.RecursivePotentials.CofiniteSubspace line 85

    Also declared: ComparatorChallenges/RecursivePotentials.lean:85 (same declaration text).

  14. def OAI.RecursivePotentials.averagedGain line 94

    Also declared: ComparatorChallenges/RecursivePotentials.lean:94 (same declaration text).

  15. def OAI.RecursivePotentials.averagedInner line 96

    Also declared: ComparatorChallenges/RecursivePotentials.lean:96 (same declaration text).

  16. def OAI.RecursivePotentials.averagedModulus line 99

    Also declared: ComparatorChallenges/RecursivePotentials.lean:99 (same declaration text).

  17. def OAI.RecursivePotentials.sequenceTree line 105

    Also declared: ComparatorChallenges/RecursivePotentials.lean:105 (same declaration text).

  18. abbrev OAI.RecursivePotentials.ComponentNode line 116

    Also declared: ComparatorChallenges/RecursivePotentials.lean:116 (same declaration text).

  19. abbrev OAI.RecursivePotentials.JoinedNode line 118

    Also declared: ComparatorChallenges/RecursivePotentials.lean:118 (same declaration text).

  20. def OAI.RecursivePotentials.joinedTree line 120

    Also declared: ComparatorChallenges/RecursivePotentials.lean:120 (same declaration text).

  21. def OAI.RecursivePotentials.WeaklyNull line 147

    Also declared: ComparatorChallenges/RecursivePotentials.lean:147 (same declaration text).

  22. structure OAI.RecursivePotentials.EquivalentNorm line 150

    Also declared: ComparatorChallenges/RecursivePotentials.lean:150 (same declaration text).

  23. def OAI.RecursivePotentials.EquivalentNorm.inner line 163

    Also declared: ComparatorChallenges/RecursivePotentials.lean:163 (same declaration text).

  24. def OAI.RecursivePotentials.EquivalentNorm.modulus line 166

    Also declared: ComparatorChallenges/RecursivePotentials.lean:166 (same declaration text).

  25. def OAI.RecursivePotentials.EquivalentNorm.AUC line 169

    Also declared: ComparatorChallenges/RecursivePotentials.lean:169 (same declaration text).

  26. def OAI.RecursivePotentials.IsReflexive line 179

    Also declared: ComparatorChallenges/RecursivePotentials.lean:175 (same declaration text).

  27. abbrev OAI.RecursivePotentials.SquareSum.Space line 187

    Also declared: ComparatorChallenges/RecursivePotentials.lean:183 (same declaration text).

  28. def OAI.RecursivePotentials.completionEquivOfDense line 197

    Also declared: ComparatorChallenges/RecursivePotentials.lean:189 (same declaration text).

  29. def OAI.RecursivePotentials.componentTree line 222

    Also declared: ComparatorChallenges/RecursivePotentials.lean:212 (same declaration text).

  30. def OAI.RecursivePotentials.logarithmicGamma line 236

    Distinct definitions of this name: ComparatorChallenges/RecursivePotentials.lean:224 (same statement text; different proof or body). Qualify references as OAI.RecursivePotentials.logarithmicGamma@path.

  31. structure OAI.RecursivePotentials.ChildExponent line 249

    Also declared: ComparatorChallenges/RecursivePotentials.lean:235 (same declaration text).

  32. def OAI.RecursivePotentials.ChildExponent.agg line 257

    Also declared: ComparatorChallenges/RecursivePotentials.lean:243 (same declaration text).

  33. def OAI.RecursivePotentials.FiniteRootedTree.pfields line 267

    Distinct definitions of this name: ComparatorChallenges/RecursivePotentials.lean:253 (different declaration text). Qualify references as OAI.RecursivePotentials.FiniteRootedTree.pfields@path.

  34. def OAI.RecursivePotentials.VariableExponent.heightExponent line 284

    Also declared: ComparatorChallenges/RecursivePotentials.lean:270 (same declaration text).

  35. def OAI.RecursivePotentials.VariableExponent.cubicConstant line 286

    Also declared: ComparatorChallenges/RecursivePotentials.lean:272 (same declaration text).

  36. def OAI.RecursivePotentials.VariableExponent.sixthConstant line 288

    Also declared: ComparatorChallenges/RecursivePotentials.lean:274 (same declaration text).

  37. abbrev OAI.ComparatorModel.RecursivePotentials.leastPair line 304

    Also declared: ComparatorChallenges/RecursivePotentials.lean:290 (same declaration text).

  38. abbrev OAI.ComparatorModel.RecursivePotentials.FiniteRootedTree line 306

    Also declared: ComparatorChallenges/RecursivePotentials.lean:292 (same declaration text).

  39. abbrev OAI.ComparatorModel.RecursivePotentials.FiniteRootedTree.Initial line 315

    Also declared: ComparatorChallenges/RecursivePotentials.lean:301 (same declaration text).

  40. abbrev OAI.ComparatorModel.RecursivePotentials.FiniteRootedTree.restrict line 321

    Also declared: ComparatorChallenges/RecursivePotentials.lean:307 (same declaration text).

  41. abbrev OAI.ComparatorModel.RecursivePotentials.FiniteRootedTree.extend line 323

    Also declared: ComparatorChallenges/RecursivePotentials.lean:309 (same declaration text).

  42. abbrev OAI.ComparatorModel.RecursivePotentials.FiniteRootedTree.head line 325

    Also declared: ComparatorChallenges/RecursivePotentials.lean:311 (same declaration text).

  43. class OAI.ComparatorModel.RecursivePotentials.FiniteRootedTree.Heads line 327

    Also declared: ComparatorChallenges/RecursivePotentials.lean:313 (same declaration text).

  44. def OAI.ComparatorModel.RecursivePotentials.FiniteRootedTree.P line 333

    Also declared: ComparatorChallenges/RecursivePotentials.lean:319 (same declaration text).

  45. def OAI.ComparatorModel.RecursivePotentials.FiniteRootedTree.Q line 337

    Also declared: ComparatorChallenges/RecursivePotentials.lean:323 (same declaration text).

  46. def OAI.ComparatorModel.RecursivePotentials.FiniteRootedTree.normSum line 341

    Also declared: ComparatorChallenges/RecursivePotentials.lean:327 (same declaration text).

  47. abbrev OAI.ComparatorModel.RecursivePotentials.FiniteRootedTree.projectHead line 343

    Also declared: ComparatorChallenges/RecursivePotentials.lean:329 (same declaration text).

  48. def OAI.ComparatorModel.RecursivePotentials.TreeVector line 349

    Also declared: ComparatorChallenges/RecursivePotentials.lean:335 (same declaration text).

  49. instance OAI.ComparatorModel.RecursivePotentials.TreeVector.(instance at line 355) line 355
  50. instance OAI.ComparatorModel.RecursivePotentials.TreeVector.(instance at line 357) line 357
  51. instance OAI.ComparatorModel.RecursivePotentials.TreeVector.(instance at line 359) line 359
  52. instance OAI.ComparatorModel.RecursivePotentials.TreeVector.(instance at line 361) line 361
  53. class OAI.ComparatorModel.RecursivePotentials.TreeVector.Construction line 363

    Also declared: ComparatorChallenges/RecursivePotentials.lean:349 (same declaration text).

  54. instance OAI.ComparatorModel.RecursivePotentials.TreeVector.(instance at line 373) line 373
  55. instance OAI.ComparatorModel.RecursivePotentials.TreeVector.(instance at line 376) line 376
  56. def OAI.ComparatorModel.RecursivePotentials.TreeVector.coordinateLinear line 378

    Also declared: ComparatorChallenges/RecursivePotentials.lean:364 (same declaration text).

  57. def OAI.ComparatorModel.RecursivePotentials.TreeVector.coordinate line 383

    Also declared: ComparatorChallenges/RecursivePotentials.lean:369 (same declaration text).

  58. def OAI.ComparatorModel.RecursivePotentials.TreeVector.projectionLinear line 389

    Also declared: ComparatorChallenges/RecursivePotentials.lean:375 (same declaration text).

  59. def OAI.ComparatorModel.RecursivePotentials.TreeVector.projection line 404

    Also declared: ComparatorChallenges/RecursivePotentials.lean:390 (same declaration text).

  60. abbrev OAI.ComparatorModel.RecursivePotentials.TreeSpace line 415

    Also declared: ComparatorChallenges/RecursivePotentials.lean:401 (same declaration text).

  61. def OAI.ComparatorModel.RecursivePotentials.TreeSpace.coordinate line 424

    Also declared: ComparatorChallenges/RecursivePotentials.lean:410 (same declaration text).

  62. def OAI.ComparatorModel.RecursivePotentials.TreeSpace.P line 426

    Also declared: ComparatorChallenges/RecursivePotentials.lean:412 (same declaration text).

  63. def OAI.ComparatorModel.RecursivePotentials.TreeSpace.Q line 429

    Also declared: ComparatorChallenges/RecursivePotentials.lean:415 (same declaration text).

  64. def OAI.ComparatorModel.RecursivePotentials.TreeSpace.projection line 432

    Also declared: ComparatorChallenges/RecursivePotentials.lean:418 (same declaration text).

  65. def OAI.ComparatorModel.RecursivePotentials.TreeSpace.tail line 435

    Also declared: ComparatorChallenges/RecursivePotentials.lean:421 (same declaration text).

  66. abbrev OAI.ComparatorModel.RecursivePotentials.averagedModulus line 444

    Also declared: ComparatorChallenges/RecursivePotentials.lean:430 (same declaration text).

  67. abbrev OAI.ComparatorModel.RecursivePotentials.sequenceTree line 448

    Also declared: ComparatorChallenges/RecursivePotentials.lean:434 (same declaration text).

  68. abbrev OAI.ComparatorModel.RecursivePotentials.ComponentNode line 450

    Also declared: ComparatorChallenges/RecursivePotentials.lean:436 (same declaration text).

  69. abbrev OAI.ComparatorModel.RecursivePotentials.JoinedNode line 452

    Also declared: ComparatorChallenges/RecursivePotentials.lean:438 (same declaration text).

  70. abbrev OAI.ComparatorModel.RecursivePotentials.joinedTree line 454

    Also declared: ComparatorChallenges/RecursivePotentials.lean:440 (same declaration text).

  71. abbrev OAI.ComparatorModel.RecursivePotentials.XSigma line 456

    Also declared: ComparatorChallenges/RecursivePotentials.lean:442 (same declaration text).

  72. abbrev OAI.ComparatorModel.RecursivePotentials.XJoined line 458

    Also declared: ComparatorChallenges/RecursivePotentials.lean:444 (same declaration text).

  73. def OAI.ComparatorModel.RecursivePotentials.ZeroTreeVector line 460

    Also declared: ComparatorChallenges/RecursivePotentials.lean:446 (same declaration text).

  74. instance OAI.ComparatorModel.RecursivePotentials.ZeroTreeVector.(instance at line 467) line 467
  75. instance OAI.ComparatorModel.RecursivePotentials.ZeroTreeVector.(instance at line 470) line 470
  76. def OAI.ComparatorModel.RecursivePotentials.ZeroTreeVector.toTree line 473

    Also declared: ComparatorChallenges/RecursivePotentials.lean:459 (same declaration text).

  77. instance OAI.ComparatorModel.RecursivePotentials.ZeroTreeVector.(instance at line 476) line 476
  78. class OAI.ComparatorModel.RecursivePotentials.ZeroTreeVector.Construction line 478

    Also declared: ComparatorChallenges/RecursivePotentials.lean:464 (same declaration text).

  79. instance OAI.ComparatorModel.RecursivePotentials.ZeroTreeVector.(instance at line 486) line 486
  80. instance OAI.ComparatorModel.RecursivePotentials.ZeroTreeVector.(instance at line 488) line 488
  81. def OAI.ComparatorModel.RecursivePotentials.ZeroTreeVector.inclusion line 490

    Also declared: ComparatorChallenges/RecursivePotentials.lean:476 (same declaration text).

  82. def OAI.ComparatorModel.RecursivePotentials.ZeroTreeVector.projectionLinear line 493

    Also declared: ComparatorChallenges/RecursivePotentials.lean:479 (same declaration text).

  83. def OAI.ComparatorModel.RecursivePotentials.ZeroTreeVector.projection line 502

    Also declared: ComparatorChallenges/RecursivePotentials.lean:488 (same declaration text).

  84. abbrev OAI.ComparatorModel.RecursivePotentials.ZeroTreeSpace line 512

    Also declared: ComparatorChallenges/RecursivePotentials.lean:498 (same declaration text).

  85. def OAI.ComparatorModel.RecursivePotentials.ZeroTreeSpace.inclusion line 521

    Also declared: ComparatorChallenges/RecursivePotentials.lean:507 (same declaration text).

  86. def OAI.ComparatorModel.RecursivePotentials.ZeroTreeSpace.projection line 523

    Also declared: ComparatorChallenges/RecursivePotentials.lean:509 (same declaration text).

  87. def OAI.ComparatorModel.RecursivePotentials.ZeroTreeSpace.tail line 526

    Also declared: ComparatorChallenges/RecursivePotentials.lean:512 (same declaration text).

  88. abbrev OAI.ComparatorModel.RecursivePotentials.XZero line 531

    Also declared: ComparatorChallenges/RecursivePotentials.lean:517 (same declaration text).

  89. def OAI.ComparatorModel.RecursivePotentials.ZeroTreeSpace.coordinate line 539

    Distinct definitions of this name: ComparatorChallenges/RecursivePotentials.lean:525 (different declaration text). Qualify references as OAI.ComparatorModel.RecursivePotentials.ZeroTreeSpace.coordinate@path.

  90. def OAI.ComparatorModel.RecursivePotentials.ZeroTreeSpace.P line 542

    Distinct definitions of this name: ComparatorChallenges/RecursivePotentials.lean:528 (different declaration text). Qualify references as OAI.ComparatorModel.RecursivePotentials.ZeroTreeSpace.P@path.

  91. def OAI.ComparatorModel.RecursivePotentials.ZeroTreeSpace.Q line 544

    Distinct definitions of this name: ComparatorChallenges/RecursivePotentials.lean:530 (different declaration text). Qualify references as OAI.ComparatorModel.RecursivePotentials.ZeroTreeSpace.Q@path.

  92. abbrev OAI.ComparatorModel.RecursivePotentials.WeaklyNull line 550

    Also declared: ComparatorChallenges/RecursivePotentials.lean:536 (same declaration text).

  93. abbrev OAI.ComparatorModel.RecursivePotentials.EquivalentNorm line 552

    Also declared: ComparatorChallenges/RecursivePotentials.lean:538 (same declaration text).

  94. abbrev OAI.ComparatorModel.RecursivePotentials.EquivalentNorm.modulus line 558

    Also declared: ComparatorChallenges/RecursivePotentials.lean:544 (same declaration text).

  95. abbrev OAI.ComparatorModel.RecursivePotentials.EquivalentNorm.AUC line 560

    Also declared: ComparatorChallenges/RecursivePotentials.lean:546 (same declaration text).

  96. abbrev OAI.ComparatorModel.RecursivePotentials.IsReflexive line 570

    Also declared: ComparatorChallenges/RecursivePotentials.lean:552 (same declaration text).

  97. abbrev OAI.ComparatorModel.RecursivePotentials.SquareSum.Space line 577

    Also declared: ComparatorChallenges/RecursivePotentials.lean:559 (same declaration text).

  98. abbrev OAI.ComparatorModel.RecursivePotentials.completionEquivOfDense line 587

    Also declared: ComparatorChallenges/RecursivePotentials.lean:565 (same declaration text).

  99. abbrev OAI.ComparatorModel.RecursivePotentials.componentTree line 591

    Also declared: ComparatorChallenges/RecursivePotentials.lean:567 (same declaration text).

  100. abbrev OAI.ComparatorModel.RecursivePotentials.logarithmicGamma line 595

    Distinct definitions of this name: ComparatorChallenges/RecursivePotentials.lean:569 (same statement text; different proof or body). Qualify references as OAI.ComparatorModel.RecursivePotentials.logarithmicGamma@path.

  101. def OAI.ComparatorModel.RecursivePotentials.XJoined_separated_familiesStatement line 603

    Distinct definitions of this name: ComparatorChallenges/RecursivePotentials.lean:575 (same statement text; different proof or body). Qualify references as OAI.ComparatorModel.RecursivePotentials.XJoined_separated_familiesStatement@path.

  102. abbrev OAI.ComparatorModel.RecursivePotentials.ChildExponent line 610

    Also declared: ComparatorChallenges/RecursivePotentials.lean:582 (same declaration text).

  103. abbrev OAI.ComparatorModel.RecursivePotentials.VariableExponent.heightExponent line 614

    Also declared: ComparatorChallenges/RecursivePotentials.lean:586 (same declaration text).

  104. abbrev OAI.ComparatorModel.RecursivePotentials.VariableExponent.cubicConstant line 616

    Also declared: ComparatorChallenges/RecursivePotentials.lean:588 (same declaration text).

  105. abbrev OAI.ComparatorModel.RecursivePotentials.VariableExponent.sixthConstant line 618

    Also declared: ComparatorChallenges/RecursivePotentials.lean:590 (same declaration text).

  106. def OAI.ComparatorModel.RecursivePotentials.VariableTree.P line 629

    Also declared: ComparatorChallenges/RecursivePotentials.lean:601 (same declaration text).

  107. def OAI.ComparatorModel.RecursivePotentials.VariableTree.Q line 633

    Also declared: ComparatorChallenges/RecursivePotentials.lean:605 (same declaration text).

  108. def OAI.ComparatorModel.RecursivePotentials.VariableTree.normSum line 637

    Also declared: ComparatorChallenges/RecursivePotentials.lean:609 (same declaration text).

  109. def OAI.ComparatorModel.RecursivePotentials.AggregationVector line 641

    Also declared: ComparatorChallenges/RecursivePotentials.lean:613 (same declaration text).

  110. instance OAI.ComparatorModel.RecursivePotentials.AggregationVector.(instance at line 648) line 648
  111. instance OAI.ComparatorModel.RecursivePotentials.AggregationVector.(instance at line 650) line 650
  112. instance OAI.ComparatorModel.RecursivePotentials.AggregationVector.(instance at line 652) line 652
  113. instance OAI.ComparatorModel.RecursivePotentials.AggregationVector.(instance at line 654) line 654
  114. class OAI.ComparatorModel.RecursivePotentials.AggregationVector.Construction line 656

    Also declared: ComparatorChallenges/RecursivePotentials.lean:628 (same declaration text).

  115. instance OAI.ComparatorModel.RecursivePotentials.AggregationVector.(instance at line 664) line 664
  116. instance OAI.ComparatorModel.RecursivePotentials.AggregationVector.(instance at line 667) line 667
  117. def OAI.ComparatorModel.RecursivePotentials.AggregationVector.coordinateLinear line 669

    Also declared: ComparatorChallenges/RecursivePotentials.lean:641 (same declaration text).

  118. def OAI.ComparatorModel.RecursivePotentials.AggregationVector.coordinate line 674

    Also declared: ComparatorChallenges/RecursivePotentials.lean:646 (same declaration text).

  119. abbrev OAI.ComparatorModel.RecursivePotentials.AggregationSpace line 684

    Also declared: ComparatorChallenges/RecursivePotentials.lean:656 (same declaration text).

  120. def OAI.ComparatorModel.RecursivePotentials.AggregationSpace.coordinate line 695

    Also declared: ComparatorChallenges/RecursivePotentials.lean:667 (same declaration text).

  121. def OAI.ComparatorModel.RecursivePotentials.AggregationSpace.P line 698

    Also declared: ComparatorChallenges/RecursivePotentials.lean:670 (same declaration text).

  122. def OAI.ComparatorModel.RecursivePotentials.AggregationSpace.Q line 701

    Also declared: ComparatorChallenges/RecursivePotentials.lean:673 (same declaration text).

  123. def OAI.ComparatorModel.RecursivePotentials.AggregationVector.basisVector line 711

    Distinct definitions of this name: ComparatorChallenges/RecursivePotentials.lean:683 (different declaration text). Qualify references as OAI.ComparatorModel.RecursivePotentials.AggregationVector.basisVector@path.

  124. instance OAI.ComparatorModel.RecursivePotentials.ChildExponent.(instance at line 721) line 721
  125. abbrev OAI.ComparatorModel.RecursivePotentials.AggregationVector.CoordinateLp line 733

    Distinct definitions of this name: ComparatorChallenges/RecursivePotentials.lean:703 (different declaration text). Qualify references as OAI.ComparatorModel.RecursivePotentials.AggregationVector.CoordinateLp@path.

  126. def OAI.ComparatorModel.RecursivePotentials.AggregationVector.toLpLinear line 735

    Distinct definitions of this name: ComparatorChallenges/RecursivePotentials.lean:705 (different declaration text). Qualify references as OAI.ComparatorModel.RecursivePotentials.AggregationVector.toLpLinear@path.

  127. class OAI.ComparatorModel.RecursivePotentials.AggregationVector.LpConstruction line 738

    Distinct definitions of this name: ComparatorChallenges/RecursivePotentials.lean:708 (different declaration text). Qualify references as OAI.ComparatorModel.RecursivePotentials.AggregationVector.LpConstruction@path.

  128. def OAI.ComparatorModel.RecursivePotentials.AggregationVector.toLp line 750

    Distinct definitions of this name: ComparatorChallenges/RecursivePotentials.lean:720 (different declaration text). Qualify references as OAI.ComparatorModel.RecursivePotentials.AggregationVector.toLp@path.

  129. def OAI.ComparatorModel.RecursivePotentials.AggregationSpace.lpEquiv line 767

    Distinct definitions of this name: ComparatorChallenges/RecursivePotentials.lean:737 (different declaration text). Qualify references as OAI.ComparatorModel.RecursivePotentials.AggregationSpace.lpEquiv@path.

  130. def OAI.ComparatorModel.RecursivePotentials.Variable.exponent line 785

    Also declared: ComparatorChallenges/RecursivePotentials.lean:755 (same declaration text).

  131. abbrev OAI.ComparatorModel.RecursivePotentials.Variable.Component line 790

    Also declared: ComparatorChallenges/RecursivePotentials.lean:760 (same declaration text).

  132. abbrev OAI.ComparatorModel.RecursivePotentials.Variable.Xv line 792

    Also declared: ComparatorChallenges/RecursivePotentials.lean:762 (same declaration text).

  133. abbrev OAI.ComparatorModel.RecursivePotentials.Variable.Node line 794

    Also declared: ComparatorChallenges/RecursivePotentials.lean:764 (same declaration text).

  134. def OAI.ComparatorModel.RecursivePotentials.Variable.componentEquiv line 796

    Also declared: ComparatorChallenges/RecursivePotentials.lean:766 (same declaration text).

  135. def OAI.ComparatorModel.RecursivePotentials.Variable.componentCoordinate line 809

    Also declared: ComparatorChallenges/RecursivePotentials.lean:779 (same declaration text).

  136. def OAI.ComparatorModel.RecursivePotentials.Variable.coordinate line 812

    Also declared: ComparatorChallenges/RecursivePotentials.lean:782 (same declaration text).

  137. def OAI.ComparatorModel.RecursivePotentials.Variable.basis line 815

    Also declared: ComparatorChallenges/RecursivePotentials.lean:785 (same declaration text).

  138. def OAI.ComparatorModel.RecursivePotentials.Variable.FiniteTotalSupport line 818

    Also declared: ComparatorChallenges/RecursivePotentials.lean:788 (same declaration text).

  139. def OAI.ComparatorModel.RecursivePotentials.Variable.projection line 820

    Also declared: ComparatorChallenges/RecursivePotentials.lean:790 (same declaration text).

  140. def OAI.ComparatorModel.RecursivePotentials.Variable.AdmissibleHeads line 822

    Also declared: ComparatorChallenges/RecursivePotentials.lean:792 (same declaration text).

  141. def OAI.ComparatorModel.RecursivePotentials.Variable.cubic_stabilityStatement line 827

    Distinct definitions of this name: ComparatorChallenges/RecursivePotentials.lean:797 (same statement text; different proof or body). Qualify references as OAI.ComparatorModel.RecursivePotentials.Variable.cubic_stabilityStatement@path.

  142. def OAI.ComparatorModel.RecursivePotentials.Variable.sixth_stabilityStatement line 831

    Distinct definitions of this name: ComparatorChallenges/RecursivePotentials.lean:801 (same statement text; different proof or body). Qualify references as OAI.ComparatorModel.RecursivePotentials.Variable.sixth_stabilityStatement@path.

  143. def OAI.ComparatorModel.RecursivePotentials.Variable.weakTailConstant line 835

    Also declared: ComparatorChallenges/RecursivePotentials.lean:807 (same declaration text).

  144. def OAI.ComparatorModel.RecursivePotentials.Variable.theta line 837

    Also declared: ComparatorChallenges/RecursivePotentials.lean:809 (same declaration text).

  145. def OAI.ComparatorModel.RecursivePotentials.Variable.weak_tailStatement line 839

    Distinct definitions of this name: ComparatorChallenges/RecursivePotentials.lean:811 (same statement text; different proof or body). Qualify references as OAI.ComparatorModel.RecursivePotentials.Variable.weak_tailStatement@path.

  146. def OAI.ComparatorModel.RecursivePotentials.Variable.one_sided_modulus_zeroStatement line 850

    Also declared: ComparatorChallenges/RecursivePotentials.lean:822 (same declaration text).

  147. def OAI.ComparatorModel.RecursivePotentials.Variable.no_equivalent_AUCStatement line 853

    Also declared: ComparatorChallenges/RecursivePotentials.lean:825 (same declaration text).

  148. structure OAI.ComparatorModel.RecursivePotentials.RootSumCompletionStatement line 860

    Also declared: ComparatorChallenges/RecursivePotentials.lean:832 (same declaration text).

  149. structure OAI.ComparatorModel.RecursivePotentials.ZeroRootCompletionStatement line 881

    Also declared: ComparatorChallenges/RecursivePotentials.lean:853 (same declaration text).

  150. def OAI.ComparatorModel.RecursivePotentials.rec_completionStatement line 905

    Also declared: ComparatorChallenges/RecursivePotentials.lean:877 (same declaration text).

  151. def OAI.ComparatorModel.RecursivePotentials.rec_mainStatement line 909

    Also declared: ComparatorChallenges/RecursivePotentials.lean:881 (same declaration text).

  152. def OAI.ComparatorModel.RecursivePotentials.stop_all_radiiStatement line 918

    Distinct definitions of this name: ComparatorChallenges/RecursivePotentials.lean:890 (same statement text; different proof or body). Qualify references as OAI.ComparatorModel.RecursivePotentials.stop_all_radiiStatement@path.

  153. def OAI.ComparatorModel.RecursivePotentials.Variable.nu line 925

    Distinct definitions of this name: ComparatorChallenges/RecursivePotentials.lean:895 (different declaration text). Qualify references as OAI.ComparatorModel.RecursivePotentials.Variable.nu@path.

  154. structure OAI.ComparatorModel.RecursivePotentials.Variable.SourceNormStatement line 929

    Distinct definitions of this name: ComparatorChallenges/RecursivePotentials.lean:899 (different declaration text). Qualify references as OAI.ComparatorModel.RecursivePotentials.Variable.SourceNormStatement@path.

  155. def OAI.ComparatorModel.RecursivePotentials.Variable.spaceStatement line 937

    Distinct definitions of this name: ComparatorChallenges/RecursivePotentials.lean:907 (different declaration text). Qualify references as OAI.ComparatorModel.RecursivePotentials.Variable.spaceStatement@path.

  156. def OAI.ComparatorModel.RecursivePotentials.Variable.aggregateChildren line 948

    Distinct definitions of this name: ComparatorChallenges/RecursivePotentials.lean:918 (different declaration text). Qualify references as OAI.ComparatorModel.RecursivePotentials.Variable.aggregateChildren@path.

  157. def OAI.ComparatorModel.RecursivePotentials.Variable.lpPotentials line 952

    Distinct definitions of this name: ComparatorChallenges/RecursivePotentials.lean:922 (different declaration text). Qualify references as OAI.ComparatorModel.RecursivePotentials.Variable.lpPotentials@path.

  158. def OAI.ComparatorModel.RecursivePotentials.Variable.lp_model_exactStatement line 957

    Distinct definitions of this name: ComparatorChallenges/RecursivePotentials.lean:927 (different declaration text). Qualify references as OAI.ComparatorModel.RecursivePotentials.Variable.lp_model_exactStatement@path.

  159. def OAI.ComparatorModel.RecursivePotentials.MainClaim line 973

    Also declared: ComparatorChallenges/RecursivePotentials.lean:937 (same declaration text).