OAI/Analysis/BoxTransport/Expressions.lean

GitHub source file

121 declarations, 0 contain sorry, 0 declared as axioms

Smooth expression calculus and effective mixed derivatives.

  1. abbrev OAI.BoxTransport.Routing.Computation.Expr line 16
  2. def OAI.BoxTransport.Routing.Computation.node line 18
  3. def OAI.BoxTransport.Routing.Computation.cst line 20
  4. def OAI.BoxTransport.Routing.Computation.invE line 22
  5. def OAI.BoxTransport.Routing.Computation.flatE line 24
  6. def OAI.BoxTransport.Routing.Computation.varE line 26
  7. def OAI.BoxTransport.Routing.Computation.unaryValue line 30
  8. def OAI.BoxTransport.Routing.Computation.value line 34
  9. def OAI.BoxTransport.Routing.Computation.Valid line 44
  10. theorem OAI.BoxTransport.Routing.Computation.value_node line 51
  11. theorem OAI.BoxTransport.Routing.Computation.value_cst line 53
  12. theorem OAI.BoxTransport.Routing.Computation.value_invE line 56
  13. theorem OAI.BoxTransport.Routing.Computation.value_flatE line 58
  14. theorem OAI.BoxTransport.Routing.Computation.valid_node line 60
  15. theorem OAI.BoxTransport.Routing.Computation.valid_cst line 63
  16. theorem OAI.BoxTransport.Routing.Computation.valid_flatE line 64
  17. theorem OAI.BoxTransport.Routing.Computation.valid_invE line 66
  18. theorem OAI.BoxTransport.Routing.Computation.value_varE line 69
  19. theorem OAI.BoxTransport.Routing.Computation.valid_varE line 74
  20. theorem OAI.BoxTransport.Routing.Computation.nonzero_of_inverse_bound line 79
  21. theorem OAI.BoxTransport.Routing.Computation.smooth_value line 83
  22. def OAI.BoxTransport.Routing.Computation.diffUnary line 100
  23. def OAI.BoxTransport.Routing.Computation.diff line 106
  24. theorem OAI.BoxTransport.Routing.Computation.valid_diff line 116
  25. theorem OAI.BoxTransport.Routing.Computation.value_diff line 130
  26. def OAI.BoxTransport.Routing.Computation.qGuardInv line 215
  27. theorem OAI.BoxTransport.Routing.Computation.qGuardInv_error line 218
  28. def OAI.BoxTransport.Routing.Computation.unaryBound line 265
  29. def OAI.BoxTransport.Routing.Computation.boundE line 269
  30. def OAI.BoxTransport.Routing.Computation.unaryAmp line 276
  31. def OAI.BoxTransport.Routing.Computation.ampE line 281
  32. theorem OAI.BoxTransport.Routing.Computation.coord_le_norm line 288
  33. theorem OAI.BoxTransport.Routing.Computation.value_bound line 295
  34. def OAI.BoxTransport.Routing.Computation.unaryEval line 320
  35. def OAI.BoxTransport.Routing.Computation.evalE line 324
  36. theorem OAI.BoxTransport.Routing.Computation.mul_approx line 334
  37. theorem OAI.BoxTransport.Routing.Computation.evalE_error line 355
  38. theorem OAI.BoxTransport.Routing.Computation.pr_add line 417
  39. theorem OAI.BoxTransport.Routing.Computation.pr_mul line 419
  40. theorem OAI.BoxTransport.Routing.Computation.pr_sub line 421
  41. theorem OAI.BoxTransport.Routing.Computation.pr_div line 423
  42. theorem OAI.BoxTransport.Routing.Computation.pr_mod line 425
  43. theorem OAI.BoxTransport.Routing.Computation.pr_square line 427
  44. theorem OAI.BoxTransport.Routing.Computation.pr_pair line 429
  45. theorem OAI.BoxTransport.Routing.Computation.pr_comp line 431
  46. theorem OAI.BoxTransport.Routing.Computation.pr_prec line 433
  47. theorem OAI.BoxTransport.Routing.Computation.pr_qAdd line 437
  48. theorem OAI.BoxTransport.Routing.Computation.pr_qMul line 439
  49. theorem OAI.BoxTransport.Routing.Computation.primrec_node line 442
  50. theorem OAI.BoxTransport.Routing.Computation.pr_node line 444
  51. theorem OAI.BoxTransport.Routing.Computation.primrec_cst line 446
  52. theorem OAI.BoxTransport.Routing.Computation.pr_invE line 447
  53. theorem OAI.BoxTransport.Routing.Computation.pr_flatE line 449
  54. theorem OAI.BoxTransport.Routing.Computation.primrec_diffUnary line 452
  55. theorem OAI.BoxTransport.Routing.Computation.diff_eq_rec line 459
  56. theorem OAI.BoxTransport.Routing.Computation.primrec_diff line 470
  57. theorem OAI.BoxTransport.Routing.Computation.primrec_unaryBound line 482
  58. theorem OAI.BoxTransport.Routing.Computation.boundE_eq_rec line 488
  59. theorem OAI.BoxTransport.Routing.Computation.primrec_boundE line 493
  60. theorem OAI.BoxTransport.Routing.Computation.primrec_unaryAmp line 497
  61. theorem OAI.BoxTransport.Routing.Computation.ampE_eq_rec line 503
  62. theorem OAI.BoxTransport.Routing.Computation.primrec_ampE line 509
  63. theorem OAI.BoxTransport.Routing.Computation.primrec_qGuardInv line 513
  64. theorem OAI.BoxTransport.Routing.Computation.computable_unaryEval line 519
  65. theorem OAI.BoxTransport.Routing.Computation.evalE_eq_rec line 526
  66. theorem OAI.BoxTransport.Routing.Computation.computable_Expr_recOn line 532
  67. theorem OAI.BoxTransport.Routing.Computation.computable_evalE line 549
  68. def OAI.BoxTransport.Routing.Computation.pointBound line 560
  69. theorem OAI.BoxTransport.Routing.Computation.primrec_pointBound line 563
  70. theorem OAI.BoxTransport.Routing.Computation.norm_code_le line 565
  71. def OAI.BoxTransport.Routing.Computation.evalPrecise line 582
  72. theorem OAI.BoxTransport.Routing.Computation.computable_evalPrecise line 585
  73. theorem OAI.BoxTransport.Routing.Computation.amplification_precision line 590
  74. theorem OAI.BoxTransport.Routing.Computation.evalPrecise_error line 599
  75. def OAI.BoxTransport.Routing.Computation.mixedE line 603
  76. theorem OAI.BoxTransport.Routing.Computation.mixedE_nil line 605
  77. theorem OAI.BoxTransport.Routing.Computation.mixedE_cons line 606
  78. theorem OAI.BoxTransport.Routing.Computation.primrec_mixedE line 609
  79. theorem OAI.BoxTransport.Routing.Computation.valid_mixedE line 613
  80. theorem OAI.BoxTransport.Routing.Computation.smooth_mixedDerivative line 618
  81. theorem OAI.BoxTransport.Routing.Computation.mixedDerivative_component line 624
  82. theorem OAI.BoxTransport.Routing.Computation.tsupport_mixedDerivative_subset line 638
  83. theorem OAI.BoxTransport.Routing.Computation.exists_supportRadius line 644
  84. def OAI.BoxTransport.Routing.Computation.familyBound line 652
  85. theorem OAI.BoxTransport.Routing.Computation.primrec_familyBound line 655
  86. theorem OAI.BoxTransport.Routing.Computation.boundE_le_familyBound line 658
  87. theorem OAI.BoxTransport.Routing.Computation.uniform_mixed_bound line 662
  88. theorem OAI.BoxTransport.Routing.Computation.spacetime_decomposition line 674
  89. theorem OAI.BoxTransport.Routing.Computation.opnorm_from_coordinates line 682
  90. def OAI.BoxTransport.Routing.Computation.gradientBound line 698
  91. theorem OAI.BoxTransport.Routing.Computation.pr_list_cons line 702
  92. theorem OAI.BoxTransport.Routing.Computation.primrec_gradientBound line 705
  93. theorem OAI.BoxTransport.Routing.Computation.familyBound_le_gradientBound line 708
  94. theorem OAI.BoxTransport.Routing.Computation.mixed_component_lipschitz line 714
  95. theorem OAI.BoxTransport.Routing.Computation.effective_of_expressions line 730
  96. def OAI.BoxTransport.Routing.Computation.Representable line 778
  97. theorem OAI.BoxTransport.Routing.Computation.Representable.rational line 784
  98. theorem OAI.BoxTransport.Routing.Computation.Representable.nat line 788
  99. theorem OAI.BoxTransport.Routing.Computation.Representable.ofNat line 791
  100. theorem OAI.BoxTransport.Routing.Computation.Representable.zero line 793
  101. theorem OAI.BoxTransport.Routing.Computation.Representable.one line 794
  102. theorem OAI.BoxTransport.Routing.Computation.Representable.time line 795
  103. theorem OAI.BoxTransport.Routing.Computation.Representable.space line 797
  104. theorem OAI.BoxTransport.Routing.Computation.Representable.add line 800
  105. theorem OAI.BoxTransport.Routing.Computation.Representable.mul line 806
  106. theorem OAI.BoxTransport.Routing.Computation.Representable.neg line 812
  107. theorem OAI.BoxTransport.Routing.Computation.Representable.sub line 817
  108. theorem OAI.BoxTransport.Routing.Computation.Representable.div_rat line 820
  109. theorem OAI.BoxTransport.Routing.Computation.Representable.div_nat line 824
  110. theorem OAI.BoxTransport.Routing.Computation.Representable.div_ofNat line 827
  111. theorem OAI.BoxTransport.Routing.Computation.Representable.flat line 830
  112. theorem OAI.BoxTransport.Routing.Computation.Representable.glue line 835
  113. lemma OAI.BoxTransport.Routing.Computation.Representable.exists_inv_nat_le line 839
  114. theorem OAI.BoxTransport.Routing.Computation.Representable.inv line 846
  115. theorem OAI.BoxTransport.Routing.Computation.Representable.div line 854
  116. theorem OAI.BoxTransport.Routing.Computation.Representable.transition_denom_lower line 858
  117. theorem OAI.BoxTransport.Routing.Computation.Representable.transition line 865
  118. theorem OAI.BoxTransport.Routing.Computation.Representable.directional line 872
  119. theorem OAI.BoxTransport.Routing.Computation.Representable.smooth line 877
  120. theorem OAI.BoxTransport.Routing.Computation.Representable.sum line 881
  121. theorem OAI.BoxTransport.Routing.Computation.Representable.prod line 890