OAI/Combinatorics/ContingencyTables/Rooted/RootedScaledPenalty.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Convexity and the physical scaled Lipschitz bound for selected roots

  1. def OAI.ContingencyTables.RootedScaledPenalty.normalizedOffset line 18
  2. def OAI.ContingencyTables.RootedScaledPenalty.normalizedCoefficient line 22
  3. def OAI.ContingencyTables.RootedScaledPenalty.scaledTree line 26
  4. def OAI.ContingencyTables.RootedScaledPenalty.rootConstant line 30
  5. def OAI.ContingencyTables.RootedScaledPenalty.penalty line 34
  6. lemma OAI.ContingencyTables.RootedScaledPenalty.penalty_nonnegative line 38
  7. theorem OAI.ContingencyTables.RootedScaledPenalty.penalty_change line 47
  8. theorem OAI.ContingencyTables.RootedScaledPenalty.penalty_convex line 79
  9. theorem OAI.ContingencyTables.RootedScaledPenalty.penalty_continuous line 98