OAI/Analysis/Steinitz/PathLaws.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

Gaussian heat kernels and autoregressive path laws.

  1. lemma OAI.GaussianKernel.scaleMap_selfAdjoint line 14
  2. def OAI.GaussianKernel.symbol line 24
  3. lemma OAI.GaussianKernel.symbol_eq line 27
  4. lemma OAI.GaussianKernel.symbol_continuous line 40
  5. lemma OAI.GaussianKernel.symbol_nonneg line 45
  6. lemma OAI.GaussianKernel.average_diagonal_eq line 49
  7. lemma OAI.GaussianKernel.average_diagonal_heat line 59
  8. def OAI.GaussianKernel.kernel line 66
  9. lemma OAI.GaussianKernel.kernel_symmetric line 70
  10. lemma OAI.GaussianKernel.kernel_norm_eq line 75
  11. lemma OAI.GaussianKernel.gaussianPDF_logconcave line 91
  12. lemma OAI.GaussianKernel.density_logconcave line 117
  13. lemma OAI.HeatL2.integral_pi_fin_cons line 141
  14. def OAI.HeatL2.tailWeight line 164
  15. lemma OAI.HeatL2.tailWeight_measurable line 168
  16. lemma OAI.HeatL2.tailWeight_nonneg line 176
  17. lemma OAI.HeatL2.tailWeight_le line 181
  18. lemma OAI.HeatL2.tailWeight_integrable line 188
  19. def OAI.HeatL2.walk line 197
  20. lemma OAI.HeatL2.walk_zero line 200
  21. lemma OAI.HeatL2.walk_succ line 203
  22. lemma OAI.HeatL2.walk_measurable line 212
  23. lemma OAI.HeatL2.walk_nonneg line 215
  24. lemma OAI.HeatL2.walk_le line 218
  25. lemma OAI.HeatL2.kernel_pow_one_coe line 225
  26. def OAI.HeatL2.chainWeight line 240
  27. lemma OAI.HeatL2.chainWeight_measurable line 243
  28. lemma OAI.HeatL2.chainWeight_integrable line 250
  29. lemma OAI.HeatL2.pathMass_pi line 258
  30. lemma OAI.HeatL2.tailWeight_continuous line 276
  31. lemma OAI.HeatL2.chainWeight_continuous line 287
  32. lemma OAI.HeatL2.tailWeight_pos line 294
  33. lemma OAI.HeatL2.tailWeight_logconcave line 305
  34. lemma OAI.HeatL2.chainWeight_logconcave line 322
  35. lemma OAI.HeatL2.chainWeight_prod line 336
  36. lemma OAI.HeatL2.fin_sum_differences line 345
  37. lemma OAI.GaussianAR.measurePreserving_curry line 361
  38. def OAI.GaussianAR.unpack line 373
  39. lemma OAI.GaussianAR.unpack_apply line 378
  40. lemma OAI.GaussianAR.unpack_preserving line 381
  41. def OAI.GaussianAR.transition line 407
  42. lemma OAI.GaussianAR.transition_nonneg line 411
  43. lemma OAI.GaussianAR.transition_le line 417
  44. lemma OAI.GaussianAR.path_density_eq line 433
  45. lemma OAI.GaussianAR.path_density_le line 450
  46. lemma OAI.GaussianAR.survival_le_pathMass line 491
  47. lemma OAI.GaussianAR.kernel_norm_of_survival line 537