OAI/Probability/SKRatio/Entropy/GibbsObservation.lean

GitHub source file

25 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKRatio.Observation.abs_quadratic_le_opNorm line 16
  2. def OAI.SKRatio.Observation.shiftedCoupling line 30
  3. lemma OAI.SKRatio.Observation.shiftedCoupling_quad line 32
  4. lemma OAI.SKRatio.Observation.shiftedCoupling_nonneg line 43
  5. def OAI.SKRatio.Observation.observationMatrix line 60
  6. lemma OAI.SKRatio.Observation.observationMatrix_symm line 62
  7. lemma OAI.SKRatio.Observation.observationMatrix_square line 65
  8. lemma OAI.SKRatio.Observation.symmetric_mulVec_dot line 69
  9. lemma OAI.SKRatio.Observation.observationMatrix_normSq line 81
  10. lemma OAI.SKRatio.Observation.observationMatrix_normSq_le line 91
  11. def OAI.SKRatio.Observation.gibbsFeature line 99
  12. lemma OAI.SKRatio.Observation.gibbsFeature_normSq line 102
  13. lemma OAI.SKRatio.Observation.gibbsFeature_linear line 117
  14. lemma OAI.SKRatio.Observation.hamiltonian_scale line 124
  15. lemma OAI.SKRatio.Observation.channel_weight_identity line 131
  16. lemma OAI.SKRatio.Observation.channel_posterior_gibbs line 145
  17. def OAI.SKRatio.Observation.observedField line 167
  18. lemma OAI.SKRatio.Observation.history_posterior_gibbs line 172
  19. def OAI.SKRatio.Observation.fieldPrior line 185
  20. lemma OAI.SKRatio.Observation.fieldPrior_pos line 192
  21. lemma OAI.SKRatio.Observation.zero_scale_product line 195
  22. lemma OAI.SKRatio.Observation.history_endpoint_product line 208
  23. lemma OAI.SKRatio.Observation.history_endpoint_entropy line 215
  24. theorem OAI.SKRatio.Observation.entropy_of_scaled_covariance line 234
  25. theorem OAI.SKRatio.Observation.zero_field_mlsi line 266