OAI/MathematicalPhysics/PEPSFilters/Clipping.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Simplex stationarity and clipped marginal coordinates.

  1. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Stationarity.deriv_nonpos_of_right_max line 21
  2. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.Stationarity.simplex_clip line 32
  3. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.inner_insertion_eq_trace line 73
  4. def OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.spectralAffineCurve line 117
  5. def OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.spectralLogDirection line 121
  6. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.spectralAffineCurve_zero line 125
  7. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.deriv_spectralAffineCurve line 129
  8. def OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.marginalDiagonal line 170
  9. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.marginalDiagonal_nonneg line 173
  10. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.sum_marginalDiagonal line 178
  11. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.re_trace_spectralLogDirection line 186
  12. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.regularized_output_update line 198
  13. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.simplex_affine_vertex line 215
  14. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.deriv_sq_norm_complex line 229
  15. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.deriv_regularized_norm_sq line 253
  16. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.regularized_maximizer_gradient line 292
  17. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.output_ne_zero_of_invertible line 342
  18. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.regularized_output_ne_zero line 362
  19. lemma OAI.PolynomialPEPS.PinnedEntropy.NestedFilter.regularized_maximizer_clip line 367