OAI/Analysis/ModularRecovery/CanonicalTomita.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Canonical square roots, the Tomita graph, and standard modular data.

  1. def OAI.BoundedRecovery.intervalRoot line 17
  2. def OAI.BoundedRecovery.intervalCoRoot line 18
  3. lemma OAI.BoundedRecovery.intervalRoot_nonneg line 20
  4. lemma OAI.BoundedRecovery.intervalCoRoot_nonneg line 23
  5. lemma OAI.BoundedRecovery.intervalRoot_sq line 27
  6. lemma OAI.BoundedRecovery.intervalCoRoot_sq line 31
  7. lemma OAI.BoundedRecovery.intervalRootSum_pos line 36
  8. def OAI.BoundedRecovery.intervalHalfRes line 40
  9. def OAI.BoundedRecovery.intervalRootSumInv line 46
  10. lemma OAI.BoundedRecovery.intervalRootSumInv_mul line 52
  11. lemma OAI.BoundedRecovery.intervalRootSum_mul_halfRes line 57
  12. lemma OAI.BoundedRecovery.halfResolvent_logit line 63
  13. lemma OAI.BoundedRecovery.weightedPullback_halfResolvent line 77
  14. def OAI.BoundedRecovery.CyclicSeparatingData.rootA line 90
  15. def OAI.BoundedRecovery.CyclicSeparatingData.coRootA line 91
  16. lemma OAI.BoundedRecovery.CyclicSeparatingData.rootA_sq line 93
  17. lemma OAI.BoundedRecovery.CyclicSeparatingData.coRootA_sq line 96
  18. lemma OAI.BoundedRecovery.CyclicSeparatingData.rootA_injective line 99
  19. lemma OAI.BoundedRecovery.CyclicSeparatingData.rootA_mul_coRootA line 106
  20. lemma OAI.BoundedRecovery.CyclicSeparatingData.rootSum_injective line 120
  21. lemma OAI.BoundedRecovery.CyclicSeparatingData.D_halfResolvent line 130
  22. lemma OAI.BoundedRecovery.CyclicSeparatingData.halfGraph_iff_roots line 133
  23. lemma OAI.BoundedRecovery.CyclicSeparatingData.Jcl_A line 167
  24. lemma OAI.BoundedRecovery.CyclicSeparatingData.Jcl_B line 176
  25. lemma OAI.BoundedRecovery.CyclicSeparatingData.B_eq_Q_Jcl line 179
  26. lemma OAI.BoundedRecovery.CyclicSeparatingData.graph_iff_roots line 182
  27. lemma OAI.BoundedRecovery.CyclicSeparatingData.graph_iff_halfGraph line 217
  28. lemma OAI.BoundedRecovery.CyclicSeparatingData.graph_iff_closure line 222
  29. lemma OAI.BoundedRecovery.CyclicSeparatingData.tomita_graph line 239
  30. def OAI.BoundedRecovery.CyclicSeparatingData.toStandardModularData line 252