OAI/Computability/FourierCircuit/PivotJoin.lean

GitHub source file

52 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactFourier.Pivot.ofMatrix line 10
  2. theorem OAI.ExactFourier.Pivot.of_fromBlocks line 13
  3. def OAI.ExactFourier.Pivot.reverseJoin line 18
  4. theorem OAI.ExactFourier.Pivot.reverseJoin_eq line 23
  5. theorem OAI.ExactFourier.Pivot.of_join line 34
  6. theorem OAI.ExactFourier.CellJoin.scalar_price line 65
  7. theorem OAI.ExactFourier.Pivot.of_unit line 91
  8. theorem OAI.ExactFourier.Pivot.of_reindex_data line 95
  9. theorem OAI.ExactFourier.Pivot.of_one line 104
  10. theorem OAI.ExactFourier.Pivot.run_block_units line 110
  11. theorem OAI.ExactFourier.Pivot.reverseJoin_scalar_price line 127
  12. theorem OAI.ExactFourier.Pivot.run_scalar_price line 132
  13. theorem OAI.ExactFourier.Pivot.run_pivot_price line 141
  14. theorem OAI.ExactFourier.MatrixPrice.scalar_pivot_le line 159
  15. theorem OAI.ExactFourier.MatrixPrice.scalar_pivot line 184

    Source documentation

    Exact scalar pivot invariance, 07-pivots:175--240. The proof uses finite single-port chains; its constant four is amortized without any continuity law.

    theorem scalar_pivot (p : MatrixPrice) (A : Matrix α α ℂ)
    (C : Matrix α PUnit ℂ) (B : Matrix PUnit α ℂ) (D : Matrix PUnit PUnit ℂ)
    (hA : IsUnit A) (hD : IsUnit D) (hK : IsUnit (Matrix.fromBlocks A C B D)) :
    p.value (Pivot.matrix A C B D)=p.value (Matrix.fromBlocks A C B D) := by
…

    Mentions: OAI.ExactFourier.MatrixPrice, OAI.ExactFourier.Pivot.matrix

  16. def OAI.ExactFourier.BasisExchange.mix line 203
  17. theorem OAI.ExactFourier.BasisExchange.mix_mul line 207
  18. theorem OAI.ExactFourier.BasisExchange.mix_one_left line 215
  19. theorem OAI.ExactFourier.BasisExchange.mix_one_right line 221
  20. theorem OAI.ExactFourier.BasisExchange.price_split line 227
  21. def OAI.ExactFourier.BasisExchange.isolate line 256
  22. theorem OAI.ExactFourier.BasisExchange.update_isolate line 262
  23. theorem OAI.ExactFourier.BasisExchange.price line 273

    Source documentation

    Exchange any corresponding members of two bases, assuming exactly that both original and both exchanged lists are bases.

    theorem price (p : MatrixPrice) (U V : Matrix ι ι ℂ) (i : ι)
    (hU : IsUnit U) (hV : IsUnit V)
    (hU' : IsUnit (U.updateRow i (V i))) (hV' : IsUnit (V.updateRow i (U i))) :
    p.value (V.updateRow i (U i)*(U.updateRow i (V i))⁻¹)=p.value (V*U⁻¹) := by
…

    Mentions: OAI.ExactFourier.MatrixPrice

  24. def OAI.ExactFourier.DensePair.J line 297
  25. def OAI.ExactFourier.DensePair.X line 299
  26. def OAI.ExactFourier.DensePair.Xb line 301
  27. def OAI.ExactFourier.DensePair.Xd line 303
  28. def OAI.ExactFourier.DensePair.Y1 line 305
  29. def OAI.ExactFourier.DensePair.Y2 line 307
  30. def OAI.ExactFourier.DensePair.Y3 line 309
  31. def OAI.ExactFourier.DensePair.Y4 line 311
  32. def OAI.ExactFourier.DensePair.Y5 line 313
  33. def OAI.ExactFourier.DensePair.Y6 line 315
  34. def OAI.ExactFourier.DensePair.cycle line 318
  35. theorem OAI.ExactFourier.DensePair.J_monomial line 324
  36. theorem OAI.ExactFourier.DensePair.X_eq line 329
  37. theorem OAI.ExactFourier.DensePair.det_J line 332
  38. theorem OAI.ExactFourier.DensePair.det_X line 340
  39. theorem OAI.ExactFourier.DensePair.det_Xb line 348
  40. theorem OAI.ExactFourier.DensePair.det_Xd line 356
  41. theorem OAI.ExactFourier.DensePair.det_Y1 line 364
  42. theorem OAI.ExactFourier.DensePair.det_Y2 line 372
  43. theorem OAI.ExactFourier.DensePair.det_Y3 line 380
  44. theorem OAI.ExactFourier.DensePair.det_Y4 line 388
  45. theorem OAI.ExactFourier.DensePair.det_Y5 line 396
  46. theorem OAI.ExactFourier.DensePair.det_Y6 line 404
  47. theorem OAI.ExactFourier.DensePair.exchange01 line 412
  48. theorem OAI.ExactFourier.DensePair.exchange23 line 418
  49. theorem OAI.ExactFourier.DensePair.exchange34 line 423
  50. theorem OAI.ExactFourier.DensePair.exchange56 line 428
  51. theorem OAI.ExactFourier.DensePair.shear12 line 433
  52. theorem OAI.ExactFourier.DensePair.shear45 line 437