OAI/MathematicalPhysics/SheetFlows/CircuitPrograms.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

SheetFlows circuit programs.

  1. theorem OAI.Solenoidal.Computing.atom_argument line 13
  2. theorem OAI.Solenoidal.Computing.atom_bound line 19
  3. theorem OAI.Solenoidal.Computing.atom_approx line 28
  4. theorem OAI.Solenoidal.Computing.circuit_data line 38
  5. theorem OAI.Solenoidal.Computing.circuit_const line 42
  6. theorem OAI.Solenoidal.Computing.circuit_atom line 45
  7. theorem OAI.Solenoidal.Computing.circuit_add line 48
  8. theorem OAI.Solenoidal.Computing.circuit_mul line 49
  9. theorem OAI.Solenoidal.Computing.circuit_sub line 50
  10. theorem OAI.Solenoidal.Computing.circuit_bound line 53
  11. theorem OAI.Solenoidal.Computing.circuit_approx line 70
  12. theorem OAI.Solenoidal.Computing.atom_withKind line 88
  13. theorem OAI.Solenoidal.Computing.atom_reflect line 92
  14. theorem OAI.Solenoidal.Computing.circuit_atomDiff line 97
  15. theorem OAI.Solenoidal.Computing.circuit_diff line 117
  16. theorem OAI.Solenoidal.Computing.circuit_mixed line 138
  17. def OAI.Solenoidal.HasCircuit line 153
  18. theorem OAI.Solenoidal.HasRationalFormula.circuit line 156
  19. def OAI.Solenoidal.Circuit.jetBound line 166
  20. theorem OAI.Solenoidal.Circuit.jetBound_nonneg line 169
  21. theorem OAI.Solenoidal.Circuit.jetBound_correct line 172
  22. def OAI.Solenoidal.Circuit.wrapRat line 182
  23. theorem OAI.Solenoidal.Circuit.wrapRat_correct line 186
  24. def OAI.Solenoidal.Circuit.jetApprox line 193
  25. theorem OAI.Solenoidal.circuit_periodic_jet line 198
  26. theorem OAI.Solenoidal.circuit_periodic_bound line 211
  27. theorem OAI.Solenoidal.circuit_periodic_approx line 228
  28. theorem OAI.Solenoidal.Computing.fin_sum_rat line 239
  29. theorem OAI.Solenoidal.Computing.circuit_jetBound line 246
  30. theorem OAI.Solenoidal.Computing.circuit_wrapRat line 249
  31. theorem OAI.Solenoidal.Computing.circuit_jetApprox line 260
  32. theorem OAI.Solenoidal.Computing.partrec_code line 269
  33. theorem OAI.Solenoidal.HasCircuit.effectiveBounds line 280
  34. theorem OAI.Solenoidal.norm_flatten line 287
  35. theorem OAI.Solenoidal.spacetime_expansion line 305
  36. def OAI.Solenoidal.jetLipschitz line 312
  37. theorem OAI.Solenoidal.jetLipschitz_nonneg line 315
  38. theorem OAI.Solenoidal.mixed_lipschitz line 318
  39. theorem OAI.Solenoidal.Computing.jetLipschitz_pr line 347