OAI/Combinatorics/SumProduct/Alignment/PivotPaths02.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SourceIntegerArrays.GlobalJoint.SourceFrozenFamily.source_uniform_prefix_extension line 51
  2. def OAI.SourcePivotPaths.sourcePlan line 168
  3. def OAI.SourcePivotPaths.gain line 172
  4. lemma OAI.SourcePivotPaths.gain_pos line 175
  5. lemma OAI.SourcePivotPaths.gain_le_one line 180
  6. def OAI.SourcePivotPaths.delta line 188
  7. def OAI.SourcePivotPaths.errorCost line 192
  8. lemma OAI.SourcePivotPaths.delta_pos line 196
  9. lemma OAI.SourcePivotPaths.delta_le_one line 201
  10. def OAI.SourcePivotPaths.runSuccess line 211
  11. theorem OAI.SourcePivotPaths.runSuccess_final line 218
  12. def OAI.SourcePivotPaths.stepBounds line 242
  13. lemma OAI.SourcePivotPaths.through_disjointed line 252
  14. theorem OAI.SourcePivotPaths.iterate_mass line 262
  15. def OAI.SourcePivotPaths.localEstimates line 325
  16. lemma OAI.SourcePivotPaths.eventually_stepBounds line 338
  17. theorem OAI.SourcePivotPaths.iterate_eventually line 355
  18. theorem OAI.SourcePivotPaths.eventual_final_alignment line 377