OAI/Probability/ParisiFinite/ParisiHankelDerivative.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

Parisi Hankel Derivative.

  1. lemma OAI.ParisiSpectral.posSemidef_anchor line 21
  2. def OAI.ParisiSpectral.HankelCPD line 32
  3. def OAI.ParisiSpectral.HankelPD line 35
  4. lemma OAI.ParisiSpectral.HankelPD.cpd line 38
  5. lemma OAI.ParisiSpectral.scaled_taylorOn_tendsto line 43
  6. lemma OAI.ParisiSpectral.secondForward_tendsto line 61
  7. lemma OAI.ParisiSpectral.HankelCPD.secondDeriv line 84
  8. lemma OAI.ParisiSpectral.HankelCPD.add line 130
  9. lemma OAI.ParisiSpectral.HankelCPD.of_rightQuotient line 147
  10. lemma OAI.ParisiSpectral.HankelPD.midpoint_le line 178
  11. lemma OAI.ParisiSpectral.HankelPD.midpoint_lt line 186
  12. lemma OAI.ParisiSpectral.posSemidef_weight line 211
  13. lemma OAI.ParisiSpectral.hankelPD_heat_observation line 225
  14. def OAI.ParisiSpectral.backwardC line 252
  15. def OAI.ParisiSpectral.backwardG line 253
  16. lemma OAI.ParisiSpectral.backwardG_reflection line 255
  17. lemma OAI.ParisiSpectral.backwardC_neg_rpow line 269
  18. lemma OAI.ParisiSpectral.exp_abs_shift_le line 295
  19. lemma OAI.ParisiSpectral.exp_abs_shift_near_le line 302
  20. lemma OAI.ParisiSpectral.integrable_scale_prod line 308
  21. lemma OAI.ParisiSpectral.integrable_coord_scale_prod line 318
  22. lemma OAI.ParisiSpectral.hasDerivAt_scale_prod line 332
  23. lemma OAI.ParisiSpectral.integrable_scale_gaussian line 357
  24. lemma OAI.ParisiSpectral.integrable_coord_scale_gaussian line 365
  25. lemma OAI.ParisiSpectral.scale_gaussian_ibp line 377
  26. lemma OAI.ParisiSpectral.hasDerivAt_scale_prod_second line 389
  27. def OAI.ParisiSpectral.heatObservation line 408
  28. lemma OAI.ParisiSpectral.hasDerivAt_heatObservation line 411
  29. lemma OAI.ParisiSpectral.continuous_scale_prod line 427
  30. lemma OAI.ParisiSpectral.continuous_heatObservation line 442
  31. lemma OAI.ParisiSpectral.exp_neg_mul_le line 458
  32. lemma OAI.ParisiSpectral.exp_neg_quotient_bound line 465
  33. lemma OAI.ParisiSpectral.integral_exp_rightDerivative line 478
  34. def OAI.ParisiSpectral.heatLaw line 521
  35. instance OAI.ParisiSpectral.(instance at line 522) line 522
  36. lemma OAI.ParisiSpectral.integral_heatLaw line 526
  37. lemma OAI.ParisiSpectral.heatLaw_firstMoment line 530
  38. lemma OAI.ParisiSpectral.abs_log_cosh_le line 539
  39. lemma OAI.ParisiSpectral.backwardC_pos line 548
  40. lemma OAI.ParisiSpectral.backwardC_log line 552
  41. lemma OAI.ParisiSpectral.backwardC_log_integrable line 557
  42. lemma OAI.ParisiSpectral.hankelPD_heatLaw line 568
  43. lemma OAI.ParisiSpectral.backwardG_observation_constant line 584
  44. lemma OAI.ParisiSpectral.backwardG_bound line 599
  45. lemma OAI.ParisiSpectral.hankelCPD_linearEntropy line 602
  46. lemma OAI.ParisiSpectral.hankelPD_entropyRemainder line 641