OAI/Combinatorics/Progressions/Lattices/NormalizedIntegerDual.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Erdos3.BooleanCubeKernel.frameProjection_form_homogeneous line 17
  2. theorem OAI.Erdos3.BooleanCubeKernel.frameLift_siteEvaluation line 28
  3. theorem OAI.Erdos3.BooleanCubeKernel.exists_affine_vanishing_product line 37
  4. def OAI.Erdos3.BooleanCubeKernel.homogeneousDual line 85
  5. theorem OAI.Erdos3.BooleanCubeKernel.homogeneousDual_homogeneous line 89
  6. theorem OAI.Erdos3.BooleanCubeKernel.homogeneousDual_eval line 95
  7. theorem OAI.Erdos3.BooleanCubeKernel.homogeneousDual_boolean line 104
  8. def OAI.Erdos3.BooleanCubeKernel.pivotDual line 113
  9. theorem OAI.Erdos3.BooleanCubeKernel.pivotDual_boolean line 118
  10. theorem OAI.Erdos3.BooleanCubeKernel.pivotDual_homogeneous line 125
  11. theorem OAI.Erdos3.BooleanCubeKernel.homogeneousDual_mass line 141
  12. def OAI.Erdos3.BooleanCubeKernel.formMassBound line 159
  13. theorem OAI.Erdos3.BooleanCubeKernel.frameCoordinate_mass line 161
  14. theorem OAI.Erdos3.BooleanCubeKernel.frameProjection_form_mass line 198
  15. theorem OAI.Erdos3.BooleanCubeKernel.pivotDual_mass line 218
  16. def OAI.Erdos3.BooleanCubeKernel.scaledFrameForm line 241
  17. theorem OAI.Erdos3.BooleanCubeKernel.scaledFrameForm_homogeneous line 250
  18. theorem OAI.Erdos3.BooleanCubeKernel.scaledFrameForm_map line 267
  19. theorem OAI.Erdos3.BooleanCubeKernel.affineSite_map line 296
  20. theorem OAI.Erdos3.BooleanCubeKernel.affineSite_eval_map line 302
  21. theorem OAI.Erdos3.BooleanCubeKernel.scaledFrameProduct_map line 310
  22. theorem OAI.Erdos3.BooleanCubeKernel.exists_bounded_vanishing_product line 338
  23. theorem OAI.Erdos3.BooleanCubeKernel.exists_pivot_vanishing_product line 362
  24. def OAI.Erdos3.BooleanCubeKernel.integerDifferencePivot line 398
  25. theorem OAI.Erdos3.BooleanCubeKernel.integerDifferencePivot_adjugate_dual line 401
  26. def OAI.Erdos3.BooleanCubeKernel.integerPivotNumerator line 409
  27. theorem OAI.Erdos3.BooleanCubeKernel.integerPivotNumerator_homogeneous line 414
  28. theorem OAI.Erdos3.BooleanCubeKernel.integerPivotNumerator_eval line 419
  29. theorem OAI.Erdos3.BooleanCubeKernel.integerDifferencePivot_det_cast line 426
  30. theorem OAI.Erdos3.BooleanCubeKernel.integerDifferencePivot_adjugate_cast line 432
  31. theorem OAI.Erdos3.BooleanCubeKernel.integerDifferencePivot_det_bound line 438
  32. theorem OAI.Erdos3.BooleanCubeKernel.integerDifferencePivot_adjugate_bound line 446
  33. theorem OAI.Erdos3.BooleanCubeKernel.homogeneousDual_map line 454
  34. theorem OAI.Erdos3.BooleanCubeKernel.integerPivotNumerator_mass line 460
  35. def OAI.Erdos3.BooleanCubeKernel.normalizedIntegerDual line 483
  36. theorem OAI.Erdos3.BooleanCubeKernel.normalizedIntegerDual_clear line 487
  37. theorem OAI.Erdos3.BooleanCubeKernel.normalizedIntegerDual_homogeneous line 493
  38. theorem OAI.Erdos3.BooleanCubeKernel.normalizedIntegerDual_boolean line 500