OAI/Combinatorics/ContingencyTables/Transport/IntegerCorrectionKernel.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

The literal sum of future-slot correction kernels

Each summand gives exactly one unexposed ordinary pair occupancy M+1, with multiplier a(M+1-a); every other pair is summed at its ordinary balance. The coordinate changes below preserve complete configurations.

  1. def OAI.ContingencyTables.IntegerWeightedTransport.exposePullback line 19
  2. lemma OAI.ContingencyTables.IntegerWeightedTransport.exposed_profile line 24
  3. lemma OAI.ContingencyTables.IntegerWeightedTransport.expose_pair line 34
  4. lemma OAI.ContingencyTables.IntegerWeightedTransport.exposed_double_profile line 41
  5. lemma OAI.ContingencyTables.IntegerWeightedTransport.eliminate_sum line 62
  6. lemma OAI.ContingencyTables.IntegerWeightedTransport.eliminate_mul line 69
  7. lemma OAI.ContingencyTables.IntegerWeightedTransport.weighted_exposed_commute line 76

    Source documentation

    The same current and future profiles occur on both sides, including the complete fixed-domain sum over every other ordinary slot.

    lemma weighted_exposed_commute {I : Type u} (Ms : List ℕ) (U V : ℕ)
    (F : (((Coordinates I Ms ⊕ Bool) ⊕ Bool) → ℕ) → ℝ) (z : I → ℕ) :
    weightedFuture (exposedFamily Ms (marginal F U)) (V+1) z =
      marginal (weightedFuture (exposedFamily Ms (exposePullback (V::Ms) F)) (V+1)) U z := by
…

    Mentions: OAI.ContingencyTables.IntegerWeightedTransport.weightedFuture, OAI.ContingencyTables.IntegerWeightedTransport.exposedFamily, OAI.ContingencyTables.IntegerWeightedTransport.exposePullback

  8. lemma OAI.ContingencyTables.IntegerWeightedTransport.pullback_marginal line 86
  9. lemma OAI.ContingencyTables.IntegerWeightedTransport.marginal_swap_commute line 96
  10. def OAI.ContingencyTables.IntegerWeightedTransport.correctionKernel line 108
  11. theorem OAI.ContingencyTables.IntegerWeightedTransport.correctionKernel_nonnegative line 114
  12. theorem OAI.ContingencyTables.IntegerWeightedTransport.correctionKernel_current_commute line 130

    Source documentation

    Summing the currently exposed pair commutes with the literal sum of all the other future corrections.

    theorem correctionKernel_current_commute : ∀ (Ms : List ℕ) {I : Type u}
    (U : ℕ) (F : ((Coordinates I Ms ⊕ Bool) → ℕ) → ℝ),
    correctionKernel Ms (marginal F U) =
      marginal (correctionKernel Ms (exposePullback Ms F)) U := by
…

    Mentions: OAI.ContingencyTables.IntegerWeightedTransport.correctionKernel, OAI.ContingencyTables.IntegerWeightedTransport.exposePullback