OAI/Combinatorics/Progressions/Polynomial/BooleanBlockCoefficientPhase.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Erdos3.booleanBlockValue line 12
  2. def OAI.Erdos3.booleanBlockPhase line 16
  3. theorem OAI.Erdos3.booleanBlockValue_eq_polynomial line 20
  4. def OAI.Erdos3.frozenBooleanConstant line 27
  5. theorem OAI.Erdos3.booleanAffine_resample line 31
  6. theorem OAI.Erdos3.booleanBlockValue_resample line 42
  7. theorem OAI.Erdos3.booleanCoefficient_degreeOf_le line 58
  8. theorem OAI.Erdos3.booleanSelectedColumn_degreeOf_le line 72
  9. theorem OAI.Erdos3.booleanBlockJet_eq_sampler line 97
  10. theorem OAI.Erdos3.booleanBlockPhase_eq_sampler line 108
  11. def OAI.Erdos3.frozenBooleanFactor line 125
  12. def OAI.Erdos3.frozenBooleanPhasePolynomial line 130
  13. theorem OAI.Erdos3.frozenBooleanFactor_degree line 135
  14. theorem OAI.Erdos3.frozenBooleanProduct_degree line 147
  15. theorem OAI.Erdos3.frozenBooleanPhasePolynomial_degree line 154
  16. theorem OAI.Erdos3.frozenBooleanPhasePolynomial_eval line 165
  17. theorem OAI.Erdos3.booleanBlock_scaled_jet_eq_sampler line 189
  18. theorem OAI.Erdos3.booleanBlock_scaled_phase_eq_sampler line 204