OAI/Combinatorics/ContingencyTables/Transport/FactorialSignatures.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

Factorial congruence for the two binary lifts

The integer-to-binary signature transfer in paper 200-02, Lemma lem:binary-signatures. Coordinates with zero remaining copies are allowed; a single remaining copy gives an invalid repeated removal. The copy matrix is proved to be dominated by the integer form compressed to group means. The difference is the nonnegative within-group variance.

  1. theorem OAI.ContingencyTables.FactorialSignatures.onePositive_of_dominated_compression line 23

    Source documentation

    Domination by a compressed one-positive form preserves the signature. This is the precise group-mean argument, including forms with no positive direction.

    theorem onePositive_of_dominated_compression
    {V W : Type*} [AddCommGroup V] [Module ℝ V] [AddCommGroup W] [Module ℝ W]
    (B : BilinForm ℝ V) (C : BilinForm ℝ W) (L : W →ₗ[ℝ] V)
    (hsymm : ∀ x y, C x y = C y x) (hsig : OnePositiveDirection B)
    (hdom : ∀ v, C v v ≤ B (L v) (L v)) : OnePositiveDirection C := by
…

    Mentions: OAI.ContingencyTables.OnePositiveDirection

  2. abbrev OAI.ContingencyTables.FactorialSignatures.Copies line 38
  3. def OAI.ContingencyTables.FactorialSignatures.groupAverage line 40
  4. def OAI.ContingencyTables.FactorialSignatures.groupIndicator line 47
  5. def OAI.ContingencyTables.FactorialSignatures.groupOuter line 49
  6. def OAI.ContingencyTables.FactorialSignatures.withinCoefficient line 52
  7. def OAI.ContingencyTables.FactorialSignatures.normalizedMatrix line 55
  8. def OAI.ContingencyTables.FactorialSignatures.scaledPullback line 59
  9. def OAI.ContingencyTables.FactorialSignatures.copyMatrix line 64

    Source documentation

    Exact normalized copy matrix, including the within-group diagonal correction.

    noncomputable def copyMatrix (n : G → ℕ) (H : Matrix G G ℝ) (c : ℝ) :
    Matrix (Copies n) (Copies n) ℝ :=
…

    Mentions: OAI.ContingencyTables.FactorialSignatures.Copies

  10. lemma OAI.ContingencyTables.FactorialSignatures.grouped_form line 70
  11. lemma OAI.ContingencyTables.FactorialSignatures.groupOuter_form line 83
  12. lemma OAI.ContingencyTables.FactorialSignatures.normalized_form line 90
  13. lemma OAI.ContingencyTables.FactorialSignatures.diagonal_form line 112
  14. theorem OAI.ContingencyTables.FactorialSignatures.copyMatrix_form line 123

    Source documentation

    The factorial copy form equals the integer form on group averages minus the sum of within-group variances with their actual coefficients.

    theorem copyMatrix_form (n : G → ℕ) (H : Matrix G G ℝ) (c : ℝ) (x : Copies n → ℝ) :
    (copyMatrix n H c).toBilin' x x =
      c * H.toBilin' (groupAverage n x) (groupAverage n x) -
        ∑ u, withinCoefficient n H c u *
          ((∑ i : Fin (n u), x ⟨u, i⟩ ^ 2) -
            (∑ i : Fin (n u), x ⟨u, i⟩) ^ 2 / n u) := by
