OAI/Probability/SKBarriers/Parisi/CDFSupportGap.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SK.Analytic.chain_coefficients_squares line 16
2. theorem OAI.SK.Analytic.scalarMagnetization_square_lipschitz line 25
3. theorem OAI.SK.Analytic.scalarCDFValue_duration_zero line 35
4. theorem OAI.SK.Analytic.scalarCDFGradient_duration_zero line 42
5. theorem OAI.SK.Analytic.scalarCDFOverlap_one_lt line 50
6. theorem OAI.SK.Analytic.scalarCDFParisi_support_away_one line 70