OAI/Probability/SKValue/GroundState/LogComparison.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKValueG.expected_logPartition_reindex line 12
  2. lemma OAI.SKValueG.expected_logPartition_le_orthogonal line 19
  3. lemma OAI.SKValueG.expected_logPartition_embedLeft line 37
  4. lemma OAI.SKValueG.expected_logPartition_embedRight line 54
  5. lemma OAI.SKValueG.expected_logPartition_le line 71
  6. lemma OAI.SKValueG.finiteMaximum_mono line 95
  7. lemma OAI.SKValueG.finiteMaximum_add_const line 101
  8. lemma OAI.SKValueG.affineMaximum_integrable line 111
  9. lemma OAI.SKValueG.replicated_partition_bounds line 121