OAI/Probability/LogConcave/Numerics/RowGaussian.lean

GitHub source file

44 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LogConcaveSampling.MeanTree.rowGaussian line 17
  2. lemma OAI.LogConcaveSampling.MeanTree.measurable_rowGaussian line 21
  3. theorem OAI.LogConcaveSampling.MeanTree.rowGaussian_law line 25
  4. theorem OAI.LogConcaveSampling.MeanTree.compileTerms_squared line 63
  5. def OAI.LogConcaveSampling.MeanTree.DeclaredValid line 137
  6. def OAI.LogConcaveSampling.MeanTree.declaredError line 141
  7. theorem OAI.LogConcaveSampling.MeanTree.compileDeclared_squared line 147
  8. def OAI.LogConcaveSampling.MeanTree.DeclaredRootValid line 198
  9. def OAI.LogConcaveSampling.MeanTree.declaredRootError line 202
  10. theorem OAI.LogConcaveSampling.MeanTree.compileDeclaredRoot_squared line 208
  11. lemma OAI.LogConcaveSampling.MeanTree.centers_mono line 259
  12. lemma OAI.LogConcaveSampling.MeanTree.DirectCenter.radius line 266
  13. lemma OAI.LogConcaveSampling.MeanTree.DirectCenter.radius_pos line 279
  14. lemma OAI.LogConcaveSampling.MeanTree.oriented_norm line 286
  15. lemma OAI.LogConcaveSampling.MeanTree.DirectCenter.norm_displacement line 295
  16. def OAI.LogConcaveSampling.MeanTree.rootScales line 313
  17. lemma OAI.LogConcaveSampling.MeanTree.rootScales_anchor line 316
  18. lemma OAI.LogConcaveSampling.MeanTree.rootScales_scale line 318
  19. lemma OAI.LogConcaveSampling.MeanTree.rootScales_add line 320
  20. lemma OAI.LogConcaveSampling.MeanTree.rootScales_sumFin line 327
  21. lemma OAI.LogConcaveSampling.MeanTree.rootScales_sumFamily line 332
  22. lemma OAI.LogConcaveSampling.MeanTree.meanCircuit_final_radius line 336
  23. lemma OAI.LogConcaveSampling.MeanTree.declaredValid_of_radius_bounds line 349
  24. def OAI.LogConcaveSampling.MeanTree.centerValues line 378
  25. lemma OAI.LogConcaveSampling.MeanTree.child_depth_le line 381
  26. lemma OAI.LogConcaveSampling.MeanTree.centerValues_of_bounds line 386
  27. lemma OAI.LogConcaveSampling.MeanTree.directCenter_scalar_bounds line 403
  28. theorem OAI.LogConcaveSampling.MeanTree.centerValues_of_direct line 413
  29. def OAI.LogConcaveSampling.MeanTree.ErrorLimits line 443
  30. theorem OAI.LogConcaveSampling.MeanTree.declaredError_uniform line 450
  31. theorem OAI.LogConcaveSampling.MeanTree.declaredRootError_bound line 475
  32. lemma OAI.LogConcaveSampling.MeanTree.normalizedErrorLimits line 520
  33. theorem OAI.LogConcaveSampling.MeanTree.declaredError_normalized line 541
  34. theorem OAI.LogConcaveSampling.MeanTree.declaredRootError_normalized line 560
  35. def OAI.LogConcaveSampling.MeanTree.DriftData line 600
  36. def OAI.LogConcaveSampling.MeanTree.DriftData.root line 603
  37. def OAI.LogConcaveSampling.MeanTree.DriftValid line 606
  38. def OAI.LogConcaveSampling.MeanTree.compileTermsShift line 609
  39. lemma OAI.LogConcaveSampling.MeanTree.compileTerms_equivariant line 618
  40. lemma OAI.LogConcaveSampling.MeanTree.compileTermsShift_energy line 635
  41. def OAI.LogConcaveSampling.MeanTree.inverseChildShift line 653
  42. def OAI.LogConcaveSampling.MeanTree.compileDeclaredShift line 657
  43. def OAI.LogConcaveSampling.MeanTree.ShiftReady line 666
  44. theorem OAI.LogConcaveSampling.MeanTree.compileDeclared_equivariant line 669