OAI/Computability/FourierCircuit/SparseShear.lean

GitHub source file

43 declarations, 0 contain sorry, 0 declared as axioms

Sparse whole-block cancellations in triangular monotonicity.

  1. theorem OAI.ExactFourier.MatrixPrice.rectangularShear_add_le line 14
  2. theorem OAI.ExactFourier.MatrixPrice.rectangularShear_single line 20
  3. theorem OAI.ExactFourier.MatrixPrice.rectangularShear_sum_le line 28
  4. theorem OAI.ExactFourier.MatrixPrice.rectangularShear_sparse line 39

    Source documentation

    A rectangular shear costs at most one per nonzero matrix entry.

    theorem rectangularShear_sparse (G : Matrix ι κ ℂ) :
    p.value (rectangularShear G) ≤
      ((Finset.univ.filter fun ij : ι × κ => G ij.1 ij.2 ≠ 0).card : ℝ) := by
…

    Mentions: OAI.ExactFourier.rectangularShear

  5. def OAI.ExactFourier.Triangular.flat line 82
  6. def OAI.ExactFourier.Triangular.liftRows line 84
  7. def OAI.ExactFourier.Triangular.freshRows line 87
  8. def OAI.ExactFourier.Triangular.nextRows line 90
  9. theorem OAI.ExactFourier.Triangular.liftRows_mul line 94
  10. theorem OAI.ExactFourier.Triangular.nextRows_change line 110
  11. theorem OAI.ExactFourier.Triangular.flat_next_normalized line 118
  12. theorem OAI.ExactFourier.Triangular.span_rows_unit_mul line 136

    Source documentation

    Ordinary matrix row spaces are unchanged by an invertible row multiplier.

    theorem span_rows_unit_mul {δ : Type} (V : Matrix σ σ ℂ) (R : Matrix σ δ ℂ)
    (hV : IsUnit V) :
    Submodule.span ℂ (Set.range (V * R)) = Submodule.span ℂ (Set.range R) := by
…
  13. def OAI.ExactFourier.Triangular.nnz line 152

    Source documentation

    Number of supported scalar positions.

    noncomputable def nnz {δ : Type} [Fintype δ] (v : δ → ℂ) : ℕ :=
…
  14. theorem OAI.ExactFourier.Triangular.nnz_lift_one line 155
  15. theorem OAI.ExactFourier.Triangular.nnz_fresh line 173
  16. theorem OAI.ExactFourier.Triangular.nnz_nextRows line 190
  17. abbrev OAI.ExactFourier.Triangular.Bottom line 207

    Source documentation

    Recursive axis/fiber indexing; no extra workspace is introduced.

    abbrev Bottom (β : Type) : ℕ → Type
  | 0 => PUnit
  | k+1 => Bottom β k × β
  18. abbrev OAI.ExactFourier.Triangular.Calls line 211
  19. instance OAI.ExactFourier.Triangular.bottomFintype line 215
  20. instance OAI.ExactFourier.Triangular.callsFintype line 218
  21. instance OAI.ExactFourier.Triangular.bottomDecidableEq line 221
  22. instance OAI.ExactFourier.Triangular.callsDecidableEq line 224
  23. theorem OAI.ExactFourier.Triangular.bottom_card_zero line 230
  24. theorem OAI.ExactFourier.Triangular.calls_card_zero line 232
  25. theorem OAI.ExactFourier.Triangular.bottom_card_succ line 234
  26. theorem OAI.ExactFourier.Triangular.calls_card_succ line 238
  27. theorem OAI.ExactFourier.Triangular.calls_card_relation line 243
  28. theorem OAI.ExactFourier.Triangular.bottom_card_pos line 249
  29. def OAI.ExactFourier.Triangular.tensorPower line 254
  30. def OAI.ExactFourier.Triangular.contamination line 257
  31. def OAI.ExactFourier.Triangular.generators line 261
  32. def OAI.ExactFourier.Triangular.rowBasis line 265
  33. theorem OAI.ExactFourier.Triangular.tensorPower_unit line 269
  34. theorem OAI.ExactFourier.Triangular.rowBasis_unit line 275
  35. theorem OAI.ExactFourier.Triangular.rowBasis_normalizes line 281
  36. theorem OAI.ExactFourier.Triangular.generators_sparse line 292
  37. theorem OAI.ExactFourier.Triangular.tensorPower_price line 298
  38. theorem OAI.ExactFourier.Triangular.experiment_price line 307
  39. theorem OAI.ExactFourier.Triangular.flat_left line 341
  40. theorem OAI.ExactFourier.Triangular.nnz_flat line 347
  41. theorem OAI.ExactFourier.Triangular.nnz_selected_le line 355
  42. theorem OAI.ExactFourier.Triangular.cancellation_identity line 370
  43. theorem OAI.ExactFourier.Triangular.compressed_price line 384