OAI/Probability/FreeIsing/Martingales/BoundedMartingaleDriftEnergy.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem367.MartingaleDriftEnergy.stronglyMeasurable_timePrimitive line 12
2. theorem OAI.Problem367.MartingaleDriftEnergy.ae_timePrimitive_bound_of_totalVariation line 36
3. theorem OAI.Problem367.MartingaleDriftEnergy.ae_norm_martingale_le_of_bounded_process line 55
4. theorem OAI.Problem367.MartingaleDriftEnergy.mixed_integrability_of_bounded_process line 70
5. theorem OAI.Problem367.MartingaleDriftEnergy.integral_sq_of_bounded_process line 97