OAI/Probability/ParisiFinite/VarianceProdDecomposition.lean

GitHub source file

48 declarations, 0 contain sorry, 0 declared as axioms

Variance Prod Decomposition.

  1. lemma OAI.GaussianConcentration.variance_prod_decomposition line 61
  2. def OAI.GaussianConcentration.firstMean line 78
  3. lemma OAI.GaussianConcentration.CoordinateLipschitz.first_slice line 81
  4. lemma OAI.GaussianConcentration.CoordinateLipschitz.firstMean line 88
  5. theorem OAI.GaussianConcentration.CoordinateLipschitz.variance_le line 106
  6. lemma OAI.GaussianConcentration.logPartition_lipschitz line 158
  7. lemma OAI.GaussianConcentration.logPartition_coordinate line 163
  8. lemma OAI.GaussianConcentration.variance_reindex_field line 181
  9. lemma OAI.GaussianConcentration.variance_field_logPartition_le line 202
  10. theorem OAI.GaussianConcentration.sk_logPartition_variance_le line 213
  11. lemma OAI.GaussianConcentration.sk_pressureDensity_variance_le line 232
  12. theorem OAI.GaussianConcentration.tendsto_sk_pressureDensity_variance line 245
  13. def OAI.SKCavity.replicaMean line 263
  14. lemma OAI.SKCavity.replicaMean_single line 266
  15. lemma OAI.SKCavity.replicaMean_sum line 283
  16. lemma OAI.SKCavity.replicaMean_sum_same line 291
  17. lemma OAI.SKCavity.replicaWeight_snoc line 297
  18. lemma OAI.SKCavity.sum_tuples_snoc line 302
  19. lemma OAI.SKCavity.replicaMean_snoc line 308
  20. lemma OAI.SKCavity.replicaMean_marginal line 314
  21. lemma OAI.SKCavity.integrable_replicaMean line 319
  22. lemma OAI.SKCavity.integrable_replica_energy line 325
  23. lemma OAI.SKCavity.integrable_replicaWeight_derivative line 348
  24. def OAI.SKCavity.crossKernel line 358
  25. lemma OAI.SKCavity.replica_covariance_algebra line 361
  26. lemma OAI.SKCavity.integral_replica_linear line 381
  27. lemma OAI.SKCavity.replica_covariance_snoc line 404
  28. theorem OAI.SKCavity.integral_replica_energy_covariance line 418
  29. def OAI.SKCavity.crossCov line 475
  30. lemma OAI.SKCavity.crossCov_reindex line 478
  31. lemma OAI.SKCavity.integral_reindex_pair line 486
  32. lemma OAI.SKCavity.integrable_field_replicaWeight line 504
  33. lemma OAI.SKCavity.integrable_field_replicaMean line 511
  34. lemma OAI.SKCavity.integrable_field_replica_energy line 515
  35. theorem OAI.SKCavity.integral_field_replica_energy_covariance line 528
  36. def OAI.SKCavity.pSpinCoeff line 554
  37. lemma OAI.SKCavity.pSpinCoeff_abs line 557
  38. lemma OAI.SKCavity.pSpinCoeff_kernel line 563
  39. lemma OAI.SKCavity.pSpinCoeff_diag line 584
  40. def OAI.SKCavity.perturbedCoeff line 589
  41. lemma OAI.SKCavity.perturbedCoeff_kernel line 593
  42. lemma OAI.SKCavity.variance_logPartition_le_diagonal line 606
  43. lemma OAI.SKCavity.perturbedCoeff_abs line 615
  44. lemma OAI.SKCavity.perturbed_logPartition_variance_le line 624
  45. lemma OAI.ParisiInterpolation.replicaAverage_abs_le line 645
  46. lemma OAI.ParisiInterpolation.replicaMean_abs_le line 659
  47. lemma OAI.ParisiInterpolation.expected_difference_le_orthogonal line 668
  48. lemma OAI.ParisiInterpolation.expected_difference_le line 698