OAI/Combinatorics/ContingencyTables/Transport/EqualitySoftening.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

Root penalties and exact nonroot equations

Root lines carry their actual absolute-deviation penalty. Nonroot lines carry a positive equality softener; its limit is the exact prescribed-line indicator. Unary interval penalties include the companion's tree factors. All balanced large-cell sums are performed before this finite limit.

  1. def OAI.ContingencyTables.EqualitySoftening.lineFactor line 23
  2. def OAI.ContingencyTables.EqualitySoftening.exactLineFactor line 27
  3. def OAI.ContingencyTables.EqualitySoftening.affineDistance line 33

    Source documentation

    A physical affine coordinate, including a reflected tree coordinate.

    noncomputable def affineDistance (ell slope cap : ℝ) (n : ℕ) : ℝ :=
…
  4. lemma OAI.ContingencyTables.EqualitySoftening.affineDistance_convex line 36
  5. def OAI.ContingencyTables.EqualitySoftening.unaryFactor line 50
  6. def OAI.ContingencyTables.EqualitySoftening.softenedWeight line 53
  7. def OAI.ContingencyTables.EqualitySoftening.exactWeight line 58
  8. lemma OAI.ContingencyTables.EqualitySoftening.softenedWeight_positive line 62
  9. theorem OAI.ContingencyTables.EqualitySoftening.softenedWeight_removal line 69

    Source documentation

    The actual positive factors prove the raw signature; it is not an assumption about a previously lifted binary weight.

    theorem softenedWeight_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) (z : C → ℕ) :
    OnePositiveDirection
      (integerRemovalMatrix (softenedWeight line root rate offset slope urate ell uslope cap L) z).toBilin' := by
…

    Mentions: OAI.ContingencyTables.OnePositiveDirection, OAI.ContingencyTables.EqualitySoftening.softenedWeight

  10. lemma OAI.ContingencyTables.EqualitySoftening.lineFactor_tendsto line 88
  11. theorem OAI.ContingencyTables.EqualitySoftening.softenedWeight_tendsto line 96
  12. theorem OAI.ContingencyTables.EqualitySoftening.exactWeight_removal line 106

    Source documentation

    The exact-equality product itself inherits its finite raw signature.

    theorem exactWeight_removal (line : C → G) (root : G → Bool)
    (rate offset slope : G → ℝ) (urate ell uslope cap : C → ℝ)
    (hrate : ∀ g, 0 ≤ rate g) (hu : ∀ i, 0 ≤ urate i) (z : C → ℕ) :
    OnePositiveDirection
      (integerRemovalMatrix (exactWeight line root rate offset slope urate ell uslope cap) z).toBilin' := by
…

    Mentions: OAI.ContingencyTables.OnePositiveDirection, OAI.ContingencyTables.EqualitySoftening.exactWeight

  13. theorem OAI.ContingencyTables.EqualitySoftening.exact_marginal_removal line 123

    Source documentation

    This is the actual finite balanced large-cell marginal with exact nonroot equations. Positive softening is retained through every sum and removed only after the last sum.

    theorem exact_marginal_removal (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 (eliminate Ms (exactWeight line root rate offset slope urate ell uslope cap)) m R := by
…

    Mentions: OAI.ContingencyTables.EqualitySoftening.exactWeight