OAI/Computability/DirectedFeedback/Games/PositiveMultiplier.lean

GitHub source file

56 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DFVSGames.Decoder.PositiveMultiplier.retained_mass_of_acceptance line 17
  2. theorem OAI.DFVSGames.Decoder.PositiveMultiplier.positive_multiplier_comparison line 54
  3. theorem OAI.DFVSGames.Decoder.PositiveMultiplier.good_fiber_mass line 87
  4. def OAI.DFVSGames.Decoder.PositiveMultiplier.equalityAcceptance line 118
  5. theorem OAI.DFVSGames.Decoder.PositiveMultiplier.color_pair_sum line 124
  6. theorem OAI.DFVSGames.Decoder.PositiveMultiplier.equalityAcceptance_fourier line 131
  7. theorem OAI.DFVSGames.Decoder.PositiveMultiplier.matrix_test_comparison line 159
  8. def OAI.DFVSGames.Decoder.PositiveMultiplier.subspaceLaw line 199
  9. theorem OAI.DFVSGames.Decoder.PositiveMultiplier.subspaceLaw_nonneg line 204
  10. theorem OAI.DFVSGames.Decoder.PositiveMultiplier.subspaceLaw_sum line 213
  11. theorem OAI.DFVSGames.Decoder.PositiveMultiplier.subspaceLaw_normalized line 223
  12. theorem OAI.DFVSGames.Decoder.PositiveMultiplier.subspaceLaw_eigenvalue line 228
  13. theorem OAI.DFVSGames.Decoder.PositiveMultiplier.subspaceLaw_eigenvalue_lower line 255
  14. theorem OAI.DFVSGames.Decoder.PositiveMultiplier.matrix_spectral_comparison line 271
  15. def OAI.DFVSGames.Fourier.SplitMaps.codomainSplit line 305
  16. def OAI.DFVSGames.Fourier.SplitMaps.domainSplit line 308
  17. theorem OAI.DFVSGames.Fourier.SplitMaps.codomainSplit_symm_apply line 311
  18. theorem OAI.DFVSGames.Fourier.SplitMaps.domainSplit_symm_apply line 314
  19. theorem OAI.DFVSGames.Fourier.SplitMaps.expect_codomain_product line 317
  20. theorem OAI.DFVSGames.Fourier.SplitMaps.expect_domain_product line 327
  21. theorem OAI.DFVSGames.Fourier.SplitMaps.sum_domain_product line 339
  22. def OAI.DFVSGames.Decoder.SurrogateFibers.shortcodeAcceptance line 369
  23. theorem OAI.DFVSGames.Decoder.SurrogateFibers.product_perturbation line 375
  24. theorem OAI.DFVSGames.Decoder.SurrogateFibers.surrogate_acceptance_eq_fiber_average line 381
  25. theorem OAI.DFVSGames.Decoder.ActualSpectral.expect_prod line 426
  26. theorem OAI.DFVSGames.Decoder.ActualSpectral.expect_eq_uniform_sum line 431
  27. theorem OAI.DFVSGames.Decoder.ActualSpectral.eigenvalue_eq_kernelProbability line 436
  28. theorem OAI.DFVSGames.Decoder.ActualSpectral.acceptance_nested line 445
  29. theorem OAI.DFVSGames.Decoder.ActualSpectral.acceptance_eq_equality_mean line 466
  30. def OAI.DFVSGames.Decoder.ActualSpectral.fiberAcceptance line 485
  31. theorem OAI.DFVSGames.Decoder.ActualSpectral.fiberAcceptance_le_one line 491
  32. theorem OAI.DFVSGames.Decoder.ActualSpectral.weighted_fiber_mean_lower line 504
  33. theorem OAI.DFVSGames.Decoder.ActualSpectral.actual_fiber_mean_lower line 526
  34. def OAI.DFVSGames.Decoder.ActualSpectral.eta line 547
  35. theorem OAI.DFVSGames.Decoder.ActualSpectral.eta_pos line 549
  36. theorem OAI.DFVSGames.Decoder.ActualSpectral.actual_good_fiber_mass line 551
  37. def OAI.DFVSGames.Inverse.RowErasure.indicator line 588
  38. theorem OAI.DFVSGames.Inverse.RowErasure.indicator_true line 592
  39. theorem OAI.DFVSGames.Inverse.RowErasure.indicator_false line 593
  40. theorem OAI.DFVSGames.Inverse.RowErasure.indicator_nonneg line 595
  41. theorem OAI.DFVSGames.Inverse.RowErasure.indicator_le_one line 600
  42. def OAI.DFVSGames.Inverse.RowErasure.uniformMass line 605
  43. theorem OAI.DFVSGames.Inverse.RowErasure.uniformMass_nonneg line 608
  44. theorem OAI.DFVSGames.Inverse.RowErasure.uniformMass_le_one line 612
  45. def OAI.DFVSGames.Inverse.RowErasure.replaceOn line 616
  46. theorem OAI.DFVSGames.Inverse.RowErasure.replaceOn_of_not_mem line 620
  47. theorem OAI.DFVSGames.Inverse.RowErasure.replaceOn_of_mem line 625
  48. def OAI.DFVSGames.Inverse.RowErasure.equalityAcceptance line 630
  49. theorem OAI.DFVSGames.Inverse.RowErasure.acceptance_le_modified_add_two_mass line 634
  50. theorem OAI.DFVSGames.Inverse.RowErasure.acceptance_ge_original_sub_two_mass line 669
  51. def OAI.DFVSGames.Inverse.RowErasure.goodUnion line 682
  52. def OAI.DFVSGames.Inverse.RowErasure.adviceMass line 685
  53. theorem OAI.DFVSGames.Inverse.RowErasure.adviceMass_nonneg line 689
  54. theorem OAI.DFVSGames.Inverse.RowErasure.union_mass_le_card_mul_adviceMass line 693
  55. theorem OAI.DFVSGames.Inverse.RowErasure.adviceMass_ge_union_div_card line 712
  56. theorem OAI.DFVSGames.Inverse.RowErasure.adviceMass_ge_of_union_mass line 720