OAI/Combinatorics/Progressions/Estimates/AllocatedReferenceJetWindow.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.BooleanCubeKernel.translatePhysicalCube line 12
  2. theorem OAI.Erdos3.BooleanCubeKernel.physicalCubeVertexValue_translate line 16
  3. theorem OAI.Erdos3.BooleanCubeKernel.physicalResidueReconstruction_translate line 24
  4. theorem OAI.Erdos3.BooleanCubeKernel.physicalCubeCoveredSample_translate line 33
  5. theorem OAI.Erdos3.BooleanCubeKernel.physicalCubeEuclideanSample_translate line 54
  6. theorem OAI.Erdos3.BooleanCubeKernel.physicalCubeRowSample_translate line 77
  7. theorem OAI.Erdos3.BooleanCubeKernel.physicalResidueReconstruction_injective line 102
  8. theorem OAI.Erdos3.BooleanCubeKernel.physicalResidueReconstruction_columnResidue line 112
  9. theorem OAI.Erdos3.BooleanCubeKernel.physicalResidueReconstruction_jet_sum line 123
  10. theorem OAI.Erdos3.BooleanCubeKernel.spatialWindow_four_coordinate_bound line 149
  11. theorem OAI.Erdos3.BooleanCubeKernel.physicalCube_zero_residue_bound line 165
  12. def OAI.Erdos3.BooleanCubeKernel.referenceJetEnvelopeWidths line 186
  13. theorem OAI.Erdos3.BooleanCubeKernel.referenceJetEnvelopeWidths_pos line 190
  14. theorem OAI.Erdos3.BooleanCubeKernel.referenceJetEnvelopeWidths_residue line 195
  15. theorem OAI.Erdos3.BooleanCubeKernel.physicalResidueReconstruction_envelope line 202
  16. theorem OAI.Erdos3.BooleanCubeKernel.referenceJetEnvelopeWidths_trimmed line 239
  17. theorem OAI.Erdos3.VectorPolynomial.allocatedPhysicalCube_coefficient_row_sum line 264
  18. theorem OAI.Erdos3.VectorPolynomial.allocatedNarrow_reference_jet_geometry line 275
  19. theorem OAI.Erdos3.VectorPolynomial.allocatedNarrow_reference_comparison_geometry line 307