OAI/Probability/FreeIsing/Energy/DiscrepancyEnergy.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem367.DiscrepancyEnergy.absolutelyContinuousOnInterval_congr_on line 12
  2. theorem OAI.Problem367.DiscrepancyEnergy.absolutelyContinuousOnInterval_of_integral_representation line 31
  3. theorem OAI.Problem367.DiscrepancyEnergy.integral_timePrimitive line 43
  4. theorem OAI.Problem367.DiscrepancyEnergy.intervalIntegrable_mean line 57
  5. theorem OAI.Problem367.DiscrepancyEnergy.secondMoment_integral_representation line 65
  6. theorem OAI.Problem367.DiscrepancyEnergy.secondMoment_absolutelyContinuous line 96
  7. theorem OAI.Problem367.DiscrepancyEnergy.ae_deriv_of_integral_representation line 112
  8. theorem OAI.Problem367.DiscrepancyEnergy.secondMoment_ae_deriv line 127
  9. theorem OAI.Problem367.DiscrepancyEnergy.integral_martingale_eq_zero line 142
  10. theorem OAI.Problem367.DiscrepancyEnergy.secondMoment_analysis_of_martingale line 153