OAI/Combinatorics/Progressions/Estimates/PreparedFiniteNestedForwardCanonicalFixedCenterSource.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.unconditionedSpatialTrimFraction_inv_pow_bound line 13
  2. theorem OAI.Erdos3.unconditionedSpatialTrimFraction_exp_bounds line 23
  3. theorem OAI.Erdos3.VectorPolynomial.preparedUniformDegreeDirectLate_extra_le line 43
  4. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteScheduleDirectLate_extra_le_sum line 49
  5. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteScheduleScale_le_exp_late line 62
  6. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteSchedule_kernel_input_le line 71
  7. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardPairedSourcePrecision_gain_lower line 93
  8. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteScheduleLocalPhysical_gain line 106
  9. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteScheduleLocalPhysical_tau_inv line 128
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedExternalCandidatePreparedGood_of_model line 186
  11. theorem OAI.Erdos3.VectorPolynomial.preparedScalarFiniteScheduleLocalPhysical_model_add line 250
  12. theorem OAI.Erdos3.VectorPolynomial.preparedScalarFiniteScheduleLocalPhysical_model line 274
  13. theorem OAI.Erdos3.VectorPolynomial.preparedFiniteForwardWork_cubic_lower line 299
  14. theorem OAI.Erdos3.VectorPolynomial.preparedScalarFiniteScheduleLocalPhysical_exp_trim line 312
  15. theorem OAI.Erdos3.VectorPolynomial.preparedScalarFiniteScheduleLocalPhysical_nested_exp_trim line 334
  16. theorem OAI.Erdos3.VectorPolynomial.allocatedExternalPreparedProductiveCenter_of_model line 367
  17. theorem OAI.Erdos3.VectorPolynomial.exists_preparedFiniteScheduleProductiveFixedCenterSource line 502
  18. theorem OAI.Erdos3.VectorPolynomial.exists_preparedFiniteNestedForwardProductiveFixedCenterSource line 656
  19. theorem OAI.Erdos3.VectorPolynomial.exists_preparedFiniteNestedForwardCanonicalFixedCenterSource line 1034