OAI/Probability/GaussianReplacement/HybridModel.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CurrentProjection.blockInput line 16

    Also declared: ComparatorChallenges/GaussianReplacement.lean:265 (same declaration text).

  2. lemma OAI.CurrentProjection.measurable_blockInput line 20

    Also declared: ComparatorChallenges/GaussianReplacement.lean:269 (same declaration text).

  3. def OAI.CurrentProjection.blockLaw line 26

    Also declared: ComparatorChallenges/GaussianReplacement.lean:275 (same declaration text).

  4. instance OAI.CurrentProjection.blockLaw_probability line 32

    Also declared: ComparatorChallenges/GaussianReplacement.lean:281 (same declaration text).

  5. def OAI.CurrentProjection.endingSignalLaw line 40

    Also declared: ComparatorChallenges/GaussianReplacement.lean:289 (same declaration text).

  6. instance OAI.CurrentProjection.endingSignalLaw_probability line 46

    Also declared: ComparatorChallenges/GaussianReplacement.lean:295 (same declaration text).

  7. def OAI.CurrentProjection.freshInformation line 54

    Also declared: ComparatorChallenges/GaussianReplacement.lean:303 (same declaration text).

  8. def OAI.CurrentProjection.hybridFirst line 58

    Also declared: ComparatorChallenges/GaussianReplacement.lean:307 (same declaration text).

  9. def OAI.CurrentProjection.hybridLast line 60

    Also declared: ComparatorChallenges/GaussianReplacement.lean:309 (same declaration text).

  10. def OAI.CurrentProjection.hybridCount line 62

    Also declared: ComparatorChallenges/GaussianReplacement.lean:311 (same declaration text).

  11. def OAI.CurrentProjection.averagedFreshInformation line 64

    Also declared: ComparatorChallenges/GaussianReplacement.lean:313 (same declaration text).

  12. def OAI.CurrentProjection.HybridBlockMain line 71

    Also declared: ComparatorChallenges/GaussianReplacement.lean:319 (same declaration text).

  13. def OAI.CurrentProjection.FiberBlockMain line 87

    Also declared: ComparatorChallenges/GaussianReplacement.lean:335 (same declaration text).