OAI/Computability/FourierTransform/PolynomialBounds.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

Uniform elementary bound helpers (natural envelopes; later compare to the real bounds).

  1. def OAI.PowerSaving.RAM.Small line 13

    Source documentation

    Pointwise polynomial bound with absolute constants. The bound relevant to word sizes will use n as B. Local computations may also have polynomial work in a different B.

    def Small {ι : Type u} (B F : ι → ℕ) : Prop := ∃ d : ℕ, ∀ i, F i ≤ (B i+2)^d
…
  2. theorem OAI.PowerSaving.RAM.Small.const line 18
  3. theorem OAI.PowerSaving.RAM.Small.self line 23
  4. theorem OAI.PowerSaving.RAM.Small.reindex line 25
  5. theorem OAI.PowerSaving.RAM.Small.mono line 29
  6. theorem OAI.PowerSaving.RAM.Small.mul line 33
  7. theorem OAI.PowerSaving.RAM.Small.pow_mono_degree line 38
  8. theorem OAI.PowerSaving.RAM.Small.add line 42
  9. theorem OAI.PowerSaving.RAM.Small.max line 53
  10. theorem OAI.PowerSaving.RAM.Small.pow line 57
  11. theorem OAI.PowerSaving.RAM.Small.trans line 62
  12. def OAI.PowerSaving.RAM.Dom line 69

    Source documentation

    Least data needed for a "big-O with +1" natural work budget convenience.

    def Dom {ι : Type u} (W F : ι → ℕ) : Prop :=
…
  13. theorem OAI.PowerSaving.RAM.Dom.of_le line 75
  14. theorem OAI.PowerSaving.RAM.Dom.self line 78
  15. theorem OAI.PowerSaving.RAM.Dom.const line 80
  16. theorem OAI.PowerSaving.RAM.Dom.add line 85
  17. theorem OAI.PowerSaving.RAM.Dom.trans line 95