OAI/Combinatorics/Progressions/Dynamics/ScalarCubeBoundaryLogBudget.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.scalarCubeProductBoundaryRadius line 13
  2. theorem OAI.Erdos3.scalarCubeProductBoundaryRadius_pos line 17
  3. theorem OAI.Erdos3.scalarCubeProductBoundaryRadius_loss line 21
  4. def OAI.Erdos3.scalarCubeProductDerivativeConstant line 36
  5. theorem OAI.Erdos3.scalarCubeProductBoundaryRadius_derivative line 41
  6. theorem OAI.Erdos3.exists_scalarCubeProductWeight_with_error line 65
  7. def OAI.Erdos3.scalarCubeBoundaryLog line 93
  8. def OAI.Erdos3.scalarCubeDerivativeLog line 94
  9. theorem OAI.Erdos3.scalarCubeBoundaryConstant_le_exp line 96
  10. theorem OAI.Erdos3.scalarCubeProductBoundaryRadius_inverse_le_exp line 115
  11. theorem OAI.Erdos3.scalarCubeProductDerivativeConstant_le_exp line 128