OAI/Analysis/FreeEntropy/ActualTuple.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.FiniteEntropySeparation.FreeTensor.semicircularB_selfAdjoint line 13
  2. theorem OAI.FiniteEntropySeparation.FreeTensor.semicircularN_selfAdjoint line 15
  3. theorem OAI.FiniteEntropySeparation.FreeTensor.backgroundAlgebra_le line 18
  4. theorem OAI.FiniteEntropySeparation.FreeTensor.semicircularB_mem_background line 26
  5. theorem OAI.FiniteEntropySeparation.FreeTensor.semicircularN_mem_background line 29
  6. theorem OAI.FiniteEntropySeparation.FreeTensor.heatTuple_selfAdjoint line 33
  7. theorem OAI.FiniteEntropySeparation.FreeTensor.heatTuple_mem_background line 41
  8. abbrev OAI.FiniteEntropySeparation.Model.H line 52
  9. abbrev OAI.FiniteEntropySeparation.Model.M line 53
  10. abbrev OAI.FiniteEntropySeparation.Model.τ line 54
  11. def OAI.FiniteEntropySeparation.Model.C line 55
  12. def OAI.FiniteEntropySeparation.Model.initialIndex line 57
  13. def OAI.FiniteEntropySeparation.Model.auxiliaryIndex line 58
  14. def OAI.FiniteEntropySeparation.Model.initialNoise line 59
  15. def OAI.FiniteEntropySeparation.Model.auxiliaryNoise line 60
  16. def OAI.FiniteEntropySeparation.Model.oldNoise line 61
  17. def OAI.FiniteEntropySeparation.Model.X line 62
  18. theorem OAI.FiniteEntropySeparation.Model.initialIndex_injective line 65
  19. theorem OAI.FiniteEntropySeparation.Model.auxiliaryIndex_injective line 68
  20. theorem OAI.FiniteEntropySeparation.Model.auxiliaryIndex_fresh line 71
  21. theorem OAI.FiniteEntropySeparation.Model.C_last line 78
  22. theorem OAI.FiniteEntropySeparation.Model.C_castSucc line 79
  23. theorem OAI.FiniteEntropySeparation.Model.C_selfAdjoint line 81
  24. theorem OAI.FiniteEntropySeparation.Model.C_mem_background line 86
  25. theorem OAI.FiniteEntropySeparation.Model.C_mem line 92
  26. theorem OAI.FiniteEntropySeparation.Model.C_norm_le line 94
  27. theorem OAI.FiniteEntropySeparation.Model.initialNoise_free line 99
  28. theorem OAI.FiniteEntropySeparation.Model.X_mem_background line 103
  29. theorem OAI.FiniteEntropySeparation.Model.auxiliaryNoise_free line 109
  30. theorem OAI.FiniteEntropySeparation.Model.X_mem line 113
  31. theorem OAI.FiniteEntropySeparation.Model.X_selfAdjoint line 115
  32. theorem OAI.FiniteEntropySeparation.Model.auxiliaryNoise_mem line 120
  33. theorem OAI.FiniteEntropySeparation.Model.auxiliaryNoise_selfAdjoint line 123
  34. theorem OAI.FiniteEntropySeparation.Model.X_norm_le line 126
  35. theorem OAI.FiniteEntropySeparation.Model.heat_fisher_le line 135
  36. theorem OAI.FiniteEntropySeparation.Model.heat_fisher_measurable line 140