OAI/Combinatorics/Progressions/Lattices/AllocatedRecoveredIntegerFullChart.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.jointIntegerFullChart line 15
  2. theorem OAI.Erdos3.VectorPolynomial.jointIntegerFullChart_support line 18
  3. theorem OAI.Erdos3.VectorPolynomial.jointIntegerFullChart_spatial line 33
  4. theorem OAI.Erdos3.VectorPolynomial.cast_jointIntegerPhysicalSite_eq_frame line 42
  5. theorem OAI.Erdos3.VectorPolynomial.eval_jointIntegerPhysicalSite_eq_frame line 50
  6. def OAI.Erdos3.VectorPolynomial.allocatedRecoveredIntegerFullChart line 76
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedRecoveredIntegerFullChart_support line 86
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedRecoveredIntegerFullChart_spatial line 95
  9. theorem OAI.Erdos3.VectorPolynomial.AllocatedCenteredFramedRecoveredSampleAt.integerFullChart_remainder line 104
  10. theorem OAI.Erdos3.VectorPolynomial.AllocatedCenteredFramedRecoveredSampleAt.integerFullChart_residual line 135
  11. theorem OAI.Erdos3.VectorPolynomial.AllocatedCenteredFramedRecoveredSampleAt.integerFullChart_low_residual line 156