CouplingBudget.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

theorem OAI.FiniteFactor.sourceStage_L_mono line 11
theorem OAI.FiniteFactor.staged_rho_first line 16
theorem OAI.FiniteFactor.staged_rho_second line 26
theorem OAI.FiniteFactor.staged_rho_budget line 42
Source documentation
Both conditional crossing budgets now follow from the numerical source construction. The tag location j does not affect these two mixture weights.
```
theorem staged_rho_budget (j s : ℕ) (hjs : j ≤ s) (w : Fin 2) (hw : w = 0 → j < s) :
    (sourceStage j).L ≤ (sourceBlockSize s : ℝ)*(stagedCouplingParameters j s).rho w := by
…
```
Mentions: OAI.FiniteFactor.sourceStage, OAI.FiniteFactor.sourceBlockSize, OAI.FiniteFactor.stagedCouplingParameters
theorem OAI.FiniteFactor.staged_drop_budget line 55
Source documentation
The source coefficient L_j is bounded by the drop in each assigned block.
```
theorem staged_drop_budget (j s : ℕ) (hjs : j ≤ s) :
    (sourceStage j).L ≤ (sourceStage s).C :=
…
```
Mentions: OAI.FiniteFactor.sourceStage