RootedPhaseComposition.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Actual companion phase history and counting-error composition

Each stored multiplier is the explicit initial rational value followed by the actual empirical plain/defect update. Successful finite observations propagate goodness and add at most 4 eta to the logarithmic counting error.

def OAI.ContingencyTables.RootedPhaseComposition.Accurate line 26
theorem OAI.ContingencyTables.RootedPhaseComposition.weights_good line 31
Source documentation
Goodness is obtained for the actual stored phase multipliers from exact initialization and every preceding successful observation.
```
theorem weights_good (A : Instance I J) (R : RootedCompletion.Selection A.T) (samples : ℕ → List (Set (Labels A×Bool)))
    (eta : ℝ) (he0 : 0≤ eta) (he : eta≤1/4) (L : ℕ)
    (hall : ∀ j< L,Accurate A R samples eta j) :
    GoodMultipliers pairs (weight A R L) (weights A samples L) := by
…
```
Mentions: OAI.ContingencyTables.RootedCompletion.Selection, OAI.ContingencyTables.RootedPhaseComposition.Accurate
def OAI.ContingencyTables.RootedPhaseComposition.observedRatio line 45
lemma OAI.ContingencyTables.RootedPhaseComposition.observedRatio_positive line 48
def OAI.ContingencyTables.RootedPhaseComposition.estimate line 66
theorem OAI.ContingencyTables.RootedPhaseComposition.estimate_log_error line 72
Source documentation
The actual product estimator has total logarithmic error at most 4 L eta on the event that every preceding phase observation is accurate.
```
theorem estimate_log_error (A : Instance I J) (R : RootedCompletion.Selection A.T) (samples : ℕ → List (Set (Labels A×Bool)))
    (eta : ℝ) (he0 : 0≤ eta) (he : eta≤1/4) (L : ℕ)
    (hall : ∀ j< L,Accurate A R samples eta j) :
    0< estimate A R samples L ∧
      |Real.log (estimate A R samples L/total A R L)|≤4*(L:ℝ)*eta := by
…
```
Mentions: OAI.ContingencyTables.RootedCompletion.Selection, OAI.ContingencyTables.RootedPhaseComposition.Accurate, OAI.ContingencyTables.RootedPhaseComposition.estimate