OAI/Probability/GaussianReplacement/Hybrid.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.CurrentProjection.shannonEntropy_finite line 13
2. lemma OAI.CurrentProjection.freshInformation_finite line 21
3. lemma OAI.CurrentProjection.hybrid_block_bound line 29
4. lemma OAI.CurrentProjection.hybrid_block_numeric line 68
5. theorem OAI.CurrentProjection.hybridBlockMain line 97

   Distinct definitions of this name: ComparatorChallenges/GaussianReplacement.lean:511 (same statement text; different proof or body). Qualify references as OAI.CurrentProjection.hybridBlockMain@path.