OAI/Combinatorics/ContingencyTables/Rooted/RootedForestDataProgram.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Preparing a tree penalty from executed coefficients and offsets

All signed affine data are computed internally from the graph, capacities, baseline and two stored views. Only ordinary cell indices and values occur in the input; no affine coefficient or offset is supplied.

  1. abbrev OAI.ContingencyTables.RootedForestDataProgram.TermInput line 17
  2. abbrev OAI.ContingencyTables.RootedForestDataProgram.Input line 18
  3. def OAI.ContingencyTables.RootedForestDataProgram.scale line 20
  4. def OAI.ContingencyTables.RootedForestDataProgram.scaleRealizer line 23
  5. lemma OAI.ContingencyTables.RootedForestDataProgram.polynomial_scale line 29
  6. lemma OAI.ContingencyTables.RootedForestDataProgram.scale_value line 34
  7. def OAI.ContingencyTables.RootedForestDataProgram.term line 39
  8. def OAI.ContingencyTables.RootedForestDataProgram.termRealizer line 42
  9. lemma OAI.ContingencyTables.RootedForestDataProgram.polynomial_term line 51
  10. def OAI.ContingencyTables.RootedForestDataProgram.numeratorOffset line 59
  11. def OAI.ContingencyTables.RootedForestDataProgram.numeratorOffsetRealizer line 62
  12. lemma OAI.ContingencyTables.RootedForestDataProgram.polynomial_numeratorOffset line 68
  13. def OAI.ContingencyTables.RootedForestDataProgram.prepare line 74
  14. def OAI.ContingencyTables.RootedForestDataProgram.prepareRealizer line 77
  15. theorem OAI.ContingencyTables.RootedForestDataProgram.polynomial_prepare line 81
  16. lemma OAI.ContingencyTables.RootedForestDataProgram.term_input line 89
  17. def OAI.ContingencyTables.RootedForestDataProgram.data line 100
  18. theorem OAI.ContingencyTables.RootedForestDataProgram.prepare_data line 109

    Source documentation

    The generated binary input equals the exact affine tree input used by the selected-root penalty evaluation.

    theorem prepare_data {m n nc nf : ℕ} (A : Instance (Fin m) (Fin n))
    (B : ℕ) (t : GraphCompletionCounts.TreeCell A.T) (x q : Fin m → Fin n → ℤ)
    (cells : Fin nc ≃ Fin m×Fin n) (free : Fin nf ≃ FreeCell A.small A.T)
    (v : FreeCell A.small A.T → ℕ) :
    prepare (data A B t x q cells free v)=
      RootedIntegerEvaluation.forestData A (rowColumn A.T) B t x q free v := by
…

    Mentions: OAI.ContingencyTables.GraphCompletionCounts.TreeCell, OAI.ContingencyTables.RootedForestDataProgram.prepare, OAI.ContingencyTables.RootedForestDataProgram.data, OAI.ContingencyTables.RootedIntegerEvaluation.forestData

  19. theorem OAI.ContingencyTables.RootedForestDataProgram.evaluate_prepare line 128