OAI/Probability/LogConcave/OraclePrograms/CircuitD.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.LogConcaveSampling.circuitD line 12
2. lemma OAI.LogConcaveSampling.circuitD_nonneg line 14
3. lemma OAI.LogConcaveSampling.sqrt_le_circuitD line 16
4. lemma OAI.LogConcaveSampling.field_zero_eq_gradient line 18
5. def OAI.LogConcaveSampling.circuitGrowthConstant line 21
6. lemma OAI.LogConcaveSampling.circuitGrowthConstant_pos line 22
7. lemma OAI.LogConcaveSampling.probabilityInitialRms_growth line 26
8. lemma OAI.LogConcaveSampling.conditionalMean_flow_growth line 68
9. lemma OAI.LogConcaveSampling.harmonicStationaryMoment_growth line 110
10. lemma OAI.LogConcaveSampling.circuitD_change line 154
11. lemma OAI.LogConcaveSampling.primitiveExpectedField_growth line 163
12. theorem OAI.LogConcaveSampling.MeanTree.eval_circuitD_bound line 179