SoftWeightUpper.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform upper mass of the positive physical softening family

lemma OAI.ContingencyTables.EqualitySoftening.factor_le_one line 13

theorem OAI.ContingencyTables.EqualitySoftening.softenedWeight_le_one line 25

Source documentation

Every actual line/unary soft factor lies in (0,1], even before the exact nonroot equations are imposed.

theorem softenedWeight_le_one (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 → ℕ) :
    softenedWeight line root rate offset slope urate ell uslope cap L z ≤ 1 := by
…

Mentions: OAI.ContingencyTables.EqualitySoftening.softenedWeight

theorem OAI.ContingencyTables.BalancedEnumeration.eliminate_le_card line 61
Source documentation
The positive softened marginal is bounded by its finite number of physical balanced assignments, uniformly in the softening parameter.
```
theorem eliminate_le_card {S : Type*} (Ms : List ℕ)
    (F : (Coordinates S Ms → ℕ) → ℝ) (hF : ∀ z,F z ≤ 1) (z : S → ℕ) :
    eliminate Ms F z ≤ (Fintype.card (Assignments Ms):ℝ) := by
…
```
Mentions: OAI.ContingencyTables.BalancedEnumeration.Assignments