OAI/Combinatorics/Progressions/Geometry/NativeCoordinateSplitFreezing.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.eval_eq_of_support_agreement line 14
  2. theorem OAI.Erdos3.MultidegreeLieFiltration.polynomialOrbitEval_eq_on_active_coordinates line 35
  3. def OAI.Erdos3.coordinateSplitBound line 66
  4. def OAI.Erdos3.coordinateSplitDownset line 69
  5. theorem OAI.Erdos3.coordinateSplitBound_le line 72
  6. theorem OAI.Erdos3.coordinateSplitDownset_lower line 77
  7. theorem OAI.Erdos3.coordinateSplitDownset_covers line 81
  8. theorem OAI.Erdos3.coordinateSplitDownset_terminal line 105
  9. structure OAI.Erdos3.NativeCoordinateSplit line 123
  10. theorem OAI.Erdos3.NativeCoordinateSplit.exists_fixed_correlating_term line 161
  11. theorem OAI.Erdos3.NativeCoordinateSplit.first_eval_eq line 212
  12. def OAI.Erdos3.NativeCoordinateSplit.firstFactor line 227
  13. theorem OAI.Erdos3.NativeCoordinateSplit.first_eval_firstFactor line 230
  14. theorem OAI.Erdos3.NativeCoordinateSplit.firstFactor_norm line 234
  15. theorem OAI.Erdos3.NativeCoordinateSplit.exists_second_expansion_budget line 253