OAI/Computability/FourierTransform/Main.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

Exact uniform Fourier transforms and convolution.

The construction formalizes the exact arithmetic algorithms of An explicit power saving for the exact discrete Fourier transform (OpenAI). The finite phase network originates in the complex construction of Integer multiplication below n log n.

transform_main and convolution_main give fixed finite RAM programs, including preparation and index work, polynomial storage bounds, and a canonical root whose order is computed from the input length. Each includes the paper exponent, decimal power saving, and little-o bound. The _order variants also specify the root order.

The implementation uses a smaller concrete tensor network (32 binary coordinates per factor, 4060 triples, and a 2^50 role envelope) with a stronger saving that implies the stated paper constants. The general rational-algebra extraction, symbolic certificate search, circuit printer, and bounded-printer uniformization from the synthesis appendix are outside this formalization.

  1. lemma OAI.PowerSaving.Skies.multiplier_range line 30
  2. lemma OAI.PowerSaving.Skies.theta_lt line 33
  3. lemma OAI.PowerSaving.Skies.alpha_theta line 39
  4. lemma OAI.PowerSaving.Skies.decimal_range line 59
  5. def OAI.PowerSaving.Skies.speed line 62
  6. lemma OAI.PowerSaving.Skies.flight_little line 64
  7. lemma OAI.PowerSaving.Skies.speed_little line 79
  8. theorem OAI.PowerSaving.Skies.decimal_little line 95
  9. lemma OAI.PowerSaving.Skies.speed_paper line 100
  10. lemma OAI.PowerSaving.Skies.time_bound line 111
  11. theorem OAI.PowerSaving.transform_main_order line 122
  12. theorem OAI.PowerSaving.convolution_main_order line 129
  13. theorem OAI.PowerSaving.transform_main line 137

    Distinct definitions of this name: ComparatorChallenges/UniformFourier.lean:326 (same statement text; different proof or body). Qualify references as OAI.PowerSaving.transform_main@path.

  14. theorem OAI.PowerSaving.convolution_main line 141

    Distinct definitions of this name: ComparatorChallenges/UniformFourier.lean:330 (same statement text; different proof or body). Qualify references as OAI.PowerSaving.convolution_main@path.

  15. lemma OAI.PowerSaving.matrix_definition line 145