OAI/Probability/LatticeSurface/Dynamics/ProjectionKernel.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ProjectionComparison.mem_faceComponent line 12
  2. lemma OAI.ProjectionComparison.faceComponent_eq line 16
  3. lemma OAI.ProjectionComparison.faceFree_iff line 23
  4. def OAI.ProjectionComparison.faceKernel line 30
  5. lemma OAI.ProjectionComparison.faceKernel_nonneg line 34
  6. lemma OAI.ProjectionComparison.faceKernel_symm line 39
  7. lemma OAI.ProjectionComparison.faceAverage_eq_sum line 47
  8. lemma OAI.ProjectionComparison.faceKernel_row line 67
  9. lemma OAI.ProjectionComparison.faceKernel_column line 80
  10. lemma OAI.ProjectionComparison.faceAverage_constant line 83
  11. lemma OAI.ProjectionComparison.faceAverage_idempotent line 89