OAI/Computability/DirectedFeedback/Encoding/SelectedPolicies.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DFVSGames.Decoder.SelectedPolicies.matrixTable line 19
  2. def OAI.DFVSGames.Decoder.SelectedPolicies.fullTable line 27
  3. theorem OAI.DFVSGames.Decoder.SelectedPolicies.matrixTable_fold line 32
  4. def OAI.DFVSGames.Decoder.SelectedPolicies.GoodAdvice line 54
  5. def OAI.DFVSGames.Decoder.SelectedPolicies.normalizedDescription line 60
  6. theorem OAI.DFVSGames.Decoder.SelectedPolicies.normalizedDescription_spec line 69
  7. def OAI.DFVSGames.Decoder.SelectedPolicies.normalizedResponse line 89
  8. theorem OAI.DFVSGames.Decoder.SelectedPolicies.normalizedResponse_dimension line 100
  9. def OAI.DFVSGames.Decoder.SelectedPolicies.goodPredicate line 109
  10. theorem OAI.DFVSGames.Decoder.SelectedPolicies.chosenWitness_eq_normalizedResponse line 116
  11. theorem OAI.DFVSGames.Decoder.SelectedPolicies.leftPolicy_eq_candidateLaw line 126
  12. theorem OAI.DFVSGames.Decoder.SelectedPolicies.normalized_point_row line 136
  13. theorem OAI.DFVSGames.Decoder.SelectedPolicies.normalized_target line 152
  14. abbrev OAI.DFVSGames.Decoder.ActualSeedEvents.Seed line 179
  15. abbrev OAI.DFVSGames.Decoder.ActualSeedEvents.Datum line 182
  16. def OAI.DFVSGames.Decoder.ActualSeedEvents.law line 185
  17. def OAI.DFVSGames.Decoder.ActualSeedEvents.draw line 191
  18. def OAI.DFVSGames.Decoder.ActualSeedEvents.pad line 194
  19. def OAI.DFVSGames.Decoder.ActualSeedEvents.slice line 198
  20. def OAI.DFVSGames.Decoder.ActualSeedEvents.targetHit line 203
  21. theorem OAI.DFVSGames.Decoder.ActualSeedEvents.pad_eq line 208
  22. theorem OAI.DFVSGames.Decoder.ActualSeedEvents.slice_eq_selectedEvent line 215
  23. theorem OAI.DFVSGames.Decoder.ActualSeedEvents.targetHit_eq_selectedMatch line 226
  24. theorem OAI.DFVSGames.Decoder.ActualSeedEvents.slice_good line 237
  25. theorem OAI.DFVSGames.Decoder.ActualSeedVariation.uniform_pushforward_equiv line 274
  26. theorem OAI.DFVSGames.Decoder.ActualSeedVariation.totalVariation_pushforward_equiv line 283
  27. theorem OAI.DFVSGames.Decoder.ActualSeedVariation.ideal_full_uniform line 291
  28. theorem OAI.DFVSGames.Decoder.ActualSeedVariation.ideal_pad_coordinates line 303
  29. theorem OAI.DFVSGames.Decoder.ActualSeedVariation.actual_totalVariation_le_slope line 312
  30. instance OAI.DFVSGames.Decoder.SelectedDecoding.affineSliceFintype line 352
  31. theorem OAI.DFVSGames.Decoder.SelectedDecoding.selectedEvent_iff_normalized line 362
  32. theorem OAI.DFVSGames.Decoder.SelectedDecoding.selectedMatch_iff_normalized line 386
  33. theorem OAI.DFVSGames.Decoder.SelectedDecoding.rowKernel_reciprocal_le line 424
  34. def OAI.DFVSGames.Decoder.SelectedDecoding.transferredAgreement line 432
  35. theorem OAI.DFVSGames.Decoder.SelectedDecoding.observedAgreement_lower line 445
  36. theorem OAI.DFVSGames.Decoder.ProjectedColumnSlice.column_agreement_iff line 495
  37. theorem OAI.DFVSGames.Decoder.ProjectedColumnSlice.contains_padded_iff line 510
  38. def OAI.DFVSGames.Decoder.ProjectedColumnSlice.paddedSliceEquiv line 547
  39. theorem OAI.DFVSGames.Decoder.ProjectedColumnSlice.paddedSlice_expect line 564
  40. theorem OAI.DFVSGames.Decoder.ProjectedColumnSlice.fullTable_padded line 584
  41. theorem OAI.DFVSGames.Decoder.ProjectedColumnSlice.normalized_contains_iff line 596
  42. theorem OAI.DFVSGames.Decoder.ProjectedColumnSlice.normalized_target_padded line 617
  43. theorem OAI.DFVSGames.Decoder.UniformConditioning.sum_over_event line 646
  44. theorem OAI.DFVSGames.Decoder.UniformConditioning.probability_as_subtype_sum line 651
  45. theorem OAI.DFVSGames.Decoder.UniformConditioning.probability_and_as_subtype_sum line 655
  46. theorem OAI.DFVSGames.Decoder.UniformConditioning.probability_of_constant_weight line 667
  47. theorem OAI.DFVSGames.Decoder.UniformConditioning.condition_probability_uniform line 678
  48. theorem OAI.DFVSGames.Decoder.UniformConditioning.condition_probability_equiv line 704