OAI/Computability/DirectedFeedback/Games/NonlinearRecurrence.lean

GitHub source file

75 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.DFVSGames.Gadget.EmbeddedConditional.expect_uniform_output_embedded line 16
  2. theorem OAI.DFVSGames.Gadget.EmbeddedConditional.expect_equivariant_output line 40
  3. theorem OAI.DFVSGames.Gadget.EmbeddedConditional.expect_linear_surjective line 48
  4. theorem OAI.DFVSGames.Gadget.EmbeddedConditional.expect_uniform_difference_embedded line 54
  5. def OAI.DFVSGames.Gadget.NonlinearRecurrence.change line 78
  6. theorem OAI.DFVSGames.Gadget.NonlinearRecurrence.change_zero line 82
  7. theorem OAI.DFVSGames.Gadget.NonlinearRecurrence.compLeft_surjective line 86
  8. theorem OAI.DFVSGames.Gadget.NonlinearRecurrence.aggregate_single line 93
  9. theorem OAI.DFVSGames.Gadget.NonlinearRecurrence.child_outputs_perturb line 101
  10. theorem OAI.DFVSGames.Gadget.NonlinearRecurrence.parent_output_perturb line 113
  11. theorem OAI.DFVSGames.Gadget.NonlinearRecurrence.expect_change_at_index line 119
  12. theorem OAI.DFVSGames.Gadget.NonlinearRecurrence.kernel_all line 162
  13. theorem OAI.DFVSGames.Gadget.NonlinearRecurrence.parent_change_recurrence line 172
  14. def OAI.DFVSGames.Gadget.StageNoiseRecurrence.average line 213
  15. theorem OAI.DFVSGames.Gadget.StageNoiseRecurrence.average_eq_expect line 217
  16. def OAI.DFVSGames.Gadget.StageNoiseRecurrence.error line 227
  17. theorem OAI.DFVSGames.Gadget.StageNoiseRecurrence.error_eq_expect line 232
  18. theorem OAI.DFVSGames.Gadget.StageNoiseRecurrence.base_error line 245
  19. theorem OAI.DFVSGames.Gadget.StageNoiseRecurrence.next_error line 273
  20. theorem OAI.DFVSGames.Gadget.StageNoiseRecurrence.iterate_error line 294
  21. theorem OAI.DFVSGames.Gadget.StageNoiseRecurrence.quotient_error line 307
  22. def OAI.DFVSGames.Quadratic.basisCoord line 339
  23. theorem OAI.DFVSGames.Quadratic.basisCoord_ne_zero line 341
  24. theorem OAI.DFVSGames.Quadratic.Q_smul_basisCoord line 346
  25. theorem OAI.DFVSGames.Quadratic.dot_smul_basisCoord_of_ne line 351
  26. theorem OAI.DFVSGames.Quadratic.basisCoord_decomposition line 355
  27. theorem OAI.DFVSGames.Quadratic.horizontal_mem_U_basisCoord line 362
  28. theorem OAI.DFVSGames.Quadratic.vertical_mem_U_basisCoord_of_ne line 368
  29. def OAI.DFVSGames.Quadratic.coordinateBlockSpan line 374
  30. theorem OAI.DFVSGames.Quadratic.U_basisCoord_le_coordinateBlockSpan line 377
  31. theorem OAI.DFVSGames.Quadratic.horizontal_mem_coordinateBlockSpan line 384
  32. theorem OAI.DFVSGames.Quadratic.vertical_mem_coordinateBlockSpan line 389
  33. theorem OAI.DFVSGames.Quadratic.mem_coordinateBlockSpan line 401
  34. theorem OAI.DFVSGames.Quadratic.coordinateBlockSpan_eq_top line 419
  35. theorem OAI.DFVSGames.Quadratic.iSup_U_nonzero_eq_top line 425
  36. def OAI.DFVSGames.Quadratic.blockEmbedding line 449
  37. def OAI.DFVSGames.Quadratic.blockAggregate line 453
  38. theorem OAI.DFVSGames.Quadratic.blockAggregate_single line 456
  39. theorem OAI.DFVSGames.Quadratic.fieldLine_block_le_range_aggregate line 469
  40. theorem OAI.DFVSGames.Quadratic.blockAggregate_surjective line 481
  41. theorem OAI.DFVSGames.Quadratic.aggregate_blockEmbedding_surjective line 497
  42. def OAI.DFVSGames.Gadget.QuadraticStageNoise.rate line 525
  43. theorem OAI.DFVSGames.Gadget.QuadraticStageNoise.actual_kernel line 528
  44. def OAI.DFVSGames.Gadget.QuadraticStageNoise.stage line 535
  45. theorem OAI.DFVSGames.Gadget.QuadraticStageNoise.stage_error line 538
  46. def OAI.DFVSGames.Gadget.QuadraticStageNoise.quotientStage line 546
  47. theorem OAI.DFVSGames.Gadget.QuadraticStageNoise.quotientStage_error line 549
  48. theorem OAI.DFVSGames.Gadget.Parameters.harmonic_double line 562
  49. theorem OAI.DFVSGames.Gadget.Parameters.harmonic_pow_two line 583
  50. def OAI.DFVSGames.Gadget.Parameters.rankFor line 592
  51. theorem OAI.DFVSGames.Gadget.Parameters.rankFor_pos line 594
  52. theorem OAI.DFVSGames.Gadget.Parameters.le_harmonic_rankFor line 598
  53. theorem OAI.DFVSGames.Gadget.Parameters.harmonic_unbounded line 604
  54. def OAI.DFVSGames.Gadget.Parameters.genericityError line 608
  55. theorem OAI.DFVSGames.Gadget.Parameters.genericityError_pos line 610
  56. theorem OAI.DFVSGames.Gadget.Parameters.genericityError_lt_one line 615
  57. theorem OAI.DFVSGames.Gadget.Parameters.genericityError_budget line 621
  58. theorem OAI.DFVSGames.Gadget.Parameters.geometric_reciprocal_bound line 629
  59. theorem OAI.DFVSGames.Gadget.Parameters.geometric_at_depth_le line 649
  60. def OAI.DFVSGames.Gadget.Parameters.initialRank line 666
  61. theorem OAI.DFVSGames.Gadget.Parameters.initialRank_pos line 668
  62. theorem OAI.DFVSGames.Gadget.Parameters.initialRank_large line 670
  63. theorem OAI.DFVSGames.Gadget.Parameters.effective_parameters line 673
  64. def OAI.DFVSGames.Quadratic.SquarefreeExponent line 691
  65. theorem OAI.DFVSGames.Quadratic.coeff_expand_mul_monomial_of_ne line 693
  66. theorem OAI.DFVSGames.Quadratic.coeff_expand_mul_monomial_self line 717
  67. theorem OAI.DFVSGames.Quadratic.coeff_sum_expand_mul_monomial line 722
  68. theorem OAI.DFVSGames.Quadratic.sum_expand_mul_monomial_eq_zero_iff line 737
  69. def OAI.DFVSGames.Quadratic.blockExponent line 750
  70. theorem OAI.DFVSGames.Quadratic.blockExponent_apply line 755
  71. theorem OAI.DFVSGames.Quadratic.blockExponent_squarefree line 761
  72. theorem OAI.DFVSGames.Quadratic.blockExponent_injective line 768
  73. theorem OAI.DFVSGames.Quadratic.blockExponent_eq_sum line 777
  74. theorem OAI.DFVSGames.Quadratic.monomial_blockExponent line 791
  75. theorem OAI.DFVSGames.Quadratic.sum_expand_mul_blockMonomial_eq_zero_iff line 798