OAI/Combinatorics/SquareDifference/ResidueLift.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LiftAnalysis.SquareDifference.IsSquareDifferenceFree line 14
  2. def OAI.LiftAnalysis.SquareDifference.squareStepChild line 17
  3. lemma OAI.LiftAnalysis.SquareDifference.squareStepChild_subset line 20
  4. lemma OAI.LiftAnalysis.SquareDifference.squareStepChild_free line 23
  5. lemma OAI.LiftAnalysis.SquareDifference.squareStepChild_mem line 33
  6. lemma OAI.LiftAnalysis.SquareDifference.sum_range_blocks line 37
  7. lemma OAI.LiftAnalysis.SquareDifference.squareStep_padded_sum line 63
  8. lemma OAI.LiftAnalysis.SquareDifference.ceil_square_scale line 93
  9. lemma OAI.LiftAnalysis.SquareDifference.residueGate_plus_one line 121
  10. lemma OAI.LiftAnalysis.SquareDifference.sum_exactGate_powerset line 127
  11. lemma OAI.LiftAnalysis.SquareDifference.exactGate_union line 145
  12. lemma OAI.LiftAnalysis.SquareDifference.sum_exactGate_frozen line 149
  13. lemma OAI.LiftAnalysis.SquareDifference.liftPiece_frozen_complete line 169
  14. lemma OAI.LiftAnalysis.SquareDifference.residueGate_mul_unit line 188
  15. lemma OAI.LiftAnalysis.SquareDifference.exactGate_affine line 197
  16. lemma OAI.LiftAnalysis.SquareDifference.exactGate_square_progression line 210
  17. lemma OAI.LiftAnalysis.SquareDifference.fiber_squareStep_lift line 220
  18. def OAI.SquareDifference.freezeCoordinates line 250
  19. lemma OAI.SquareDifference.freeze_update_outside line 253
  20. lemma OAI.SquareDifference.freeze_update_inside line 266
  21. lemma OAI.SquareDifference.ExactSupport.freeze line 279
  22. lemma OAI.SquareDifference.ExactSupport.finset_sum line 293
  23. lemma OAI.SquareDifference.expect_fixed_update_le line 309
  24. lemma OAI.SquareDifference.expect_freeze_le line 326
  25. lemma OAI.SquareDifference.grouped_conditional_decay line 346
  26. lemma OAI.SquareDifference.multilinearIntegral_slot line 379
  27. lemma OAI.SquareDifference.multilinearIntegral_update_sub line 388
  28. lemma OAI.SquareDifference.multilinearIntegral_telescope line 398
  29. lemma OAI.SquareDifference.diagonalRoot_zero line 436
  30. lemma OAI.SquareDifference.diagonalRoot_nonneg_smul line 445
  31. lemma OAI.SquareDifference.diagonalRoot_sum_le line 453
  32. lemma OAI.SquareDifference.diagonalRoot_expect_le line 464
  33. lemma OAI.SquareDifference.multilinear_truncation_error line 481
  34. lemma OAI.LiftAnalysis.SquareDifference.uniform_lift_moment_constant line 533
  35. def OAI.LiftAnalysis.SquareDifference.supportFamily line 550
  36. def OAI.LiftAnalysis.SquareDifference.truncatedLift line 553
  37. def OAI.LiftAnalysis.SquareDifference.remainingFamily line 556
  38. lemma OAI.LiftAnalysis.SquareDifference.primeProduct_pos line 559
  39. lemma OAI.LiftAnalysis.SquareDifference.primeProduct_mono line 566
  40. lemma OAI.LiftAnalysis.SquareDifference.primeProduct_split line 569
  41. lemma OAI.LiftAnalysis.SquareDifference.remaining_complete_sum line 576
  42. lemma OAI.LiftAnalysis.SquareDifference.frozen_low_lift_identity line 619
  43. lemma OAI.LiftAnalysis.SquareDifference.exactGate_square_progression_on line 633
  44. lemma OAI.LiftAnalysis.SquareDifference.fiber_squareStep_lift_on line 646