OAI/Combinatorics/Progressions/Dynamics/CanonicalZeroLayerBudgetedInitialization.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.exists_allocatedZeroLayerInitialization_power_budget line 14
  2. def OAI.Erdos3.unconditionedCommonSide line 80
  3. theorem OAI.Erdos3.unconditionedCommonSide_pos line 82
  4. theorem OAI.Erdos3.le_unconditionedCommonSide line 87
  5. theorem OAI.Erdos3.unconditionedCommonSide_le line 93
  6. theorem OAI.Erdos3.unconditionedCommonSide_cast line 106
  7. theorem OAI.Erdos3.unconditionedCommonSide_density line 110
  8. theorem OAI.Erdos3.unconditionedCommonSide_root_budget line 129
  9. theorem OAI.Erdos3.unconditionedSpatialWidthCutoff_common_side_le line 137
  10. theorem OAI.Erdos3.exists_unconditioned_late_prime_common_side_budget line 163
  11. def OAI.Erdos3.unconditionedCommonSideScalarRatio line 205
  12. theorem OAI.Erdos3.unconditionedCommonSide_scalar_bound line 208
  13. theorem OAI.Erdos3.unconditionedCommonSide_scalar_bound_of_range line 224
  14. def OAI.Erdos3.unconditionedCommonSideExtra line 232
  15. theorem OAI.Erdos3.unconditionedCommonSideExtra_nonneg line 235
  16. theorem OAI.Erdos3.exp_unconditionedCommonSideExtra line 240
  17. theorem OAI.Erdos3.unconditionedCommonSide_le_exp_extra_mul line 244
  18. theorem OAI.Erdos3.VectorPolynomial.exists_allocatedZeroLayer_budgeted_initialization line 262
  19. def OAI.Erdos3.VectorPolynomial.CanonicalEmptyLayerGeometry.zeroLayerScale line 387
  20. theorem OAI.Erdos3.VectorPolynomial.CanonicalEmptyLayerGeometry.zeroLayerScale_value line 391
  21. theorem OAI.Erdos3.VectorPolynomial.CanonicalEmptyLayerGeometry.zeroLayer_one_pos line 394
  22. theorem OAI.Erdos3.VectorPolynomial.exists_canonicalZeroLayer_budgeted_initialization line 405