OAI/Probability/SKValue/GroundState/AffineComparison.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.SKValueG.expected_affine_max_le line 13
  2. lemma OAI.SKValueG.product_inner_sum line 111
  3. lemma OAI.SKValueG.sq_distance_sum line 123
  4. def OAI.SKValueG.leafFieldCoeff line 130
  5. def OAI.SKValueG.leafAuxCoeff line 133
  6. def OAI.SKValueG.guerraCoeff line 136
  7. lemma OAI.SKValueG.leafField_inner line 140
  8. lemma OAI.SKValueG.leafField_sq line 146
  9. lemma OAI.SKValueG.leafAux_inner line 154
  10. lemma OAI.SKValueG.leafAux_sq line 169
  11. theorem OAI.SKValueG.guerra_metric_remainder line 176
  12. lemma OAI.SKValueG.guerra_metric_le line 193