OAI/Combinatorics/EditApproximation/Geometry/BandActionPolynomial.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

A fixed-degree envelope for the full labeled action selector, including its final logarithm-gradient and argmax, after the iterative optimizer.

  1. abbrev OAI.EditApproximation.CE line 11

    Distinct definitions of this name: OAI/Combinatorics/EditApproximation/Numerics/OptimizerBitEnvelope.lean:83 (same statement text; different proof or body). Qualify references as OAI.EditApproximation.CE@path.

  2. def OAI.EditApproximation.baSize line 12
  3. def OAI.EditApproximation.baMax line 13
  4. def OAI.EditApproximation.expressionLogStorage line 15

    Distinct definitions of this name: OAI/Combinatorics/EditApproximation/Numerics/OptimizerBitEnvelope.lean:88 (same statement text; different proof or body). Qualify references as OAI.EditApproximation.expressionLogStorage@path.

  5. def OAI.EditApproximation.expressionGradientStorage line 18

    Distinct definitions of this name: OAI/Combinatorics/EditApproximation/Numerics/OptimizerBitEnvelope.lean:91 (same statement text; different proof or body). Qualify references as OAI.EditApproximation.expressionGradientStorage@path.

  6. def OAI.EditApproximation.expressionPoint line 21

    Distinct definitions of this name: OAI/Combinatorics/EditApproximation/Numerics/OptimizerBitEnvelope.lean:94 (same statement text; different proof or body). Qualify references as OAI.EditApproximation.expressionPoint@path.

  7. def OAI.EditApproximation.expressionLogUniversal line 24

    Distinct definitions of this name: OAI/Combinatorics/EditApproximation/Numerics/OptimizerBitEnvelope.lean:97 (same statement text; different proof or body). Qualify references as OAI.EditApproximation.expressionLogUniversal@path.

  8. def OAI.EditApproximation.expressionLogStep line 28

    Distinct definitions of this name: OAI/Combinatorics/EditApproximation/Numerics/OptimizerBitEnvelope.lean:101 (same statement text; different proof or body). Qualify references as OAI.EditApproximation.expressionLogStep@path.

  9. def OAI.EditApproximation.expressionLogBit line 32

    Also declared: OAI/Combinatorics/EditApproximation/Numerics/OptimizerBitEnvelope.lean:105 (same declaration text).

  10. def OAI.EditApproximation.expressionGradientBit line 37

    Distinct definitions of this name: OAI/Combinatorics/EditApproximation/Numerics/OptimizerBitEnvelope.lean:110 (same statement text; different proof or body). Qualify references as OAI.EditApproximation.expressionGradientBit@path.

  11. def OAI.EditApproximation.expressionMaximizer line 47

    Distinct definitions of this name: OAI/Combinatorics/EditApproximation/Numerics/OptimizerBitEnvelope.lean:120 (same statement text; different proof or body). Qualify references as OAI.EditApproximation.expressionMaximizer@path.

  12. def OAI.EditApproximation.expressionUpdate line 51

    Distinct definitions of this name: OAI/Combinatorics/EditApproximation/Numerics/OptimizerBitEnvelope.lean:124 (same statement text; different proof or body). Qualify references as OAI.EditApproximation.expressionUpdate@path.

  13. def OAI.EditApproximation.expressionOptimizer line 57

    Distinct definitions of this name: OAI/Combinatorics/EditApproximation/Numerics/OptimizerBitEnvelope.lean:130 (same statement text; different proof or body). Qualify references as OAI.EditApproximation.expressionOptimizer@path.

  14. def OAI.EditApproximation.expressionBandSumStorage line 63

    Distinct definitions of this name: OAI/Combinatorics/EditApproximation/Numerics/OptimizerBitEnvelope.lean:189 (same statement text; different proof or body). Qualify references as OAI.EditApproximation.expressionBandSumStorage@path.

  15. def OAI.EditApproximation.expressionBandVertexWord line 66

    Also declared: OAI/Combinatorics/EditApproximation/Numerics/OptimizerBitEnvelope.lean:192 (same declaration text).

  16. def OAI.EditApproximation.expressionStoredSumWord line 69

    Distinct definitions of this name: OAI/Combinatorics/EditApproximation/Numerics/OptimizerBitEnvelope.lean:195 (same statement text; different proof or body). Qualify references as OAI.EditApproximation.expressionStoredSumWord@path.

  17. def OAI.EditApproximation.expressionStoredSumBit line 72

    Also declared: OAI/Combinatorics/EditApproximation/Numerics/OptimizerBitEnvelope.lean:198 (same declaration text).

  18. def OAI.EditApproximation.expressionBandCoordinateBit line 75

    Also declared: OAI/Combinatorics/EditApproximation/Numerics/OptimizerBitEnvelope.lean:201 (same declaration text).

  19. def OAI.EditApproximation.expressionBandPreparation line 78

    Also declared: OAI/Combinatorics/EditApproximation/Numerics/OptimizerBitEnvelope.lean:204 (same declaration text).

  20. def OAI.EditApproximation.expressionOptimisticStorage line 81

    Also declared: OAI/Combinatorics/EditApproximation/Numerics/OptimizerBitEnvelope.lean:207 (same declaration text).

  21. def OAI.EditApproximation.expressionOnlineStorage line 83

    Also declared: OAI/Combinatorics/EditApproximation/Numerics/OptimizerBitEnvelope.lean:209 (same declaration text).

  22. def OAI.EditApproximation.expressionGainBit line 87

    Also declared: OAI/Combinatorics/EditApproximation/Numerics/OptimizerBitEnvelope.lean:213 (same declaration text).

  23. def OAI.EditApproximation.expressionDecrementBit line 89

    Also declared: OAI/Combinatorics/EditApproximation/Numerics/OptimizerBitEnvelope.lean:215 (same declaration text).

  24. def OAI.EditApproximation.expressionCoefficientBit line 92

    Also declared: OAI/Combinatorics/EditApproximation/Numerics/OptimizerBitEnvelope.lean:218 (same declaration text).

  25. def OAI.EditApproximation.expressionOptimisticBit line 95

    Also declared: OAI/Combinatorics/EditApproximation/Numerics/OptimizerBitEnvelope.lean:221 (same declaration text).

  26. def OAI.EditApproximation.expressionOnlineBit line 100

    Also declared: OAI/Combinatorics/EditApproximation/Numerics/OptimizerBitEnvelope.lean:226 (same declaration text).

  27. def OAI.EditApproximation.expressionSelection line 107
  28. def OAI.EditApproximation.expressionEnvelopeWord line 113
  29. def OAI.EditApproximation.expressionEnvelopeWork line 114
  30. def OAI.EditApproximation.bandActionExpression line 120
  31. def OAI.EditApproximation.bandActionBitDegree line 140
  32. def OAI.EditApproximation.bandActionEnvironment line 142
  33. theorem OAI.EditApproximation.bandActionExpression_eval line 156
  34. theorem OAI.EditApproximation.bandActionBitBudget_fixedPower line 194