OAI/Dynamics/StandardMap/TreeLine.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.StandardMapEntropy.TreeLine line 11
  2. lemma OAI.StandardMapEntropy.realArray_treeLine line 18
  3. def OAI.StandardMapEntropy.lineB line 22
  4. lemma OAI.StandardMapEntropy.TreeLine.self line 26
  5. lemma OAI.StandardMapEntropy.TreeLine.reverse line 30
  6. lemma OAI.StandardMapEntropy.TreeLine.b_nonneg line 34
  7. lemma OAI.StandardMapEntropy.TreeLine.b_symm line 38
  8. lemma OAI.StandardMapEntropy.TreeLine.min_b line 40
  9. lemma OAI.StandardMapEntropy.TreeLine.b_nonbacktrack line 42
  10. def OAI.StandardMapEntropy.NoFastCancellation line 50
  11. def OAI.StandardMapEntropy.ExteriorUnitRays line 53
  12. lemma OAI.StandardMapEntropy.matched_ray_distance line 56
  13. lemma OAI.StandardMapEntropy.crossing_excess_bound line 87
  14. lemma OAI.StandardMapEntropy.exterior_ray_crossloss line 140
  15. lemma OAI.StandardMapEntropy.exterior_ray_shortfall line 187
  16. lemma OAI.StandardMapEntropy.exterior_rays_nondegenerate line 198