OAI/MathematicalPhysics/AlternatingFlow/DerivativeBounds.lean

GitHub source file

95 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.AlternatingNS.Bounds.BoundedJets line 14
  2. def OAI.AlternatingNS.Bounds.ScaledJets line 17
  3. lemma OAI.AlternatingNS.Bounds.compact_bounded line 21
  4. lemma OAI.AlternatingNS.Bounds.ScaledJets.congr line 29
  5. lemma OAI.AlternatingNS.Bounds.ScaledJets.const line 34
  6. lemma OAI.AlternatingNS.Bounds.ScaledJets.fixed line 43
  7. lemma OAI.AlternatingNS.Bounds.ScaledJets.add line 49
  8. lemma OAI.AlternatingNS.Bounds.ScaledJets.sub line 60
  9. lemma OAI.AlternatingNS.Bounds.ScaledJets.smul line 71
  10. lemma OAI.AlternatingNS.Bounds.ScaledJets.mul line 86
  11. lemma OAI.AlternatingNS.Bounds.ScaledJets.sum line 114
  12. lemma OAI.AlternatingNS.Bounds.ScaledJets.ite line 124
  13. lemma OAI.AlternatingNS.Bounds.ScaledJets.comp line 136
  14. lemma OAI.AlternatingNS.Bounds.norm_comp_linear line 165
  15. lemma OAI.AlternatingNS.Bounds.ScaledJets.comp_linear line 171
  16. lemma OAI.AlternatingNS.Bounds.BoundedJets.comp_scaled_linear line 186
  17. lemma OAI.AlternatingNS.Bounds.ScaledJets.constant line 197
  18. lemma OAI.AlternatingNS.Bounds.ScaledJets.cmul line 201
  19. lemma OAI.AlternatingNS.Bounds.ScaledJets.const_mul line 205
  20. lemma OAI.AlternatingNS.Bounds.ScaledJets.div_const line 209
  21. lemma OAI.AlternatingNS.Bounds.decoder_bounded line 213
  22. lemma OAI.AlternatingNS.Bounds.selector_bounded line 219
  23. def OAI.AlternatingNS.Bounds.readScale line 230
  24. lemma OAI.AlternatingNS.Bounds.readScale_ge_one line 233
  25. lemma OAI.AlternatingNS.Bounds.readScale_nonneg line 236
  26. lemma OAI.AlternatingNS.Bounds.inverse_power_bound line 239
  27. lemma OAI.AlternatingNS.Bounds.scaled_decoder line 244
  28. lemma OAI.AlternatingNS.Bounds.readC_scaled line 255
  29. lemma OAI.AlternatingNS.Bounds.readB_scaled line 259
  30. lemma OAI.AlternatingNS.Bounds.readA_scaled line 263
  31. lemma OAI.AlternatingNS.Bounds.updateLeft_scaled line 269
  32. lemma OAI.AlternatingNS.Bounds.updateRight_scaled line 280
  33. lemma OAI.AlternatingNS.Bounds.branchNumerator_scaled line 295
  34. lemma OAI.AlternatingNS.Bounds.branch_scaled line 302
  35. def OAI.AlternatingNS.Bounds.writeCore line 315
  36. lemma OAI.AlternatingNS.Bounds.writeCore_scaled line 322
  37. lemma OAI.AlternatingNS.Bounds.write_factor line 336
  38. lemma OAI.AlternatingNS.Bounds.haltWeight_scaled line 341
  39. lemma OAI.AlternatingNS.Bounds.ScaledJets.finite_family line 351
  40. lemma OAI.AlternatingNS.Bounds.norm_postcomp_linear line 361
  41. lemma OAI.AlternatingNS.Bounds.norm_directional_iterated line 367
  42. lemma OAI.AlternatingNS.Bounds.norm_e line 378
  43. lemma OAI.AlternatingNS.Bounds.norm_iterated_curl line 380
  44. lemma OAI.AlternatingNS.Bounds.cutoff_coordinate_bounded line 404
  45. lemma OAI.AlternatingNS.Bounds.scaled_coord_comp line 410
  46. def OAI.AlternatingNS.Bounds.fixedPotential line 420
  47. def OAI.AlternatingNS.Bounds.corePotential line 423
  48. lemma OAI.AlternatingNS.Bounds.fixedPotential_scaled line 428
  49. lemma OAI.AlternatingNS.Bounds.corePotential_scaled line 434
  50. lemma OAI.AlternatingNS.Bounds.potential_decomposition line 444
  51. lemma OAI.AlternatingNS.Bounds.potential_bound line 453
  52. theorem OAI.AlternatingNS.Bounds.slot_estimate line 494
  53. lemma OAI.AlternatingNS.Bounds.uniform_read_cost line 505
  54. theorem OAI.AlternatingNS.Bounds.slot_decay line 528
  55. def OAI.AlternatingNS.Bounds.amplitude line 536
  56. lemma OAI.AlternatingNS.Bounds.amplitude_nonneg line 540
  57. lemma OAI.AlternatingNS.Bounds.weighted_amplitude_summable line 545
  58. lemma OAI.AlternatingNS.Bounds.piece_decay line 559
  59. lemma OAI.AlternatingNS.Bounds.pulse_bounded line 573
  60. def OAI.AlternatingNS.Bounds.pulsePiece line 581
  61. lemma OAI.AlternatingNS.Bounds.pulsePiece_smooth line 584
  62. lemma OAI.AlternatingNS.Bounds.pulsePiece_decay line 589
  63. def OAI.AlternatingNS.Bounds.RapidJets line 626
  64. lemma OAI.AlternatingNS.Bounds.box_norm line 630
  65. lemma OAI.AlternatingNS.Bounds.pulsePiece_support line 640
  66. lemma OAI.AlternatingNS.Bounds.pulsePiece_weighted line 650
  67. theorem OAI.AlternatingNS.Bounds.velocity_rapidJets line 669
  68. lemma OAI.AlternatingNS.Bounds.RapidJets.congr line 697
  69. lemma OAI.AlternatingNS.Bounds.RapidJets.add line 700
  70. lemma OAI.AlternatingNS.Bounds.RapidJets.linear line 714
  71. lemma OAI.AlternatingNS.Bounds.RapidJets.const_smul line 725
  72. lemma OAI.AlternatingNS.Bounds.RapidJets.sub line 728
  73. lemma OAI.AlternatingNS.Bounds.RapidJets.zero line 732
  74. lemma OAI.AlternatingNS.Bounds.RapidJets.sum line 736
  75. lemma OAI.AlternatingNS.Bounds.RapidJets.directional line 745
  76. lemma OAI.AlternatingNS.Bounds.dx_eq_full_directional line 756
  77. lemma OAI.AlternatingNS.Bounds.fullDt_eq_full_directional line 768
  78. lemma OAI.AlternatingNS.Bounds.RapidJets.dx line 780
  79. lemma OAI.AlternatingNS.Bounds.RapidJets.fullDt line 784
  80. lemma OAI.AlternatingNS.Bounds.RapidJets.smul line 788
  81. lemma OAI.AlternatingNS.Bounds.advection_eq_sum line 809
  82. lemma OAI.AlternatingNS.Bounds.RapidJets.advection line 817
  83. lemma OAI.AlternatingNS.Bounds.RapidJets.laplacian line 824
  84. lemma OAI.AlternatingNS.Bounds.RapidJets.fullResidual line 828
  85. def OAI.AlternatingNS.Bounds.HalfEq line 833
  86. lemma OAI.AlternatingNS.Bounds.HalfEq.dx line 835
  87. lemma OAI.AlternatingNS.Bounds.HalfEq.dt line 840
  88. lemma OAI.AlternatingNS.Bounds.HalfEq.spatial line 845
  89. lemma OAI.AlternatingNS.Bounds.HalfEq.mixed line 855
  90. lemma OAI.AlternatingNS.Bounds.RapidJets.spatial line 861
  91. lemma OAI.AlternatingNS.Bounds.fullDt_iterate line 870
  92. lemma OAI.AlternatingNS.Bounds.RapidJets.rapid line 880
  93. lemma OAI.AlternatingNS.Bounds.Rapid.congr_half line 888
  94. theorem OAI.AlternatingNS.Bounds.velocity_rapid line 895
  95. theorem OAI.AlternatingNS.Bounds.force_rapid line 898