OAI/Probability/LogConcave/JetEstimates/JetMaterial.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.LogConcaveSampling.TensorAtom.lastEquiv_symm_inl line 15
  2. lemma OAI.LogConcaveSampling.TensorAtom.lastEquiv_symm_inr line 19
  3. lemma OAI.LogConcaveSampling.TensorAtom.HasMaterial.congr line 25
  4. def OAI.LogConcaveSampling.TensorAtom.jetMaterial line 34
  5. lemma OAI.LogConcaveSampling.TensorAtom.jetMaterial_weight line 38
  6. lemma OAI.LogConcaveSampling.TensorAtom.hasMaterial_jetList line 50
  7. def OAI.LogConcaveSampling.TensorExpression.atom line 69
  8. lemma OAI.LogConcaveSampling.TensorExpression.atom_eval line 70
  9. lemma OAI.LogConcaveSampling.TensorExpression.atom_weight line 72
  10. lemma OAI.LogConcaveSampling.TensorExpression.jet_atom_eval line 74
  11. lemma OAI.LogConcaveSampling.TensorExpression.jet_hasMaterial line 83
  12. lemma OAI.LogConcaveSampling.TensorExpression.atom_contract_eval line 110
  13. lemma OAI.LogConcaveSampling.TensorExpression.atom_adjoint_eval line 131
  14. theorem OAI.LogConcaveSampling.TensorExpression.hasMaterial line 145
  15. theorem OAI.LogConcaveSampling.TensorAtom.hasMaterial line 219
  16. def OAI.LogConcaveSampling.TensorSum.combine line 229
  17. lemma OAI.LogConcaveSampling.TensorSum.combine_eval line 232
  18. lemma OAI.LogConcaveSampling.TensorSum.weightLE_combine line 238
  19. def OAI.LogConcaveSampling.TensorSum.HasMaterial line 241
  20. lemma OAI.LogConcaveSampling.TensorSum.HasMaterial.pure line 248
  21. lemma OAI.LogConcaveSampling.TensorSum.HasMaterial.scale line 254
  22. lemma OAI.LogConcaveSampling.TensorSum.HasMaterial.combine line 269
  23. lemma OAI.LogConcaveSampling.TensorSum.HasMaterial.congr line 280
  24. theorem OAI.LogConcaveSampling.TensorSum.hasMaterial line 287
  25. lemma OAI.LogConcaveSampling.JetCalculus.dir_congr_nonneg_time line 331
  26. lemma OAI.LogConcaveSampling.JetCalculus.mdir_congr_nonneg_time line 349
  27. def OAI.LogConcaveSampling.JetCalculus.materialIter line 360
  28. lemma OAI.LogConcaveSampling.JetCalculus.materialIter_timeSmooth line 364
  29. def OAI.LogConcaveSampling.TensorSum.RepresentsMaterial line 377
  30. theorem OAI.LogConcaveSampling.TensorSum.representsMaterial line 384
  31. lemma OAI.LogConcaveSampling.JetCalculus.gadj_add_at line 417
  32. def OAI.LogConcaveSampling.TensorSum.insertOne line 432
  33. lemma OAI.LogConcaveSampling.TensorSum.weightLE_insertOne line 435
  34. lemma OAI.LogConcaveSampling.TensorSum.insertOne_eval line 441
  35. lemma OAI.LogConcaveSampling.TensorSum.insertOne_mean line 452
  36. def OAI.LogConcaveSampling.TensorSum.outer line 466
  37. lemma OAI.LogConcaveSampling.TensorSum.outer_timeSmooth line 472
  38. lemma OAI.LogConcaveSampling.TensorSum.outer_add line 482
  39. lemma OAI.LogConcaveSampling.TensorSum.outer_scale line 500
  40. theorem OAI.LogConcaveSampling.TensorSum.outer_material line 518