OAI/Probability/SKFluctuations/ReplicaMixedInsertion.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

Replica Mixed Insertion.

  1. def OAI.SKFluctuations.Hierarchy.ClockPolynomial.lowJet line 24
  2. theorem OAI.SKFluctuations.Hierarchy.ClockPolynomial.iteratedDeriv_lowJet line 29
  3. theorem OAI.SKFluctuations.Hierarchy.ClockPolynomial.rootEval_continuous line 53
  4. theorem OAI.SKFluctuations.Hierarchy.ClockPolynomial.mixed_lowJet_hasDerivAt line 65
  5. def OAI.SKFluctuations.Hierarchy.ClockExpr.cumulativeEval line 114
  6. def OAI.SKFluctuations.Hierarchy.ClockExpr.cumulativeCov line 119
  7. def OAI.SKFluctuations.Hierarchy.ClockExpr.iterCumulativeCov line 123
  8. theorem OAI.SKFluctuations.Hierarchy.ClockExpr.cumulativeEval_affine line 128
  9. theorem OAI.SKFluctuations.Hierarchy.ClockTree.iteratedDeriv_disorderExpect line 141
  10. theorem OAI.SKFluctuations.Hierarchy.ClockTree.disorderExpect_reindex line 178
  11. def OAI.SKFluctuations.Hierarchy.ClockExpr.finiteCumulativeCov line 188
  12. def OAI.SKFluctuations.Hierarchy.ClockExpr.finiteCumulativeEval line 193
  13. theorem OAI.SKFluctuations.Hierarchy.ClockTree.iteratedDeriv_finiteDisorderExpect line 202
  14. def OAI.SKFluctuations.Hierarchy.ClockPolynomial.finiteEval line 236
  15. def OAI.SKFluctuations.Hierarchy.ClockPolynomial.finiteLowJet line 245
  16. def OAI.SKFluctuations.Hierarchy.ClockPolynomial.finiteMixedJet line 254
  17. theorem OAI.SKFluctuations.Hierarchy.ClockTree.mixed_finiteDisorderExpect line 266
  18. def OAI.SKFluctuations.Hierarchy.ClockPolynomial.finiteInsert line 328
  19. theorem OAI.SKFluctuations.Hierarchy.ClockPolynomial.finiteEval_continuous line 336
  20. theorem OAI.SKFluctuations.Hierarchy.ClockPolynomial.finiteEval_affine line 353
  21. theorem OAI.SKFluctuations.Hierarchy.ClockPolynomial.hasDerivAt_finite_frozen line 367
  22. theorem OAI.SKFluctuations.Hierarchy.ClockPolynomial.hasDerivAt_finite_diagonal line 383
  23. theorem OAI.SKFluctuations.Hierarchy.ClockPolynomial.finiteLowJet_succ_eval line 400
  24. theorem OAI.SKFluctuations.Hierarchy.ClockPolynomial.finiteLowJet_hasDerivAt_low line 413
  25. theorem OAI.SKFluctuations.Hierarchy.ClockPolynomial.finiteLowJet_hasDerivAt_high line 428
  26. def OAI.SKFluctuations.Cavity.cutFullVariance line 469
  27. def OAI.SKFluctuations.Cavity.rowInterpolationSlope line 474
  28. def OAI.SKFluctuations.Cavity.cutTBase line 478
  29. def OAI.SKFluctuations.Cavity.cutTSlope line 481
  30. theorem OAI.SKFluctuations.Cavity.cutFullVariance_t_affine line 485
  31. theorem OAI.SKFluctuations.Cavity.cutFullVariance_nonneg line 494
  32. theorem OAI.SKFluctuations.Cavity.cutFullVariance_monotone line 503
  33. theorem OAI.SKFluctuations.Cavity.cutT_affine_monotone line 512
  34. theorem OAI.SKFluctuations.Cavity.hasDerivAt_cutDisorderExpect_t line 525
  35. def OAI.SKFluctuations.Cavity.cutLBase line 549
  36. def OAI.SKFluctuations.Cavity.cutLSlope line 552
  37. theorem OAI.SKFluctuations.Cavity.cutFullVariance_l_affine line 555
  38. theorem OAI.SKFluctuations.Cavity.cutL_affine_monotone line 564
  39. theorem OAI.SKFluctuations.Cavity.hasDerivAt_cutDisorderExpect_l line 577
  40. theorem OAI.SKFluctuations.Cavity.iteratedDeriv_cutDisorderExpect_l line 609
  41. theorem OAI.SKFluctuations.Cavity.iteratedDeriv_cutDisorderExpect_t line 632