OAI/Computability/DirectedFeedback/Games/VisibleTransfer.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DFVSGames.Decoder.VisibleTransfer.fiberEvent line 15
  2. def OAI.DFVSGames.Decoder.VisibleTransfer.fiberMass line 19
  3. theorem OAI.DFVSGames.Decoder.VisibleTransfer.fiberMass_nonnegative line 24
  4. theorem OAI.DFVSGames.Decoder.VisibleTransfer.fiberMass_mono line 29
  5. theorem OAI.DFVSGames.Decoder.VisibleTransfer.sum_fiberMass line 38
  6. theorem OAI.DFVSGames.Decoder.VisibleTransfer.observation_weight line 48
  7. def OAI.DFVSGames.Decoder.VisibleTransfer.visibleWitness line 54
  8. theorem OAI.DFVSGames.Decoder.VisibleTransfer.witness_margin_le_visible_probability line 61
  9. theorem OAI.DFVSGames.Decoder.VisibleTransfer.visibleWitness_conditional line 103
  10. theorem OAI.DFVSGames.Decoder.VisibleTransfer.visibleWitness_good line 126
  11. theorem OAI.DFVSGames.Decoder.VisibleTransfer.margin_transfer line 148
  12. theorem OAI.DFVSGames.Decoder.VisibleTransfer.wholeTable_transfer_to_visibleWitness line 159
  13. theorem OAI.DFVSGames.Decoder.VisibleTransfer.projected_witness_mass line 178
  14. def OAI.DFVSGames.Decoder.UniformFibers.selectedFiberEquiv line 208
  15. theorem OAI.DFVSGames.Decoder.UniformFibers.selectedFiberEquiv_point line 228
  16. theorem OAI.DFVSGames.Decoder.UniformFibers.conditional_probability line 234
  17. theorem OAI.DFVSGames.Decoder.ActualConditionalLaw.probability_condition_complete line 277
  18. theorem OAI.DFVSGames.Decoder.ActualConditionalLaw.observedAgreement_completeDraw line 300
  19. def OAI.DFVSGames.Decoder.ActualConditionalLaw.datumAgreement line 312
  20. theorem OAI.DFVSGames.Decoder.ActualConditionalLaw.datumAgreement_nonneg line 318
  21. theorem OAI.DFVSGames.Decoder.ActualConditionalLaw.observedAgreement_seed line 325
  22. theorem OAI.DFVSGames.Decoder.SelectedFiberLaw.univ_congr_inline_SelectedFiberLaw line 361
  23. theorem OAI.DFVSGames.Decoder.SelectedFiberLaw.condition_prob_enumeration line 366
  24. def OAI.DFVSGames.Decoder.SelectedFiberLaw.datumLeft line 381
  25. def OAI.DFVSGames.Decoder.SelectedFiberLaw.datumMatrix line 384
  26. def OAI.DFVSGames.Decoder.SelectedFiberLaw.datumProjection line 387
  27. theorem OAI.DFVSGames.Decoder.SelectedFiberLaw.datumLeft_eq line 390
  28. theorem OAI.DFVSGames.Decoder.SelectedFiberLaw.datumMatrix_rows line 396
  29. theorem OAI.DFVSGames.Decoder.SelectedFiberLaw.datumMatrix_rowAdvice line 400
  30. theorem OAI.DFVSGames.Decoder.SelectedFiberLaw.slice_assemble_iff line 410
  31. theorem OAI.DFVSGames.Decoder.SelectedFiberLaw.target_assemble_iff line 427
  32. theorem OAI.DFVSGames.Decoder.SelectedFiberLaw.exists_selected_private line 460
  33. theorem OAI.DFVSGames.Decoder.SelectedFiberLaw.good_of_selected_private line 486
  34. def OAI.DFVSGames.Decoder.SelectedFiberLaw.selectedPrivateEquiv line 497
  35. theorem OAI.DFVSGames.Decoder.SelectedFiberLaw.selectedPrivateEquiv_val line 545
  36. theorem OAI.DFVSGames.Decoder.SelectedFiberLaw.conditional_eq_transferred line 556
  37. theorem OAI.DFVSGames.Decoder.SelectedFiberLaw.visibleWitness_decoding line 637
  38. def OAI.DFVSGames.Decoder.ActualProjectedTransfer.slopeVariation line 675
  39. theorem OAI.DFVSGames.Decoder.ActualProjectedTransfer.visible_mass line 681
  40. theorem OAI.DFVSGames.Decoder.ActualProjectedTransfer.event_expectation_lower line 707
  41. theorem OAI.DFVSGames.Decoder.ActualProjectedTransfer.actual_success_lower line 725