OAI/Combinatorics/SumProduct/Alignment/IntegerArrays15.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SourceIntegerArrays.GlobalJoint.SourceFrozenFamily.residue_abs_le line 31
2. lemma OAI.SourceIntegerArrays.GlobalJoint.SourceFrozenFamily.actual_slot_bound line 40
3. lemma OAI.SourceIntegerArrays.GlobalJoint.SourceFrozenFamily.source_heightCoeff_bound line 53
4. lemma OAI.SourceIntegerArrays.GlobalJoint.SourceFrozenFamily.perm_inside line 65
5. lemma OAI.SourceIntegerArrays.GlobalJoint.SourceFrozenFamily.reconstruct_outside_bound line 73
6. lemma OAI.SourceIntegerArrays.GlobalJoint.SourceFrozenFamily.source_qValue_bound line 91
7. def OAI.SourceIntegerArrays.GlobalJoint.SourceFrozenFamily.previousProduct line 129
8. lemma OAI.SourceIntegerArrays.GlobalJoint.SourceFrozenFamily.previousProduct_pos line 132
9. lemma OAI.SourceIntegerArrays.GlobalJoint.SourceFrozenFamily.le_previousProduct line 136
10. lemma OAI.SourceIntegerArrays.GlobalJoint.SourceFrozenFamily.tail_product_le_previous line 140
11. def OAI.SourceIntegerArrays.GlobalJoint.SourceFrozenFamily.modelBudget line 162
12. lemma OAI.SourceIntegerArrays.GlobalJoint.SourceFrozenFamily.modelBudget_nonneg line 169
13. lemma OAI.SourceIntegerArrays.GlobalJoint.SourceFrozenFamily.modelBudget_slot line 173
14. lemma OAI.SourceIntegerArrays.GlobalJoint.SourceFrozenFamily.modelBudget_input line 180
15. theorem OAI.SourceIntegerArrays.GlobalJoint.SourceFrozenFamily.source_actual_harmonic line 213