FirstPaperContextTransport.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Raw transport for the literal first-paper completion counts

An actual small-coordinate bijection isolates a fixed balanced prefix, the special pair, and the remaining ordinary pairs. Large completions are still the original physical finite sum; the prefix coordinates are excluded from every exchange in the transport graph.

def OAI.ContingencyTables.FirstPaperContextTransport.contextHard line 26
def OAI.ContingencyTables.FirstPaperContextTransport.contextSoft line 32
theorem OAI.ContingencyTables.FirstPaperContextTransport.contextSoft_nonnegative line 39

theorem OAI.ContingencyTables.FirstPaperContextTransport.contextSoft_slices line 51

Source documentation

The two needed slices are obtained from the physical large-cell marginal's proved raw signature, then by a principal prefix restriction.

theorem contextSoft_slices (small : I → J → Bool) (B : I → J → ℕ)
    (r : I → ℕ) (c : J → ℕ) (L : ℕ) (Ms : List ℕ)
    (e : (C ⊕ Coordinates Bool Ms) ≃ SmallView (fun a : I×J => small a.1 a.2))
    (σ mC : C → ℕ) (m : Bool → ℕ) (R : ℕ)
    (hprefix : InBox mC σ) (a : ℝ) (ha : 0 ≤ a)
    (hlarge : ∀ i j, small i j=false → 2 ≤ B i j) :
    PositiveSlice (contextSoft small B r c L Ms e σ a) (bounds m Ms) (R+Ms.sum) ∧
      RemovalSlice (contextSoft small B r c L Ms e σ a) (bounds m Ms) (R+Ms.sum) := by
…

Mentions: OAI.ContingencyTables.FirstPaperContextTransport.contextSoft

theorem OAI.ContingencyTables.FirstPaperContextTransport.contextSoft_tendsto line 66

theorem OAI.ContingencyTables.FirstPaperContextTransport.context_transport line 76

Source documentation

Hard transport for the actual padded completion count, with the prefix fixed and only the two endpoint count sums required positive.

theorem context_transport (small : I → J → Bool) (B : I → J → ℕ)
    (r : I → ℕ) (c : J → ℕ) (L : ℕ) (Ms : List ℕ)
    (e : (C ⊕ Coordinates Bool Ms) ≃ SmallView (fun a : I×J => small a.1 a.2))
    (σ mC : C → ℕ) (m z : Bool → ℕ) (R W : ℕ)
    (hprefix : InBox mC σ)
    (hlarge : ∀ i j, small i j=false → 2 ≤ B i j)
    (hlower : ∀ U ∈ Ms, 2 ≤ U) (hupper : ∀ U ∈ Ms, U ≤ W)
    (hz : InBox m z) (htotal : (∑ i, z i)=R+1)
    (H : (Coordinates Bool Ms → ℕ) → ℝ)
    (V : Finset (Coordinates Bool Ms → ℕ)) (hV : leafVertices Ms z ⊆ V)
    (hs : 0 < oneHole (eliminate Ms (contextHard small B r c L Ms e σ)) z false)
    (ht : 0 < oneHole (eliminate Ms (contextHard small B r c L Ms e σ)) z true) :
…

Mentions: OAI.ContingencyTables.FirstPaperContextTransport.contextHard