OAI/Probability/LogConcave/JetEstimates/ContractLeftSplit.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LogConcaveSampling.TensorEnergy.contractLeftSplit line 17
  2. def OAI.LogConcaveSampling.TensorEnergy.contractRightSplit line 23
  3. def OAI.LogConcaveSampling.TensorEnergy.appendCoordinate line 29
  4. def OAI.LogConcaveSampling.TensorEnergy.prependCoordinate line 33
  5. lemma OAI.LogConcaveSampling.TensorEnergy.allSplit_contract_oriented line 37
  6. lemma OAI.LogConcaveSampling.TensorEnergy.allSplit_contract_reverse line 62
  7. lemma OAI.LogConcaveSampling.TensorEnergy.allSplit_contract_either line 74
  8. def OAI.LogConcaveSampling.TensorEnergy.singleContract line 86
  9. def OAI.LogConcaveSampling.TensorEnergy.partEquiv line 99
  10. def OAI.LogConcaveSampling.TensorEnergy.outputCoords line 102
  11. def OAI.LogConcaveSampling.TensorEnergy.inputCoords line 109
  12. lemma OAI.LogConcaveSampling.TensorEnergy.splitOrientation line 117
  13. lemma OAI.LogConcaveSampling.TensorEnergy.part_colors_left line 143
  14. lemma OAI.LogConcaveSampling.TensorEnergy.part_colors_right line 156
  15. lemma OAI.LogConcaveSampling.TensorEnergy.singleContract_split_bound line 168
  16. lemma OAI.LogConcaveSampling.TensorEnergy.allSplitBound_of_proper line 225
  17. lemma OAI.LogConcaveSampling.TensorEnergy.AllSplitBound.singleContract line 240
  18. lemma OAI.LogConcaveSampling.TensorEnergy.AllSplitBound.mono line 262
  19. lemma OAI.LogConcaveSampling.TensorEnergy.AllSplitBound.const_mul line 267
  20. lemma OAI.LogConcaveSampling.TensorEnergy.Bound.finite_sum_norm line 273
  21. lemma OAI.LogConcaveSampling.TensorEnergy.AllSplitBound.finite_sum line 284
  22. lemma OAI.LogConcaveSampling.TensorEnergy.nonempty_properSplit line 291
  23. lemma OAI.LogConcaveSampling.TensorEnergy.AllSplitBound.entry_le line 296