OAI/Probability/SKFluctuations/MarkedPairExpectation.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

Marked Pair Expectation.

  1. def OAI.SKFluctuations.Hierarchy.ReplicaTree.markedPairExpectation line 23
  2. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.powerJet_cons_marked line 31
  3. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.powerJet_two_marked line 39
  4. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.list_sum_finset_sum line 48
  5. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.markedPairExpectation_finsetSum line 54
  6. def OAI.SKFluctuations.Hierarchy.ReplicaTree.blockKernel line 63
  7. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.powerTrace_eq_markedPair line 67
  8. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.powerTrace_zero_one line 77
  9. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.hasDerivWithinAt_root_covariance line 85
  10. def OAI.SKFluctuations.Hierarchy.ReplicaTree.markedOffDiagonal line 113
  11. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.markedPlacement_diagonal_test line 121
  12. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.markedPair_eq_offDiagonal line 146
  13. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.markedPair_zero_eq_offDiagonal line 179
  14. theorem OAI.SKFluctuations.Hierarchy.HeatJet.nonnegativeProfileValue_constant line 192
  15. theorem OAI.SKFluctuations.Hierarchy.scalarParisiValue_dirac_zero line 214
  16. theorem OAI.SKFluctuations.Hierarchy.scalarParisiMinimizer_not_dirac_zero line 235
  17. theorem OAI.SKFluctuations.Hierarchy.HeatJet.grid_dyadic_cut line 266
  18. theorem OAI.SKFluctuations.Hierarchy.HeatJet.profileValue_dyadic_cut line 366
  19. theorem OAI.SKFluctuations.Hierarchy.HeatJet.nonnegativeProfileValue_dyadic_cut line 391
  20. def OAI.SKFluctuations.Hierarchy.scalarDyadicBelow line 444
  21. theorem OAI.SKFluctuations.Hierarchy.scalarDyadicBelow_nonneg line 447
  22. theorem OAI.SKFluctuations.Hierarchy.scalarDyadicBelow_le line 451
  23. theorem OAI.SKFluctuations.Hierarchy.scalarDyadicBelow_numerator line 456
  24. theorem OAI.SKFluctuations.Hierarchy.scalarDyadicBelow_tendsto line 460
  25. theorem OAI.SKFluctuations.Hierarchy.diracMassProfile_tendsto_below line 466
  26. theorem OAI.SKFluctuations.Hierarchy.scalarParisiValue_dirac_tendsto line 483
  27. theorem OAI.SKFluctuations.Hierarchy.scalarRSValue_tendsto line 490
  28. theorem OAI.SKFluctuations.Hierarchy.scalarParisiValue_dirac_dyadic_cut line 505
  29. theorem OAI.SKFluctuations.Hierarchy.scalarParisiValue_dirac line 538
  30. def OAI.SKFluctuations.Hierarchy.twoAtomMassProfile line 553
  31. theorem OAI.SKFluctuations.Hierarchy.twoAtomMassProfile_mem line 567
  32. theorem OAI.SKFluctuations.Hierarchy.twoAtomMassProfile_apply line 579
  33. theorem OAI.SKFluctuations.Hierarchy.scalarPenalty_twoAtom line 585
  34. theorem OAI.SKFluctuations.Hierarchy.twoAtomMassProfile_tendsto_below line 602
  35. def OAI.SKFluctuations.Hierarchy.HeatJet.rootBoundarySchedule line 620
  36. theorem OAI.SKFluctuations.Hierarchy.HeatJet.rootCumulativeClock_uniform line 627