OAI/Computability/DirectedFeedback/Games/FinalParameters.lean

GitHub source file

92 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.DFVSGames.Integration.FinalParameters.rho line 10
  2. def OAI.DFVSGames.Integration.FinalParameters.levelConstant line 11
  3. def OAI.DFVSGames.Integration.FinalParameters.alpha line 12
  4. def OAI.DFVSGames.Integration.FinalParameters.beta line 13
  5. def OAI.DFVSGames.Integration.FinalParameters.theta line 14
  6. def OAI.DFVSGames.Integration.FinalParameters.repetitionRate line 15
  7. theorem OAI.DFVSGames.Integration.FinalParameters.levelConstant_pos line 17
  8. theorem OAI.DFVSGames.Integration.FinalParameters.rho_pos line 21
  9. theorem OAI.DFVSGames.Integration.FinalParameters.theta_pos line 25
  10. theorem OAI.DFVSGames.Integration.FinalParameters.repetitionRate_bounds line 30
  11. theorem OAI.DFVSGames.Integration.FinalParameters.exists_symbol_dimension line 33
  12. theorem OAI.DFVSGames.Integration.FinalParameters.exists_repetition_and_dimension line 49
  13. def OAI.DFVSGames.Integration.FinalParameters.gamma line 66
  14. theorem OAI.DFVSGames.Integration.FinalParameters.gamma_bounds line 68
  15. theorem OAI.DFVSGames.Integration.FinalParameters.exists_source_error line 78
  16. theorem OAI.DFVSGames.Integration.FinalParameters.exists_parameters line 87
  17. theorem OAI.DFVSGames.Integration.FinalParameters.completeness_budget line 110
  18. abbrev OAI.DFVSGames.Gadget.ActualGadget.F2 line 121
  19. structure OAI.DFVSGames.Gadget.ActualGadget.Data line 123
  20. def OAI.DFVSGames.Gadget.ActualGadget.failureIndicator line 142
  21. def OAI.DFVSGames.Gadget.ActualGadget.stabilityError line 146
  22. def OAI.DFVSGames.Gadget.ActualGadget.kernelIndicator line 149
  23. def OAI.DFVSGames.Gadget.ActualGadget.kernelError line 154
  24. theorem OAI.DFVSGames.Gadget.ActualGadget.stabilityError_nonneg line 158
  25. theorem OAI.DFVSGames.Gadget.ActualGadget.stabilityError_le_one line 165
  26. theorem OAI.DFVSGames.Gadget.ActualGadget.kernelError_nonneg line 172
  27. theorem OAI.DFVSGames.Gadget.ActualGadget.kernelError_le_one line 180
  28. def OAI.DFVSGames.Gadget.ActualGadget.leaf line 188
  29. def OAI.DFVSGames.Gadget.ActualGadget.Satisfies line 197
  30. def OAI.DFVSGames.Gadget.ActualGadget.StableNonlinearDispersion line 202
  31. structure OAI.DFVSGames.Reduction.ActualSource.Source line 214
  32. def OAI.DFVSGames.Reduction.ActualSource.Source.sourceList line 220
  33. def OAI.DFVSGames.Reduction.ActualSource.Source.ofList line 223
  34. theorem OAI.DFVSGames.Reduction.ActualSource.Source.sourceList_ofList line 230
  35. theorem OAI.DFVSGames.Reduction.ActualSource.Source.sourceList_length line 235
  36. theorem OAI.DFVSGames.Reduction.ActualSource.Source.sourceList_nonempty line 238
  37. instance OAI.DFVSGames.Reduction.ActualSource.sourceIndexNonempty line 246
  38. def OAI.DFVSGames.Reduction.ActualSource.Source.satisfied line 249
  39. def OAI.DFVSGames.Reduction.ActualSource.Source.failure line 252
  40. def OAI.DFVSGames.Reduction.ActualSource.Source.DistinctNames line 255
  41. abbrev OAI.DFVSGames.Reduction.ActualSource.Alphabet line 260
  42. abbrev OAI.DFVSGames.Reduction.ActualSource.Ambient line 261
  43. def OAI.DFVSGames.Reduction.ActualSource.alphabetEmbedding line 263
  44. theorem OAI.DFVSGames.Reduction.ActualSource.alphabetEmbedding_apply line 266
  45. structure OAI.DFVSGames.Reduction.ActualSource.SplitGadget line 269
  46. def OAI.DFVSGames.Reduction.ActualSource.SplitGadget.stabilityError line 279
  47. def OAI.DFVSGames.Reduction.ActualSource.SplitGadget.kernelError line 283
  48. theorem OAI.DFVSGames.Reduction.ActualSource.SplitGadget.stabilityError_nonneg line 287
  49. theorem OAI.DFVSGames.Reduction.ActualSource.SplitGadget.stabilityError_le_one line 293
  50. theorem OAI.DFVSGames.Integration.SplitGadget.exists_split_equiv line 307
  51. def OAI.DFVSGames.Integration.SplitGadget.kernelProbability line 326
  52. theorem OAI.DFVSGames.Integration.SplitGadget.kernelProbability_eq_kernelError line 332
  53. def OAI.DFVSGames.Integration.SplitGadget.transport line 340
  54. theorem OAI.DFVSGames.Integration.SplitGadget.transport_stabilityError line 353
  55. theorem OAI.DFVSGames.Integration.SplitGadget.transport_kernelError line 362
  56. theorem OAI.DFVSGames.Integration.SplitGadget.transport_symbol_map line 372
  57. theorem OAI.DFVSGames.Integration.SplitGadget.transport_kernelProbability line 383
  58. theorem OAI.DFVSGames.Integration.SplitGadget.transport_satisfies line 392
  59. theorem OAI.DFVSGames.Integration.SplitGadget.exists_split_gadget line 408
  60. theorem OAI.DFVSGames.Integration.SplitGadget.exists_split_gadget_general line 418
  61. theorem OAI.DFVSGames.Integration.RealBounds.rho_eq_two_div_pow line 441
  62. theorem OAI.DFVSGames.Integration.RealBounds.rho_real_eq_two_div_pow line 448
  63. theorem OAI.DFVSGames.Integration.RealBounds.beta_eq_div line 452
  64. theorem OAI.DFVSGames.Integration.RealBounds.theta_real_product line 458
  65. theorem OAI.DFVSGames.Integration.RealBounds.fourth_root_as_rpow line 464
  66. theorem OAI.DFVSGames.Integration.RealBounds.exists_symbol_dimension_real line 471
  67. theorem OAI.DFVSGames.Integration.RealBounds.kernelProbability_real line 479
  68. theorem OAI.DFVSGames.Integration.RealBounds.kernelProbability_real_le line 493
  69. theorem OAI.DFVSGames.Integration.RealBounds.comparison_square_budget line 503
  70. theorem OAI.DFVSGames.Soundness.ActualMapComparison.actual_partner_expectation_comparison line 517
  71. theorem OAI.DFVSGames.Soundness.ActualMapComparison.actual_partner_expectation_comparison_dimension line 546
  72. theorem OAI.DFVSGames.Soundness.ActualMapComparison.actual_partner_expectation_quarter line 565
  73. def OAI.DFVSGames.Soundness.ActualMapComparison.sourcePrecomposeEquiv line 585
  74. theorem OAI.DFVSGames.Soundness.ActualMapComparison.uniformMean_sourcePrecompose line 602
  75. theorem OAI.DFVSGames.Soundness.ActualMapComparison.actual_partner_expectation_quarter_equiv line 613
  76. theorem OAI.DFVSGames.Soundness.RawTargetLaw.partnerProjection_congr_slots line 649
  77. theorem OAI.DFVSGames.Soundness.RawTargetLaw.rawProjection_congr_slots line 658
  78. theorem OAI.DFVSGames.Soundness.RawTargetLaw.precompose_rawProjection line 666
  79. theorem OAI.DFVSGames.Soundness.RawTargetLaw.partner_row_column_expectation line 676
  80. def OAI.DFVSGames.Soundness.UniformPartition.mean line 715
  81. theorem OAI.DFVSGames.Soundness.UniformPartition.mean_equiv line 718
  82. def OAI.DFVSGames.Soundness.UniformPartition.fiberSum line 723
  83. def OAI.DFVSGames.Soundness.UniformPartition.fiberSize line 727
  84. theorem OAI.DFVSGames.Soundness.UniformPartition.fiberSize_eq_card line 730
  85. theorem OAI.DFVSGames.Soundness.UniformPartition.sum_fiberSum line 738
  86. theorem OAI.DFVSGames.Soundness.UniformPartition.fiberSize_mul line 747
  87. theorem OAI.DFVSGames.Soundness.UniformPartition.fiberSize_pos line 756
  88. theorem OAI.DFVSGames.Soundness.UniformPartition.fiberSize_mul_conditional line 765
  89. theorem OAI.DFVSGames.Soundness.UniformPartition.total_mean line 775
  90. theorem OAI.DFVSGames.Soundness.UniformPartition.mean_mono line 794
  91. theorem OAI.DFVSGames.Soundness.UniformPartition.mean_le_partition_bound line 798
  92. theorem OAI.DFVSGames.Soundness.UniformPartition.fiber_conditional_eq_subtype_mean line 808