OAI/Probability/SKGap/Stability/ConditionalMean.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKGapCutoff.Static.conditionalMean line 47
  2. def OAI.SKGapCutoff.Static.lawDirichlet line 51
  3. def OAI.SKGapCutoff.Static.lawDensityEnergy line 55
  4. lemma OAI.SKGapCutoff.Static.binary_root_energy line 58
  5. lemma OAI.SKGapCutoff.Static.binary_conditional_mean_energy line 70
  6. lemma OAI.SKGapCutoff.Static.conditionalMean_flip line 108
  7. lemma OAI.SKGapCutoff.Static.lawDensityEnergy_eq line 113
  8. theorem OAI.SKGapCutoff.Static.conditional_means_energy line 126
  9. lemma OAI.SKGapCutoff.Static.conditionalMean_mul_mass line 154
  10. lemma OAI.SKGapCutoff.Static.conditionalMean_abs_le line 165
  11. lemma OAI.SKGapCutoff.Static.law_coordinate_mean line 174
  12. lemma OAI.SKGapCutoff.Static.law_integration_by_parts line 192
  13. lemma OAI.SKGapCutoff.Static.law_integration_by_parts_variance line 217
  14. lemma OAI.SKGapCutoff.Static.gibbs_flipRate_fraction line 228
  15. lemma OAI.SKGapCutoff.Static.conditionalMean_gibbs line 240
  16. lemma OAI.SKGapCutoff.Static.lawDirichlet_gibbs line 253
  17. theorem OAI.SKGapCutoff.Static.gibbs_conditional_means_energy line 289
  18. lemma OAI.SKGapCutoff.Static.lawDensityEnergy_nonneg line 298
  19. lemma OAI.SKGapCutoff.Static.lawDensityEnergy_le line 306
  20. lemma OAI.SKGapCutoff.Static.weighted_cauchy_sq line 334
  21. theorem OAI.SKGapCutoff.Static.weak_residual_base line 343