OAI/Probability/FreeIsing/Energy/DiscrepancyRowEnergy.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem367.DiscrepancyEnergy.summable_sq_sub line 12
  2. theorem OAI.Problem367.DiscrepancyEnergy.tsum_sq_sub_le line 20
  3. theorem OAI.Problem367.DiscrepancyEnergy.abs_noise_add_drift_le line 30
  4. theorem OAI.Problem367.DiscrepancyEnergy.integrable_sq_difference_row line 51
  5. theorem OAI.Problem367.DiscrepancyEnergy.integrable_noise_add_drift line 67
  6. theorem OAI.Problem367.DiscrepancyEnergy.hasSum_integral_sq_row line 92
  7. theorem OAI.Problem367.DiscrepancyEnergy.integral_noise_add_drift line 106
  8. theorem OAI.Problem367.DiscrepancyEnergy.sq_row_integrable_of_summable_integrals line 138
  9. def OAI.Problem367.DiscrepancyEnergy.density line 166
  10. theorem OAI.Problem367.DiscrepancyEnergy.secondMoment_row_analysis_of_martingale line 170