OAI/Probability/SKSupport/Regularity/BoundedSmoothFamily.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.ZeroTemperatureSK.Heat.BoundedSmoothFamily line 18
  2. lemma OAI.ZeroTemperatureSK.Heat.BoundedSmoothFamily.bound line 23
  3. lemma OAI.ZeroTemperatureSK.Heat.BoundedSmoothFamily.deriv line 26
  4. lemma OAI.ZeroTemperatureSK.Heat.BoundedSmoothFamily.mul line 33
  5. lemma OAI.ZeroTemperatureSK.Heat.BoundedSmoothFamily.timeConst line 54
  6. lemma OAI.ZeroTemperatureSK.Heat.BoundedSmoothFamily.iteratedDeriv line 63
  7. lemma OAI.ZeroTemperatureSK.Heat.finiteGradient_family line 70
  8. lemma OAI.ZeroTemperatureSK.Heat.finiteCoeff_family line 79
  9. lemma OAI.ZeroTemperatureSK.Heat.finiteSource_family line 85
  10. def OAI.ZeroTemperatureSK.Heat.finiteBurgersSource line 92
  11. lemma OAI.ZeroTemperatureSK.Heat.finiteBurgersSource_family line 95
  12. lemma OAI.ZeroTemperatureSK.Heat.deriv_finiteSource line 101
  13. lemma OAI.ZeroTemperatureSK.Heat.finiteGradient_mild line 114