OAI/Probability/SKFluctuations/Diagonal.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

Diagonal.

  1. theorem OAI.SKFluctuations.GaussianCalculus.ExpNormBounded.diagonal line 21
  2. theorem OAI.SKFluctuations.GaussianCalculus.ExpNormBounded.diagonal_integrable line 33
  3. theorem OAI.SKFluctuations.GaussianCalculus.ExpNormBounded.diagonal_coord_integrable line 38
  4. theorem OAI.SKFluctuations.GaussianCalculus.standardGaussianVector_diagonal_stein line 45
  5. theorem OAI.SKFluctuations.GaussianCalculus.hasDerivAt_diagonal_heat_continuation line 78
  6. theorem OAI.SKFluctuations.GaussianCalculus.hasDerivAt_signed_variance_continuation line 173
  7. theorem OAI.SKFluctuations.Hierarchy.integral_diagonalGaussian line 229
  8. def OAI.SKFluctuations.Hierarchy.varianceContinuation line 238
  9. def OAI.SKFluctuations.Hierarchy.varianceTest line 241
  10. theorem OAI.SKFluctuations.Hierarchy.varianceContinuation_eq line 244
  11. theorem OAI.SKFluctuations.Hierarchy.varianceTest_eq line 253
  12. def OAI.SKFluctuations.Hierarchy.signedVarianceDerivative line 271
  13. theorem OAI.SKFluctuations.Hierarchy.parametric_signed_variance line 277
  14. def OAI.SKFluctuations.Hierarchy.hierarchyAtom line 352
  15. theorem OAI.SKFluctuations.Hierarchy.hierarchyAtom_nonneg line 357
  16. theorem OAI.SKFluctuations.Hierarchy.hierarchyAtom_smooth line 364
  17. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchyMean_atoms line 370
  18. theorem OAI.SKFluctuations.Hierarchy.hierarchyAtom_sum line 384
  19. def OAI.SKFluctuations.Hierarchy.hierarchyPairMean line 394
  20. theorem OAI.SKFluctuations.Hierarchy.hierarchyPairMean_smooth line 398
  21. theorem OAI.SKFluctuations.Hierarchy.hierarchyPairMean_const line 410
  22. theorem OAI.SKFluctuations.Hierarchy.hierarchyPairMean_mono line 419
  23. theorem OAI.SKFluctuations.Hierarchy.hierarchyPairMean_linear line 431
  24. theorem OAI.SKFluctuations.Hierarchy.hierarchyPairMean_product line 439
  25. def OAI.SKFluctuations.Hierarchy.kernelPenalty line 455
  26. theorem OAI.SKFluctuations.Hierarchy.kernelPenalty_smooth line 462
  27. theorem OAI.SKFluctuations.Hierarchy.kernelPenalty_const line 474
  28. theorem OAI.SKFluctuations.Hierarchy.kernelPenalty_mono line 487
  29. theorem OAI.SKFluctuations.Hierarchy.kernelPenalty_linear line 503
  30. theorem OAI.SKFluctuations.Hierarchy.kernelPenalty_rankOne line 520
  31. theorem OAI.SKFluctuations.Hierarchy.kernelPenalty_const_mul line 538
  32. theorem OAI.SKFluctuations.Hierarchy.kernelPenalty_sum line 544
  33. theorem OAI.SKFluctuations.Hierarchy.kernelPenalty_weighted_features line 560
  34. theorem OAI.SKFluctuations.Hierarchy.kernelPenalty_lower_bound line 574
  35. theorem OAI.SKFluctuations.Hierarchy.kernelPenalty_chord line 584
  36. theorem OAI.SKFluctuations.Hierarchy.prefixTest_le_const line 596
  37. theorem OAI.SKFluctuations.Hierarchy.rootedPrefixTest_le_const line 605
  38. theorem OAI.SKFluctuations.orderedSK_kernel_chord line 627
  39. theorem OAI.SKFluctuations.orderedSK_kernel_chord_observed line 654