OAI/Probability/GaussianReplacement/Telescopes.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CurrentProjection.averaged_telescope_block line 13
  2. lemma OAI.CurrentProjection.prefix_charge_sum line 69
  3. lemma OAI.CurrentProjection.hybrid_average_ending line 104
  4. def OAI.CurrentProjection.processedKernel line 153
  5. instance OAI.CurrentProjection.processedKernel_markov line 159
  6. lemma OAI.CurrentProjection.processedKernel_apply_prod line 165
  7. lemma OAI.CurrentProjection.processedKernel_fst line 175
  8. lemma OAI.CurrentProjection.processedKernel_snd_apply line 183
  9. lemma OAI.CurrentProjection.processedKernel_reference line 194
  10. lemma OAI.CurrentProjection.compProd_processedKernel line 208
  11. lemma OAI.CurrentProjection.conditionalMutualInformation_processedKernel_le line 220
  12. def OAI.CurrentProjection.processedLaw line 235
  13. instance OAI.CurrentProjection.processedLaw_probability line 241
  14. lemma OAI.CurrentProjection.conditionalMutualInformation_processed_le line 248
  15. lemma OAI.CurrentProjection.compProd_map_base line 259
  16. lemma OAI.CurrentProjection.compProd_independent_swap line 270
  17. lemma OAI.CurrentProjection.probability_prod_subsingleton line 285
  18. lemma OAI.CurrentProjection.alignedExperiment_fresh line 298
  19. lemma OAI.CurrentProjection.exposedInformation_prefix_zero line 309
  20. def OAI.CurrentProjection.endingRowLaw line 322
  21. lemma OAI.CurrentProjection.measurable_endingRowMap line 327
  22. instance OAI.CurrentProjection.endingRowLaw_probability line 331
  23. lemma OAI.CurrentProjection.endingRowLaw_fst line 337
  24. lemma OAI.CurrentProjection.endingRowLaw_independence line 344
  25. def OAI.CurrentProjection.blockObservedInput line 356
  26. lemma OAI.CurrentProjection.measurable_blockObservedInput line 360
  27. def OAI.CurrentProjection.blockExposedBaseMap line 365
  28. lemma OAI.CurrentProjection.measurable_blockExposedBaseMap line 370
  29. lemma OAI.CurrentProjection.blockObservedInput_exposed line 374
  30. lemma OAI.CurrentProjection.block_exposed_processed line 382
  31. lemma OAI.CurrentProjection.block_exposed_le_fresh line 416