OAI/Probability/SKValue/GroundState/AdaptiveColumns.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SKValueG.adaptiveResidual line 13
2. def OAI.SKValueG.adaptiveOffset line 20
3. lemma OAI.SKValueG.adaptiveResidual_measurable line 34
4. lemma OAI.SKValueG.adaptiveResidual_bound line 44
5. lemma OAI.SKValueG.adaptiveOffset_measurable line 52
6. lemma OAI.SKValueG.adaptiveOffset_integrable line 68
7. theorem OAI.SKValueG.adaptive_value_identity line 92
8. theorem OAI.SKValueG.adaptive_spin_lower line 118