OAI/Probability/DilutedSpin/ScheduledMarkerEstimate.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.DilutedSpinGlass.ReducedTopology.realize_heightCast line 10
2. lemma OAI.DilutedSpinGlass.ReducedTopology.realize_marker_form line 14
3. def OAI.DilutedSpinGlass.ReducedTopology.scheduledOverlapVariance line 21
4. def OAI.DilutedSpinGlass.ReducedTopology.scheduledMarkerDefect line 26
5. lemma OAI.DilutedSpinGlass.ReducedTopology.scheduledMarkerDefect_eq_realize line 32
6. lemma OAI.DilutedSpinGlass.ReducedTopology.scheduledOverlapVariance_eq_realize line 49
7. lemma OAI.DilutedSpinGlass.HeterogeneousMarks.root_scheduled_variance_le_marker line 79