OAI/Analysis/MatrixSigning/Complexity/PolynomialValueQuery.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.CurrentKS.Realization.poly_weightedSum line 13
  2. instance OAI.CurrentKS.Realization.poly_veP line 14
  3. instance OAI.CurrentKS.Realization.poly_veY line 15
  4. instance OAI.CurrentKS.Realization.poly_veD line 16
  5. instance OAI.CurrentKS.Realization.poly_veN line 17
  6. instance OAI.CurrentKS.Realization.poly_veEye line 18
  7. instance OAI.CurrentKS.Realization.poly_veEps line 19
  8. instance OAI.CurrentKS.Realization.poly_veTime line 20
  9. instance OAI.CurrentKS.Realization.poly_veVariable line 21
  10. instance OAI.CurrentKS.Realization.poly_veSum line 22
  11. instance OAI.CurrentKS.Realization.poly_sandwich line 23
  12. instance OAI.CurrentKS.Realization.poly_eta line 24
  13. instance OAI.CurrentKS.Realization.poly_schurEval line 25
  14. instance OAI.CurrentKS.Realization.poly_lowerBox line 26
  15. instance OAI.CurrentKS.Realization.poly_upperBox line 27
  16. instance OAI.CurrentKS.Realization.poly_tinyMatrix line 28
  17. instance OAI.CurrentKS.Realization.poly_blockWith line 29
  18. instance OAI.CurrentKS.Realization.poly_valueEval line 32
  19. instance OAI.CurrentKS.Realization.poly_traceMatrix line 33
  20. instance OAI.CurrentKS.Realization.poly_valueObjective line 34
  21. instance OAI.CurrentKS.Realization.poly_valueCoeffs line 35
  22. instance OAI.CurrentKS.Realization.poly_valuePencil line 36
  23. instance OAI.CurrentKS.Realization.poly_vqView line 37
  24. instance OAI.CurrentKS.Realization.poly_vqData line 38
  25. instance OAI.CurrentKS.Realization.poly_vqDelta line 39
  26. instance OAI.CurrentKS.Realization.poly_valueLipschitz line 40
  27. instance OAI.CurrentKS.Realization.poly_valueOuterRadius line 41
  28. instance OAI.CurrentKS.Realization.poly_valueInnerRadius line 42
  29. instance OAI.CurrentKS.Realization.poly_vqOpt line 43
  30. lemma OAI.CurrentKS.Realization.runsPoly_vqFuel line 46
  31. lemma OAI.CurrentKS.Realization.runsPoly_valueQueryPoint line 63
  32. lemma OAI.CurrentKS.Realization.runsPoly_valueQuery line 71
  33. def OAI.CurrentKS.Realization.ValueQueryParams.scanCount line 79
  34. lemma OAI.CurrentKS.Realization.optFuel_le_scan line 81
  35. lemma OAI.CurrentKS.Realization.searchCount_le_scan line 84
  36. lemma OAI.CurrentKS.Realization.runsPoly_valueQuery_scan line 86