CompanionPhaseComposition.lean`

9 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.CompanionPhaseComposition.weights line 22
def OAI.ContingencyTables.CompanionPhaseComposition.Accurate line 27
theorem OAI.ContingencyTables.CompanionPhaseComposition.weights_good line 32
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) (samples : ℕ → List (Set (Labels A×Bool)))
    (eta : ℝ) (he0 : 0≤ eta) (he : eta≤1/4) (L : ℕ)
    (hall : ∀ j< L,Accurate A samples eta j) :
    GoodMultipliers pairs (weight A L) (weights A samples L) := by
…
```
Mentions: OAI.ContingencyTables.CompanionPhaseComposition.Accurate, OAI.ContingencyTables.CompanionPhaseComposition.weights
def OAI.ContingencyTables.CompanionPhaseComposition.observedRatio line 44
def OAI.ContingencyTables.CompanionPhaseComposition.total line 47
lemma OAI.ContingencyTables.CompanionPhaseComposition.total_positive line 49
lemma OAI.ContingencyTables.CompanionPhaseComposition.observedRatio_positive line 52
def OAI.ContingencyTables.CompanionPhaseComposition.estimate line 70
theorem OAI.ContingencyTables.CompanionPhaseComposition.estimate_log_error line 76
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) (samples : ℕ → List (Set (Labels A×Bool)))
    (eta : ℝ) (he0 : 0≤ eta) (he : eta≤1/4) (L : ℕ)
    (hall : ∀ j< L,Accurate A samples eta j) :
    0< estimate A samples L ∧
      |Real.log (estimate A samples L/total A L)|≤4*(L:ℝ)*eta := by
…
```
Mentions: OAI.ContingencyTables.CompanionPhaseComposition.Accurate, OAI.ContingencyTables.CompanionPhaseComposition.estimate, OAI.ContingencyTables.CompanionPhaseComposition.total