OAI/Computability/FourierCircuit/DisplacementKernel.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactFourier.Displacement.kernel line 10
  2. theorem OAI.ExactFourier.Displacement.kernel_zero_left line 13
  3. theorem OAI.ExactFourier.Displacement.kernel_zero_right line 15
  4. theorem OAI.ExactFourier.Displacement.kernel_succ line 18
  5. def OAI.ExactFourier.Displacement.lower line 24
  6. theorem OAI.ExactFourier.Displacement.kernel_eq_mul line 27
  7. def OAI.ExactFourier.Displacement.delta line 48
  8. theorem OAI.ExactFourier.Displacement.reconstruct line 52

    Source documentation

    The exact rank-three displacement reconstruction, with only the stated interior outer-product recurrence; no analytic or generic-position premise.

    theorem reconstruct (a e : ℕ) (ha : 0 < a) (he : 0 < e) (M : ℕ→ℕ→ℂ) (v w : ℕ→ℂ)
 (hrec : ∀ i j, i+1 < a → j+1 < e → M (i+1) (j+1)=M i j+v (i+1)*w (j+1)) :
 let row := fun j=>M 0 j-v 0*w j
…
  9. def OAI.ExactFourier.Displacement.extendVector line 83
  10. theorem OAI.ExactFourier.Displacement.coeff_ofFn_extend line 86
  11. theorem OAI.ExactFourier.Displacement.convolution_submatrix line 92
  12. def OAI.ExactFourier.Displacement.fullKernel line 105
  13. theorem OAI.ExactFourier.Displacement.fullKernel_sumLayered line 110
  14. theorem OAI.ExactFourier.Displacement.kernel_submatrix line 117
  15. theorem OAI.ExactFourier.Displacement.kernel_stable line 130
  16. theorem OAI.ExactFourier.Displacement.kernel_congr line 147
  17. theorem OAI.ExactFourier.Displacement.kernel_restrict line 153
  18. theorem OAI.ExactFourier.Displacement.stable_of_displacement line 160
  19. theorem OAI.ExactFourier.Displacement.small_stable line 199
  20. theorem OAI.ExactFourier.Displacement.row_chunks line 211
  21. theorem OAI.ExactFourier.Displacement.all_chunks line 236
  22. theorem OAI.ExactFourier.Layered.rect_single line 275
  23. theorem OAI.ExactFourier.Layered.rect_finset_sum line 289
  24. theorem OAI.ExactFourier.Layered.rect_dense line 304
  25. theorem OAI.ExactFourier.Displacement.exact_width line 325

    Source documentation

    Exact-width displacement shear; dirty scratch is borrowed internally.

    theorem exact_width (a e : ℕ) (M : ℕ→ℕ→ℂ) (v w : ℕ→ℂ)
 (hrec : ∀ i j,i+1<a → j+1<e → M (i+1) (j+1)=M i j+v (i+1)*w (j+1)) :
 Layered (rectangularShear (fun i : Fin a=>fun j : Fin e=>M i.val j.val))
  (2097152*(Nat.log 2 (a+e)+1)) := by
…

    Mentions: OAI.ExactFourier.Layered, OAI.ExactFourier.rectangularShear