OAI/Probability/SKGap/Localization/FockSeries.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.SKGap.Noncrossing.Primary.Tensor.Series.Seq line 14
  2. def OAI.SKGap.Noncrossing.Primary.Tensor.Series.ofVector line 16
  3. def OAI.SKGap.Noncrossing.Primary.Tensor.Series.shift line 18
  4. def OAI.SKGap.Noncrossing.Primary.Tensor.Series.act line 23
  5. lemma OAI.SKGap.Noncrossing.Primary.Tensor.Series.shift_zero line 28
  6. lemma OAI.SKGap.Noncrossing.Primary.Tensor.Series.shift_succ line 29
  7. lemma OAI.SKGap.Noncrossing.Primary.Tensor.Series.act_apply line 30
  8. lemma OAI.SKGap.Noncrossing.Primary.Tensor.Series.act_shift line 32
  9. def OAI.SKGap.Noncrossing.Primary.Tensor.Series.inverseSeq line 37
  10. lemma OAI.SKGap.Noncrossing.Primary.Tensor.Series.inverseSeq_add line 43
  11. lemma OAI.SKGap.Noncrossing.Primary.Tensor.Series.inverseSeq_smul line 54
  12. def OAI.SKGap.Noncrossing.Primary.Tensor.Series.inverse line 66
  13. lemma OAI.SKGap.Noncrossing.Primary.Tensor.Series.inverse_equation line 71
  14. lemma OAI.SKGap.Noncrossing.Primary.Tensor.Series.inverse_unique line 81
  15. lemma OAI.SKGap.Noncrossing.Primary.Tensor.Series.inverse_shift line 99
  16. lemma OAI.SKGap.Noncrossing.Primary.Tensor.Series.kernel_add_two_left line 106
  17. lemma OAI.SKGap.Noncrossing.Primary.Tensor.Series.inverse_ofVector line 122
  18. def OAI.SKGap.Noncrossing.Primary.Tensor.Series.branchSource line 148
  19. def OAI.SKGap.Noncrossing.Primary.Tensor.Series.branchField line 150
  20. def OAI.SKGap.Noncrossing.Primary.Tensor.Series.ordinary line 154
  21. lemma OAI.SKGap.Noncrossing.Primary.Tensor.Series.noise_vacuum line 159
  22. lemma OAI.SKGap.Noncrossing.Primary.Tensor.Series.branch_field_creation line 165
  23. lemma OAI.SKGap.Noncrossing.Primary.Tensor.Series.ordinary_field_creation line 180
  24. def OAI.SKGap.Noncrossing.Primary.Tensor.Series.loopSource line 192
  25. def OAI.SKGap.Noncrossing.Primary.Tensor.Series.loopField line 195
  26. lemma OAI.SKGap.Noncrossing.Primary.Tensor.Series.loop_source_equation line 200
  27. lemma OAI.SKGap.Noncrossing.Primary.Tensor.Series.loop_source_zero line 222
  28. theorem OAI.SKGap.Noncrossing.Primary.Tensor.Series.loop_field_creation line 227
  29. inductive OAI.SKGap.Noncrossing.Primary.Tensor.Series.ClosedTree line 247
  30. def OAI.SKGap.Noncrossing.Primary.Tensor.Series.ClosedTree.series line 252
  31. def OAI.SKGap.Noncrossing.Primary.Tensor.Series.ClosedTree.leafMass line 258
  32. theorem OAI.SKGap.Noncrossing.Primary.Tensor.Series.ClosedTree.field_creation line 263
  33. theorem OAI.SKGap.Noncrossing.Primary.Tensor.Series.ClosedTree.project_field line 270
  34. theorem OAI.SKGap.Noncrossing.Primary.Tensor.Series.ClosedTree.project_source line 277