OAI/Combinatorics/Progressions/Estimates/PreparedRelativeInitializerScalarInputs.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Erdos3.preparationCoordinateCap_mono line 11
2. theorem OAI.Erdos3.preparedRelativeInitializer_padded_coordinate_card_le line 23
3. abbrev OAI.Erdos3.preparedRelativeInitializerVariableCount line 34
4. theorem OAI.Erdos3.preparedRelativeInitializerVariableCount_le line 44
5. theorem OAI.Erdos3.preparedRelativeInitializerVariableCount_le_dimension line 60
6. theorem OAI.Erdos3.early_input_components line 82
7. theorem OAI.Erdos3.exists_preparedRelative_structural_input_power line 99
8. theorem OAI.Erdos3.exists_preparedRelative_candidate_input_powers line 136
9. structure OAI.Erdos3.PreparedRelativeInitializerScalarInputs line 191
10. theorem OAI.Erdos3.preparedRelativeInitializer_scalarInputs_of_bounds line 211
11. theorem OAI.Erdos3.preparedRelativeInitializer_scalarInputs line 248