OAI/Combinatorics/SumProduct/Alignment/PointLaw02.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SourcePointLaw.residue_point_law line 23
  2. lemma OAI.SourcePointLaw.residueInterval_sum line 87
  3. lemma OAI.SourcePointLaw.sum_int_Ico_zero_nat line 96
  4. lemma OAI.SourcePointLaw.sum_windowSum line 116
  5. theorem OAI.SourcePointLaw.global_point_law line 126
  6. lemma OAI.SourcePointLaw.sum_windowSum_fin line 148
  7. theorem OAI.SourcePointLaw.global_point_law_fin line 159
  8. def OAI.SourcePointLaw.betaMeasure line 185
  9. instance OAI.SourcePointLaw.betaMeasure_probability line 187
  10. def OAI.SourcePointLaw.betaImage line 194
  11. theorem OAI.SourcePointLaw.integral_betaImage line 205
  12. def OAI.SourcePointLaw.uniformMixture line 230
  13. lemma OAI.SourcePointLaw.integral_uniformMixture line 240