OAI/Analysis/CharacterCriterion/DiagonalIteration.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.KirchbergRordam.DiagonalIteration.conj line 38
  2. lemma OAI.KirchbergRordam.DiagonalIteration.conj_mul line 39
  3. lemma OAI.KirchbergRordam.DiagonalIteration.conj_one line 41
  4. lemma OAI.KirchbergRordam.DiagonalIteration.conj_star line 42
  5. lemma OAI.KirchbergRordam.DiagonalIteration.normalize_cancel line 45
  6. def OAI.KirchbergRordam.DiagonalIteration.piUnitary line 49
  7. lemma OAI.KirchbergRordam.DiagonalIteration.piUnitary_continuous line 51
  8. lemma OAI.KirchbergRordam.DiagonalIteration.mapUnitary_continuous line 56
  9. lemma OAI.KirchbergRordam.DiagonalIteration.map_pi_conj line 58
  10. structure OAI.KirchbergRordam.DiagonalIteration.System line 65
  11. def OAI.KirchbergRordam.DiagonalIteration.System.flat line 77
  12. def OAI.KirchbergRordam.DiagonalIteration.System.full line 80
  13. def OAI.KirchbergRordam.DiagonalIteration.System.unitaryPath line 84
  14. lemma OAI.KirchbergRordam.DiagonalIteration.System.full_eq line 89
  15. lemma OAI.KirchbergRordam.DiagonalIteration.System.flat_continuous line 97
  16. lemma OAI.KirchbergRordam.DiagonalIteration.System.unitaryPath_continuous line 104
  17. lemma OAI.KirchbergRordam.DiagonalIteration.System.flat_bound line 111
  18. lemma OAI.KirchbergRordam.DiagonalIteration.System.flat_eventually_small line 132
  19. abbrev OAI.KirchbergRordam.BalancedDropIteration.diagonalSystem line 154
  20. lemma OAI.KirchbergRordam.BalancedDropIteration.eigen_lipschitz line 162
  21. lemma OAI.KirchbergRordam.BalancedDropIteration.iterate_full line 179
  22. def OAI.KirchbergRordam.BalancedDropIteration.normalizedPath line 191
  23. lemma OAI.KirchbergRordam.BalancedDropIteration.normalizedPath_continuous line 194
  24. lemma OAI.KirchbergRordam.BalancedDropIteration.normalizedPath_zero line 196
  25. lemma OAI.KirchbergRordam.BalancedDropIteration.untwist line 199
  26. lemma OAI.KirchbergRordam.BalancedDropIteration.untwist_norm line 206
  27. lemma OAI.KirchbergRordam.BalancedDropIteration.eventually_untwist_small line 214
  28. abbrev OAI.KirchbergRordam.FiniteHalfFlipSequence.conj line 229
  29. lemma OAI.KirchbergRordam.FiniteHalfFlipSequence.perturbation line 231
  30. theorem OAI.KirchbergRordam.FiniteHalfFlipSequence.exists_sequence line 246
  31. lemma OAI.KirchbergRordam.CStarInductiveLimit.approximation_common_stage line 273
  32. def OAI.KirchbergRordam.BalancedDropHalfFlip.squareMap line 293
  33. lemma OAI.KirchbergRordam.BalancedDropHalfFlip.squareMap_left line 296
  34. lemma OAI.KirchbergRordam.BalancedDropHalfFlip.squareMap_right line 299
  35. lemma OAI.KirchbergRordam.BalancedDropHalfFlip.control_map line 303
  36. lemma OAI.KirchbergRordam.BalancedDropHalfFlip.finite_stage line 310
  37. lemma OAI.KirchbergRordam.BalancedDropHalfFlip.common_stage line 333
  38. lemma OAI.KirchbergRordam.BalancedDropHalfFlip.finite_control line 337
  39. theorem OAI.KirchbergRordam.BalancedDropHalfFlip.exists_half_flip line 353