OAI/Probability/SKBarriers/Dynamics/Uniformization.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SK.Analytic.clockWeight line 15
2. theorem OAI.SK.Analytic.clockWeight_nonneg line 17
3. theorem OAI.SK.Analytic.clockWeight_hasSum line 21
4. theorem OAI.SK.Analytic.clockWeight_sum line 27
5. theorem OAI.SK.Analytic.uniformization_summable line 29
6. theorem OAI.SK.Analytic.continuousKernel_eq_clock line 36
7. theorem OAI.SK.Analytic.continuousKernel_nonneg line 41
8. theorem OAI.SK.Analytic.continuousKernel_sum line 50
9. theorem OAI.SK.Analytic.continuousKernel_stationary line 59
10. theorem OAI.SK.Analytic.continuous_sign_mass_of_tv line 74