OAI/Probability/SKValue/GroundState/RandomGuerra.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SKValueG.scalar_pairing_law line 12
  2. lemma OAI.SKValueG.field_pairing_law line 19
  3. lemma OAI.SKValueG.scalarTreeEval_integrable line 30
  4. lemma OAI.SKValueG.scalarTreeValue_integrable_prod line 34
  5. lemma OAI.SKValueG.fieldTreeValue_integrable_prod line 40
  6. lemma OAI.SKValueG.scalarTreeValue_mean line 48
  7. lemma OAI.SKValueG.fieldTreeValue_mean line 56
  8. theorem OAI.SKValueG.randomized_tree_guerra_upper line 65
  9. lemma OAI.SKValueG.coleHopf_one_sided line 94
  10. lemma OAI.SKValueG.coleHopf_lipschitz line 124
  11. def OAI.SKValueG.fieldProfile line 134
  12. def OAI.SKValueG.TreeScale line 138
  13. lemma OAI.SKValueG.fieldProfile_lipschitz line 142
  14. lemma OAI.SKValueG.gaussian_exp_sum_profile_integrable line 153
  15. lemma OAI.SKValueG.gaussian_exp_sum_coleHopf line 162