RootedCappedReturn.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Actual selected-root capped returns with their literal fallback

def OAI.ContingencyTables.RootedCappedReturn.returnWordDefault line 22
theorem OAI.ContingencyTables.RootedCappedReturn.returnWordDefault_to_path line 29
theorem OAI.ContingencyTables.RootedCappedReturn.target_returnDefault_bound line 46

theorem OAI.ContingencyTables.RootedCappedReturn.returnWordDefault_event line 61

Source documentation

The implemented total return step is compared to the exact trace, with its cap loss left explicit for subsequent warm-law averaging.

theorem returnWordDefault_event (A : Instance I J) (R : RootedCompletion.Selection A.T) (C : ℕ) (hC : 0<C) (K j k n : ℕ)
    (hK : 1≤K) (hW : 100*A.d*K≤A.W) (hB : (K:ℝ)=binWidth A C)
    (hj : j≤rationalHeight A C) (xi : ℚ) (hx0 : 0<xi) (hx1 : xi≤1/4)
    (hPL : PublishedInputs.FiniteBoxPrekopaLeindler (dimension A))
    (hCheeger : PublishedInputs.FiniteCheeger (Grid (I := Fin (dimension A)) K))
…

Mentions: OAI.ContingencyTables.RootedCompletion.Selection, OAI.ContingencyTables.PublishedInputs.FiniteBoxPrekopaLeindler, OAI.ContingencyTables.PublishedInputs.FiniteCheeger