OAI/Probability/SKFluctuations/WeightedFeatureTraceTelescope.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

Weighted Feature Trace Telescope.

  1. theorem OAI.SKFluctuations.Hierarchy.weighted_feature_trace_telescope line 22
  2. theorem OAI.SKFluctuations.Hierarchy.signedVarianceDerivative_feature_trace line 41
  3. theorem OAI.SKFluctuations.Hierarchy.rootedHierarchy_signed_variance line 93
  4. theorem OAI.SKFluctuations.Hierarchy.rootedHierarchy_corrected_signed_variance line 126
  5. theorem OAI.SKFluctuations.Hierarchy.prefixContinuation_append line 173
  6. theorem OAI.SKFluctuations.Hierarchy.prefixTest_append line 179
  7. theorem OAI.SKFluctuations.Hierarchy.rootedPrefixTest_const_mul line 185
  8. theorem OAI.SKFluctuations.Hierarchy.signedPenalty_observed_bound line 201
  9. theorem OAI.SKFluctuations.Hierarchy.rootedHierarchy_signed_derivative_bound line 231
  10. theorem OAI.SKFluctuations.GaussianCalculus.ExpNormBounded.continuous_integral_diagonal line 253
  11. theorem OAI.SKFluctuations.Hierarchy.varianceContinuation_eq_all line 289
  12. theorem OAI.SKFluctuations.Hierarchy.varianceTest_eq_all line 298
  13. theorem OAI.SKFluctuations.Hierarchy.varianceContinuation_continuous line 309
  14. theorem OAI.SKFluctuations.Hierarchy.varianceTest_continuous line 322
  15. theorem OAI.SKFluctuations.Hierarchy.parametric_continuous_variance line 337
  16. theorem OAI.SKFluctuations.Hierarchy.dynamic_diagonalPartition_continuous line 361
  17. theorem OAI.SKFluctuations.Hierarchy.dynamic_varianceTest_continuous line 409
  18. theorem OAI.SKFluctuations.Hierarchy.dynamic_varianceContinuation_continuous line 427
  19. def OAI.SKFluctuations.Hierarchy.covarianceSteps line 451
  20. theorem OAI.SKFluctuations.Hierarchy.covarianceSteps_nil line 455
  21. theorem OAI.SKFluctuations.Hierarchy.covarianceSteps_cons line 457
  22. theorem OAI.SKFluctuations.Hierarchy.covarianceFamily_lipschitz line 461
  23. theorem OAI.SKFluctuations.Hierarchy.covarianceFamily_potential_continuous line 474
  24. theorem OAI.SKFluctuations.Hierarchy.covarianceFamily_mean_continuous line 490
  25. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchyHessian_abs_le line 523
  26. theorem OAI.SKFluctuations.Hierarchy.covarianceFamily_hessian_continuous line 543
  27. abbrev OAI.SKFluctuations.Hierarchy.SignedStep line 598
  28. def OAI.SKFluctuations.Hierarchy.affineCovariances line 600
  29. def OAI.SKFluctuations.Hierarchy.affineSteps line 603
  30. theorem OAI.SKFluctuations.Hierarchy.affineSteps_nil line 607
  31. theorem OAI.SKFluctuations.Hierarchy.affineSteps_cons line 609
  32. theorem OAI.SKFluctuations.Hierarchy.affineSteps_ordered line 613
  33. theorem OAI.SKFluctuations.Hierarchy.affineCovariances_positive line 620
  34. theorem OAI.SKFluctuations.Hierarchy.affineCovariances_continuous line 632
  35. theorem OAI.SKFluctuations.Hierarchy.affineHierarchy_lipschitz line 641
  36. theorem OAI.SKFluctuations.Hierarchy.affineHierarchy_continuous line 647
  37. theorem OAI.SKFluctuations.Hierarchy.affineHierarchyMean_continuous line 653
  38. theorem OAI.SKFluctuations.Hierarchy.affineHierarchyMean_absBounded line 660
  39. theorem OAI.SKFluctuations.Hierarchy.affineHierarchyHessian_continuous line 669
  40. theorem OAI.SKFluctuations.Hierarchy.affineHierarchyHessian_absBounded line 676