FirstPaperPhysicalMarginal.lean`

16 declarations, 0 contain sorry, 0 declared as axioms

The first paper's physical hard marginal and its proved raw signature

This bridges the finite balanced-pair elimination theorem to the actual supported padded-completion count, in the original row/column coordinates.

def OAI.ContingencyTables.FirstPaperPhysicalMarginal.fullHardFamily line 21
def OAI.ContingencyTables.FirstPaperPhysicalMarginal.fullSoftFamily line 28
def OAI.ContingencyTables.FirstPaperPhysicalMarginal.hardMarginal line 35
def OAI.ContingencyTables.FirstPaperPhysicalMarginal.softMarginal line 42
theorem OAI.ContingencyTables.FirstPaperPhysicalMarginal.hardMarginal_eq_eliminate line 49
theorem OAI.ContingencyTables.FirstPaperPhysicalMarginal.softMarginal_eq_eliminate line 67

theorem OAI.ContingencyTables.FirstPaperPhysicalMarginal.softMarginal_slices line 87

Source documentation

The literal positive soft count has its raw removal signature on every required profile box and degree, before taking the hard limit.

theorem softMarginal_slices (small : I → J → Bool) (B : I → J → ℕ)
    (r : I → ℕ) (c : J → ℕ) (L : ℕ) (a : ℝ) (ha : 0≤a)
    (m : SmallView (fun a : I×J => small a.1 a.2) → ℕ) (R : ℕ)
    (hwidth : ∀ i j, small i j=false → 2≤B i j) :
    PositiveSlice (softMarginal small B r c L a) m R ∧
      RemovalSlice (softMarginal small B r c L a) m R := by
…

Mentions: OAI.ContingencyTables.FirstPaperPhysicalMarginal.softMarginal

theorem OAI.ContingencyTables.FirstPaperPhysicalMarginal.softMarginal_tendsto line 104
theorem OAI.ContingencyTables.FirstPaperPhysicalMarginal.hardMarginal_removal line 119
theorem OAI.ContingencyTables.FirstPaperPhysicalMarginal.hardMarginal_reflected line 135

theorem OAI.ContingencyTables.FirstPaperPhysicalMarginal.hardMarginal_eq_completionCount line 153

Source documentation

The exact finite marginal agrees with the original supported padded completion count, on its actual capacity box.

theorem hardMarginal_eq_completionCount (small : I → J → Bool) (B : I → J → ℕ)
    (r : I → ℕ) (c : J → ℕ) (L : ℕ)
    (z : SmallView (fun a : I×J => small a.1 a.2) → ℕ)
    (hz : ∀ u, z u≤B u.1.val.1 u.1.val.2)
    (hB : ∀ i j, small i j=false →
      (∑ k, (r k-smallRow small (smallView small z false) k+rowLargeCount small k*L))≤B i j) :
    hardMarginal small B r c L z=
      if OriginalResidualsNonnegative small B (smallView small z false) (smallView small z true) r c
      then (Fintype.card (LargeCompletion small
        (fun i => r i-smallRow small (smallView small z false) i+rowLargeCount small i*L)
        (fun j => c j-smallColumn small B (smallView small z true) j+columnLargeCount small j*L)):ℝ)
      else 0 := by
…

Mentions: OAI.ContingencyTables.FirstPaperPhysicalMarginal.hardMarginal

def OAI.ContingencyTables.FirstPaperPhysicalMarginal.paperSmall line 174
def OAI.ContingencyTables.FirstPaperPhysicalMarginal.firstMarginal line 177
theorem OAI.ContingencyTables.FirstPaperPhysicalMarginal.firstMarginal_eq_hard line 183
Source documentation
This specializes the finite-count identification to the manuscript's exact d, d^12 padding, d^20 small capacity and C=N+dL+U+2.
```
theorem firstMarginal_eq_hard (r : I → ℕ) (c : J → ℕ)
    (z : SmallView (fun a : I×J => paperSmall r c a.1 a.2) → ℕ)
    (hz : ∀ u, z u≤dimensionAllowance (I := I) (J := J)^20) :
…
```
Mentions: OAI.ContingencyTables.FirstPaperPhysicalMarginal.paperSmall
theorem OAI.ContingencyTables.FirstPaperPhysicalMarginal.firstMarginal_removal line 208
Source documentation
The original supported completion weight inherits its hard-limit raw signature. It is allowed to vanish; no hard degree positivity is claimed.
```
theorem firstMarginal_removal (r : I → ℕ) (c : J → ℕ) (R : ℕ) :
    RemovalSlice (firstMarginal r c)
      (fun _ => dimensionAllowance (I := I) (J := J)^20) R := by
…
```
Mentions: OAI.ContingencyTables.FirstPaperPhysicalMarginal.firstMarginal
theorem OAI.ContingencyTables.FirstPaperPhysicalMarginal.firstMarginal_reflected line 223