OAI/Probability/LogConcave/Sampling/AnalyticBase.lean

GitHub source file

33 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.LogConcaveSampling.spatial_contract_allSplit line 13
  2. lemma OAI.LogConcaveSampling.spatialEnvelope_contract line 50
  3. theorem OAI.LogConcaveSampling.spatialEnvelope_contract_moment line 64
  4. def OAI.LogConcaveSampling.analyticBase line 112
  5. lemma OAI.LogConcaveSampling.analyticBase_one_le line 114
  6. lemma OAI.LogConcaveSampling.analyticBase_nat_le line 118
  7. lemma OAI.LogConcaveSampling.analyticBase_double line 122
  8. lemma OAI.LogConcaveSampling.analyticBase_mono line 129
  9. lemma OAI.LogConcaveSampling.traceMomentOrder_budget line 135
  10. def OAI.LogConcaveSampling.TameAt line 146
  11. lemma OAI.LogConcaveSampling.TameAt.with_base line 151
  12. lemma OAI.LogConcaveSampling.TameAt.constant_mono line 158
  13. lemma OAI.LogConcaveSampling.ofReal_base_one_le line 167
  14. structure OAI.LogConcaveSampling.TameScore line 170
  15. lemma OAI.LogConcaveSampling.subset_sum_le_common line 192
  16. lemma OAI.LogConcaveSampling.profile_base_double line 199
  17. theorem OAI.LogConcaveSampling.TameAt.contract line 209
  18. def OAI.LogConcaveSampling.adjointConstant line 276
  19. lemma OAI.LogConcaveSampling.adjointConstant_bounds line 278
  20. lemma OAI.LogConcaveSampling.adjoint_base_budget line 293
  21. lemma OAI.LogConcaveSampling.adjoint_score_budget line 325
  22. lemma OAI.LogConcaveSampling.adjoint_trace_prefactor line 347
  23. lemma OAI.LogConcaveSampling.natural_moment_add line 368
  24. lemma OAI.LogConcaveSampling.scoreField_arbitrary_allSplit line 392
  25. def OAI.LogConcaveSampling.scoreContractSlots line 406
  26. def OAI.LogConcaveSampling.adjointCommutator line 409
  27. lemma OAI.LogConcaveSampling.spatialTensor_adjoint_sum line 415
  28. lemma OAI.LogConcaveSampling.adjointCommutator_allSplit line 433
  29. lemma OAI.LogConcaveSampling.spatialEnvelope_adjoint line 455
  30. lemma OAI.LogConcaveSampling.adjoint_base_enn line 494
  31. lemma OAI.LogConcaveSampling.adjoint_score_enn line 502
  32. lemma OAI.LogConcaveSampling.adjoint_trace_enn line 511
  33. theorem OAI.LogConcaveSampling.TameAt.adjoint line 523