OAI/Combinatorics/ContingencyTables/Transport/ReflectedNested.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Both literal factorial lifts of the first paper's nested marginal

Reflection changes the affine offsets and signs in the full-line and small-subset penalties. The same actual positive nested factors therefore prove the complementary lift's addition property, including its hard limit.

  1. lemma OAI.ContingencyTables.ReflectedNested.smallTotal_reflect_add line 24
  2. theorem OAI.ContingencyTables.ReflectedNested.softWeight_reflect line 29
  3. theorem OAI.ContingencyTables.ReflectedNested.reflected_soft_removal line 47
  4. theorem OAI.ContingencyTables.ReflectedNested.reflected_soft_marginal line 60
  5. theorem OAI.ContingencyTables.ReflectedNested.reflected_hard_marginal line 81
  6. theorem OAI.ContingencyTables.ReflectedNested.softened_twoLift_data line 98

    Source documentation

    Both actual positive factorial lifts have their original manuscript degree and signature conventions, derived from the explicit penalties.

    theorem softened_twoLift_data {A : Type*} [Fintype A] (group : A → I)
    (Ms : List ℕ) (R : ℕ) (hR : R ≤ Fintype.card A) (D : ℝ) (hD : 0 < D)
    (line : Coordinates I Ms → G) (inner : Coordinates I Ms → Bool)
    (offset slope smallOffset smallSlope : G → ℝ) (L : ℝ) (hL : 0 ≤ L)
    (hwidth : ∀ M ∈ Ms, 2 ≤ M) :
    let h := eliminate Ms (softWeight line inner offset slope smallOffset smallSlope L)
…