OAI/Combinatorics/SquareDifference/ScaleTransfer.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SquareDifference.ExactSupport.freeze_disjoint line 18
  2. lemma OAI.SquareDifference.ExactSupport.project line 40
  3. def OAI.SquareDifference.coordinateProjection line 64
  4. def OAI.SquareDifference.maskedCoordinate line 67
  5. lemma OAI.SquareDifference.coordinateProjection_translates line 69
  6. lemma OAI.SquareDifference.diagonalRoot_projection_le line 85
  7. def OAI.SquareDifference.frozenFamily line 112
  8. lemma OAI.SquareDifference.frozenFamily_moment line 116
  9. lemma OAI.SquareDifference.frozenFamily_sub_filter line 125
  10. lemma OAI.SquareDifference.frozen_family_telescope line 142
  11. abbrev OAI.SquareDifference.liftSupportFamily line 193
  12. abbrev OAI.SquareDifference.actualLiftPiece line 195
  13. abbrev OAI.SquareDifference.actualTruncatedLift line 197
  14. abbrev OAI.SquareDifference.actualRemainingFamily line 199
  15. lemma OAI.SquareDifference.actualLiftPiece_exactSupport line 206
  16. lemma OAI.SquareDifference.actualLift_projection line 214
  17. lemma OAI.SquareDifference.actualLift_projection_diagonal_le line 230
  18. lemma OAI.SquareDifference.uniform_common_lift_moments line 245
  19. lemma OAI.SquareDifference.actual_low_lift_affine_sum line 280
  20. lemma OAI.SquareDifference.diagonalIntegral_average_le line 325
  21. lemma OAI.SquareDifference.diagonalRoot_change_variables line 340
  22. lemma OAI.SquareDifference.diagonalIntegral_change_variables line 347
  23. lemma OAI.SquareDifference.diagonalIntegral_affine_average_le line 353
  24. instance OAI.SquareDifference.tupleVertexNontrivial line 374
  25. lemma OAI.SquareDifference.actual_frozen_lift_error line 385
  26. lemma OAI.SquareDifference.actual_projected_lift_error line 408
  27. lemma OAI.SquareDifference.productTupleLaw_inverse_square line 439
  28. lemma OAI.SquareDifference.scale_sum_eq_expect line 462
  29. lemma OAI.SquareDifference.diagonal_transfer_close line 468
  30. lemma OAI.SquareDifference.actual_frozen_diagonal_transfer line 475