ReflectedSlices.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Reflected actual penalties and the complementary factorial lift

Reflecting a physical box changes affine offsets and reverses their slopes. The root/equality and unary interval factors therefore have the same proved scalar signatures. All finite balanced pairs are reflected as well, before transferring the resulting addition signature to labels.

lemma OAI.ContingencyTables.ReflectedSlices.lineTotal_reflect_add line 25
lemma OAI.ContingencyTables.ReflectedSlices.affine_reflect line 36
theorem OAI.ContingencyTables.ReflectedSlices.softenedWeight_reflect line 42
lemma OAI.ContingencyTables.ReflectedSlices.removal_congr_box line 63

theorem OAI.ContingencyTables.ReflectedSlices.reflected_softened_removal line 73

Source documentation

The original globally reflected positive weight has its raw removal signature throughout the physical box, from explicit reflected factors.

theorem reflected_softened_removal (line : C → G) (root : G → Bool)
    (rate offset slope : G → ℝ) (urate ell uslope cap : C → ℝ) (L : ℝ)
    (hrate : ∀ g, 0 ≤ rate g) (hu : ∀ i, 0 ≤ urate i) (hL : 0 ≤ L)
    (m z : C → ℕ) (hz : InBox m z) :
    OnePositiveDirection (integerRemovalMatrix
      (fun x => softenedWeight line root rate offset slope urate ell uslope cap L (reflect m x)) z).toBilin' := by
…

Mentions: OAI.ContingencyTables.OnePositiveDirection

theorem OAI.ContingencyTables.ReflectedSlices.reflected_softened_marginal line 89

Source documentation

The companion's actual positive finite marginal has the reflected removal signature needed for its two-addition matrix.

theorem reflected_softened_marginal (Ms : List ℕ) (m : I → ℕ) (R : ℕ)
    (line : Coordinates I Ms → G) (root : G → Bool) (rate offset slope : G → ℝ)
    (urate ell uslope cap : Coordinates I Ms → ℝ) (L : ℝ)
    (hwidth : ∀ M ∈ Ms, 2 ≤ M) (hrate : ∀ g, 0 ≤ rate g)
    (hu : ∀ i, 0 ≤ urate i) (hL : 0 ≤ L) :
    RemovalSlice
      (fun z => eliminate Ms (softenedWeight line root rate offset slope urate ell uslope cap L)
        (reflect m z)) m R := by
…

theorem OAI.ContingencyTables.ReflectedSlices.reflected_exact_marginal line 115

Source documentation

The reflected addition input survives the nonroot-equality limit after all balanced large-cell sums, exactly as the removal input does.

theorem reflected_exact_marginal (Ms : List ℕ) (m : I → ℕ) (R : ℕ)
    (line : Coordinates I Ms → G) (root : G → Bool) (rate offset slope : G → ℝ)
    (urate ell uslope cap : Coordinates I Ms → ℝ)
    (hwidth : ∀ M ∈ Ms, 2 ≤ M) (hrate : ∀ g, 0 ≤ rate g) (hu : ∀ i, 0 ≤ urate i) :
    RemovalSlice
      (fun z => eliminate Ms (exactWeight line root rate offset slope urate ell uslope cap)
        (reflect m z)) m R := by
…

lemma OAI.ContingencyTables.ReflectedSlices.groupCount_complement line 138

theorem OAI.ContingencyTables.ReflectedSlices.secondLift_addition_reflected_slice line 150

Source documentation

The actual reflected raw slice proves the addition property of the literal complementary-factorial lift in the original coordinates.

theorem secondLift_addition_reflected_slice (group : A → C) (h : (C → ℕ) → ℝ)
    (D : ℝ) (R : ℕ) (hR : R ≤ Fintype.card A) (hD : 0 < D) (hh : ∀ z, 0 ≤ h z)
    (hsig : RemovalSlice (fun z => h (reflect (groupCount group Set.univ) z))
      (groupCount group Set.univ) (Fintype.card A-R)) :
    BinaryContraction.AdditionProperty (secondLift group h D) R := by
…

Mentions: OAI.ContingencyTables.BinaryContraction.AdditionProperty