OAI/Computability/FourierCircuit/Main.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ExactFourier.PrimeInventory.count_fourth line 10
2. def OAI.ExactFourier.PrimeInventory.upper line 39
3. theorem OAI.ExactFourier.PrimeInventory.family line 41
4. theorem OAI.ExactFourier.PrimeInventory.family_coprime line 64
5. def OAI.ExactFourier.FourierTransfer.depth line 78
6. theorem OAI.ExactFourier.FourierTransfer.depth_bound line 80
7. theorem OAI.ExactFourier.FourierTransfer.family_cost line 102
8. theorem OAI.ExactFourier.FourierTransfer.log_square_littleO line 152
9. theorem OAI.ExactFourier.FourierTransfer.log_power_ratio line 164
10. theorem OAI.ExactFourier.FourierTransfer.shifted_log_power_ratio line 172
11. theorem OAI.ExactFourier.CircuitCost.exists_circuit line 196
12. theorem OAI.ExactFourier.win_to_fourier line 224

    Source documentation

    An actual finite win transfers to arbitrarily large exact Fourier DAGs, with every scalar multiplication charged.

    theorem win_to_fourier (win : FiniteWinStatement) : MainStatement := by
    …

    Mentions: OAI.ExactFourier.FiniteWinStatement, OAI.ExactFourier.MainStatement

13. theorem OAI.ExactFourier.main_theorem line 277

    Distinct definitions of this name: ComparatorChallenges/ExactFourier.lean:57 (same statement text; different proof or body). Qualify references as OAI.ExactFourier.main_theorem@path.

14. theorem OAI.ExactFourier.finite_win_exists line 279
15. theorem OAI.ExactFourier.exists_fourier_circuit line 291

    Source documentation

    Existence of an exact circuit in every width, used only to define the minimum.

    theorem exists_fourier_circuit (n : ℕ) : ∃ k : ℕ,∃ C : Circuit n,
     C.size=k ∧ C.Computes (fourierMatrix n) := by
    …

    Mentions: OAI.ExactFourier.Circuit, OAI.ExactFourier.fourierMatrix

16. def OAI.ExactFourier.L line 296
17. theorem OAI.ExactFourier.L_attained line 300
18. theorem OAI.ExactFourier.L_le line 304
19. theorem OAI.ExactFourier.fourier_denominator_pos line 308
20. theorem OAI.ExactFourier.main_liminf line 314

    Source documentation

    The liminf formulation of the same main theorem, for the literal minimum L.

    theorem main_liminf :
     Filter.liminf (fun n : ℕ=>(L n : ℝ)/((n:ℝ)*Real.logb 2 (n:ℝ))) atTop=0 := by
    …

    Mentions: OAI.ExactFourier.L