OAI/Analysis/TreePotential/SegmentMixtures.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.BoundedTreePotentials.Segments.coreLift_norm line 13
  2. lemma OAI.BoundedTreePotentials.Segments.norm_segment_sum line 16
  3. def OAI.BoundedTreePotentials.Segments.Atom.replaced line 36
  4. def OAI.BoundedTreePotentials.Segments.Atom.replacement line 39
  5. lemma OAI.BoundedTreePotentials.Segments.Atom.inCore_sum line 42
  6. lemma OAI.BoundedTreePotentials.Segments.Atom.replacement_error line 46
  7. lemma OAI.BoundedTreePotentials.Segments.Segment.ext line 64
  8. def OAI.BoundedTreePotentials.Segments.Segment.suffixAt line 72
  9. lemma OAI.BoundedTreePotentials.Segments.Segment.suffixAt_start line 75
  10. lemma OAI.BoundedTreePotentials.Segments.Segment.suffixAt_finish line 79
  11. lemma OAI.BoundedTreePotentials.Segments.Segment.suffixAt_eq line 83
  12. def OAI.BoundedTreePotentials.Segments.segmentCutVector line 88
  13. lemma OAI.BoundedTreePotentials.Segments.cutVector_apply line 91
  14. lemma OAI.BoundedTreePotentials.Segments.core_tail_segment line 95
  15. lemma OAI.BoundedTreePotentials.Segments.cutVector_empty line 105
  16. lemma OAI.BoundedTreePotentials.Segments.cutVector_segment line 109
  17. lemma OAI.BoundedTreePotentials.Segments.eval_ne_zero_start line 113
  18. lemma OAI.BoundedTreePotentials.Segments.Segment.exit_unique line 121
  19. lemma OAI.BoundedTreePotentials.Segments.segment_exit_decomposition line 127
  20. def OAI.BoundedTreePotentials.Segments.Atom.terminal line 151
  21. lemma OAI.BoundedTreePotentials.Segments.Atom.terminal_start line 153
  22. lemma OAI.BoundedTreePotentials.Segments.Atom.exit_piece_sum line 155
  23. lemma OAI.BoundedTreePotentials.Segments.Atom.replacement_exits line 170
  24. lemma OAI.BoundedTreePotentials.Segments.core_norm_le_tests line 184
  25. lemma OAI.BoundedTreePotentials.Segments.test_coreLift line 189
  26. lemma OAI.BoundedTreePotentials.Segments.unit_exit_family line 193
  27. lemma OAI.BoundedTreePotentials.Segments.norm_exit_mixture line 208
  28. lemma OAI.BoundedTreePotentials.Segments.eval_antichainTest line 263
  29. lemma OAI.BoundedTreePotentials.Segments.unit_antichainTest line 271
  30. lemma OAI.BoundedTreePotentials.Segments.coordinate_coreLift line 309
  31. lemma OAI.BoundedTreePotentials.Segments.head_test_sum line 313
  32. lemma OAI.BoundedTreePotentials.Segments.antichain_coordinates_sq line 329
  33. lemma OAI.BoundedTreePotentials.Segments.coordinate_exit_segment line 363
  34. lemma OAI.BoundedTreePotentials.Segments.coordinates_exit_mixture line 377
  35. lemma OAI.BoundedTreePotentials.Segments.signed_exit_mass_sq line 391