OAI/Combinatorics/Progressions/Estimates/UnitVerticalNativeInverseModels.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.exists_native_derivative_correlators line 11
  2. theorem OAI.Erdos3.exists_native_degree_one_derivative_correlators line 31
  3. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_common_observable_correlators line 63
  4. structure OAI.Erdos3.NativeUnitVerticalData line 146
  5. def OAI.Erdos3.NativeUnitVerticalData.mono line 168
  6. def OAI.Erdos3.NativeUnitVerticalData.test line 181
  7. theorem OAI.Erdos3.NativeUnitVerticalData.test_zero_evalCyclic line 190
  8. theorem OAI.Erdos3.NativeUnitVerticalData.test_normalized line 194
  9. theorem OAI.Erdos3.NativeUnitVerticalData.test_complexity line 198
  10. theorem OAI.Erdos3.NativeUnitVerticalData.test_zero_correlation line 205
  11. theorem OAI.Erdos3.exists_native_inverse_quadruples line 231
  12. theorem OAI.Erdos3.exists_native_common_derivative_models line 285
  13. theorem OAI.Erdos3.NativeCommonDerivativeModels.exists_large_common_observable line 367
  14. theorem OAI.Erdos3.exists_native_unit_vertical_data line 385
  15. theorem OAI.Erdos3.exists_normalized_native_inverse_models line 426
  16. theorem OAI.Erdos3.exists_vertical_native_inverse_models line 454
  17. theorem OAI.Erdos3.exists_unit_vertical_native_inverse_models line 481