OAI/Probability/SKSupport/Density/FiniteForwardRatio.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ZeroTemperatureSK.Heat.backwardSegment line 14
  2. lemma OAI.ZeroTemperatureSK.Heat.backwardSegment_initial line 17
  3. lemma OAI.ZeroTemperatureSK.Heat.backwardSegment_terminal line 31
  4. lemma OAI.ZeroTemperatureSK.Heat.backwardSegment_reverse line 39
  5. lemma OAI.ZeroTemperatureSK.Heat.backwardSegment_shape line 44
  6. def OAI.ZeroTemperatureSK.Heat.boundaryRatio line 52
  7. lemma OAI.ZeroTemperatureSK.Heat.forwardSegment_ratio line 56
  8. theorem OAI.ZeroTemperatureSK.Heat.boundaryRatio_nonneg line 89
  9. theorem OAI.ZeroTemperatureSK.Heat.finite_forward_ratio line 124
  10. def OAI.ZeroTemperatureSK.Heat.certR line 143
  11. def OAI.ZeroTemperatureSK.Heat.certK line 144
  12. def OAI.ZeroTemperatureSK.Heat.certV line 145
  13. def OAI.ZeroTemperatureSK.Heat.certW line 146
  14. def OAI.ZeroTemperatureSK.Heat.certZ line 147
  15. def OAI.ZeroTemperatureSK.Heat.certB line 148
  16. def OAI.ZeroTemperatureSK.Heat.certJ line 149
  17. def OAI.ZeroTemperatureSK.Heat.certL line 150
  18. def OAI.ZeroTemperatureSK.Heat.certFlux line 152
  19. def OAI.ZeroTemperatureSK.Heat.certDivergence line 155
  20. lemma OAI.ZeroTemperatureSK.Heat.cert_flux_derivative line 159
  21. lemma OAI.ZeroTemperatureSK.Heat.cert_halfLine_signs line 181
  22. lemma OAI.ZeroTemperatureSK.Heat.cert_halfLine_coercive line 216