OAI/GroupTheory/PolycyclicRecognition/Algebra/SubexponentialBounds.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

The finite algebra of subexponential losses

  1. def OAI.PolycyclicRecognition.HasSubexponentialLowerBound line 14

    Source documentation

    A lower bound of the form exp (-o(r)), expressed without a choice of error function.

    def HasSubexponentialLowerBound (f : ℝ → ℝ) : Prop :=
…
  2. def OAI.PolycyclicRecognition.HasSubexponentialUpperBound line 18

    Source documentation

    An upper bound of the form exp (o(r)).

    def HasSubexponentialUpperBound (f : ℝ → ℝ) : Prop :=
…
  3. theorem OAI.PolycyclicRecognition.HasSubexponentialLowerBound.eventually_pos line 21
  4. theorem OAI.PolycyclicRecognition.HasSubexponentialLowerBound.mono line 25
  5. theorem OAI.PolycyclicRecognition.HasSubexponentialUpperBound.mono line 32
  6. theorem OAI.PolycyclicRecognition.subexponential_lower_const line 39
  7. theorem OAI.PolycyclicRecognition.subexponential_upper_const line 46
  8. theorem OAI.PolycyclicRecognition.HasSubexponentialLowerBound.mul line 52
  9. theorem OAI.PolycyclicRecognition.HasSubexponentialUpperBound.mul line 64
  10. theorem OAI.PolycyclicRecognition.HasSubexponentialLowerBound.div line 76