OAI/Geometry/PeriodicTiling/ActivationTiles.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PeriodicTilingThree.activationBatch line 15
  2. theorem OAI.PeriodicTilingThree.mem_activationBatch line 23
  3. theorem OAI.PeriodicTilingThree.activationBatch_nonempty line 38
  4. theorem OAI.PeriodicTilingThree.activationBatch_q0 line 49
  5. theorem OAI.PeriodicTilingThree.activationBatch_disjoint line 63
  6. def OAI.PeriodicTilingThree.activationSource line 72
  7. theorem OAI.PeriodicTilingThree.activationSource_eq_sub line 75
  8. theorem OAI.PeriodicTilingThree.activationSource_shear line 85
  9. def OAI.PeriodicTilingThree.targetBeta line 92
  10. theorem OAI.PeriodicTilingThree.shear_targetBeta line 95
  11. theorem OAI.PeriodicTilingThree.targetBeta_point line 100
  12. theorem OAI.PeriodicTilingThree.difference_mem_activationBatch line 105
  13. def OAI.PeriodicTilingThree.ordinaryActivationTile line 174
  14. def OAI.PeriodicTilingThree.seedActivationTile line 180
  15. def OAI.PeriodicTilingThree.ordinarySource line 186
  16. def OAI.PeriodicTilingThree.seedSource line 189
  17. theorem OAI.PeriodicTilingThree.ordinarySource_horizontal line 192
  18. theorem OAI.PeriodicTilingThree.ordinarySource_own line 196
  19. theorem OAI.PeriodicTilingThree.seedSource_horizontal line 201
  20. theorem OAI.PeriodicTilingThree.seedSource_own line 205
  21. theorem OAI.PeriodicTilingThree.ordinarySource_lineValue line 210
  22. theorem OAI.PeriodicTilingThree.seedSource_residue line 217
  23. def OAI.PeriodicTilingThree.ordinaryActivationMap line 227
  24. def OAI.PeriodicTilingThree.seedActivationMap line 232
  25. def OAI.PeriodicTilingThree.ordinaryTarget line 237
  26. def OAI.PeriodicTilingThree.seedTarget line 240
  27. theorem OAI.PeriodicTilingThree.ordinarySource_injective line 244
  28. theorem OAI.PeriodicTilingThree.seedSource_injective line 251
  29. theorem OAI.PeriodicTilingThree.difference_mem_ordinaryActivationTile line 258
  30. theorem OAI.PeriodicTilingThree.difference_mem_seedActivationTile line 282
  31. theorem OAI.PeriodicTilingThree.existsUnique_source_iff line 307
  32. theorem OAI.PeriodicTilingThree.ordinaryTarget_surjective line 321
  33. theorem OAI.PeriodicTilingThree.seedTarget_surjective line 331
  34. theorem OAI.PeriodicTilingThree.ordinaryActivationTile_iff line 341
  35. theorem OAI.PeriodicTilingThree.seedActivationTile_iff line 356
  36. theorem OAI.PeriodicTilingThree.ordinaryActivationTile_nonempty line 371
  37. theorem OAI.PeriodicTilingThree.seedActivationTile_nonempty line 383