OAI/Probability/ParisiFinite/AbsMulExpLe.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

Abs Mul Exp Le.

  1. lemma OAI.ParisiFinite.abs_mul_exp_le line 56
  2. lemma OAI.ParisiFinite.exp_scale_near_le line 63
  3. lemma OAI.ParisiFinite.coord_exp_scale_near_le line 81
  4. lemma OAI.ParisiFinite.integrable_coord_exp_weight line 91
  5. lemma OAI.ParisiFinite.hasDerivAt_scale_expMass line 103
  6. lemma OAI.ParisiFinite.hasDerivAt_scale_average line 131
  7. lemma OAI.ParisiFinite.gaussian_tilt_ibp line 150
  8. lemma OAI.ParisiFinite.hasDerivAt_step_scale line 193
  9. lemma OAI.ParisiFinite.hasDerivAt_transform_scale line 219
  10. def OAI.ParisiFinite.fieldOnInterval line 227
  11. lemma OAI.ParisiFinite.hasDerivAt_fieldOnInterval_time line 232
  12. lemma OAI.ParisiFinite.fieldOnInterval_right line 242
  13. lemma OAI.ParisiFinite.fieldOnInterval_spatial1 line 248
  14. lemma OAI.ParisiFinite.fieldOnInterval_spatial2 line 252
  15. lemma OAI.ParisiFinite.fieldOnInterval_terminal line 257
  16. def OAI.ParisiFinite.ambientStep line 275
  17. def OAI.ParisiFinite.ambientMass line 278
  18. def OAI.ParisiFinite.ambientMoment line 281
  19. def OAI.ParisiFinite.ambientTilt line 284
  20. lemma OAI.ParisiFinite.line_lipschitz line 287
  21. lemma OAI.ParisiFinite.integrable_ambient line 295
  22. lemma OAI.ParisiFinite.integrable_exp_ambient line 299
  23. lemma OAI.ParisiFinite.ambientMass_pos line 303
  24. lemma OAI.ParisiFinite.integrable_ambient_weight line 306
  25. lemma OAI.ParisiFinite.ambientStep_lipschitz line 312
  26. lemma OAI.ParisiFinite.ambient_exp_near_le line 323
  27. lemma OAI.ParisiFinite.continuous_ambientMoment line 344
  28. lemma OAI.ParisiFinite.continuous_ambientTilt line 362
  29. lemma OAI.ParisiFinite.ambientTilt_zero line 373
  30. lemma OAI.ParisiFinite.abs_ambientTilt_le line 377
  31. lemma OAI.ParisiFinite.ambient_exp_near_le_radius line 402
  32. lemma OAI.ParisiFinite.hasDerivAt_ambientMoment line 425
  33. lemma OAI.ParisiFinite.hasDerivAt_ambientMass line 468
  34. lemma OAI.ParisiFinite.hasDerivAt_ambientMean line 483
  35. lemma OAI.ParisiFinite.hasDerivAt_ambientStep line 499
  36. lemma OAI.ParisiFinite.ambientMoment_add line 534
  37. lemma OAI.ParisiFinite.ambientMoment_const_mul line 542
  38. lemma OAI.ParisiFinite.ambientTilt_add line 546
  39. lemma OAI.ParisiFinite.ambientTilt_const_mul line 553
  40. lemma OAI.ParisiFinite.ambientTilt_mono line 557
  41. lemma OAI.ParisiFinite.ambientTilt_const line 568
  42. lemma OAI.ParisiFinite.hasDerivAt_ambientTilt line 575
  43. structure OAI.ParisiFinite.DirectionalField line 611
  44. def OAI.ParisiFinite.DirectionalField.transform line 631
  45. def OAI.ParisiFinite.DirectionalField.slice line 677
  46. lemma OAI.ParisiFinite.DirectionalField.hasDerivAt_transform_scale line 690