OAI/Probability/SKSupport/Backward/GaussianBackwardShapes.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ZeroTemperatureSK.Heat.gaussianBurgers_shape line 16
  2. theorem OAI.ZeroTemperatureSK.Heat.logSemigroup_backward_shape line 36
  3. lemma OAI.ZeroTemperatureSK.Heat.softAbs_backward_shape line 49
  4. theorem OAI.ZeroTemperatureSK.Heat.cascade_backward_shape line 76
  5. theorem OAI.ZeroTemperatureSK.Heat.finiteHead_backward_shape line 103
  6. lemma OAI.ZeroTemperatureSK.Heat.RegularDatum.exists_lipschitz line 142
  7. lemma OAI.ZeroTemperatureSK.Heat.RegularDatum.sub_mul line 148
  8. def OAI.ZeroTemperatureSK.Heat.backwardBoundary line 159
  9. def OAI.ZeroTemperatureSK.Heat.forwardBoundary line 162
  10. lemma OAI.ZeroTemperatureSK.Heat.forwardBoundary_regular line 169
  11. lemma OAI.ZeroTemperatureSK.Heat.backwardBoundary_shape line 185
  12. lemma OAI.ZeroTemperatureSK.Heat.backwardBoundary_third_nonpos line 191
  13. lemma OAI.ZeroTemperatureSK.Heat.forwardBoundary_shape line 202