OAI/Probability/LogConcave/Sampling/NoiseKernel.lean

GitHub source file

45 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LogConcaveSampling.noiseKernel line 16
  2. instance OAI.LogConcaveSampling.noiseKernel_markov line 19
  3. lemma OAI.LogConcaveSampling.noiseKernel_apply line 23
  4. lemma OAI.LogConcaveSampling.noiseKernel_comp line 29
  5. def OAI.LogConcaveSampling.proximalKernel line 39
  6. lemma OAI.LogConcaveSampling.proximalKernel_markov line 42
  7. lemma OAI.LogConcaveSampling.measure_eq_of_bounded_integral line 48
  8. lemma OAI.LogConcaveSampling.posteriorKernel_invariant line 57
  9. lemma OAI.LogConcaveSampling.proximalKernel_invariant line 67
  10. def OAI.LogConcaveSampling.kernelAction line 74
  11. lemma OAI.LogConcaveSampling.kernelAction_measurable line 77
  12. lemma OAI.LogConcaveSampling.kernelAction_bounded line 81
  13. lemma OAI.LogConcaveSampling.kernelAction_unit line 85
  14. lemma OAI.LogConcaveSampling.kernelAction_comp line 93
  15. lemma OAI.LogConcaveSampling.noiseKernel_action_lipschitz line 100
  16. lemma OAI.LogConcaveSampling.proximal_action_lipschitz line 117
  17. lemma OAI.LogConcaveSampling.proximal_action_smoothing line 132
  18. lemma OAI.LogConcaveSampling.affine_primitive_posterior line 169
  19. lemma OAI.LogConcaveSampling.noised_affine_law line 183
  20. def OAI.LogConcaveSampling.OracleCompiler.proximalProgram line 199
  21. lemma OAI.LogConcaveSampling.OracleCompiler.proximalProgram_run line 205
  22. def OAI.LogConcaveSampling.OracleCompiler.approximateProximalKernel line 211
  23. lemma OAI.LogConcaveSampling.OracleCompiler.approximateProximalKernel_markov line 216
  24. lemma OAI.LogConcaveSampling.OracleCompiler.approximateProximalKernel_apply line 223
  25. lemma OAI.LogConcaveSampling.OracleCompiler.approximateProximalKernel_tv line 233
  26. lemma OAI.LogConcaveSampling.posterior_joint_reconstruction line 295
  27. def OAI.LogConcaveSampling.halvingKernel line 329
  28. lemma OAI.LogConcaveSampling.halvingKernel_markov line 332
  29. lemma OAI.LogConcaveSampling.halvingKernel_apply line 338
  30. lemma OAI.LogConcaveSampling.halving_gaussian_law line 345
  31. lemma OAI.LogConcaveSampling.halvingKernel_invariant line 368
  32. def OAI.LogConcaveSampling.OracleCompiler.halvingProgram line 404
  33. def OAI.LogConcaveSampling.OracleCompiler.approximateHalvingKernel line 408
  34. lemma OAI.LogConcaveSampling.OracleCompiler.approximateHalvingKernel_markov line 412
  35. lemma OAI.LogConcaveSampling.OracleCompiler.approximateHalvingKernel_apply line 418
  36. lemma OAI.LogConcaveSampling.OracleCompiler.approximateHalvingKernel_tv line 427
  37. def OAI.LogConcaveSampling.markovChain line 454
  38. instance OAI.LogConcaveSampling.markovChain_probability line 458
  39. def OAI.LogConcaveSampling.markovAction line 465
  40. lemma OAI.LogConcaveSampling.markovAction_measurable line 468
  41. lemma OAI.LogConcaveSampling.markovAction_bounded line 475
  42. lemma OAI.LogConcaveSampling.markovAction_unit line 483
  43. lemma OAI.LogConcaveSampling.markovChain_integral line 491
  44. lemma OAI.LogConcaveSampling.markovChain_invariant line 503
  45. lemma OAI.LogConcaveSampling.markovChain_perturbation line 509