OAI/Computability/MinUncut/Analysis/FaceCorrelation.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.MinUncut.Inner.faceCorrelation line 21
  2. lemma OAI.MinUncut.Inner.code_correlation_le line 25
  3. lemma OAI.MinUncut.Inner.faceCorrelation_nonneg line 29
  4. lemma OAI.MinUncut.Inner.faceCorrelation_le line 32
  5. lemma OAI.MinUncut.Inner.faceCorrelation_le_l1 line 36
  6. lemma OAI.MinUncut.Inner.faceCorrelation_add_le line 45
  7. lemma OAI.MinUncut.Inner.faceCorrelation_neg line 52
  8. lemma OAI.MinUncut.Inner.faceCorrelation_lipschitz line 56
  9. lemma OAI.MinUncut.Inner.representation_correlation line 68
  10. theorem OAI.MinUncut.Inner.gradient_convex_correlation line 87