OAI/Probability/LogConcave/Numerics/KernelCorrectionPicard.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LogConcaveSampling.RMSIntegral.lipschitz_error_sq line 18
2. lemma OAI.LogConcaveSampling.RMSIntegral.add_error_sq line 36
3. lemma OAI.LogConcaveSampling.RMSIntegral.compose_error_sq line 48
4. def OAI.LogConcaveSampling.kernelCorrectionPicard line 72
5. def OAI.LogConcaveSampling.harmonicRmsBudget line 79
6. theorem OAI.LogConcaveSampling.kernelCorrectionPicard_rms line 85
7. lemma OAI.LogConcaveSampling.harmonicPicard_continuous line 192
8. lemma OAI.LogConcaveSampling.kernelCorrectionPicard_continuous line 202