OAI/Probability/LogConcave/Sampling/MaterialScalar.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.LogConcaveSampling.quadraticTilt_derivative_apply line 15
  2. theorem OAI.LogConcaveSampling.fderiv_quadraticExpectation line 26
  3. lemma OAI.LogConcaveSampling.hasDerivAt_conditionalParameter_time line 58
  4. theorem OAI.LogConcaveSampling.deriv_conditional_integral line 77
  5. theorem OAI.LogConcaveSampling.conditionalIntegral_dir_cov line 124
  6. theorem OAI.LogConcaveSampling.conditionalU_one_cov line 157
  7. lemma OAI.LogConcaveSampling.conditional_observable_memLp line 178
  8. lemma OAI.LogConcaveSampling.conditional_covariance_eq line 187
  9. lemma OAI.LogConcaveSampling.conditional_covariance_smooth line 200
  10. lemma OAI.LogConcaveSampling.directional_conditional_covariance line 211
  11. lemma OAI.LogConcaveSampling.covariance_third_diagonal line 258
  12. lemma OAI.LogConcaveSampling.covariance_inner_synthesis line 269
  13. lemma OAI.LogConcaveSampling.covariance_norm_sq_sum line 281
  14. def OAI.LogConcaveSampling.materialScalar line 304
  15. lemma OAI.LogConcaveSampling.deriv_conditional_integral_cov line 308
  16. lemma OAI.LogConcaveSampling.directional_position_covariance line 337
  17. theorem OAI.LogConcaveSampling.material_conditional_expectation line 355
  18. lemma OAI.LogConcaveSampling.conditionalLaw_probability_sq line 438
  19. lemma OAI.LogConcaveSampling.conditionalLaw_hasExpMoments_sq line 454
  20. lemma OAI.LogConcaveSampling.conditionalFieldMean_inner_sq line 472
  21. theorem OAI.LogConcaveSampling.material_conditionalFieldMean line 484