OAI/Probability/SKSupport/Density/Certificate.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ZeroTemperatureSK.Certificate.A line 10
  2. abbrev OAI.ZeroTemperatureSK.Certificate.C line 11
  3. abbrev OAI.ZeroTemperatureSK.Certificate.k line 12
  4. abbrev OAI.ZeroTemperatureSK.Certificate.T₀ line 13
  5. abbrev OAI.ZeroTemperatureSK.Certificate.g₀ line 14
  6. abbrev OAI.ZeroTemperatureSK.Certificate.h line 15
  7. abbrev OAI.ZeroTemperatureSK.Certificate.x₀ line 16
  8. abbrev OAI.ZeroTemperatureSK.Certificate.y line 17
  9. abbrev OAI.ZeroTemperatureSK.Certificate.m line 18
  10. abbrev OAI.ZeroTemperatureSK.Certificate.n₀ line 19
  11. def OAI.ZeroTemperatureSK.Certificate.Q line 21
  12. def OAI.ZeroTemperatureSK.Certificate.T line 22
  13. def OAI.ZeroTemperatureSK.Certificate.F₁ line 23
  14. def OAI.ZeroTemperatureSK.Certificate.F₂ line 25
  15. def OAI.ZeroTemperatureSK.Certificate.P₀ line 27
  16. def OAI.ZeroTemperatureSK.Certificate.P₁ line 28
  17. def OAI.ZeroTemperatureSK.Certificate.P₂ line 29
  18. def OAI.ZeroTemperatureSK.Certificate.P₃ line 30
  19. def OAI.ZeroTemperatureSK.Certificate.P₄ line 31
  20. def OAI.ZeroTemperatureSK.Certificate.weightedSquares line 33
  21. def OAI.ZeroTemperatureSK.Certificate.remainder line 37
  22. def OAI.ZeroTemperatureSK.Certificate.F₂R line 47
  23. def OAI.ZeroTemperatureSK.Certificate.F₂K line 48
  24. def OAI.ZeroTemperatureSK.Certificate.F₂v line 49
  25. def OAI.ZeroTemperatureSK.Certificate.F₂b line 52
  26. def OAI.ZeroTemperatureSK.Certificate.F₂j line 53
  27. def OAI.ZeroTemperatureSK.Certificate.DF₂ line 55
  28. def OAI.ZeroTemperatureSK.Certificate.WF₂ line 60
  29. theorem OAI.ZeroTemperatureSK.Certificate.rational_identity line 62
  30. theorem OAI.ZeroTemperatureSK.Certificate.hasDerivAt_F₂ line 71
  31. theorem OAI.ZeroTemperatureSK.Certificate.remainder_lower_bound line 92
  32. theorem OAI.ZeroTemperatureSK.Certificate.pointwise_coercivity line 107
  33. theorem OAI.ZeroTemperatureSK.Certificate.coercivity_constant line 124
  34. theorem OAI.ZeroTemperatureSK.Certificate.hasDerivAt_flux line 127
  35. theorem OAI.ZeroTemperatureSK.Certificate.integrated_coercivity_of_flux line 165
  36. theorem OAI.ZeroTemperatureSK.Certificate.coercivity_constant_integral line 196