OAI/Combinatorics/SumProduct/Alignment/PivotExtension02.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SourcePivotExtension.unit_atom_pos line 20
2. lemma OAI.SourcePivotExtension.outside_atom_pos line 31
3. lemma OAI.SourcePivotExtension.label_source_cell line 39
4. lemma OAI.SourcePivotExtension.full_support_mem line 51
5. lemma OAI.SourcePivotExtension.raw_cell_product line 58
6. lemma OAI.SourcePivotExtension.joint_rectangle_real line 73
7. theorem OAI.SourcePivotExtension.conditional_slot_source_ratio line 84
8. abbrev OAI.SourceIntegerArrays.GlobalJoint.SourceFrozenFamily.slotCount line 165
9. def OAI.SourceIntegerArrays.GlobalJoint.SourceFrozenFamily.rawSlot line 166
10. def OAI.SourceIntegerArrays.GlobalJoint.SourceFrozenFamily.pivotSet line 169
11. theorem OAI.SourceIntegerArrays.GlobalJoint.SourceFrozenFamily.source_posterior_domination line 173
12. def OAI.SourceIntegerArrays.GlobalJoint.SourceFrozenFamily.slotBudget line 257
13. theorem OAI.SourceIntegerArrays.GlobalJoint.SourceFrozenFamily.source_actual_extension line 260