OAI/Probability/SKRatio/Gaussian/Planted.lean

GitHub source file

28 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SKRatio.Planted.gauge line 14
  2. lemma OAI.SKRatio.Planted.coupling_gauge line 17
  3. lemma OAI.SKRatio.Planted.gauge_twice line 24
  4. lemma OAI.SKRatio.Planted.gauge_continuous line 35
  5. lemma OAI.SKRatio.Planted.hamiltonian_gauge line 40
  6. lemma OAI.SKRatio.Planted.hamiltonian_edges line 53
  7. lemma OAI.SKRatio.Planted.gaussianReal_tilt line 74
  8. lemma OAI.SKRatio.Planted.lintegral_fin_nat_prod_eq_prod line 93
  9. lemma OAI.SKRatio.Planted.lintegral_fintype_prod_eq_prod line 127
  10. lemma OAI.SKRatio.Planted.product_tilt line 140
  11. def OAI.SKRatio.Planted.law line 157
  12. instance OAI.SKRatio.Planted.law_probability line 160
  13. def OAI.SKRatio.Planted.normalizingExponent line 163
  14. lemma OAI.SKRatio.Planted.law_density line 166
  15. lemma OAI.SKRatio.Planted.gauge_preserving line 177
  16. lemma OAI.SKRatio.Planted.integrable_exp_linear line 188
  17. lemma OAI.SKRatio.Planted.integral_exp_linear line 195
  18. lemma OAI.SKRatio.Planted.weight_linear line 207
  19. lemma OAI.SKRatio.Planted.weight_integrable line 215
  20. lemma OAI.SKRatio.Planted.integral_weight line 220
  21. lemma OAI.SKRatio.Planted.partition_integrable line 231
  22. lemma OAI.SKRatio.Planted.integral_partition line 235
  23. def OAI.SKRatio.Planted.badWeight line 243
  24. lemma OAI.SKRatio.Planted.badWeight_nonneg line 246
  25. lemma OAI.SKRatio.Planted.badWeight_le_partition line 253
  26. lemma OAI.SKRatio.Planted.badWeight_integrable line 261
  27. lemma OAI.SKRatio.Planted.integral_planted_weight line 267
  28. lemma OAI.SKRatio.Planted.integral_badWeight line 285