OAI/Probability/LogConcave/Sampling/DirectionalBasisSum.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LogConcaveSampling.directional_basis_sum line 15
2. lemma OAI.LogConcaveSampling.basis_jet_growth_all line 24
3. lemma OAI.LogConcaveSampling.PolySmooth.of_basis_growth line 48
4. lemma OAI.LogConcaveSampling.growth_of_bounded line 54
5. lemma OAI.LogConcaveSampling.normalizedTensor_spatial_allSplit line 75
6. lemma OAI.LogConcaveSampling.normalizedTensor_polySmooth line 103
7. lemma OAI.LogConcaveSampling.conditionalFieldMean_jet_normalized line 141
8. lemma OAI.LogConcaveSampling.conditionalFieldMean_component_polySmooth line 172