OAI/Combinatorics/Progressions/Geometry/AnisotropicSpatialCapBudget.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.normalizedIntegerColumns_variable_entry_bound line 11
  2. theorem OAI.Erdos3.normalizedIntegerColumns_variable_norm_bound line 22
  3. theorem OAI.Erdos3.anisotropicSpatialPivot_control line 30
  4. theorem OAI.Erdos3.anisotropicSpatialFree_scaled_bound line 44
  5. theorem OAI.Erdos3.anisotropicSpatial_free_norm_bound line 54
  6. def OAI.Erdos3.anisotropicSpatialDensityCap line 95
  7. def OAI.Erdos3.anisotropicSpatialDensityLip line 100
  8. theorem OAI.Erdos3.anisotropicSpatialDensityCap_nonneg line 106
  9. theorem OAI.Erdos3.anisotropicSpatialDensityLip_nonneg line 111
  10. theorem OAI.Erdos3.anisotropicSpatialKernelDensity_bounds line 116
  11. def OAI.Erdos3.anisotropicSpatialCapLog line 166
  12. theorem OAI.Erdos3.anisotropicSpatialCapLog_nonneg line 169
  13. theorem OAI.Erdos3.anisotropicSpatialDensityCap_exp_bound line 174