OAI/Computability/PerfectCompleteness/Sampling/FixedSourcePairVariation.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.FixedSourcePairVariation.sigma_variation_le_const line 25
  2. abbrev OAI.PerfectCompleteness.FixedSourcePairVariation.Outer line 42
  3. def OAI.PerfectCompleteness.FixedSourcePairVariation.flags line 46
  4. abbrev OAI.PerfectCompleteness.FixedSourcePairVariation.positiveRows line 51
  5. abbrev OAI.PerfectCompleteness.FixedSourcePairVariation.experiment line 58
  6. abbrev OAI.PerfectCompleteness.FixedSourcePairVariation.Descriptor line 66
  7. def OAI.PerfectCompleteness.FixedSourcePairVariation.externalLaw line 70
  8. abbrev OAI.PerfectCompleteness.FixedSourcePairVariation.background line 76
  9. abbrev OAI.PerfectCompleteness.FixedSourcePairVariation.scalarLaw line 80
  10. abbrev OAI.PerfectCompleteness.FixedSourcePairVariation.upperRows line 84
  11. abbrev OAI.PerfectCompleteness.FixedSourcePairVariation.PairFiber line 99
  12. abbrev OAI.PerfectCompleteness.FixedSourcePairVariation.PairRecord line 104
  13. theorem OAI.PerfectCompleteness.FixedSourcePairVariation.fiber_lt_six line 107
  14. def OAI.PerfectCompleteness.FixedSourcePairVariation.actualLaw line 174
  15. def OAI.PerfectCompleteness.FixedSourcePairVariation.referenceLaw line 181
  16. theorem OAI.PerfectCompleteness.FixedSourcePairVariation.totalVariation_le_six line 188
  17. theorem OAI.PerfectCompleteness.FixedSourcePairVariation.totalVariation_le_ten line 206