OAI/MathematicalPhysics/PEPSFilters/MarginalLimit.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Residual bounds and exact marginal-coordinate limits.

  1. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Stationarity.clipped_residual_bounds line 22
  2. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Stationarity.clipped_normalized_residual line 52
  3. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.marginalDiagonal_continuous line 84
  4. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.coordinateDensity_continuous line 94
  5. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.clipped_limit_matrix line 110
  6. theorem OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.exists_maximizer_marginal_coordinates line 188