OAI/Probability/LatticeSurface/Dynamics/ProjectionPattern.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ProjectionComparison.faceGraph line 12
  2. def OAI.ProjectionComparison.faceComponent line 17
  3. def OAI.ProjectionComparison.faceAverage line 20
  4. def OAI.ProjectionComparison.activePattern line 32
  5. lemma OAI.ProjectionComparison.mem_activePattern line 35
  6. lemma OAI.ProjectionComparison.faceGraph_pattern line 38
  7. lemma OAI.ProjectionComparison.faceComponent_pattern line 43
  8. lemma OAI.ProjectionComparison.measurableSet_activePattern line 48
  9. def OAI.ProjectionComparison.patternWeight line 65
  10. lemma OAI.ProjectionComparison.measurable_patternWeight line 68
  11. lemma OAI.ProjectionComparison.intervalIntegrable_patternWeight line 74
  12. lemma OAI.ProjectionComparison.sum_patternWeight line 85
  13. lemma OAI.ProjectionComparison.sum_patternWeight_mul line 90