RootShiftIntegrability.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

lemma OAI.DilutedSpinGlass.HeterogeneousMarks.measurable_root_projectionShiftError line 30
Source documentation
The exact single-copy shift error is measurable at the physical root, including all Poisson counts and its countable variable marker alphabet.
```
lemma measurable_root_projectionShiftError (Q : α → Fin L) :
    Measurable (fun z : FullRootState Y X I M =>
      projectionShiftError a C e (rootTower T P m base old z) (rootVector V z) Q) := by
…
```
Mentions: OAI.DilutedSpinGlass.FullRootState, OAI.DilutedSpinGlass.HeterogeneousMarks.rootTower, OAI.DilutedSpinGlass.HeterogeneousMarks.rootVector
lemma OAI.DilutedSpinGlass.HeterogeneousMarks.integrable_root_projectionShiftError line 49
theorem OAI.DilutedSpinGlass.HeterogeneousMarks.physical_root_shift_average line 61