OAI/Combinatorics/Progressions/Estimates/AllocatedFiniteModelPhysicalExpansion.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.VectorPolynomial.coveredJetAmbientTorus_nsmul_output line 16
  2. theorem OAI.Erdos3.VectorPolynomial.coveredJetAmbientTorus_mk line 22
  3. theorem OAI.Erdos3.VectorPolynomial.ambient_nsmul_lipschitz line 32
  4. def OAI.Erdos3.VectorPolynomial.rowsAmbientSite line 42
  5. theorem OAI.Erdos3.VectorPolynomial.rowsAmbientSite_eq line 49
  6. theorem OAI.Erdos3.VectorPolynomial.rowsAmbientSite_lipschitz line 58
  7. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_masked_cover_factor line 110
  8. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_masked_ambient_lift line 226
  9. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_physical_masked_factor line 338
  10. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_physical_masked_expansion line 433
  11. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_long_physical_expansion_identity line 532
  12. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_grid_physical_expansion_identity line 560
  13. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_finite_model_physical_expansion line 639
  14. theorem OAI.Erdos3.VectorPolynomial.exists_allocated_finite_model_uniform_physical_expansion line 683