OAI/Combinatorics/Progressions/Estimates/BooleanMinorDimension.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.booleanSamplerMap line 18
  2. def OAI.Erdos3.booleanSelectedMinor line 22
  3. theorem OAI.Erdos3.booleanSamplerMap_formula line 27
  4. theorem OAI.Erdos3.booleanSamplerMap_contDiff line 35
  5. theorem OAI.Erdos3.booleanSelectedMinor_degreeOf_le line 39
  6. theorem OAI.Erdos3.booleanSelectedMinor_fderiv line 46
  7. theorem OAI.Erdos3.booleanSelectedMinor_specialization line 58
  8. theorem OAI.Erdos3.booleanFeature_abs_le_one line 85
  9. theorem OAI.Erdos3.booleanCoefficient_abs_le line 91
  10. theorem OAI.Erdos3.booleanAffinePolynomial_eval_abs_le line 104
  11. theorem OAI.Erdos3.booleanSelectedColumn_eval_abs_le line 119
  12. def OAI.Erdos3.productMinorEntryBound line 140
  13. theorem OAI.Erdos3.productMinorEntryBound_nonneg line 143
  14. theorem OAI.Erdos3.booleanSelectedMinor_entry_bound line 148
  15. def OAI.Erdos3.restrictBlockParameters line 176
  16. theorem OAI.Erdos3.booleanSelectedColumn_restrict_eval line 180
  17. theorem OAI.Erdos3.booleanSelectedMinor_restrict_eval line 190
  18. theorem OAI.Erdos3.exists_allocated_boolean_labels line 212
  19. theorem OAI.Erdos3.exists_boolean_minor_specialization line 223
  20. theorem OAI.Erdos3.blockParameter_card line 241
  21. theorem OAI.Erdos3.booleanAffinePolynomial_pderiv_eval_abs_le line 255
  22. theorem OAI.Erdos3.booleanSelectedColumn_pderiv_eval_abs_le line 266
  23. def OAI.Erdos3.productMinorPartialBound line 299
  24. theorem OAI.Erdos3.productMinorPartialBound_nonneg line 302
  25. theorem OAI.Erdos3.booleanSelectedMinor_partial_bound line 307
  26. theorem OAI.Erdos3.mvPolynomial_eq_constant_of_degreeOf_zero line 335
  27. theorem OAI.Erdos3.booleanLinearMinor_eval_eq line 344
  28. theorem OAI.Erdos3.exists_boolean_linear_minor_uniform_lower line 362
  29. def OAI.Erdos3.booleanMinorDeterminant line 393
  30. theorem OAI.Erdos3.booleanMinorDeterminant_contDiff line 400
  31. def OAI.Erdos3.productMinorDeterminantDerivativeBound line 409
  32. theorem OAI.Erdos3.productMinorDeterminantDerivativeBound_nonneg line 413
  33. theorem OAI.Erdos3.booleanMinorDeterminant_fderiv_norm_le line 421
  34. theorem OAI.Erdos3.realAffineCube_abs_le line 453
  35. theorem OAI.Erdos3.real_monomial_eval_abs_le line 470
  36. theorem OAI.Erdos3.boundedDegreeRealJetMatrix_entry_bound line 487
  37. theorem OAI.Erdos3.exists_boolean_minor_sublevel_bound line 513
  38. theorem OAI.Erdos3.exists_weighted_boolean_minor_sublevel_bound line 538
  39. def OAI.Erdos3.booleanBlockParameterEquiv line 574
  40. theorem OAI.Erdos3.boolean_minor_parameter_count_pos line 578
  41. theorem OAI.Erdos3.boolean_minor_degree_bound_pos line 583
  42. abbrev OAI.Erdos3.BoundedBooleanMonomial line 587
  43. instance OAI.Erdos3.boundedBooleanMonomialNonempty line 589
  44. theorem OAI.Erdos3.boundedBooleanMonomial_injective line 593
  45. theorem OAI.Erdos3.boundedBooleanMonomial_card_le line 597
  46. theorem OAI.Erdos3.boundedBooleanMonomial_parameter_count_pos line 600