OAI/Probability/SKFluctuations/ScalarWeightedJet.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

Scalar Weighted Jet.

  1. def OAI.SKFluctuations.Hierarchy.scalarWeightedJet line 21
  2. theorem OAI.SKFluctuations.Hierarchy.scalarWeightedJet_F line 51
  3. theorem OAI.SKFluctuations.Hierarchy.scalarWeightedJet_mass_one line 55
  4. theorem OAI.SKFluctuations.Hierarchy.scalarWeightedSquare_derivative_zero line 63
  5. theorem OAI.SKFluctuations.Hierarchy.scalarWeightedSquare_initial line 77
  6. theorem OAI.SKFluctuations.Hierarchy.integral_hasDerivWithinAt_zero line 89
  7. def OAI.SKFluctuations.Hierarchy.scalarInsertedOverlap line 132
  8. theorem OAI.SKFluctuations.Hierarchy.scalarInsertedOverlap_zero line 135
  9. theorem OAI.SKFluctuations.Hierarchy.scalarInsertedOverlap_derivative_zero line 140
  10. theorem OAI.SKFluctuations.Hierarchy.scalarInsertedSlope_continuous line 167
  11. theorem OAI.SKFluctuations.Hierarchy.scalarInsertedSlope_supercritical line 191
  12. theorem OAI.SKFluctuations.Hierarchy.integral_fin_one line 217
  13. theorem OAI.SKFluctuations.Hierarchy.scalar_clockDerivative line 229
  14. def OAI.SKFluctuations.Hierarchy.scalarInsertedPotential line 248
  15. theorem OAI.SKFluctuations.Hierarchy.scalarInsertedPotential_continuous line 252
  16. theorem OAI.SKFluctuations.Hierarchy.scalarInsertedPotential_derivative line 262
  17. def OAI.SKFluctuations.Hierarchy.scalarRSBIncrement line 280
  18. theorem OAI.SKFluctuations.Hierarchy.scalarRSBIncrement_zero line 284
  19. theorem OAI.SKFluctuations.Hierarchy.scalarRSBIncrement_continuous line 287
  20. theorem OAI.SKFluctuations.Hierarchy.scalarRSBIncrement_derivative line 293
  21. theorem OAI.SKFluctuations.Hierarchy.scalarRSB_descent line 312
  22. theorem OAI.SKFluctuations.Hierarchy.scalarInsertedPotential_zero line 360
  23. theorem OAI.SKFluctuations.Hierarchy.scalarTwoClockPressure_collapse line 376
  24. theorem OAI.SKFluctuations.Scalar.gaussian_integral_rescale line 405
  25. theorem OAI.SKFluctuations.Scalar.rsHeatSlope_gaussian line 416
  26. theorem OAI.SKFluctuations.Scalar.rsVariationSlope_gaussian line 427
  27. theorem OAI.SKFluctuations.Scalar.rs_minimizer_fixed_point line 433
  28. theorem OAI.SKFluctuations.Scalar.curvature_pos line 443
  29. theorem OAI.SKFluctuations.Scalar.rsVariationSlope_one_pos line 447
  30. theorem OAI.SKFluctuations.Scalar.rs_one_not_minimizer line 464
  31. theorem OAI.SKFluctuations.Hierarchy.scalarParisiDiracMinimizer_replicon line 489
  32. theorem OAI.SKFluctuations.Hierarchy.scalarParisiValue_twoAtom_increment line 522
  33. theorem OAI.SKFluctuations.Hierarchy.scalarParisi_no_dirac_minimizer line 543
  34. theorem OAI.SKFluctuations.GaussianCalculus.LipschitzWith.hasDerivAt_curve line 569
  35. theorem OAI.SKFluctuations.GaussianCalculus.exp_scaledSource_bound line 596
  36. theorem OAI.SKFluctuations.GaussianCalculus.integrable_exp_scaledSource line 613
  37. theorem OAI.SKFluctuations.GaussianCalculus.hasDerivAt_integral_exp_scaledSource line 624