OAI/Combinatorics/SumProduct/Alignment/PivotPaths01.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SourceRawPrefix.Earlier line 26
  2. def OAI.SourceRawPrefix.Through line 29
  3. lemma OAI.SourceRawPrefix.Earlier.update_iff line 32
  4. lemma OAI.SourceRawPrefix.Through.earlier line 38
  5. lemma OAI.SourceRawPrefix.earlier_univ line 45
  6. lemma OAI.SourceRawPrefix.through_inter line 49
  7. theorem OAI.SourceRawPrefix.resample_preserves line 56
  8. lemma OAI.SourceRawPrefix.raw_resample line 95
  9. lemma OAI.SourceRawPrefix.raw_resample_real line 102
  10. abbrev OAI.SourcePivotPaths.ScalarModels line 130
  11. def OAI.SourcePivotPaths.comparison line 133
  12. def OAI.SourcePivotPaths.outcome line 147
  13. def OAI.SourcePivotPaths.success line 151
  14. lemma OAI.SourcePivotPaths.comparison_congr line 156
  15. lemma OAI.SourcePivotPaths.comparison_through line 171
  16. lemma OAI.SourcePivotPaths.outcome_through line 178
  17. lemma OAI.SourcePivotPaths.success_through line 189
  18. lemma OAI.SourcePivotPaths.success_update_iff line 200
  19. def OAI.SourcePivotPaths.scalarModels line 227
  20. lemma OAI.SourcePivotPaths.original_success line 232
  21. theorem OAI.SourcePivotPaths.success_mass_resample line 252