OAI/Combinatorics/Progressions/Lattices/RelativeSliceAffineThreeFactorLaw.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.ResidueBoxSlice.fiberParameterLength line 19
  2. def OAI.Erdos3.ResidueBoxSlice.fiberParameterStart line 23
  3. def OAI.Erdos3.ResidueBoxSlice.fiberParameterStride line 28
  4. theorem OAI.Erdos3.ResidueBoxSlice.fiberParameterLength_pos line 31
  5. theorem OAI.Erdos3.ResidueBoxSlice.fiberParameterLength_of_keep line 40
  6. theorem OAI.Erdos3.ResidueBoxSlice.fiberParameterLength_of_not_keep line 46
  7. def OAI.Erdos3.ResidueBoxSlice.fiberFullParameters line 51
  8. def OAI.Erdos3.ResidueBoxSlice.fiberKeptParameters line 59
  9. def OAI.Erdos3.ResidueBoxSlice.fiberFullParameterEquiv line 65
  10. def OAI.Erdos3.ResidueBoxSlice.fiberAffineIntegerPoint line 84
  11. theorem OAI.Erdos3.ResidueBoxSlice.fiberAffineIntegerPoint_eq line 91
  12. def OAI.Erdos3.ResidueBoxSlice.fiberAffinePointInBox line 104
  13. theorem OAI.Erdos3.ResidueBoxSlice.fiberSliceLaw_complexMean line 113
  14. theorem OAI.Erdos3.ResidueBoxSlice.fiberSliceLaw_affine_complexMean line 123
  15. def OAI.Erdos3.ResidueBoxSlice.fiberAffineLaw line 140
  16. theorem OAI.Erdos3.ResidueBoxSlice.fiberAffineLaw_complexMean line 150
  17. theorem OAI.Erdos3.ResidueBoxSlice.weights_eq_of_complexMean line 161
  18. theorem OAI.Erdos3.ResidueBoxSlice.fiberSliceLaw_eq_affineLaw line 175
  19. def OAI.Erdos3.principalAffineIntervalPoint line 199
  20. theorem OAI.Erdos3.principalAffineIntervalPoint_value line 205
  21. theorem OAI.Erdos3.principalAffineIntervalPoint_cube line 212
  22. def OAI.Erdos3.principalAffineIntervalLaw line 223
  23. theorem OAI.Erdos3.principalAffineIntervalLaw_mean line 228
  24. theorem OAI.Erdos3.principalAffineIntervalLaw_complexMean line 234
  25. theorem OAI.Erdos3.principalAffineIntervalLaw_support line 240
  26. theorem OAI.Erdos3.principalAffineIntervalLaw_cube_support line 252
  27. theorem OAI.Erdos3.principalAffineIntervalLaw_coordinate_support line 260
  28. def OAI.Erdos3.principalAffineIntervalAxisLaw line 272
  29. theorem OAI.Erdos3.principalAffineIntervalAxisLaw_complexMean line 277
  30. theorem OAI.Erdos3.principalAffineIntervalAxisLaw_mass_one line 285
  31. theorem OAI.Erdos3.ResidueBoxSlice.fiberParameter_inside line 300
  32. theorem OAI.Erdos3.ResidueBoxSlice.fiberSliceLaw_affine_sum_complexMean line 328
  33. theorem OAI.Erdos3.ResidueBoxSlice.fiberSliceLaw_affine_sum_value_complexMean line 340
  34. theorem OAI.Erdos3.ResidueBoxSlice.fiberSliceLaw_kernel_principal_complexMean line 362
  35. def OAI.Erdos3.ResidueBoxSlice.fiberKernelParameterEquiv line 384
  36. theorem OAI.Erdos3.ResidueBoxSlice.fiberSliceLaw_kernel_principal_intervals_complexMean line 396
  37. def OAI.Erdos3.principalZeroTupleFromIntegerBox line 426
  38. theorem OAI.Erdos3.principalZeroTupleFromIntegerBox_value line 432
  39. def OAI.Erdos3.principalFiberSliceLaw line 442
  40. theorem OAI.Erdos3.principalFiberSliceLaw_complexMean line 445
  41. theorem OAI.Erdos3.principalZeroTupleFromIntegerBox_affinePoint line 452
  42. theorem OAI.Erdos3.principalFiberSliceLaw_eq_affine line 467
  43. def OAI.Erdos3.ResidueBoxSlice.fiberKernelActiveShortPoint line 508
  44. theorem OAI.Erdos3.ResidueBoxSlice.fiberSliceLaw_kernel_active_short_complexMean line 524
  45. theorem OAI.Erdos3.ResidueBoxSlice.fiberSliceLaw_short_kernel_active_complexMean line 552