OAI/Combinatorics/Progressions/Geometry/AllocatedPhysicalLongBoxVolume.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.VectorPolynomial.allocatedPhysicalLongJetRowBox line 23
  2. def OAI.Erdos3.VectorPolynomial.allocatedPhysicalLongJetBox line 30
  3. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalLongJetRowBox_measurable line 33
  4. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalLongJetBox_measurable line 42
  5. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalLongJetRowBox_measure_lt_top line 46
  6. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalLongJetBox_measure_lt_top line 56
  7. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalLongJetBox_of_normalizedCoordinates line 62
  8. theorem OAI.Erdos3.VectorPolynomial.allocatedActiveIntegerPhysicalScale_one_le line 116
  9. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalLongJetRowBox_measure_bound line 124
  10. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalLongJetBox_measure_bound line 148