LabelledFactorial.lean`

15 declarations, 0 contain sorry, 0 declared as axioms

Literal subset factorial lifts and their conditioned copy displays

A display is the actual subtype of available labelled elements. Its group fibres are reindexed by Fin of their exact cardinalities. Removing or adding actual labels changes the group counts by the exact integer updates, so the conditioned subset matrices are congruent to the proved factorial copy matrices. No binary-lift signature is assumed.

def OAI.ContingencyTables.LabelledFactorial.groupCount line 22
lemma OAI.ContingencyTables.LabelledFactorial.groupCount_insert line 26
lemma OAI.ContingencyTables.LabelledFactorial.groupCount_remove line 60
lemma OAI.ContingencyTables.LabelledFactorial.groupCount_removeTwo line 77
lemma OAI.ContingencyTables.LabelledFactorial.groupCount_addTwo line 85
lemma OAI.ContingencyTables.LabelledFactorial.fibre_card line 94
def OAI.ContingencyTables.LabelledFactorial.displayCopyEquiv line 106
Source documentation
The actual finite display, reindexed fibre by fibre by its exact copy count.
```
noncomputable def displayCopyEquiv (group : I → G) (S : Set I) :
    {i // i ∈ S} ≃ Copies (groupCount group S) :=
…
```
Mentions: OAI.ContingencyTables.LabelledFactorial.groupCount
lemma OAI.ContingencyTables.LabelledFactorial.displayCopyEquiv_group line 112
lemma OAI.ContingencyTables.LabelledFactorial.groupCount_total line 115
def OAI.ContingencyTables.LabelledFactorial.firstLift line 123
def OAI.ContingencyTables.LabelledFactorial.secondLift line 126
theorem OAI.ContingencyTables.LabelledFactorial.firstLift_omission_matrix line 131
Source documentation
Every entry of the literal subset omission matrix equals the copy matrix entry at the canonical labels of the available display.
```
theorem firstLift_omission_matrix (group : I → G) (h : (G → ℕ) → ℝ) (D : ℝ) (A : Set I) :
    faceHessian (complementWeight (firstLift group h D)) A =
      (removalLiftMatrix h (groupCount group Aᶜ) D).submatrix
        (displayCopyEquiv group Aᶜ) (displayCopyEquiv group Aᶜ) := by
…
```
Mentions: OAI.ContingencyTables.LabelledFactorial.firstLift, OAI.ContingencyTables.LabelledFactorial.groupCount, OAI.ContingencyTables.LabelledFactorial.displayCopyEquiv
theorem OAI.ContingencyTables.LabelledFactorial.secondLift_addition_matrix line 148
Source documentation
The literal second-lift addition matrix has the exact remaining-capacity factorials of the canonical copy matrix.
```
theorem secondLift_addition_matrix (group : I → G) (h : (G → ℕ) → ℝ) (D : ℝ) (A : Set I) :
    faceHessian (secondLift group h D) A =
      (additionLiftMatrix h (groupCount group A) (groupCount group Aᶜ) D).submatrix
        (displayCopyEquiv group Aᶜ) (displayCopyEquiv group Aᶜ) := by
…
```
Mentions: OAI.ContingencyTables.LabelledFactorial.secondLift, OAI.ContingencyTables.LabelledFactorial.groupCount, OAI.ContingencyTables.LabelledFactorial.displayCopyEquiv
theorem OAI.ContingencyTables.LabelledFactorial.firstLift_omission line 166
Source documentation
Integer removal signatures imply the omission property of the literal first factorial lift, through the proved exact copy-display congruence.
```
theorem firstLift_omission (group : I → G) (h : (G → ℕ) → ℝ) (D : ℝ) (k : ℕ)
    (hD : 0 < D) (hh : ∀ n, 0 ≤ h n)
    (hsig : ∀ A : Set I, A.ncard + 2 = Fintype.card I - k →
      OnePositiveDirection (integerRemovalMatrix h (groupCount group Aᶜ)).toBilin') :
    OmissionProperty (firstLift group h D) k := by
…
```
Mentions: OAI.ContingencyTables.OnePositiveDirection, OAI.ContingencyTables.LabelledFactorial.groupCount, OAI.ContingencyTables.LabelledFactorial.firstLift
theorem OAI.ContingencyTables.LabelledFactorial.secondLift_addition line 185
Source documentation
Integer addition signatures imply the addition property of the literal complementary-factorial lift.
```
theorem secondLift_addition (group : I → G) (h : (G → ℕ) → ℝ) (D : ℝ) (k : ℕ)
    (hD : 0 < D) (hh : ∀ n, 0 ≤ h n)
    (hsig : ∀ A : Set I, A.ncard + 2 = k →
      OnePositiveDirection (integerAdditionMatrix h (groupCount group A) (groupCount group Aᶜ)).toBilin') :
    AdditionProperty (secondLift group h D) k := by
…
```
Mentions: OAI.ContingencyTables.OnePositiveDirection, OAI.ContingencyTables.LabelledFactorial.groupCount, OAI.ContingencyTables.LabelledFactorial.secondLift