…

    Mentions: OAI.ContingencyTables.FactorialSignatures.Copies, OAI.ContingencyTables.FactorialSignatures.copyMatrix, OAI.ContingencyTables.FactorialSignatures.groupAverage, OAI.ContingencyTables.FactorialSignatures.withinCoefficient

  15. lemma OAI.ContingencyTables.FactorialSignatures.within_variance_nonnegative line 140
  16. theorem OAI.ContingencyTables.FactorialSignatures.copyMatrix_onePositive line 152

    Source documentation

    Raw integer signatures imply signatures of the actual copy matrix. Zero groups are harmless and single-copy groups require no division argument.

    theorem copyMatrix_onePositive (n : G → ℕ) (H : Matrix G G ℝ) (c : ℝ)
    (hc : 0 < c) (hH : ∀ u v, H u v = H v u)
    (hsig : OnePositiveDirection H.toBilin') (hdiag : ∀ u, 0 ≤ H u u) :
    OnePositiveDirection (copyMatrix n H c).toBilin' := by
…

    Mentions: OAI.ContingencyTables.OnePositiveDirection, OAI.ContingencyTables.FactorialSignatures.copyMatrix

  17. lemma OAI.ContingencyTables.FactorialSignatures.normalization_identity line 188
  18. theorem OAI.ContingencyTables.FactorialSignatures.copyMatrix_apply line 206

    Source documentation

    The normalization has exactly the zero diagonal and the factorial removal denominator, including single-copy and empty groups.

    theorem copyMatrix_apply (n : G → ℕ) (H : Matrix G G ℝ) (c : ℝ)
    (hzero : ∀ u, n u < 2 → H u u = 0) (i j : Copies n) :
    copyMatrix n H c i j = if i = j then 0 else
      c * H i.1 j.1 / ((n i.1 : ℝ) *
        (if i.1 = j.1 then ((n i.1 - 1 : ℕ) : ℝ) else n j.1)) := by
…

    Mentions: OAI.ContingencyTables.FactorialSignatures.Copies, OAI.ContingencyTables.FactorialSignatures.copyMatrix

  19. def OAI.ContingencyTables.FactorialSignatures.factorialProduct line 226
  20. def OAI.ContingencyTables.FactorialSignatures.removeOne line 228
  21. def OAI.ContingencyTables.FactorialSignatures.removeTwo line 230
  22. lemma OAI.ContingencyTables.FactorialSignatures.factorialProduct_positive line 233
  23. lemma OAI.ContingencyTables.FactorialSignatures.factorialProduct_removeOne line 239

    Source documentation

    Removing one labeled copy cancels precisely its coordinate count.

    lemma factorialProduct_removeOne (n : G → ℕ) (u : G) (hu : 0 < n u) :
    factorialProduct (removeOne n u) = factorialProduct n / n u := by
…

    Mentions: OAI.ContingencyTables.FactorialSignatures.factorialProduct, OAI.ContingencyTables.FactorialSignatures.removeOne

  24. theorem OAI.ContingencyTables.FactorialSignatures.factorialProduct_removeTwo line 263

    Source documentation

    Two factorial reductions yield the exact cross-group or repeated-group multiplicity denominator.

    theorem factorialProduct_removeTwo (n : G → ℕ) (u v : G)
    (hu : 0 < n u) (hv : 0 < n v - if v = u then 1 else 0) :
    factorialProduct (removeTwo n u v) = factorialProduct n /
      ((n u : ℝ) * (if u = v then ((n u - 1 : ℕ) : ℝ) else n v)) := by
…

    Mentions: OAI.ContingencyTables.FactorialSignatures.factorialProduct, OAI.ContingencyTables.FactorialSignatures.removeTwo

  25. lemma OAI.ContingencyTables.FactorialSignatures.distinct_copy_counts line 276

    Source documentation

    Distinct labeled copies give valid one-per-coordinate or repeated-coordinate removals.

    lemma distinct_copy_counts (n : G → ℕ) (i j : Copies n) (hij : i ≠ j) :
    0 < n i.1 ∧ 0 < n j.1 - if j.1 = i.1 then 1 else 0 := by
…

    Mentions: OAI.ContingencyTables.FactorialSignatures.Copies

  26. def OAI.ContingencyTables.FactorialSignatures.factorialMatrix line 295
  27. theorem OAI.ContingencyTables.FactorialSignatures.factorialMatrix_eq line 300

    Source documentation

    Exact factorial congruence with the normalized integer matrix.

    theorem factorialMatrix_eq (n : G → ℕ) (H : Matrix G G ℝ) (D : ℝ)
    (hzero : ∀ u, n u < 2 → H u u = 0) :
    factorialMatrix n H D = copyMatrix n H (factorialProduct n / D) := by
…

    Mentions: OAI.ContingencyTables.FactorialSignatures.factorialMatrix, OAI.ContingencyTables.FactorialSignatures.copyMatrix, OAI.ContingencyTables.FactorialSignatures.factorialProduct

  28. theorem OAI.ContingencyTables.FactorialSignatures.factorialMatrix_onePositive line 314

    Source documentation

    The literal factorial weights have the binary signature implied by their integer two-removal or remaining-capacity addition matrix.

    theorem factorialMatrix_onePositive (n : G → ℕ) (H : Matrix G G ℝ) (D : ℝ)
    (hD : 0 < D) (hH : ∀ u v, H u v = H v u)
    (hsig : OnePositiveDirection H.toBilin') (hdiag : ∀ u, 0 ≤ H u u)
    (hzero : ∀ u, n u < 2 → H u u = 0) :
    OnePositiveDirection (factorialMatrix n H D).toBilin' := by
…

    Mentions: OAI.ContingencyTables.OnePositiveDirection, OAI.ContingencyTables.FactorialSignatures.factorialMatrix

  29. def OAI.ContingencyTables.FactorialSignatures.ValidPair line 322
  30. lemma OAI.ContingencyTables.FactorialSignatures.validPair_symm line 326
  31. lemma OAI.ContingencyTables.FactorialSignatures.removeTwo_comm line 333
  32. def OAI.ContingencyTables.FactorialSignatures.integerRemovalMatrix line 338
  33. def OAI.ContingencyTables.FactorialSignatures.removalLiftMatrix line 341
  34. theorem OAI.ContingencyTables.FactorialSignatures.removalLift_onePositive line 347

    Source documentation

    The actual omission matrix of the first factorial lift, with all integer invalid-removal entries set to zero.

    theorem removalLift_onePositive (h : (G → ℕ) → ℝ) (n : G → ℕ) (D : ℝ)
    (hD : 0 < D) (hh : ∀ r, 0 ≤ h r)
    (hsig : OnePositiveDirection (integerRemovalMatrix h n).toBilin') :
    OnePositiveDirection (removalLiftMatrix h n D).toBilin' := by
…

    Mentions: OAI.ContingencyTables.OnePositiveDirection, OAI.ContingencyTables.FactorialSignatures.integerRemovalMatrix, OAI.ContingencyTables.FactorialSignatures.removalLiftMatrix

  35. def OAI.ContingencyTables.FactorialSignatures.addTwo line 369
  36. def OAI.ContingencyTables.FactorialSignatures.integerAdditionMatrix line 372
  37. def OAI.ContingencyTables.FactorialSignatures.additionLiftMatrix line 375
  38. theorem OAI.ContingencyTables.FactorialSignatures.additionLift_onePositive line 381

    Source documentation

    The actual addition matrix of the complementary factorial lift uses remaining-capacity factorials, and hence exactly the same congruence.

    theorem additionLift_onePositive (h : (G → ℕ) → ℝ) (r n : G → ℕ) (D : ℝ)
    (hD : 0 < D) (hh : ∀ a, 0 ≤ h a)
    (hsig : OnePositiveDirection (integerAdditionMatrix h r n).toBilin') :
    OnePositiveDirection (additionLiftMatrix h r n D).toBilin' := by
…

    Mentions: OAI.ContingencyTables.OnePositiveDirection, OAI.ContingencyTables.FactorialSignatures.integerAdditionMatrix, OAI.ContingencyTables.FactorialSignatures.additionLiftMatrix

  39. def OAI.ContingencyTables.FactorialSignatures.cellFactor line 405
  40. def OAI.ContingencyTables.FactorialSignatures.complementCellFactor line 408
  41. lemma OAI.ContingencyTables.FactorialSignatures.cellFactor_positive line 412
  42. lemma OAI.ContingencyTables.FactorialSignatures.balanced_cell_factors line 418

    Source documentation

    On transversals, the two cell multipliers agree exactly.

    lemma balanced_cell_factors (b x y : ℕ) (h : x + y = b) :
    complementCellFactor b x y = cellFactor b x y := by
…

    Mentions: OAI.ContingencyTables.FactorialSignatures.complementCellFactor, OAI.ContingencyTables.FactorialSignatures.cellFactor

  43. lemma OAI.ContingencyTables.FactorialSignatures.empty_cell_factors line 427

    Source documentation

    The empty-pair cell contributes (x+1)(y+1) to the lift ratio.

    lemma empty_cell_factors (b x y : ℕ) (h : x + y + 1 = b) :
    complementCellFactor b x y = ((x : ℝ) + 1) * ((y : ℝ) + 1) * cellFactor b x y := by
…

    Mentions: OAI.ContingencyTables.FactorialSignatures.complementCellFactor, OAI.ContingencyTables.FactorialSignatures.cellFactor

  44. lemma OAI.ContingencyTables.FactorialSignatures.full_cell_factors line 437

    Source documentation

    The full-pair cell contributes the reciprocal product 1/(xy).

    lemma full_cell_factors (b x y : ℕ) (hx : x ≤ b) (hy : y ≤ b) (h : x + y = b + 1) :
    complementCellFactor b x y * ((x : ℝ) * y) = cellFactor b x y := by
…

    Mentions: OAI.ContingencyTables.FactorialSignatures.complementCellFactor, OAI.ContingencyTables.FactorialSignatures.cellFactor

  45. lemma OAI.ContingencyTables.FactorialSignatures.quotient_square_bounds line 454
  46. lemma OAI.ContingencyTables.FactorialSignatures.defect_product_identity line 467

    Source documentation

    The product ratio when one cell contains the hole, one contains the full pair, and all remaining cells are balanced.

    lemma defect_product_identity (F T : G → ℝ) (a b : G) (hab : a ≠ b) (A B : ℝ)
    (ha : T a = A * F a) (hb : T b = F b / B)
    (hrest : ∀ u, u ≠ a → u ≠ b → T u = F u) :
    (∏ u, T u) = (A / B) * ∏ u, F u := by
…
  47. theorem OAI.ContingencyTables.FactorialSignatures.defect_lift_comparison line 487

    Source documentation

    The exact q = W² comparison between the two factorial lifts on a single-hole/single-full defect, after their common positive base weight.

    theorem defect_lift_comparison (b x y : G → ℕ) (a d : G) (had : a ≠ d)
    (W : ℕ) (hW : 0 < W) (hbW : ∀ u, b u < W)
    (hx : ∀ u, x u ≤ b u) (hy : ∀ u, y u ≤ b u)
    (ha : x a + y a + 1 = b a) (hd : x d + y d = b d + 1)
    (hrest : ∀ u, u ≠ a → u ≠ d → x u + y u = b u)
    (h : ℝ) (hh : 0 ≤ h) :
    (1 / (W : ℝ) ^ 2) * (h * ∏ u, cellFactor (b u) (x u) (y u)) ≤
      h * ∏ u, complementCellFactor (b u) (x u) (y u) ∧
    (h * ∏ u, complementCellFactor (b u) (x u) (y u)) ≤
      (W : ℝ) ^ 2 * (h * ∏ u, cellFactor (b u) (x u) (y u)) := by
…

    Mentions: OAI.ContingencyTables.FactorialSignatures.cellFactor, OAI.ContingencyTables.FactorialSignatures.complementCellFactor

  48. theorem OAI.ContingencyTables.FactorialSignatures.balanced_lift_agreement line 545

    Source documentation

    Agreement of the actual full factorial multipliers on every balanced profile.

    theorem balanced_lift_agreement (b x y : G → ℕ)
    (hbalanced : ∀ u, x u + y u = b u) (h : ℝ) :
    h * (∏ u, complementCellFactor (b u) (x u) (y u)) =
      h * ∏ u, cellFactor (b u) (x u) (y u) := by
…

    Mentions: OAI.ContingencyTables.FactorialSignatures.complementCellFactor, OAI.ContingencyTables.FactorialSignatures.cellFactor