OAI/Probability/DilutedSpin/CompoundRateAverage.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.DilutedSpinGlass.integral_add_lipschitz line 16
  2. lemma OAI.DilutedSpinGlass.integrated_compound_rate_bound line 31