IntegerExposure.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

Exposing an ordinary pair in the actual balanced marginal

Moving one pair into the retained coordinates changes only the coordinate bijection. The remaining finite assignment sum is the same, so the actual balanced marginal partitions into precisely the U+1 child families.

def OAI.ContingencyTables.IntegerWeightedTransport.exposeEquiv line 22

Source documentation

Move the outermost pair inside all the other still-summed pairs.

def exposeEquiv {I : Type u} : (Ms : List ℕ) →
    Coordinates (I ⊕ Bool) Ms ≃ Coordinates I Ms ⊕ Bool
  | [] => Equiv.refl _
  | _::Ms => (Equiv.sumCongr (exposeEquiv (I := I) Ms) (Equiv.refl Bool)).trans swapPairs

Mentions: OAI.ContingencyTables.IntegerWeightedTransport.swapPairs

lemma OAI.ContingencyTables.IntegerWeightedTransport.expose_embedding line 27
def OAI.ContingencyTables.IntegerWeightedTransport.exposedFamily line 43
theorem OAI.ContingencyTables.IntegerWeightedTransport.exposed_marginal line 49
Source documentation
The literal child family sums back to its actual parent; the domain is the same Cartesian product of all remaining balanced profiles.
```
theorem exposed_marginal {I : Type*} (Ms : List ℕ) (U : ℕ)
    (F : ((Coordinates I Ms ⊕ Bool) → ℕ) → ℝ) :
    marginal (exposedFamily Ms F) U = eliminate (U::Ms) F := by
…
```
Mentions: OAI.ContingencyTables.IntegerWeightedTransport.exposedFamily
lemma OAI.ContingencyTables.IntegerWeightedTransport.expose_bounds line 65
lemma OAI.ContingencyTables.IntegerWeightedTransport.expose_bounds_forward line 80

theorem OAI.ContingencyTables.IntegerWeightedTransport.exposed_slices line 88

Source documentation

Remaining balanced marginalization supplies the exposed child family's positivity and signature on the exact required total slice.

theorem exposed_slices {I : Type*} [Fintype I] [DecidableEq I]
    (Ms : List ℕ) (U : ℕ) (m : I → ℕ) (R : ℕ)
    (F : ((Coordinates I Ms ⊕ Bool) → ℕ) → ℝ)
    (hwidth : ∀ M ∈ Ms, 2 ≤ M)
    (hpos : BalancedBox.PositiveSlice F (profile (bounds m Ms) U U) (R+U+Ms.sum))
    (hsig : BalancedBox.RemovalSlice F (profile (bounds m Ms) U U) (R+U+Ms.sum)) :
    BalancedBox.PositiveSlice (exposedFamily Ms F) (profile m U U) (R+U) ∧
      BalancedBox.RemovalSlice (exposedFamily Ms F) (profile m U U) (R+U) := by
…

Mentions: OAI.ContingencyTables.BalancedBox.PositiveSlice, OAI.ContingencyTables.BalancedBox.RemovalSlice, OAI.ContingencyTables.IntegerWeightedTransport.exposedFamily

theorem OAI.ContingencyTables.IntegerWeightedTransport.expose_source_positive line 107
theorem OAI.ContingencyTables.IntegerWeightedTransport.eliminate_positive line 118
theorem OAI.ContingencyTables.IntegerWeightedTransport.exposed_positive line 130