OAI/Combinatorics/ContingencyTables/Transport/AffinePenalty.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

The softened affine feasibility penalty

The dense sampler uses the maximum of zero and the negatives of its normalized affine table entries, minus a fixed slack. This actual penalty is continuous and convex. Its change bound is proved from the entry coefficients, including the dependent row and column entries.

  1. def OAI.ContingencyTables.AffinePenalty.affineValue line 24
  2. theorem OAI.ContingencyTables.AffinePenalty.affineValue_combine line 27
  3. theorem OAI.ContingencyTables.AffinePenalty.affineValue_change line 37
  4. def OAI.ContingencyTables.AffinePenalty.component line 55
  5. def OAI.ContingencyTables.AffinePenalty.penalty line 60
  6. theorem OAI.ContingencyTables.AffinePenalty.component_le_penalty line 64
  7. theorem OAI.ContingencyTables.AffinePenalty.penalty_nonnegative line 70
  8. theorem OAI.ContingencyTables.AffinePenalty.component_combine line 75
  9. theorem OAI.ContingencyTables.AffinePenalty.penalty_convex line 85
  10. theorem OAI.ContingencyTables.AffinePenalty.component_change line 98
  11. theorem OAI.ContingencyTables.AffinePenalty.penalty_sub_le line 115
  12. theorem OAI.ContingencyTables.AffinePenalty.penalty_change line 125
  13. theorem OAI.ContingencyTables.AffinePenalty.penalty_continuous line 137