OAI/Computability/FourierTransform/Goal.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

Main proof targets.

  1. abbrev OAI.PowerSaving.root line 12

    Source documentation

    Positive-sign, canonical roots. Need only at positive order.

    Also declared: ComparatorChallenges/UniformFourier.lean:278 (same declaration text).

    abbrev root := ExactFourier.zeta

    Mentions: OAI.ExactFourier.zeta

  2. abbrev OAI.PowerSaving.Vec line 14

    Also declared: ComparatorChallenges/UniformFourier.lean:280 (same declaration text).

  3. abbrev OAI.PowerSaving.dftMatrix line 16
  4. def OAI.PowerSaving.dft line 18

    Also declared: ComparatorChallenges/UniformFourier.lean:282 (same declaration text).

  5. def OAI.PowerSaving.conv line 21

    Also declared: ComparatorChallenges/UniformFourier.lean:285 (same declaration text).

  6. def OAI.PowerSaving.paperM line 25

    Source documentation

    Exact exponent from the TeX (natural logarithms).

    Also declared: ComparatorChallenges/UniformFourier.lean:264 (same declaration text).

    def paperM : ℝ := 1000000
  7. def OAI.PowerSaving.paperW line 26

    Also declared: ComparatorChallenges/UniformFourier.lean:265 (same declaration text).

  8. def OAI.PowerSaving.paperDelta line 27

    Also declared: ComparatorChallenges/UniformFourier.lean:266 (same declaration text).

  9. def OAI.PowerSaving.paperMultiplier line 28

    Also declared: ComparatorChallenges/UniformFourier.lean:267 (same declaration text).

  10. def OAI.PowerSaving.theta line 29

    Also declared: ComparatorChallenges/UniformFourier.lean:268 (same declaration text).

  11. def OAI.PowerSaving.decimalExponent line 30

    Also declared: ComparatorChallenges/UniformFourier.lean:269 (same declaration text).

  12. def OAI.PowerSaving.paperTime line 32

    Also declared: ComparatorChallenges/UniformFourier.lean:271 (same declaration text).

  13. def OAI.PowerSaving.decimalTime line 35

    Also declared: ComparatorChallenges/UniformFourier.lean:274 (same declaration text).

  14. def OAI.PowerSaving.nlogn line 37

    Also declared: ComparatorChallenges/UniformFourier.lean:276 (same declaration text).

  15. abbrev OAI.PowerSaving.dftInKind line 39

    Also declared: ComparatorChallenges/UniformFourier.lean:288 (same declaration text).

  16. abbrev OAI.PowerSaving.dftOutKind line 40

    Also declared: ComparatorChallenges/UniformFourier.lean:289 (same declaration text).

  17. abbrev OAI.PowerSaving.convInKind line 41

    Also declared: ComparatorChallenges/UniformFourier.lean:290 (same declaration text).

  18. abbrev OAI.PowerSaving.convOutKind line 42

    Also declared: ComparatorChallenges/UniformFourier.lean:291 (same declaration text).

  19. def OAI.PowerSaving.DFTProgram line 48

    Source documentation

    Include an integer and address bound polynomial in n. Constants inside this bound are immaterial (a constant number of logarithmic sized words is allowed). W n is the work allowance, including the order program, one root primitive and the transform program. The order program takes only the length, so its result specifies the root explicitly.

    Also declared: ComparatorChallenges/UniformFourier.lean:293 (same declaration text).

    def DFTProgram (order : Prog false w w) (solve : Prog false dftInKind dftOutKind)
    (W : ℕ → ℕ) : Prop :=
…

    Mentions: OAI.PowerSaving.dftInKind, OAI.PowerSaving.dftOutKind

  20. def OAI.PowerSaving.ConvProgram line 62

    Source documentation

    Convolution in the same model extended by pointwise field multiplication for two inputs. We even require the bound on the supplied root from the proof of the corollary.

    Also declared: ComparatorChallenges/UniformFourier.lean:305 (same declaration text).

    def ConvProgram (order : Prog false w w) (solve : Prog true convInKind convOutKind)
    (W : ℕ → ℕ) : Prop :=
…

    Mentions: OAI.PowerSaving.convInKind, OAI.PowerSaving.convOutKind

  21. def OAI.PowerSaving.TimeBounds line 75

    Source documentation

    Thm 1 (intro main) and decimal corollary estimates.

    Also declared: ComparatorChallenges/UniformFourier.lean:317 (same declaration text).

    def TimeBounds (W : ℕ → ℕ) : Prop :=
…
  22. def OAI.PowerSaving.DFTGoal line 79

    Also declared: ComparatorChallenges/UniformFourier.lean:321 (same declaration text).

  23. def OAI.PowerSaving.ConvGoal line 81

    Also declared: ComparatorChallenges/UniformFourier.lean:323 (same declaration text).