OAI/Combinatorics/Progressions/Lattices/IntegerBoxObservedMean.lean

GitHub source file

29 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.BooleanCubeKernel.integerPhysicalSite line 13
  2. theorem OAI.Erdos3.BooleanCubeKernel.integerPhysicalSite_cast_apply line 17
  3. def OAI.Erdos3.BooleanCubeKernel.integerBoxCenter line 25
  4. def OAI.Erdos3.BooleanCubeKernel.centeredIntegerPhysicalSite line 27
  5. theorem OAI.Erdos3.BooleanCubeKernel.centeredIntegerPhysicalSite_cast line 30
  6. def OAI.Erdos3.BooleanCubeKernel.physicalSiteWidth line 37
  7. theorem OAI.Erdos3.BooleanCubeKernel.integerPhysicalSite_abs_bound line 41
  8. def OAI.Erdos3.integerBaseTranslation line 62
  9. theorem OAI.Erdos3.BooleanCubeKernel.integerPhysicalSite_add line 69
  10. theorem OAI.Erdos3.BooleanCubeKernel.integerPhysicalSite_baseTranslation line 76
  11. theorem OAI.Erdos3.BooleanCubeKernel.integerPhysicalSite_baseTranslation_add line 82
  12. theorem OAI.Erdos3.BooleanCubeKernel.physicalAffineSite_baseTranslation_add line 87
  13. def OAI.Erdos3.integerBoxObservation line 107
  14. theorem OAI.Erdos3.integerBoxObservation_cast line 110
  15. theorem OAI.Erdos3.integerBoxObservation_reference line 119
  16. theorem OAI.Erdos3.BooleanCubeKernel.integerBoxObservation_physical line 129
  17. def OAI.Erdos3.ResidueBoxSlice.composeSlice line 150
  18. theorem OAI.Erdos3.ResidueBoxSlice.composeSlice_point line 158
  19. def OAI.Erdos3.ResidueBoxSlice.parameterCell line 166
  20. theorem OAI.Erdos3.ResidueBoxSlice.parameterCell_point line 172
  21. theorem OAI.Erdos3.ResidueBoxSlice.stride_mul_length_le_twice line 181
  22. theorem OAI.Erdos3.ResidueBoxSlice.composeSlice_length_lower line 188
  23. theorem OAI.Erdos3.ResidueBoxSlice.length_large_of_cost line 202
  24. theorem OAI.Erdos3.ResidueBoxSlice.stride_le_twice_exp_cost line 215
  25. def OAI.Erdos3.ResidueBoxSlice.pullbackIntegerFrame line 231
  26. theorem OAI.Erdos3.ResidueBoxSlice.integerPhysicalSite_pullback line 236
  27. theorem OAI.Erdos3.ResidueBoxSlice.pullback_normalized_slope_bound line 249
  28. theorem OAI.Erdos3.integerBoxObservation_mean line 277
  29. theorem OAI.Erdos3.integerBoxObservation_complexMean line 287