OAI/Combinatorics/Progressions/Estimates/PreparedScalarNestedPowerDetection.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.preparedEmptyLayerLocalLengthLog line 10
  2. def OAI.Erdos3.VectorPolynomial.preparedEmptyLayerLocalScaleFloor line 33
  3. theorem OAI.Erdos3.VectorPolynomial.PreparedEmptyLayerLocalScheduleBudget.lengthLog_mem line 42
  4. theorem OAI.Erdos3.VectorPolynomial.PreparedEmptyLayerLocalScheduleBudget.scaleFloor_le line 53
  5. theorem OAI.Erdos3.VectorPolynomial.exists_preparedScalarFiniteSchedule_early_scale_power_budget line 78
  6. def OAI.Erdos3.VectorPolynomial.preparedFiniteNestedForwardFixedCenterThreshold line 122
  7. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteNestedForwardFixedCenterThreshold_bounds line 130
  8. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteNestedForwardScalarBounds line 161
  9. theorem OAI.Erdos3.VectorPolynomial.preparedRelativePositiveTerminalDetection line 228
  10. theorem OAI.Erdos3.VectorPolynomial.exists_preparedScalarNestedInput_power_budget line 277
  11. theorem OAI.Erdos3.VectorPolynomial.AllocatedExternalCandidateSampler.nativeDetection_of_preparedScalarNestedSchedule line 342
  12. def OAI.Erdos3.VectorPolynomial.PreparedScalarNestedPowerDetection line 467
  13. theorem OAI.Erdos3.VectorPolynomial.exists_preparedScalarNestedSchedule_power_detection line 515