OAI/Combinatorics/Progressions/Estimates/NativeFrozenMarkedLocalMark.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.sectionCorrectedPolynomial_map line 17
  2. theorem OAI.Erdos3.NilpotentLieFiltration.real_projected_discrepancy_mem_shifted line 41
  3. theorem OAI.Erdos3.NilpotentLieFiltration.sectionCorrectedPolynomial_prescribed_symbol line 70
  4. theorem OAI.Erdos3.NilpotentLieFiltration.exists_filtered_linear_section line 131
  5. theorem OAI.Erdos3.NilpotentLieFiltration.exists_formal_marked_orbit_restoration line 163
  6. theorem OAI.Erdos3.NilpotentLieFiltration.externalCandidate_stepZero_coord_eq_zero line 226
  7. theorem OAI.Erdos3.NilpotentLieFiltration.externalCandidate_stepZero_group_eq_one line 231
  8. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_step_zero_external_marked_candidate line 248
  9. def OAI.Erdos3.RationalFilteredNilmanifold.includedRefilteredOrbit line 289
  10. theorem OAI.Erdos3.RationalFilteredNilmanifold.includedRefilteredOrbit_log line 301
  11. theorem OAI.Erdos3.RationalFilteredNilmanifold.includedRefilteredOrbit_realEval line 306
  12. def OAI.Erdos3.RationalFilteredNilmanifold.externalCandidateOrbit line 318
  13. theorem OAI.Erdos3.RationalFilteredNilmanifold.externalCandidateOrbit_realEval line 324
  14. theorem OAI.Erdos3.RationalFilteredNilmanifold.externalCandidateOrbit_mark_realEval line 337
  15. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_restored_external_candidate_of_frozen_score line 359
  16. theorem OAI.Erdos3.NilpotentLieFiltration.formal_mark_realEval line 458
  17. theorem OAI.Erdos3.NilpotentLieFiltration.formal_mark_of_realEval line 473
  18. theorem OAI.Erdos3.RationalFilteredNilmanifold.refiltered_mark_realification_commutes line 519
  19. theorem OAI.Erdos3.RationalFilteredNilmanifold.externalCandidateOrbit_marked_realEval line 543
  20. theorem OAI.Erdos3.RationalFilteredNilmanifold.externalCandidateOrbit_formal_mark line 567
  21. theorem OAI.Erdos3.RationalFilteredNilmanifold.exists_ambient_restored_candidate_of_marked_quotient_score line 583
  22. theorem OAI.Erdos3.NilpotentLieFiltration.frozenMarkedOuter_product_mark_eq line 708