OAI/Combinatorics/ContingencyTables/Sampling/PaddedCompletions.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Zero penalties are exactly padded residual completions

Retain the small x,y views and fill every large cell with the balanced pair (A,B-A). For an assignment supported on large cells, the full margin equations are precisely the padded residual margin equations. The small positive-part penalties enforce the original nonnegative residual tests.

  1. def OAI.ContingencyTables.PaddedCompletions.smallRow line 21
  2. def OAI.ContingencyTables.PaddedCompletions.smallColumn line 24
  3. def OAI.ContingencyTables.PaddedCompletions.rowLargeCount line 27
  4. def OAI.ContingencyTables.PaddedCompletions.columnLargeCount line 30
  5. def OAI.ContingencyTables.PaddedCompletions.profile line 33
  6. def OAI.ContingencyTables.PaddedCompletions.Supported line 37
  7. def OAI.ContingencyTables.PaddedCompletions.OriginalResidualsNonnegative line 40
  8. lemma OAI.ContingencyTables.PaddedCompletions.profile_inBox line 45
  9. lemma OAI.ContingencyTables.PaddedCompletions.profile_row line 58
  10. lemma OAI.ContingencyTables.PaddedCompletions.profile_column line 70
  11. lemma OAI.ContingencyTables.PaddedCompletions.profile_small_row line 82
  12. lemma OAI.ContingencyTables.PaddedCompletions.profile_small_column line 89
  13. theorem OAI.ContingencyTables.PaddedCompletions.zero_penalty_iff_padded_completion line 97

    Source documentation

    No positivity or balance assumption is imposed on the retained small profile. Thus this exact identity covers transversals and defects.

    theorem zero_penalty_iff_padded_completion (small : I → J → Bool) (B X Y A : I → J → ℕ)
    (r : I → ℕ) (c : J → ℕ) (L : ℕ) (hA : Supported small A)
    (hX : ∀ i j, small i j=true → X i j ≤ B i j)
    (hY : ∀ i j, small i j=true → Y i j ≤ B i j)
    (hcap : ∀ i j, small i j=false → A i j ≤ B i j) :
    penalty RowColumnPenalties.cellLine (smallCoordinate small)
      (fullOffset B (fun i => r i+rowLargeCount small i*L) (fun j => c j+columnLargeCount small j*L))
      viewSlope (smallOffset small B r c) viewSlope (profile small B X Y A)=0 ↔
      OriginalResidualsNonnegative small B X Y r c ∧
        HasMargins A (fun i => r i-smallRow small X i+rowLargeCount small i*L)
          (fun j => c j-smallColumn small B Y j+columnLargeCount small j*L) := by
…

    Mentions: OAI.ContingencyTables.PaddedCompletions.Supported, OAI.ContingencyTables.RowColumnPenalties.cellLine, OAI.ContingencyTables.PaddedCompletions.rowLargeCount, OAI.ContingencyTables.PaddedCompletions.columnLargeCount, OAI.ContingencyTables.PaddedCompletions.profile, OAI.ContingencyTables.PaddedCompletions.OriginalResidualsNonnegative, OAI.ContingencyTables.HasMargins, OAI.ContingencyTables.PaddedCompletions.smallRow, OAI.ContingencyTables.PaddedCompletions.smallColumn