OAI/Probability/SKFluctuations/PhysicalProjection.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

Physical Projection.

  1. theorem OAI.SKFluctuations.physicalPair_rooted_law line 21
  2. theorem OAI.SKFluctuations.integral_physicalPair_eq_segments line 44
  3. theorem OAI.SKFluctuations.eventually_physical_random_projection line 67
  4. theorem OAI.SKFluctuations.physicalPathLaw_finite line 107
  5. theorem OAI.SKFluctuations.physicalPairIncrement_moment_integrable line 116
  6. theorem OAI.SKFluctuations.norm_physicalPairIncrement line 129
  7. def OAI.SKFluctuations.physicalForkPathLaw line 141
  8. theorem OAI.SKFluctuations.eventually_physical_fork_projection line 149
  9. theorem OAI.SKFluctuations.Hierarchy.ReplicaTree.expect_atSlot line 185
  10. def OAI.SKFluctuations.Hierarchy.scalarCavityRow line 220
  11. theorem OAI.SKFluctuations.Hierarchy.scalarSourceJet_one_mean line 226
  12. theorem OAI.SKFluctuations.Hierarchy.scalarCavityRow_eq line 235
  13. theorem OAI.SKFluctuations.Hierarchy.scalarCavityRow_zero line 258
  14. theorem OAI.SKFluctuations.Hierarchy.scalarCavityRow_zero_bounds line 267
  15. def OAI.SKFluctuations.Hierarchy.ClockTree.weightVariation line 293
  16. theorem OAI.SKFluctuations.Hierarchy.ClockTree.hasDerivAt_weight_fullPath line 307
  17. theorem OAI.SKFluctuations.Hierarchy.ClockTree.hasDerivAt_expect_fullPath line 321
  18. theorem OAI.SKFluctuations.Hierarchy.continuous_monotoneProfileIntegral line 340
  19. theorem OAI.SKFluctuations.Hierarchy.continuous_monotoneProfileIntegral_between line 372
  20. def OAI.SKFluctuations.Hierarchy.inverseIntegralConstraints line 381
  21. theorem OAI.SKFluctuations.Hierarchy.inverseIntegralConstraints_closed line 386
  22. theorem OAI.SKFluctuations.Hierarchy.inverseIntegralConstraints_compact line 401
  23. theorem OAI.SKFluctuations.Hierarchy.inverseIntegralConstraints_lipschitz line 407
  24. theorem OAI.SKFluctuations.Hierarchy.lipschitz_ae_deriv_lower_iff line 442
  25. theorem OAI.SKFluctuations.Hierarchy.lipschitz_ae_deriv_upper_iff line 489
  26. def OAI.SKFluctuations.Hierarchy.inverseDifferentialConstraints line 522
  27. theorem OAI.SKFluctuations.Hierarchy.inverseDifferentialConstraints_eq line 527
  28. theorem OAI.SKFluctuations.Hierarchy.inverseDifferentialConstraints_compact line 550
  29. def OAI.SKFluctuations.Hierarchy.comparisonFloor line 559
  30. def OAI.SKFluctuations.Hierarchy.comparisonCap line 560
  31. def OAI.SKFluctuations.Hierarchy.comparisonLowerScale line 562
  32. def OAI.SKFluctuations.Hierarchy.comparisonSmallMass line 563
  33. def OAI.SKFluctuations.Hierarchy.comparisonConstraintLength line 564
  34. theorem OAI.SKFluctuations.Hierarchy.comparisonCap_continuous line 567
  35. theorem OAI.SKFluctuations.Hierarchy.comparisonCap_monotoneOn line 572
  36. theorem OAI.SKFluctuations.Hierarchy.comparisonCap_nonneg line 580
  37. theorem OAI.SKFluctuations.Hierarchy.comparisonFloor_pos line 586
  38. theorem OAI.SKFluctuations.Hierarchy.comparisonFloor_continuousOn line 592
  39. def OAI.SKFluctuations.Hierarchy.inverseRestriction line 610
  40. theorem OAI.SKFluctuations.Hierarchy.inverseRestriction_continuous line 616
  41. theorem OAI.SKFluctuations.Hierarchy.inverseRestriction_compact line 640