OAI/Computability/FourierCircuit/LiveSectors.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ExactFourier.Packing.liveMatrix line 12
  2. theorem OAI.ExactFourier.Packing.live_matrix_on line 18
  3. theorem OAI.ExactFourier.Packing.live_matrix_reindex line 63
  4. theorem OAI.ExactFourier.Packing.copy_fiber_card line 86
  5. def OAI.ExactFourier.Packing.sigmaFstFiber line 97
  6. theorem OAI.ExactFourier.Packing.copies_equiv line 103
  7. def OAI.ExactFourier.Packing.copyCoordinates line 116
  8. theorem OAI.ExactFourier.Packing.copyCoordinates_matrix line 122
  9. def OAI.ExactFourier.Packing.singleStepFin line 149
  10. theorem OAI.ExactFourier.Packing.embeddedCall_eq line 156
  11. theorem OAI.ExactFourier.Packing.singleStepFin_matrix line 176
  12. def OAI.ExactFourier.Packing.squareFinEquiv line 189
  13. theorem OAI.ExactFourier.Packing.squareFinEquiv_tensor line 193
  14. theorem OAI.ExactFourier.Packing.square_win_implies_finite_win line 200
  15. theorem OAI.ExactFourier.Packing.family_square_win line 253
  16. theorem OAI.ExactFourier.Packing.square_schedule_margin line 327

    Source documentation

    Quantitative slack for the deterministic cyclic schedule, using square sectors.

    theorem square_schedule_margin {K W G S u F L C : ℝ}
 (hK : 1≤K) (hS : 2*K≤S) (hu : L+2*C*W≤u)
 (hu0 : 0≤u) (hC : 0≤C) (hW : 0≤W)
 (hGF : G+S=2*K*W) (hF : F=(2*W-1)*u+1-L) (hFu : F≤2*W*u) :
 G*u^2+C*F≤K*u*F := by
…

    Mentions: OAI.ExactFourier.L

  17. theorem OAI.ExactFourier.Packing.square_inventory_parameters line 345