OAI/Probability/LogConcave/Sampling/ScoreAugmented.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LogConcaveSampling.TensorEnergy.allSplitBound_pair line 13
2. lemma OAI.LogConcaveSampling.TensorEnergy.Bound.add_norm line 61
3. lemma OAI.LogConcaveSampling.TensorEnergy.AllSplitBound.add line 68
4. lemma OAI.LogConcaveSampling.TensorEnergy.allSplitBound_delta line 75
5. lemma OAI.LogConcaveSampling.TensorEnergy.allSplitBound_spatial_delta line 83
6. def OAI.LogConcaveSampling.scoreAugmented line 99
7. lemma OAI.LogConcaveSampling.scoreAugmented_eq line 105