OAI/MathematicalPhysics/PEPSSubvolume/PinnedEntropy.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

Pinned entropy bounds and geometric upper comparison.

  1. def OAI.PolynomialPEPS.Subvolume.Pinning.coreColumn line 28
  2. theorem OAI.PolynomialPEPS.Subvolume.Pinning.coreColumn_norm line 33
  3. theorem OAI.PolynomialPEPS.Subvolume.Pinning.sum_coreMatrix line 45
  4. theorem OAI.PolynomialPEPS.Subvolume.Pinning.asMap_mul_apply line 52
  5. theorem OAI.PolynomialPEPS.Subvolume.Pinning.asMap_sum_apply line 56
  6. theorem OAI.PolynomialPEPS.Subvolume.Pinning.sum_pinnedVector line 60
  7. theorem OAI.PolynomialPEPS.Subvolume.Pinning.pinned_self_inner line 69
  8. theorem OAI.PolynomialPEPS.Subvolume.Pinning.pinnedVector_idempotent line 77
  9. theorem OAI.PolynomialPEPS.Subvolume.Pinning.inner_pinned_shell line 83
  10. theorem OAI.PolynomialPEPS.Subvolume.Pinning.sum_pinned_marginals line 98
  11. theorem OAI.PolynomialPEPS.Subvolume.Pinning.pinned_norm_sq line 109
  12. theorem OAI.PolynomialPEPS.Subvolume.Pinning.trace_coreMatrix line 116
  13. theorem OAI.PolynomialPEPS.Subvolume.Pinning.schmidt_weight line 131
  14. theorem OAI.PolynomialPEPS.Subvolume.Pinning.reducedDensity_smul line 143
  15. theorem OAI.PolynomialPEPS.Subvolume.Pinning.reducedDensity_zero line 154
  16. theorem OAI.PolynomialPEPS.Subvolume.Pinning.normalizedPinned_marginal line 159
  17. def OAI.PolynomialPEPS.Subvolume.Pinning.schmidtProbability line 180
  18. def OAI.PolynomialPEPS.Subvolume.Pinning.schmidtState line 184
  19. theorem OAI.PolynomialPEPS.Subvolume.Pinning.schmidtProbability_nonneg line 188
  20. theorem OAI.PolynomialPEPS.Subvolume.Pinning.schmidtProbability_sum line 191
  21. theorem OAI.PolynomialPEPS.Subvolume.Pinning.schmidtProbability_entropy line 196
  22. theorem OAI.PolynomialPEPS.Subvolume.Pinning.schmidt_shell_mixture line 200
  23. theorem OAI.PolynomialPEPS.Subvolume.Pinning.average_schmidt_shell_entropy line 215
  24. theorem OAI.PolynomialPEPS.Subvolume.Pinning.optimizer_cost_le_core_add_shell_entropy line 231
  25. theorem OAI.PolynomialPEPS.Subvolume.GeometricComparison.rectangle_weighted_conditional_contraction line 284