OAI/Probability/ParisiFinite/ParisiReflection.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Parisi Reflection.

  1. lemma OAI.ParisiSpectral.posSemidef_kernel_variable_average line 21
  2. lemma OAI.ParisiSpectral.gaussian_double_difference_general line 33
  3. lemma OAI.ParisiSpectral.PositiveDefinite.heat_reflection line 53
  4. lemma OAI.ParisiSpectral.PositiveDefinite.heat_abs_le line 82
  5. lemma OAI.ParisiSpectral.hasSum_entropy_remainder line 98
  6. lemma OAI.ParisiSpectral.posSemidef_hadamard_pow line 115
  7. lemma OAI.ParisiSpectral.posSemidef_entropy_remainder line 127
  8. lemma OAI.ParisiSpectral.posSemidef_kernel_finite_combination line 187
  9. lemma OAI.ParisiSpectral.scaled_taylor_tendsto line 201
  10. def OAI.ParisiSpectral.jetWeight line 220
  11. def OAI.ParisiSpectral.differenceJet line 231
  12. lemma OAI.ParisiSpectral.differenceJet_tendsto line 235
  13. lemma OAI.ParisiSpectral.posSemidef_spatial_jets line 261
  14. def OAI.ParisiSpectral.PositiveOnPD line 306
  15. lemma OAI.ParisiSpectral.stationary_kernel_finsupp line 309
  16. lemma OAI.ParisiSpectral.PositiveOnPD.kernel_integral line 328
  17. lemma OAI.ParisiSpectral.continuous_kernelFeature_comp line 354
  18. lemma OAI.ParisiSpectral.stationary_kernel_bounded line 374
  19. lemma OAI.ParisiSpectral.stationary_kernel_heat line 387
  20. def OAI.ParisiFinite.BoundedCoefficient.conjugateMeasure line 431
  21. lemma OAI.ParisiFinite.BoundedCoefficient.integral_conjugateMeasure line 436
  22. lemma OAI.ParisiFinite.BoundedCoefficient.conjugateMeasure_finite line 450
  23. lemma OAI.ParisiFinite.BoundedCoefficient.conjugateMeasure_positive line 461
  24. lemma OAI.ParisiFinite.BoundedCoefficient.conjugateMeasure_firstMoment line 469
  25. lemma OAI.ParisiSpectral.continuous_heat line 495
  26. lemma OAI.ParisiSpectral.heat_heat line 502
  27. lemma OAI.ParisiSpectral.PositiveDefinite.sub_heat line 513
  28. lemma OAI.ParisiSpectral.PositiveOnPD.heat_le line 566
  29. lemma OAI.ParisiFinite.BoundedCoefficient.conjugateMeasure_plateau_integral line 588
  30. lemma OAI.ParisiFinite.BoundedCoefficient.conjugateMeasure_plateau line 634