OAI/Combinatorics/SumProduct/Alignment/RoughJoint01.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.RoughAnalyticExtraction.mean_eq_expect line 27
  2. lemma OAI.RoughAnalyticExtraction.boxIndices_eq_halfOpen line 31
  3. lemma OAI.RoughAnalyticExtraction.physicalResidueBox_mod line 37
  4. lemma OAI.RoughAnalyticExtraction.physicalResidueBox_one line 47
  5. lemma OAI.RoughAnalyticExtraction.halfOpen_bounds_pointwise line 52
  6. def OAI.RoughAnalyticExtraction.integerDilation line 74
  7. lemma OAI.RoughAnalyticExtraction.polynomial_affine line 79
  8. def OAI.RoughAnalyticExtraction.CharacterObstruction line 87
  9. theorem OAI.RoughAnalyticExtraction.residue_haar_character line 118
  10. theorem OAI.RoughAnalyticExtraction.discrepancy_character line 180
  11. def OAI.RoughJointCoefficients.timeCoefficient line 260
  12. lemma OAI.RoughJointCoefficients.timeCoefficient_degree line 264
  13. lemma OAI.RoughJointCoefficients.gridEval_timeCoefficient line 270
  14. def OAI.RoughJointCoefficients.spatialEmbedding line 287
  15. lemma OAI.RoughJointCoefficients.fibre_polynomial line 292
  16. theorem OAI.RoughJointCoefficients.joint_character_coefficients line 304
  17. lemma OAI.RoughJointCoefficients.obstruction_on_coefficients line 321
  18. lemma OAI.RoughJointCoefficients.translationMatrix_self line 333
  19. lemma OAI.RoughJointCoefficients.translationMatrix_eq_zero_of_degree_le line 342
  20. lemma OAI.RoughJointCoefficients.gridTranslate_peeling line 357
  21. lemma OAI.RoughJointCoefficients.translationMatrix_degree_bound line 384