IntegerAuxiliaryEnumeration.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The auxiliary kernel enumerates exactly one excess ordinary pair

The finite assignment carries its excess-pair position. Its raw full profile recovers the position and every choice uniquely. Box truncation removes exactly the two inadmissible endpoints of that excess pair.

def OAI.ContingencyTables.IntegerWeightedTransport.ExcessAssignments line 19

Source documentation

One distinguished ordinary pair has occupancy U+1.

@[reducible] def ExcessAssignments : List ℕ → Type
  | [] => Empty
  | U::Ms => (Assignments Ms × Fin (U+2)) ⊕ (ExcessAssignments Ms × Fin (U+1))

instance OAI.ContingencyTables.IntegerWeightedTransport.excessAssignmentsFintype line 23
def OAI.ContingencyTables.IntegerWeightedTransport.excessEmbedding line 31
def OAI.ContingencyTables.IntegerWeightedTransport.ValidExcess line 37
theorem OAI.ContingencyTables.IntegerWeightedTransport.auxiliaryKernel_eq_excess_sum line 43
Source documentation
Exact finite expansion of the actual recursive auxiliary kernel.
```
theorem auxiliaryKernel_eq_excess_sum {I : Type*} (Ms : List ℕ)
    (F : (Coordinates I Ms → ℕ) → ℝ) (z : I → ℕ) :
    auxiliaryKernel Ms F z=∑ a : ExcessAssignments Ms, F (excessEmbedding Ms z a) := by
…
```
Mentions: OAI.ContingencyTables.IntegerWeightedTransport.auxiliaryKernel, OAI.ContingencyTables.IntegerWeightedTransport.ExcessAssignments, OAI.ContingencyTables.IntegerWeightedTransport.excessEmbedding
lemma OAI.ContingencyTables.IntegerWeightedTransport.excessEmbedding_injective line 68
lemma OAI.ContingencyTables.IntegerWeightedTransport.excessEmbedding_total line 110
lemma OAI.ContingencyTables.IntegerWeightedTransport.excessEmbedding_inBox_iff line 130
theorem OAI.ContingencyTables.IntegerWeightedTransport.auxiliaryKernel_truncate_eq_valid_sum line 167
Source documentation
The zero-extended auxiliary count includes precisely the admissible single-excess-pair profiles, each once.
```
theorem auxiliaryKernel_truncate_eq_valid_sum {I : Type*} [Fintype I]
    (Ms : List ℕ) (F : (Coordinates I Ms → ℕ) → ℝ) (m z : I → ℕ) (R : ℕ)
    (hz : InBox m z) (htotal : (∑ i, z i)+1=R) :
    auxiliaryKernel Ms (truncate F (bounds m Ms) (R+Ms.sum)) z=
      ∑ a ∈ Finset.univ.filter (ValidExcess Ms), F (excessEmbedding Ms z a) := by
…
```
Mentions: OAI.ContingencyTables.IntegerWeightedTransport.auxiliaryKernel, OAI.ContingencyTables.IntegerWeightedTransport.ValidExcess, OAI.ContingencyTables.IntegerWeightedTransport.excessEmbedding