OAI/Combinatorics/Progressions/Estimates/UniformPhysicalVisitBounds.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.exists_physical_record_inflation line 9
  2. theorem OAI.Erdos3.inherited_relative_width line 37
  3. def OAI.Erdos3.PhysicalEpochComparison.Controlled line 85
  4. theorem OAI.Erdos3.PhysicalEpochFrame.child_comparison_controlled line 91
  5. theorem OAI.Erdos3.PhysicalEpochFrame.extend_records_of_comparison line 126
  6. def OAI.Erdos3.physicalResidueMean line 157
  7. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.scalarAffinePullback_eval_stride line 169
  8. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.scalarAffinePullback_pair_false line 179
  9. theorem OAI.Erdos3.RationalFilteredNilmanifold.Niltest.scalarAffinePullback_pair_true line 189
  10. theorem OAI.Erdos3.exists_initial_physical_comparison line 206
  11. theorem OAI.Erdos3.exp_neg_le_of_positive_inverse_bound line 271
  12. theorem OAI.Erdos3.physical_visit_numerics line 282
  13. theorem OAI.Erdos3.PhysicalEpochFrame.uniform_visit_bounds line 379