OAI/Probability/SKGap/Localization/Map.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKGap.Noncrossing.Diagram.NoiseSplit.map line 23
  2. lemma OAI.SKGap.Noncrossing.Diagram.NoiseSplit.map_bijective line 29
  3. def OAI.SKGap.Noncrossing.Diagram.NoiseSplit.mapEquiv line 49
  4. def OAI.SKGap.Noncrossing.Diagram.NoiseSplit.appendLeft line 53
  5. def OAI.SKGap.Noncrossing.Diagram.NoiseSplit.appendRight line 58
  6. def OAI.SKGap.Noncrossing.Diagram.NoiseSplit.appendMap line 64
  7. lemma OAI.SKGap.Noncrossing.Diagram.take_noise_drop line 68
  8. lemma OAI.SKGap.Noncrossing.Diagram.NoiseSplit.appendMap_bijective line 74
  9. def OAI.SKGap.Noncrossing.Diagram.NoiseSplit.appendEquiv line 137
  10. lemma OAI.SKGap.Noncrossing.Diagram.NoiseSplit.sum_append line 141
  11. lemma OAI.SKGap.Noncrossing.InverseDiagram.expandBlocks_injective line 162
  12. lemma OAI.SKGap.Noncrossing.InverseDiagram.blockDegree_append line 179
  13. def OAI.SKGap.Noncrossing.InverseDiagram.SplitBlocks line 182
  14. def OAI.SKGap.Noncrossing.InverseDiagram.SplitChoices line 183
  15. def OAI.SKGap.Noncrossing.InverseDiagram.MarkedBlocks line 184
  16. instance OAI.SKGap.Noncrossing.InverseDiagram.splitChoicesFintype line 186
  17. instance OAI.SKGap.Noncrossing.InverseDiagram.markedBlocksFintype line 188
  18. def OAI.SKGap.Noncrossing.InverseDiagram.splitChoice line 191
  19. lemma OAI.SKGap.Noncrossing.InverseDiagram.splitChoice_bijective line 197
  20. def OAI.SKGap.Noncrossing.InverseDiagram.splitChoiceEquiv line 216
  21. instance OAI.SKGap.Noncrossing.InverseDiagram.splitBlocksFintype line 218
  22. def OAI.SKGap.Noncrossing.InverseDiagram.splitToMarked line 221
  23. lemma OAI.SKGap.Noncrossing.InverseDiagram.splitToMarked_bijective line 229
  24. def OAI.SKGap.Noncrossing.InverseDiagram.markedBlockEquiv line 253
  25. theorem OAI.SKGap.Noncrossing.InverseDiagram.sum_marked_blocks line 256