OAI/MathematicalPhysics/PEPSFilters/CollarWeights.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Harmonic collar weights with uniform total weight and quadratic cost.

  1. def OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.collarWeight line 25
  2. def OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.collarWeightSum line 26
  3. def OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.harmonicWindow line 28
  4. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.harmonicWindow_block line 30
  5. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.harmonicWindow_doubling line 46
  6. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.collarWeightSum_eq line 62
  7. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.collarWeight_pos line 66
  8. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.collarWeight_le_one line 69
  9. theorem OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Energy.exists_uniform_collar_weights line 76