OAI/Computability/PerfectCompleteness/Decoding/FixedSourceProjectionComparison.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.PerfectCompleteness.FixedSourceProjectionComparison.projectionFlag line 18
2. abbrev OAI.PerfectCompleteness.FixedSourceProjectionComparison.Observation line 27
3. def OAI.PerfectCompleteness.FixedSourceProjectionComparison.mixedLaw line 31
4. def OAI.PerfectCompleteness.FixedSourceProjectionComparison.uniformLaw line 36
5. theorem OAI.PerfectCompleteness.FixedSourceProjectionComparison.observed_totalVariation_lt line 41
6. theorem OAI.PerfectCompleteness.FixedSourceProjectionComparison.event_probability_abs_sub_lt line 58
7. theorem OAI.PerfectCompleteness.FixedSourceProjectionComparison.event_probability_transfer line 70