OAI/Probability/LogConcave/Numerics/Picard.lean

GitHub source file

71 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LogConcaveSampling.MeanTree.picard line 15
  2. lemma OAI.LogConcaveSampling.MeanTree.eval_picard line 21
  3. lemma OAI.LogConcaveSampling.MeanTree.depth_picard line 32
  4. def OAI.LogConcaveSampling.MeanTree.probability line 50
  5. lemma OAI.LogConcaveSampling.MeanTree.eval_probability line 56
  6. lemma OAI.LogConcaveSampling.MeanTree.depth_probability line 72
  7. def OAI.LogConcaveSampling.MeanTree.harmonic line 80
  8. lemma OAI.LogConcaveSampling.MeanTree.eval_harmonic line 85
  9. lemma OAI.LogConcaveSampling.MeanTree.depth_harmonic line 102
  10. def OAI.LogConcaveSampling.MeanTree.kernelCorrection line 110
  11. lemma OAI.LogConcaveSampling.MeanTree.eval_kernelCorrection line 118
  12. lemma OAI.LogConcaveSampling.MeanTree.depth_kernelCorrection line 132
  13. def OAI.LogConcaveSampling.MeanTree.kernelAction line 163
  14. def OAI.LogConcaveSampling.MeanTree.kernelQuadrature line 168
  15. lemma OAI.LogConcaveSampling.MeanTree.eval_kernelAction line 172
  16. lemma OAI.LogConcaveSampling.MeanTree.eval_kernelQuadrature line 180
  17. lemma OAI.LogConcaveSampling.MeanTree.depth_kernelQuadrature line 189
  18. def OAI.LogConcaveSampling.MeanTree.velocity line 201
  19. def OAI.LogConcaveSampling.MeanTree.pairEval line 206
  20. lemma OAI.LogConcaveSampling.MeanTree.eval_velocity line 209
  21. lemma OAI.LogConcaveSampling.MeanTree.depth_velocity line 220
  22. def OAI.LogConcaveSampling.MeanTree.pairPicard line 233
  23. lemma OAI.LogConcaveSampling.MeanTree.eval_pairPicard line 241
  24. lemma OAI.LogConcaveSampling.MeanTree.depth_pairPicard line 267
  25. def OAI.LogConcaveSampling.MeanTree.centeringStates line 307
  26. def OAI.LogConcaveSampling.MeanTree.meanCircuit line 312
  27. lemma OAI.LogConcaveSampling.MeanTree.nodes_productPointEquiv line 317
  28. lemma OAI.LogConcaveSampling.MeanTree.eval_centeringStates line 333
  29. lemma OAI.LogConcaveSampling.MeanTree.eval_meanCircuit line 346
  30. lemma OAI.LogConcaveSampling.MeanTree.depth_centeringStates line 362
  31. lemma OAI.LogConcaveSampling.MeanTree.depth_meanCircuit line 371
  32. theorem OAI.LogConcaveSampling.MeanTree.meanCircuit_fixed_depth line 383
  33. def OAI.LogConcaveSampling.MeanTree.base line 408
  34. lemma OAI.LogConcaveSampling.MeanTree.base_anchor line 411
  35. lemma OAI.LogConcaveSampling.MeanTree.base_zero line 412
  36. lemma OAI.LogConcaveSampling.MeanTree.base_scale line 413
  37. lemma OAI.LogConcaveSampling.MeanTree.base_add line 414
  38. lemma OAI.LogConcaveSampling.MeanTree.base_mean line 415
  39. lemma OAI.LogConcaveSampling.MeanTree.base_conditional line 416
  40. lemma OAI.LogConcaveSampling.MeanTree.base_sumFin line 418
  41. lemma OAI.LogConcaveSampling.MeanTree.base_sumFamily line 424
  42. def OAI.LogConcaveSampling.MeanTree.centers line 430
  43. lemma OAI.LogConcaveSampling.MeanTree.centers_anchor line 433
  44. lemma OAI.LogConcaveSampling.MeanTree.centers_zero line 435
  45. lemma OAI.LogConcaveSampling.MeanTree.centers_scale line 436
  46. lemma OAI.LogConcaveSampling.MeanTree.centers_add line 438
  47. lemma OAI.LogConcaveSampling.MeanTree.centers_mean line 454
  48. lemma OAI.LogConcaveSampling.MeanTree.centers_conditional line 459
  49. lemma OAI.LogConcaveSampling.MeanTree.centers_sumFin line 466
  50. lemma OAI.LogConcaveSampling.MeanTree.centers_sumFamily line 472
  51. lemma OAI.LogConcaveSampling.MeanTree.picard_shape line 476
  52. lemma OAI.LogConcaveSampling.MeanTree.weight_anchor line 508
  53. lemma OAI.LogConcaveSampling.MeanTree.weight_zero line 510
  54. lemma OAI.LogConcaveSampling.MeanTree.weight_scale line 511
  55. lemma OAI.LogConcaveSampling.MeanTree.weight_add line 514
  56. lemma OAI.LogConcaveSampling.MeanTree.weight_mean line 517
  57. lemma OAI.LogConcaveSampling.MeanTree.weight_nonneg line 519
  58. lemma OAI.LogConcaveSampling.MeanTree.weight_sumFin line 522
  59. lemma OAI.LogConcaveSampling.MeanTree.weight_sumFamily line 527
  60. lemma OAI.LogConcaveSampling.MeanTree.weight_conditional line 531
  61. def OAI.LogConcaveSampling.MeanTree.centersBound line 534
  62. lemma OAI.LogConcaveSampling.MeanTree.centersBound_mono line 537
  63. lemma OAI.LogConcaveSampling.MeanTree.centersBound_anchor line 543
  64. lemma OAI.LogConcaveSampling.MeanTree.centersBound_zero line 547
  65. lemma OAI.LogConcaveSampling.MeanTree.centersBound_scale line 548
  66. lemma OAI.LogConcaveSampling.MeanTree.centersBound_add line 550
  67. lemma OAI.LogConcaveSampling.MeanTree.centersBound_mean line 556
  68. lemma OAI.LogConcaveSampling.MeanTree.centersBound_sumFin line 559
  69. lemma OAI.LogConcaveSampling.MeanTree.centersBound_sumFamily line 564
  70. lemma OAI.LogConcaveSampling.MeanTree.centersBound_conditional line 567
  71. lemma OAI.LogConcaveSampling.MeanTree.weight_picard line 573