OAI/Probability/DilutedSpin/RegularBadMass.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.DepthAverage.uniform_indicator_eq line 14
2. lemma OAI.DilutedSpinGlass.DepthAverage.uniform_interval_le line 22
3. lemma OAI.DilutedSpinGlass.DepthAverage.uniform_boundary_le line 40
4. lemma OAI.DilutedSpinGlass.DepthAverage.uniform_near_le line 59
5. lemma OAI.DilutedSpinGlass.DepthAverage.average_boundary_le line 72
6. lemma OAI.DilutedSpinGlass.DepthAverage.average_near_le line 81
7. lemma OAI.DilutedSpinGlass.DepthAverage.regular_of_discrete line 93
8. lemma OAI.DilutedSpinGlass.DepthAverage.nonregular_pointwise line 121
9. lemma OAI.DilutedSpinGlass.DepthAverage.nonregular_average_bound line 151