OAI/Analysis/FreeEntropy/FisherLaw.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.FiniteEntropySeparation.wordEval_append line 11
  2. theorem OAI.FiniteEntropySeparation.star_wordEval line 15
  3. theorem OAI.FiniteEntropySeparation.inner_wordVector line 26
  4. theorem OAI.FiniteEntropySeparation.polynomialVector_norm_sq_eq_of_moments line 34
  5. theorem OAI.FiniteEntropySeparation.derivativeMoment_eq_of_moments line 48
  6. theorem OAI.FiniteEntropySeparation.freeFisher_eq_of_wordMoments line 57
  7. theorem OAI.FiniteEntropySeparation.continuous_heatTuple line 80
  8. theorem OAI.FiniteEntropySeparation.FreeTensor.heat_conjugates_exist line 87
  9. theorem OAI.FiniteEntropySeparation.FreeTensor.heat_freeFisher_measurable line 96