OAI/Probability/ClassicalON/FiniteVolume.lean

GitHub source file

161 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ClassicalON.spin_norm line 13
  2. instance OAI.ClassicalON.sphereProbability_isProbability line 16
  3. instance OAI.ClassicalON.referenceLaw_isProbability line 25
  4. theorem OAI.ClassicalON.continuous_interaction line 30
  5. theorem OAI.ClassicalON.continuous_spinDot line 35
  6. theorem OAI.ClassicalON.integrable_weight line 39
  7. theorem OAI.ClassicalON.partition_pos line 44
  8. theorem OAI.ClassicalON.integrable_twoPoint line 55
  9. theorem OAI.ClassicalON.correlation_self line 62
  10. theorem OAI.ClassicalON.hasDerivAt_integral_compact line 71
  11. def OAI.ClassicalON.spinRotation line 95
  12. theorem OAI.ClassicalON.spinRotation_val line 103
  13. theorem OAI.ClassicalON.spinRotation_preserves_surface line 107
  14. theorem OAI.ClassicalON.spinRotation_preserves_probability line 137
  15. def OAI.ClassicalON.siteReference line 142
  16. instance OAI.ClassicalON.siteReference_isProbability line 147
  17. structure OAI.ClassicalON.SpinSystem line 151
  18. abbrev OAI.ClassicalON.SpinOperator line 157
  19. instance OAI.ClassicalON.spinOperator_completeSpace line 160
  20. instance OAI.ClassicalON.spinOperator_ratNormedAlgebra line 163
  21. def OAI.ClassicalON.rotationExp line 166
  22. theorem OAI.ClassicalON.rotationExp_apply line 171
  23. theorem OAI.ClassicalON.rotationExp_symm_apply line 175
  24. def OAI.ClassicalON.SpinSystem.reference line 184
  25. instance OAI.ClassicalON.SpinSystem.reference_isProbability line 187
  26. def OAI.ClassicalON.SpinSystem.energy line 192
  27. def OAI.ClassicalON.SpinSystem.Z line 195
  28. theorem OAI.ClassicalON.SpinSystem.continuous_energy line 199
  29. theorem OAI.ClassicalON.SpinSystem.integrable_weight line 204
  30. theorem OAI.ClassicalON.SpinSystem.Z_pos line 209
  31. def OAI.ClassicalON.SpinSystem.rotateConfiguration line 220
  32. def OAI.ClassicalON.SpinSystem.rotatePins line 225
  33. def OAI.ClassicalON.SpinSystem.gauge line 230
  34. theorem OAI.ClassicalON.SpinSystem.rotateConfiguration_preserves_reference line 237
  35. theorem OAI.ClassicalON.SpinSystem.energy_gauge line 251
  36. theorem OAI.ClassicalON.SpinSystem.Z_gauge line 265
  37. theorem OAI.ClassicalON.SpinSystem.rotatePins_eq_self line 276
  38. theorem OAI.ClassicalON.SpinSystem.Z_gauge_of_fixes_pins line 288
  39. def OAI.ClassicalON.SpinSystem.W line 295
  40. theorem OAI.ClassicalON.SpinSystem.W_zero line 298
  41. def OAI.ClassicalON.SpinSystem.gaugeProduct line 302
  42. theorem OAI.ClassicalON.SpinSystem.noncommuting_gauge line 307
  43. def OAI.ClassicalON.SpinSystem.twistEnergy line 331
  44. theorem OAI.ClassicalON.SpinSystem.continuous_twistEnergy line 336
  45. theorem OAI.ClassicalON.SpinSystem.hasDerivAt_twistEnergy line 342
  46. def OAI.ClassicalON.SpinSystem.firstWeight line 357
  47. def OAI.ClassicalON.SpinSystem.secondWeight line 361
  48. theorem OAI.ClassicalON.SpinSystem.continuous_firstWeight line 367
  49. theorem OAI.ClassicalON.SpinSystem.continuous_secondWeight line 372
  50. theorem OAI.ClassicalON.SpinSystem.hasDerivAt_weight line 378
  51. theorem OAI.ClassicalON.SpinSystem.hasDerivAt_firstWeight line 384
  52. theorem OAI.ClassicalON.SpinSystem.hasDerivAt_twistZ line 390
  53. theorem OAI.ClassicalON.SpinSystem.hasDerivAt_firstVariation line 400
  54. def OAI.ClassicalON.SpinSystem.thirdWeight line 408
  55. def OAI.ClassicalON.SpinSystem.fourthWeight line 414
  56. theorem OAI.ClassicalON.SpinSystem.continuous_thirdWeight line 423
  57. theorem OAI.ClassicalON.SpinSystem.continuous_fourthWeight line 431
  58. theorem OAI.ClassicalON.SpinSystem.hasDerivAt_secondWeight line 442
  59. theorem OAI.ClassicalON.SpinSystem.hasDerivAt_thirdWeight line 451
  60. theorem OAI.ClassicalON.SpinSystem.hasDerivAt_secondVariation line 461
  61. theorem OAI.ClassicalON.SpinSystem.hasDerivAt_thirdVariation line 469
  62. theorem OAI.ClassicalON.SpinSystem.exp_smul_add line 479
  63. theorem OAI.ClassicalON.SpinSystem.W_add_gradient line 488
  64. theorem OAI.ClassicalON.SpinSystem.W_gradient line 521
  65. def OAI.ClassicalON.SpinSystem.average line 529
  66. theorem OAI.ClassicalON.SpinSystem.integrable_average_integrand line 532
  67. theorem OAI.ClassicalON.SpinSystem.average_const line 538
  68. theorem OAI.ClassicalON.SpinSystem.average_add line 545
  69. theorem OAI.ClassicalON.SpinSystem.average_mono line 553
  70. theorem OAI.ClassicalON.SpinSystem.average_nonneg line 561
  71. def OAI.ClassicalON.SpinSystem.axisGradient line 567
  72. theorem OAI.ClassicalON.SpinSystem.Z_gradient_line line 570
  73. theorem OAI.ClassicalON.SpinSystem.second_gradient_identity line 586
  74. theorem OAI.ClassicalON.SpinSystem.abs_energy_le line 617
  75. theorem OAI.ClassicalON.SpinSystem.abs_axis_secondEnergy_le line 634
  76. theorem OAI.ClassicalON.SpinSystem.gradient_current_bound line 653
  77. def OAI.ClassicalON.fourthBell line 680
  78. theorem OAI.ClassicalON.iteratedDeriv_four_integral_exp line 684
  79. def OAI.ClassicalON.expPower line 729
  80. theorem OAI.ClassicalON.hasDerivAt_expPower line 732
  81. theorem OAI.ClassicalON.continuous_expPower line 737
  82. def OAI.ClassicalON.tripleJet line 742
  83. theorem OAI.ClassicalON.continuous_tripleJet line 747
  84. theorem OAI.ClassicalON.hasDerivAt_tripleJet line 753
  85. theorem OAI.ClassicalON.expPower_zero line 762
  86. theorem OAI.ClassicalON.gaugeJets_zero_one line 766
  87. theorem OAI.ClassicalON.gaugeJet_two line 771
  88. def OAI.ClassicalON.SpinSystem.gaugeEnergy line 782
  89. theorem OAI.ClassicalON.SpinSystem.continuous_gaugeEnergy line 788
  90. theorem OAI.ClassicalON.SpinSystem.hasDerivAt_gaugeEnergy line 799
  91. theorem OAI.ClassicalON.SpinSystem.energy_zero line 811
  92. theorem OAI.ClassicalON.SpinSystem.gaugeEnergy_at_zero line 815
  93. theorem OAI.ClassicalON.SpinSystem.fourth_noncommuting_identity line 826
  94. def OAI.ClassicalON.matrixOperator line 872
  95. theorem OAI.ClassicalON.matrixOperator_apply line 875
  96. def OAI.ClassicalON.axisMatrixA line 881
  97. def OAI.ClassicalON.axisMatrixB line 882
  98. def OAI.ClassicalON.axisMatrixC line 883
  99. def OAI.ClassicalON.axisA line 884
  100. def OAI.ClassicalON.axisB line 885
  101. def OAI.ClassicalON.axisC line 886
  102. theorem OAI.ClassicalON.axisA_apply line 888
  103. theorem OAI.ClassicalON.matrixOperator_star line 895
  104. theorem OAI.ClassicalON.axisA_skew line 906
  105. theorem OAI.ClassicalON.axisA_norm_le line 912
  106. theorem OAI.ClassicalON.axisB_skew line 922
  107. theorem OAI.ClassicalON.axisC_skew line 928
  108. theorem OAI.ClassicalON.axisB_apply line 934
  109. theorem OAI.ClassicalON.axisC_apply line 941
  110. theorem OAI.ClassicalON.axisB_norm_le line 948
  111. theorem OAI.ClassicalON.axisC_norm_le line 958
  112. def OAI.ClassicalON.tripleMoment line 968
  113. theorem OAI.ClassicalON.tripleMoment_four line 973
  114. def OAI.ClassicalON.plane line 981
  115. def OAI.ClassicalON.third line 982
  116. lemma OAI.ClassicalON.plane_sub line 984
  117. lemma OAI.ClassicalON.plane_neg line 987
  118. def OAI.ClassicalON.moment4Plane line 991
  119. lemma OAI.ClassicalON.moment4_plane_even_00 line 994
  120. lemma OAI.ClassicalON.moment4_plane_even_01 line 1002
  121. lemma OAI.ClassicalON.moment4_plane_even_02 line 1010
  122. lemma OAI.ClassicalON.moment4_plane_even_10 line 1017
  123. lemma OAI.ClassicalON.moment4_plane_even_11 line 1025
  124. lemma OAI.ClassicalON.moment4_plane_even_12 line 1033
  125. lemma OAI.ClassicalON.moment4_plane_even_20 line 1040
  126. lemma OAI.ClassicalON.moment4_plane_even_21 line 1047
  127. lemma OAI.ClassicalON.moment4_plane_even_22 line 1054
  128. lemma OAI.ClassicalON.moment4_plane_even line 1062
  129. theorem OAI.ClassicalON.tripleJet_at_zero line 1068
  130. theorem OAI.ClassicalON.map_tripleMoment line 1076
  131. def OAI.ClassicalON.planeOperator line 1084
  132. theorem OAI.ClassicalON.planeOperator_eq line 1086
  133. theorem OAI.ClassicalON.plane_commutator line 1092
  134. theorem OAI.ClassicalON.planeOperator_commutator line 1097
  135. theorem OAI.ClassicalON.gaugeJet_plane_four_even line 1104
  136. def OAI.ClassicalON.mixedMatrixAB line 1122
  137. def OAI.ClassicalON.mixedMatrixAAB line 1123
  138. def OAI.ClassicalON.mixedMatrixABB line 1124
  139. def OAI.ClassicalON.mixedMatrixAABB line 1125
  140. theorem OAI.ClassicalON.plane_matrix_square line 1127
  141. theorem OAI.ClassicalON.plane_matrix_cube line 1132
  142. theorem OAI.ClassicalON.plane_matrix_four_even line 1137
  143. theorem OAI.ClassicalON.mixedMatrixAB_sym line 1143
  144. def OAI.ClassicalON.mixedAB line 1147
  145. def OAI.ClassicalON.mixedAAB line 1148
  146. def OAI.ClassicalON.mixedABB line 1149
  147. def OAI.ClassicalON.mixedAABB line 1150
  148. theorem OAI.ClassicalON.planeOperator_square line 1152
  149. theorem OAI.ClassicalON.planeOperator_cube line 1157
  150. theorem OAI.ClassicalON.planeOperator_four_even line 1163
  151. theorem OAI.ClassicalON.SpinSystem.energy_add line 1173
  152. theorem OAI.ClassicalON.SpinSystem.energy_smul line 1178
  153. theorem OAI.ClassicalON.SpinSystem.energy_neg line 1187
  154. theorem OAI.ClassicalON.SpinSystem.average_mul_const line 1191
  155. def OAI.ClassicalON.SpinSystem.fourthPolynomial line 1195
  156. def OAI.ClassicalON.SpinSystem.fourthResponse line 1198
  157. theorem OAI.ClassicalON.SpinSystem.fourthResponse_integral line 1201
  158. theorem OAI.ClassicalON.SpinSystem.fourthResponse_gauge line 1213
  159. def OAI.ClassicalON.SpinSystem.crossForm line 1227
  160. def OAI.ClassicalON.SpinSystem.planarGradient line 1231
  161. def OAI.ClassicalON.SpinSystem.secondAxisResponse line 1235