OAI/Geometry/Cannon/Flows/Node.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.CannonNode.SourceNode line 24
  2. def OAI.CannonNode.SourceNode.length line 43
  3. lemma OAI.CannonNode.SourceNode.length_pos line 45
  4. def OAI.CannonNode.SourceNode.child line 47
  5. lemma OAI.CannonNode.SourceNode.child_length line 70
  6. lemma OAI.CannonNode.SourceNode.center_mem line 80
  7. lemma OAI.CannonNode.SourceNode.root line 85
  8. def OAI.CannonMagnification.Expansion line 104
  9. lemma OAI.CannonMagnification.expansion_ball_bounds line 110
  10. theorem OAI.CannonNode.node_level_hits line 152
  11. lemma OAI.CannonNode.exists_node_interval line 175
  12. def OAI.CannonNode.LiteralGood line 205
  13. def OAI.CannonNode.LiteralTransitions line 210
  14. lemma OAI.CannonNode.candidate_slack line 220
  15. theorem OAI.CannonNode.eventually_scaled_subdivision line 246
  16. structure OAI.CannonFlow.FiniteFlow line 370
  17. lemma OAI.CannonFlow.FiniteFlow.conserve_expectation line 385
  18. lemma OAI.CannonFlow.FiniteFlow.total_mass line 395
  19. def OAI.CannonFlow.FiniteFlow.badCount line 402
  20. def OAI.CannonFlow.FiniteFlow.expectedBad line 406
  21. def OAI.CannonFlow.FiniteFlow.badMass line 408
  22. def OAI.CannonFlow.FiniteFlow.goodMass line 410
  23. lemma OAI.CannonFlow.FiniteFlow.badMass_nonneg line 412
  24. lemma OAI.CannonFlow.FiniteFlow.good_add_bad line 418
  25. lemma OAI.CannonFlow.FiniteFlow.expectedBad_succ line 427
  26. lemma OAI.CannonFlow.FiniteFlow.expectedBad_eq_sum line 435
  27. lemma OAI.CannonFlow.FiniteFlow.expectedBad_bound line 440
  28. theorem OAI.CannonFlow.FiniteFlow.arbitrarily_late_good_levels line 462
  29. lemma OAI.CannonFlow.probabilities_of_capacity line 494
  30. lemma OAI.CannonFlow.probabilities_of_mixed_capacity line 505
  31. lemma OAI.CannonFlow.FiniteFlow.weight_le_one line 522
  32. lemma OAI.CannonFlow.FiniteFlow.linear_transition_product line 526
  33. lemma OAI.CannonFlow.FiniteFlow.badCount_exp_succ line 551
  34. lemma OAI.CannonFlow.FiniteFlow.quadratic_transition_product line 560
  35. theorem OAI.CannonFlow.FiniteFlow.good_levels_of_transitions line 588