OAI/Combinatorics/ContingencyTables/Sampling/FirstPaperProfiles.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.FirstPaperProfiles.smallView line 15
2. def OAI.ContingencyTables.FirstPaperProfiles.supportedAssignmentEquiv line 22

   Source documentation

   A choice for each large cell extends uniquely by zero on small cells, exactly as used by the manuscript's supported residual completion sum.

   noncomputable def supportedAssignmentEquiv (small : I → J → Bool) (B : I → J → ℕ) :
       PhysicalAssignments (fun a : I×J => small a.1 a.2) (fun a => B a.1 a.2) ≃
         Assignment small B where
   …

3. lemma OAI.ContingencyTables.FirstPaperProfiles.physicalProfile_supported line 41
4. theorem OAI.ContingencyTables.FirstPaperProfiles.physicalHardSum_eq_supported line 59

   Source documentation

   The finite product used in the signature proof counts exactly the supported assignments used in the residual completion equivalence.

   theorem physicalHardSum_eq_supported (small : I → J → Bool) (B : I → J → ℕ)
       (z : SmallView (fun a : I×J => small a.1 a.2) → ℕ)
       (r : I → ℕ) (c : J → ℕ) (L : ℕ) :
       (∑ a : PhysicalAssignments (fun a : I×J => small a.1 a.2) (fun a => B a.1 a.2),
         NestedPenaltyApplication.hardWeight RowColumnPenalties.cellLine
           (RowColumnPenalties.smallCoordinate small)
           (RowColumnPenalties.fullOffset B
             (fun i => r i+PaddedCompletions.rowLargeCount small i*L)
             (fun j => c j+PaddedCompletions.columnLargeCount small j*L)) RowColumnPenalties.viewSlope
           (RowColumnPenalties.smallOffset small B r c) RowColumnPenalties.viewSlope
           (physicalProfile (fun a : I×J => small a.1 a.2) (fun a => B a.1 a.2) z a))=
         ∑ a : Assignment small B,
   …

   Mentions: OAI.ContingencyTables.NestedPenaltyApplication.hardWeight, OAI.ContingencyTables.RowColumnPenalties.cellLine, OAI.ContingencyTables.RowColumnPenalties.smallCoordinate, OAI.ContingencyTables.RowColumnPenalties.fullOffset, OAI.ContingencyTables.PaddedCompletions.rowLargeCount, OAI.ContingencyTables.PaddedCompletions.columnLargeCount, OAI.ContingencyTables.RowColumnPenalties.viewSlope, OAI.ContingencyTables.RowColumnPenalties.smallOffset