OAI/Probability/LogConcave/JetEstimates/SplitBundle.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LogConcaveSampling.TensorEnergy._root_.OAI.OrderedFinpartition.sum_partSize line 12
2. lemma OAI.LogConcaveSampling.TensorEnergy._root_.OAI.OrderedFinpartition.unique_of_partSize_eq line 16
3. lemma OAI.LogConcaveSampling.TensorEnergy._root_.OAI.OrderedFinpartition.length_eq_one_of_partSize_eq line 28
4. lemma OAI.LogConcaveSampling.TensorEnergy.partition_majorant_linear line 41
5. abbrev OAI.LogConcaveSampling.TensorEnergy.SplitBundle line 86
6. def OAI.LogConcaveSampling.TensorEnergy.splitBundleLinear line 89
7. def OAI.LogConcaveSampling.TensorEnergy.splitBundle line 94
8. lemma OAI.LogConcaveSampling.TensorEnergy.allSplitBound_bundle line 97
9. lemma OAI.LogConcaveSampling.TensorEnergy.bundle_norm_le line 112
10. theorem OAI.LogConcaveSampling.TensorEnergy.allSplit_gronwall line 119
11. lemma OAI.LogConcaveSampling.TensorEnergy._root_.OAI.OrderedFinpartition.sum_pred_partSize line 146
12. lemma OAI.LogConcaveSampling.TensorEnergy.partition_scale line 154
13. lemma OAI.LogConcaveSampling.TensorEnergy.partition_sum_scale line 165
14. lemma OAI.LogConcaveSampling.TensorEnergy.gronwallBound_div line 170
15. lemma OAI.LogConcaveSampling.TensorEnergy.partition_array_scale line 187
16. lemma OAI.LogConcaveSampling.TensorEnergy.array_composition_scale line 197
17. lemma OAI.LogConcaveSampling.JetCalculus.time_deriv_spatial_jet line 229
18. lemma OAI.LogConcaveSampling.multilinearTensor_iterated_eq_jet line 246
19. lemma OAI.LogConcaveSampling.spatialTensor_time_deriv line 258