OAI/Analysis/FreeEntropy/FisherVariational.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.FiniteEntropySeparation.WordPolynomial line 13
  2. def OAI.FiniteEntropySeparation.polynomialVector line 15
  3. def OAI.FiniteEntropySeparation.polynomialDerivative line 19
  4. theorem OAI.FiniteEntropySeparation.conjugate_polynomial_pairing line 23
  5. theorem OAI.FiniteEntropySeparation.polynomialVector_range line 30
  6. theorem OAI.FiniteEntropySeparation.norm_sq_eq_iSup_dense line 36
  7. def OAI.FiniteEntropySeparation.fisherTest line 71
  8. theorem OAI.FiniteEntropySeparation.freeFisher_variational line 75
  9. theorem OAI.FiniteEntropySeparation.freeFisher_lt_top_iff line 88
  10. theorem OAI.FiniteEntropySeparation.exists_conjugate_of_fisher_le line 101
  11. theorem OAI.FiniteEntropySeparation.continuous_wordEval line 106
  12. theorem OAI.FiniteEntropySeparation.continuous_wordMoment line 115
  13. theorem OAI.FiniteEntropySeparation.continuous_derivativeMoment line 121
  14. theorem OAI.FiniteEntropySeparation.continuous_fisherTest line 132
  15. theorem OAI.FiniteEntropySeparation.lowerSemicontinuous_freeFisher line 147