OAI/Probability/LogConcave/Numerics/ScalarPicard.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LogConcaveSampling.MeanTree.scalarPicard line 16
  2. def OAI.LogConcaveSampling.MeanTree.vectorPicard line 20
  3. lemma OAI.LogConcaveSampling.MeanTree.cost_picard line 24
  4. lemma OAI.LogConcaveSampling.MeanTree.cost_pairPicard line 34
  5. def OAI.LogConcaveSampling.MeanTree.flowWork line 52
  6. def OAI.LogConcaveSampling.MeanTree.kernelWork line 54
  7. def OAI.LogConcaveSampling.MeanTree.velocityWork line 57
  8. def OAI.LogConcaveSampling.MeanTree.meanWork line 60
  9. lemma OAI.LogConcaveSampling.MeanTree.cost_probability line 63
  10. lemma OAI.LogConcaveSampling.MeanTree.cost_forward line 67
  11. lemma OAI.LogConcaveSampling.MeanTree.cost_harmonic line 71
  12. lemma OAI.LogConcaveSampling.MeanTree.cost_kernelCorrection line 76
  13. lemma OAI.LogConcaveSampling.MeanTree.cost_kernelQuadrature line 83
  14. lemma OAI.LogConcaveSampling.MeanTree.cost_velocity line 91
  15. lemma OAI.LogConcaveSampling.MeanTree.cost_meanCircuit line 99
  16. lemma OAI.LogConcaveSampling.MeanTree.cost_literalMean line 110
  17. lemma OAI.LogConcaveSampling.MeanTree.cost_literalSample line 115
  18. lemma OAI.LogConcaveSampling.MeanTree.shiftReady_of_positive line 134
  19. lemma OAI.LogConcaveSampling.MeanTree.rootShiftReady_of_positive line 140
  20. structure OAI.LogConcaveSampling.OracleCompiler.MeanBudget line 149
  21. structure OAI.LogConcaveSampling.OracleCompiler.SampleBudget line 154
  22. lemma OAI.LogConcaveSampling.OracleCompiler.MeanBudget.mono line 161
  23. lemma OAI.LogConcaveSampling.OracleCompiler.SampleBudget.mono line 163
  24. lemma OAI.LogConcaveSampling.OracleCompiler.terminalMeanProgram_budget line 166
  25. lemma OAI.LogConcaveSampling.OracleCompiler.terminalReservedProgram_budget line 170
  26. lemma OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.mean_positive line 177
  27. lemma OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.sample_positive line 180
  28. lemma OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.sampleDrift_spec line 185
  29. lemma OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.sampleFrom_budget line 192
  30. lemma OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.meanFrom_budget line 238