OAI/Combinatorics/ContingencyTables/Rooted/ForestPenaltyApplication.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Literal companion row/column and unary tree penalties

The physical row view is ell+x; the physical column view is ell+M-y. The line groups are the disjoint original row and column coordinates. Roots are the actual chosen component roots of the large-cell forest. Only the false (row) coordinate of each tree cell carries its interval penalty. Thus the concrete exact factor family is precisely the source's nonroot indicator times its root/tree penalty weight.

  1. def OAI.ContingencyTables.ForestPenaltyApplication.physicalRow line 27
  2. def OAI.ContingencyTables.ForestPenaltyApplication.physicalColumn line 30
  3. def OAI.ContingencyTables.ForestPenaltyApplication.lineOffset line 34
  4. def OAI.ContingencyTables.ForestPenaltyApplication.deviation line 39
  5. lemma OAI.ContingencyTables.ForestPenaltyApplication.line_affine line 44
  6. def OAI.ContingencyTables.ForestPenaltyApplication.rootFlag line 62
  7. def OAI.ContingencyTables.ForestPenaltyApplication.unaryRate line 65
  8. def OAI.ContingencyTables.ForestPenaltyApplication.unaryEll line 69
  9. def OAI.ContingencyTables.ForestPenaltyApplication.unarySlope line 71
  10. def OAI.ContingencyTables.ForestPenaltyApplication.unaryCap line 73
  11. def OAI.ContingencyTables.ForestPenaltyApplication.rootPenalty line 75
  12. def OAI.ContingencyTables.ForestPenaltyApplication.treePenalty line 79
  13. def OAI.ContingencyTables.ForestPenaltyApplication.penalty line 84
  14. def OAI.ContingencyTables.ForestPenaltyApplication.physicalWeight line 88
  15. lemma OAI.ContingencyTables.ForestPenaltyApplication.line_product_eq line 94
  16. lemma OAI.ContingencyTables.ForestPenaltyApplication.unary_product_eq line 113
  17. theorem OAI.ContingencyTables.ForestPenaltyApplication.exact_eq line 133

    Source documentation

    This is the companion's literal root/tree exponential weight with exact nonroot margin indicators, in the actual row/column coordinates.

    theorem exact_eq (T : SimpleGraph (I⊕J)) (b : I → J → ℕ) (ell : I → J → ℤ)
    (M : I → J → ℕ) (r : I → ℤ) (c : J → ℤ) (alpha : ℝ) (z : ((I×J)×Bool) → ℕ) :
    physicalWeight T b ell M r c alpha z=
      if (∀ g, rootFlag T g=false → deviation ell M r c z g=0)
      then (2:ℝ)^(-alpha*penalty T b ell M r c z) else 0 := by
…

    Mentions: OAI.ContingencyTables.ForestPenaltyApplication.physicalWeight, OAI.ContingencyTables.ForestPenaltyApplication.rootFlag, OAI.ContingencyTables.ForestPenaltyApplication.deviation, OAI.ContingencyTables.ForestPenaltyApplication.penalty

  18. theorem OAI.ContingencyTables.ForestPenaltyApplication.physicalWeight_nonnegative line 154
  19. theorem OAI.ContingencyTables.ForestPenaltyApplication.exact_removal line 164

    Source documentation

    The concrete unsummed factor family has the required raw removal signature; its line and unary roles have all been physically instantiated.

    theorem exact_removal (T : SimpleGraph (I⊕J)) (b : I → J → ℕ) (ell : I → J → ℤ)
    (M : I → J → ℕ) (r : I → ℤ) (c : J → ℤ) (alpha : ℝ) (ha : 0≤alpha)
    (z : ((I×J)×Bool) → ℕ) :
    OnePositiveDirection
      (FactorialSignatures.integerRemovalMatrix (physicalWeight T b ell M r c alpha) z).toBilin' := by
…

    Mentions: OAI.ContingencyTables.OnePositiveDirection, OAI.ContingencyTables.FactorialSignatures.integerRemovalMatrix, OAI.ContingencyTables.ForestPenaltyApplication.physicalWeight