OAI/Probability/SKBarriers/Coverage/WeightedConcentration.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. class OAI.SK.Analytic.Weighted.Weights line 14
  2. def OAI.SK.Analytic.Weighted.partition line 19
  3. def OAI.SK.Analytic.Weighted.gibbs line 22
  4. theorem OAI.SK.Analytic.Weighted.partition_pos line 25
  5. theorem OAI.SK.Analytic.Weighted.gibbs_nonneg line 32
  6. theorem OAI.SK.Analytic.Weighted.gibbs_sum line 36
  7. def OAI.SK.Analytic.Weighted.directionalEnergy line 41
  8. theorem OAI.SK.Analytic.Weighted.directionalEnergy_exp_le line 44
  9. theorem OAI.SK.Analytic.Weighted.continuous_partition line 54
  10. theorem OAI.SK.Analytic.Weighted.continuous_gibbs line 60
  11. theorem OAI.SK.Analytic.Weighted.gibbs_le_one line 66
  12. theorem OAI.SK.Analytic.Weighted.gibbs_integrable line 71
  13. theorem OAI.SK.Analytic.Weighted.continuous_directionalEnergy line 77
  14. theorem OAI.SK.Analytic.Weighted.directionalEnergy_exp_integrable line 84
  15. theorem OAI.SK.Analytic.Weighted.directionalEnergy_exp_integral_le line 99
  16. theorem OAI.SK.Analytic.Weighted.directionalEnergy_pair_exp_integrable line 116
  17. theorem OAI.SK.Analytic.Weighted.directionalEnergy_pair_exp_integral_le line 133
  18. def OAI.SK.Analytic.Weighted.logPartition line 145
  19. theorem OAI.SK.Analytic.Weighted.continuous_logPartition line 147
  20. theorem OAI.SK.Analytic.Weighted.logPartition_hasDerivAt line 151
  21. theorem OAI.SK.Analytic.Weighted.rotation_logPartition_hasDerivAt line 169
  22. theorem OAI.SK.Analytic.Weighted.continuous_rotation_energy line 185
  23. theorem OAI.SK.Analytic.Weighted.rotation_logPartition_integral line 190
  24. theorem OAI.SK.Analytic.Weighted.rotation_exp_jensen line 205
  25. theorem OAI.SK.Analytic.Weighted.rotated_directionalEnergy_exp_integrable line 224
  26. theorem OAI.SK.Analytic.Weighted.rotated_directionalEnergy_exp_integral_le line 231
  27. def OAI.SK.Analytic.Weighted.rotationIntegrand line 247
  28. theorem OAI.SK.Analytic.Weighted.continuous_rotationIntegrand line 251
  29. theorem OAI.SK.Analytic.Weighted.rotationIntegrand_integrable line 266
  30. theorem OAI.SK.Analytic.Weighted.rotation_exp_integrable line 285
  31. theorem OAI.SK.Analytic.Weighted.rotation_exp_integral_le line 303
  32. theorem OAI.SK.Analytic.Weighted.rotateDisorder_pi_div_two_fst line 338
  33. theorem OAI.SK.Analytic.Weighted.logPartition_difference_exp_integrable line 343
  34. theorem OAI.SK.Analytic.Weighted.logPartition_exp_integrable line 349
  35. theorem OAI.SK.Analytic.Weighted.logPartition_integrable line 360
  36. theorem OAI.SK.Analytic.Weighted.logPartition_centered_exp_jensen line 377
  37. theorem OAI.SK.Analytic.Weighted.logPartition_centered_exp_integrable line 398
  38. theorem OAI.SK.Analytic.Weighted.logPartition_centered_exp_integral_le line 410
  39. theorem OAI.SK.Analytic.Weighted.logPartition_subGaussian line 437
  40. theorem OAI.SK.Analytic.Weighted.logPartition_upper_tail line 449
  41. theorem OAI.SK.Analytic.Weighted.logPartition_lower_tail line 454