OAI/Combinatorics/Progressions/Nilpotent/PolynomialPatchWeightedChartNiltest.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.PolynomialPatch.shearNiltest line 20
  2. theorem OAI.Erdos3.PolynomialPatch.shearNiltest_unitInterval line 39
  3. theorem OAI.Erdos3.PolynomialPatch.shearNiltest_eval line 45
  4. theorem OAI.Erdos3.PolynomialPatch.shearNiltest_complexity line 50
  5. theorem OAI.Erdos3.PolynomialSlots.shearObservable_eval_lift line 67
  6. theorem OAI.Erdos3.PolynomialSlots.shearObservable_eval_orbit line 78
  7. theorem OAI.Erdos3.exists_normalized_patch_niltest_budget line 100
  8. def OAI.Erdos3.PolynomialPatch.fixedObservableNiltest line 172
  9. theorem OAI.Erdos3.PolynomialPatch.fixedObservableNiltest_unitInterval line 183
  10. theorem OAI.Erdos3.PolynomialPatch.fixedObservableNiltest_eval line 189
  11. theorem OAI.Erdos3.PolynomialPatch.fixedObservableNiltest_complexity line 202
  12. theorem OAI.Erdos3.PolynomialPatch.exists_fixed_observable_family line 208
  13. theorem OAI.Erdos3.exists_mass_bounded_patch_niltest_budget line 227
  14. theorem OAI.Erdos3.exists_fixed_local_patch_ordinary_niltest_family line 279
  15. theorem OAI.Erdos3.exists_fixed_local_patch_ordinary_niltest_family_preserving_scores line 315
  16. theorem OAI.Erdos3.PolynomialPatch.exists_ordinary_niltest_of_weighted_chart line 375