OAI/Probability/SKFluctuations/RootedVariancePressure.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

Rooted Variance Pressure.

  1. def OAI.SKFluctuations.Hierarchy.rootedVariancePressure line 22
  2. theorem OAI.SKFluctuations.Hierarchy.rootedVariancePressure_continuous line 27
  3. theorem OAI.SKFluctuations.Hierarchy.rootedVariancePressure_chord_pos line 45
  4. theorem OAI.SKFluctuations.Hierarchy.rootedVariancePressure_chord line 72
  5. def OAI.SKFluctuations.Hierarchy.reindexSteps line 113
  6. theorem OAI.SKFluctuations.Hierarchy.reindexSteps_ordered line 117
  7. theorem OAI.SKFluctuations.Hierarchy.reindexSteps_positive line 124
  8. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchy_reindex_steps line 133
  9. theorem OAI.SKFluctuations.Hierarchy.zeroContinuation_reindex line 145
  10. theorem OAI.SKFluctuations.Hierarchy.rootedVariancePressure_reindex line 153
  11. theorem OAI.SKFluctuations.Hierarchy.rootedVariancePressure_chord_finite line 169
  12. def OAI.SKFluctuations.Hierarchy.reindexSignedSteps line 207
  13. theorem OAI.SKFluctuations.Hierarchy.reindexSignedSteps_nil line 211
  14. theorem OAI.SKFluctuations.Hierarchy.reindexSignedSteps_cons line 215
  15. theorem OAI.SKFluctuations.Hierarchy.reindexSignedSteps_inverse line 220
  16. theorem OAI.SKFluctuations.Hierarchy.affineSteps_reindex line 225
  17. theorem OAI.SKFluctuations.Hierarchy.featureKernel_reindex line 231
  18. theorem OAI.SKFluctuations.Hierarchy.PathKernelBound.reindex line 243
  19. theorem OAI.SKFluctuations.Hierarchy.pathKernelCost_reindex line 261
  20. theorem OAI.SKFluctuations.Hierarchy.rootedHierarchy_affine_chord_finite line 282
  21. def OAI.SKFluctuations.Hierarchy.signedClockSteps line 359
  22. theorem OAI.SKFluctuations.Hierarchy.signedClockSteps_length line 364
  23. theorem OAI.SKFluctuations.Hierarchy.signedClockSteps_zero line 370
  24. theorem OAI.SKFluctuations.Hierarchy.signedClockSteps_one line 379
  25. theorem OAI.SKFluctuations.Hierarchy.signedClockSteps_admissible line 391
  26. theorem OAI.SKFluctuations.Hierarchy.signedClockSteps_trace line 408
  27. def OAI.SKFluctuations.Hierarchy.massStepSum line 422
  28. theorem OAI.SKFluctuations.Hierarchy.featureKernel_add_difference line 434
  29. theorem OAI.SKFluctuations.Hierarchy.signedClockSteps_kernelBound line 442
  30. theorem OAI.SKFluctuations.Hierarchy.signedClockSteps_cost line 464
  31. theorem OAI.SKFluctuations.Hierarchy.disorderPressure_chord line 496
  32. def OAI.SKFluctuations.Hierarchy.featureVector line 544
  33. theorem OAI.SKFluctuations.Hierarchy.featureVector_apply line 548
  34. theorem OAI.SKFluctuations.Hierarchy.charFunDual_featureVector line 553
  35. theorem OAI.SKFluctuations.Hierarchy.finiteDual_expansion line 571
  36. theorem OAI.SKFluctuations.Hierarchy.kernel_quadratic_identity line 585
  37. theorem OAI.SKFluctuations.Hierarchy.featureVector_law_eq line 601
  38. theorem OAI.SKFluctuations.Hierarchy.massStepSum_const_mul line 633