OAI/Probability/ThorpRouting/Harmonic/Model.lean

GitHub source file

59 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ThorpNine.Harmonic.Thorp.Card line 11

    Also declared: ComparatorChallenges/CoordinateTrace.lean:11 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:89 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1180 (same declaration text).

  2. def OAI.ThorpNine.Harmonic.Thorp.switchFun line 13

    Also declared: ComparatorChallenges/CoordinateTrace.lean:13 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:91 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1182 (same declaration text).

  3. theorem OAI.ThorpNine.Harmonic.Thorp.switchFun_involutive line 16

    Also declared: ComparatorChallenges/CoordinateTrace.lean:16 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:94 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1185 (same declaration text).

  4. def OAI.ThorpNine.Harmonic.Thorp.pairSwitch line 25

    Also declared: ComparatorChallenges/CoordinateTrace.lean:25 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:103 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1194 (same declaration text).

  5. def OAI.ThorpNine.Harmonic.Thorp.Butterfly line 31

    Also declared: ComparatorChallenges/ThorpRouting.lean:1200 (same declaration text).

  6. def OAI.ThorpNine.Harmonic.Thorp.childLift line 35

    Also declared: ComparatorChallenges/ThorpRouting.lean:1204 (same declaration text).

  7. def OAI.ThorpNine.Harmonic.Thorp.butterflyPerm line 41

    Also declared: ComparatorChallenges/ThorpRouting.lean:1210 (same declaration text).

  8. def OAI.ThorpNine.Harmonic.Thorp.finiteMean line 45

    Also declared: ComparatorChallenges/ThorpRouting.lean:1214 (same declaration text).

  9. def OAI.ThorpNine.Harmonic.Thorp.SwitchIndex line 48

    Also declared: ComparatorChallenges/ThorpRouting.lean:1217 (same declaration text).

  10. instance OAI.ThorpNine.Harmonic.Thorp.(instance at line 52) line 52
  11. instance OAI.ThorpNine.Harmonic.Thorp.(instance at line 57) line 57
  12. def OAI.ThorpNine.Harmonic.Thorp.decodeButterfly line 62

    Also declared: ComparatorChallenges/ThorpRouting.lean:1231 (same declaration text).

  13. def OAI.ThorpNine.Harmonic.Thorp.PairRouting.tupleProbability line 74

    Also declared: ComparatorChallenges/ThorpRouting.lean:1243 (same declaration text).

  14. abbrev OAI.ThorpNine.Harmonic.Thorp.BenesCoins line 85

    Also declared: ComparatorChallenges/ThorpRouting.lean:1254 (same declaration text).

  15. def OAI.ThorpNine.Harmonic.Thorp.palindromePerm line 87

    Also declared: ComparatorChallenges/ThorpRouting.lean:1256 (same declaration text).

  16. abbrev OAI.ThorpNine.Harmonic.Thorp.Specht.Cell line 95

    Also declared: ComparatorChallenges/CoordinateTrace.lean:67 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:155 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1264 (same declaration text).

  17. def OAI.ThorpNine.Harmonic.Thorp.Specht.row line 97

    Also declared: ComparatorChallenges/CoordinateTrace.lean:69 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:157 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1266 (same declaration text).

  18. def OAI.ThorpNine.Harmonic.Thorp.Specht.col line 99

    Also declared: ComparatorChallenges/CoordinateTrace.lean:71 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:159 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1268 (same declaration text).

  19. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.row_lt_colLen line 101

    Also declared: ComparatorChallenges/CoordinateTrace.lean:73 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:161 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1270 (same declaration text).

  20. def OAI.ThorpNine.Harmonic.Thorp.Specht.rowIndex line 104

    Also declared: ComparatorChallenges/CoordinateTrace.lean:76 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:164 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1273 (same declaration text).

  21. abbrev OAI.ThorpNine.Harmonic.Thorp.Specht.Tabloid line 107

    Also declared: ComparatorChallenges/CoordinateTrace.lean:79 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:167 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1276 (same declaration text).

  22. instance OAI.ThorpNine.Harmonic.Thorp.Specht.(instance at line 110) line 110
  23. def OAI.ThorpNine.Harmonic.Thorp.Specht.baseTabloid line 112

    Also declared: ComparatorChallenges/CoordinateTrace.lean:84 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:172 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1281 (same declaration text).

  24. def OAI.ThorpNine.Harmonic.Thorp.Specht.tabloidAct line 114

    Also declared: ComparatorChallenges/CoordinateTrace.lean:86 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:174 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1283 (same declaration text).

  25. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.tabloidAct_apply line 129

    Also declared: ComparatorChallenges/CoordinateTrace.lean:101 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:189 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1298 (same declaration text).

  26. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.tabloidAct_one line 132

    Also declared: ComparatorChallenges/CoordinateTrace.lean:104 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:192 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1301 (same declaration text).

  27. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.tabloidAct_mul line 136

    Also declared: ComparatorChallenges/CoordinateTrace.lean:108 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:196 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1305 (same declaration text).

  28. def OAI.ThorpNine.Harmonic.Thorp.Specht.tabloidRep line 141

    Also declared: ComparatorChallenges/CoordinateTrace.lean:113 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:201 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1310 (same declaration text).

  29. def OAI.ThorpNine.Harmonic.Thorp.Specht.delta line 153

    Also declared: ComparatorChallenges/CoordinateTrace.lean:125 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:213 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1322 (same declaration text).

  30. def OAI.ThorpNine.Harmonic.Thorp.Specht.colGroup line 156

    Also declared: ComparatorChallenges/CoordinateTrace.lean:128 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:216 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1325 (same declaration text).

  31. def OAI.ThorpNine.Harmonic.Thorp.Specht.permSign line 162

    Also declared: ComparatorChallenges/CoordinateTrace.lean:134 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:222 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1331 (same declaration text).

  32. def OAI.ThorpNine.Harmonic.Thorp.Specht.alternator line 169

    Also declared: ComparatorChallenges/CoordinateTrace.lean:143 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:228 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1338 (same declaration text).

  33. def OAI.ThorpNine.Harmonic.Thorp.Specht.polytabloid line 176

    Also declared: ComparatorChallenges/CoordinateTrace.lean:153 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:235 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1345 (same declaration text).

  34. def OAI.ThorpNine.Harmonic.Thorp.Specht.space line 179

    Also declared: ComparatorChallenges/CoordinateTrace.lean:156 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:238 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1348 (same declaration text).

  35. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.orbit_mem_space line 182

    Also declared: ComparatorChallenges/CoordinateTrace.lean:159 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:241 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1351 (same declaration text).

  36. lemma OAI.ThorpNine.Harmonic.Thorp.Specht.action_mem_space line 185

    Also declared: ComparatorChallenges/CoordinateTrace.lean:162 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:244 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1354 (same declaration text).

  37. def OAI.ThorpNine.Harmonic.Thorp.Specht.subrepresentation line 197

    Also declared: ComparatorChallenges/CoordinateTrace.lean:174 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:256 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1366 (same declaration text).

  38. def OAI.ThorpNine.Harmonic.Thorp.Specht.representation line 200

    Also declared: ComparatorChallenges/CoordinateTrace.lean:177 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:259 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1369 (same declaration text).

  39. abbrev OAI.ThorpNine.Harmonic.Thorp.PermutationHilbert.H line 211

    Also declared: ComparatorChallenges/CoordinateTrace.lean:188 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:270 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1380 (same declaration text).

  40. def OAI.ThorpNine.Harmonic.Thorp.Specht.hilbertEquiv line 218

    Also declared: ComparatorChallenges/CoordinateTrace.lean:195 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:277 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1387 (same declaration text).

  41. def OAI.ThorpNine.Harmonic.Thorp.Specht.hilbertSpace line 222

    Also declared: ComparatorChallenges/CoordinateTrace.lean:199 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:281 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1391 (same declaration text).

  42. def OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.continuousRepresentation line 234

    Also declared: ComparatorChallenges/CoordinateTrace.lean:209 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:293 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1403 (same declaration text).

  43. def OAI.ThorpNine.Harmonic.Thorp.UnitaryFinite.sampleOperator line 245

    Also declared: ComparatorChallenges/CoordinateTrace.lean:222 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:304 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1414 (same declaration text).

  44. def OAI.ThorpNine.Harmonic.Thorp.Specht.spaceHilbertEquiv line 253

    Also declared: ComparatorChallenges/CoordinateTrace.lean:230 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:312 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1422 (same declaration text).

  45. def OAI.ThorpNine.Harmonic.Thorp.Specht.unitaryRepresentation line 256

    Distinct definitions of this name: ComparatorChallenges/CoordinateTrace.lean:233 (same statement text; different proof or body), ComparatorChallenges/ThorpRemaining.lean:315 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1425 (same declaration text). Qualify references as OAI.ThorpNine.Harmonic.Thorp.Specht.unitaryRepresentation@path.

  46. def OAI.ThorpNine.Harmonic.Thorp.Specht.relabelledUnitary line 262

    Also declared: ComparatorChallenges/CoordinateTrace.lean:243 (same declaration text), ComparatorChallenges/ThorpRemaining.lean:321 (same declaration text), ComparatorChallenges/ThorpRouting.lean:1431 (same declaration text).

  47. def OAI.ThorpNine.Harmonic.Thorp.SparseContact.sweepOperator line 271

    Also declared: ComparatorChallenges/ThorpRouting.lean:1440 (same declaration text).

  48. def OAI.ThorpNine.Harmonic.Thorp.StrongSmoothing.coordinateRelabel line 282

    Also declared: ComparatorChallenges/ThorpRouting.lean:1451 (same declaration text).

  49. def OAI.ThorpNine.Harmonic.Thorp.StrongSmoothing.sweep line 288

    Also declared: ComparatorChallenges/ThorpRouting.lean:1457 (same declaration text).

  50. abbrev OAI.ThorpNine.Harmonic.Thorp.StrongSmoothing.Tuples line 293

    Also declared: ComparatorChallenges/ThorpRouting.lean:1462 (same declaration text).

  51. def OAI.ThorpNine.Harmonic.Thorp.StrongSmoothing.sweepKernel line 295

    Also declared: ComparatorChallenges/ThorpRouting.lean:1464 (same declaration text).

  52. def OAI.ThorpNine.Harmonic.Thorp.StrongSmoothing.reflectedKernel line 299

    Also declared: ComparatorChallenges/ThorpRouting.lean:1468 (same declaration text).

  53. def OAI.ThorpNine.Harmonic.Thorp.StrongTail.tailDiagram line 310

    Also declared: ComparatorChallenges/ThorpRouting.lean:1479 (same declaration text).

  54. def OAI.ThorpNine.Harmonic.Thorp.Casimir.levelScale line 319

    Also declared: ComparatorChallenges/ThorpRouting.lean:1488 (same declaration text).

  55. def OAI.ThorpNine.Harmonic.Thorp.Casimir.K line 322

    Also declared: ComparatorChallenges/ThorpRouting.lean:1491 (same declaration text).

  56. abbrev OAI.ThorpNine.Harmonic.Thorp.HarmonicBounds.tail line 333

    Also declared: ComparatorChallenges/ThorpRouting.lean:1502 (same declaration text).

  57. def OAI.ThorpNine.Harmonic.Thorp.HarmonicBounds.W line 335

    Also declared: ComparatorChallenges/ThorpRouting.lean:1504 (same declaration text).

  58. def OAI.ThorpNine.Harmonic.Thorp.HarmonicBounds.tupleTrace line 337

    Also declared: ComparatorChallenges/ThorpRouting.lean:1506 (same declaration text).

  59. def OAI.ThorpNine.Harmonic.Thorp.HarmonicBounds.MainStatement line 340

    Also declared: ComparatorChallenges/ThorpRouting.lean:1509 (same declaration text).