OAI/MathematicalPhysics/PEPSSubvolume/EntropyComparison.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Marginal regularization and unpinned nested entropy comparison.

  1. theorem OAI.PolynomialPEPS.Subvolume.SpectralCurve.matrix_eq_spectralHom line 30
  2. theorem OAI.PolynomialPEPS.Subvolume.SpectralCurve.trace_rates_pairing line 34
  3. def OAI.PolynomialPEPS.Subvolume.MarginalRegularization.probabilities line 47
  4. theorem OAI.PolynomialPEPS.Subvolume.MarginalRegularization.probabilities_pos line 50
  5. theorem OAI.PolynomialPEPS.Subvolume.MarginalRegularization.probabilities_sum line 55
  6. theorem OAI.PolynomialPEPS.Subvolume.MarginalRegularization.tendsto_weight_log line 63
  7. theorem OAI.PolynomialPEPS.Subvolume.PhysicalCurve.optimizer_cost_le_sum_entropy line 85
  8. theorem OAI.PolynomialPEPS.Subvolume.PhysicalCurve.amplitude_right_of_bound line 138
  9. theorem OAI.PolynomialPEPS.Subvolume.PhysicalCurve.filter_bound_pos line 181
  10. theorem OAI.PolynomialPEPS.Subvolume.PhysicalCurve.filter_bound_cost_le_trace_rates line 207
  11. theorem OAI.PolynomialPEPS.Subvolume.PhysicalCurve.filter_bound_cost_le_sum_entropy line 244