OAI/Probability/SKSupport/Control/CoefficientApprox.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ZeroTemperatureSK.approxMesh line 14
  2. lemma OAI.ZeroTemperatureSK.approxMesh_pos line 16
  3. lemma OAI.ZeroTemperatureSK.approxMesh_horizon line 18
  4. lemma OAI.ZeroTemperatureSK.approxMesh_limit line 22
  5. lemma OAI.ZeroTemperatureSK.sample_mem line 26
  6. def OAI.ZeroTemperatureSK.approxCoeff line 31
  7. def OAI.ZeroTemperatureSK.approxGamma line 35
  8. lemma OAI.ZeroTemperatureSK.approxCoeff_eq line 38
  9. lemma OAI.ZeroTemperatureSK.approxGamma_samples line 43
  10. lemma OAI.ZeroTemperatureSK.approxGamma_bounds line 51
  11. lemma OAI.ZeroTemperatureSK.approxGamma_tendsto line 57
  12. lemma OAI.ZeroTemperatureSK.OrderParameter.ae_continuous line 78
  13. lemma OAI.ZeroTemperatureSK.approxGamma_L1 line 88
  14. lemma OAI.ZeroTemperatureSK.Heat.uniformCauchySeq_deriv_of_bound line 129
  15. theorem OAI.ZeroTemperatureSK.Heat.tendstoUniformly_deriv_of_bound line 175
  16. lemma OAI.ZeroTemperatureSK.Heat.contDiff_iteratedDeriv_infty line 193
  17. theorem OAI.ZeroTemperatureSK.Heat.smooth_limit_of_uniform_derivative_bounds line 201
  18. lemma OAI.ZeroTemperatureSK.Heat.iteratedDeriv_limit_bound line 225