OAI/MathematicalPhysics/Heisenberg/ExchangeOnMesh.lean

GitHub source file

51 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.Heisenberg.Heat.kernel line 13
  2. lemma OAI.Heisenberg.Heat._root_.OAI.Heisenberg.MatrixContraction.DoublySubstochastic.one line 16
  3. lemma OAI.Heisenberg.Heat._root_.OAI.Heisenberg.MatrixContraction.DoublySubstochastic.pow line 22
  4. def OAI.Heisenberg.Heat.entry line 28
  5. lemma OAI.Heisenberg.Heat.entry_apply line 32
  6. lemma OAI.Heisenberg.Heat.exp_scalar line 34
  7. lemma OAI.Heisenberg.Heat.uniformization line 40
  8. lemma OAI.Heisenberg.Heat.exp_series line 47
  9. lemma OAI.Heisenberg.Heat.exp_sub_identity_substochastic line 54
  10. structure OAI.Heisenberg.Heat.SubMarkovGenerator line 96
  11. lemma OAI.Heisenberg.Heat.uniformized_substochastic line 101
  12. theorem OAI.Heisenberg.Heat.kernel_substochastic line 129
  13. def OAI.Heisenberg.Heat.generator line 146
  14. lemma OAI.Heisenberg.Heat.generator_subMarkov line 149
  15. lemma OAI.Heisenberg.Heat.generator_action line 169
  16. def OAI.Heisenberg.Heat.energy line 177
  17. lemma OAI.Heisenberg.Heat.energy_nonneg line 181
  18. lemma OAI.Heisenberg.Heat.dirichlet_identity line 189
  19. lemma OAI.Heisenberg.Heat.kernel_derivative line 231
  20. theorem OAI.Heisenberg.Heat.dissipation line 243
  21. lemma OAI.ExchangeLimit.contraction_power_difference line 266
  22. theorem OAI.ExchangeLimit.contraction_product_limit line 286
  23. lemma OAI.Heisenberg.ExchangeMatrix.substochastic_norm_le line 342
  24. def OAI.Heisenberg.ExchangeMatrix.permutationMatrix line 352
  25. lemma OAI.Heisenberg.ExchangeMatrix.permutationMatrix_substochastic line 354
  26. lemma OAI.Heisenberg.ExchangeMatrix.permutationMatrix_col line 360
  27. lemma OAI.Heisenberg.ExchangeMatrix.permutationMatrix_row line 363
  28. lemma OAI.Heisenberg.ExchangeMatrix.permutationMatrix_mulVec line 368
  29. def OAI.Heisenberg.ExchangeMatrix.bernoulliStep line 372
  30. lemma OAI.Heisenberg.ExchangeMatrix.bernoulliStep_zero line 376
  31. lemma OAI.Heisenberg.ExchangeMatrix.bernoulliStep_substochastic line 379
  32. lemma OAI.Heisenberg.ExchangeMatrix.bernoulliStep_col line 394
  33. lemma OAI.Heisenberg.ExchangeMatrix.bernoulliStep_derivative line 400
  34. abbrev OAI.Heisenberg.ExchangeMatrix.Clock line 410
  35. def OAI.Heisenberg.ExchangeMatrix.meshStep line 412
  36. def OAI.Heisenberg.ExchangeMatrix.clockGenerator line 416
  37. lemma OAI.Heisenberg.ExchangeMatrix.meshStep_zero line 420
  38. lemma OAI.Heisenberg.ExchangeMatrix.meshStep_substochastic line 425
  39. lemma OAI.Heisenberg.ExchangeMatrix.meshStep_derivative line 431
  40. lemma OAI.Heisenberg.ExchangeMatrix.clockGenerator_subMarkov line 440
  41. theorem OAI.Heisenberg.ExchangeMatrix.mesh_converges line 459
  42. theorem OAI.ExchangeLimit.local_contraction_product_limit line 473
  43. def OAI.Heisenberg.ExchangeMatrix.linearStep line 529
  44. lemma OAI.Heisenberg.ExchangeMatrix.linearStep_zero line 533
  45. lemma OAI.Heisenberg.ExchangeMatrix.linearStep_substochastic line 536
  46. lemma OAI.Heisenberg.ExchangeMatrix.linearStep_derivative line 546
  47. def OAI.Heisenberg.ExchangeMatrix.linearMesh line 555
  48. lemma OAI.Heisenberg.ExchangeMatrix.linearMesh_zero line 559
  49. lemma OAI.Heisenberg.ExchangeMatrix.linearMesh_derivative line 564
  50. lemma OAI.Heisenberg.ExchangeMatrix.linearMesh_locally_substochastic line 572
  51. theorem OAI.Heisenberg.ExchangeMatrix.linear_mesh_converges line 584