OAI/Probability/SKFluctuations/FinitePrefixRoot.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Finite Prefix Root.

  1. theorem OAI.SKFluctuations.Hierarchy.scalarClockProfileSlice_residual_root_pos line 24
  2. theorem OAI.SKFluctuations.Hierarchy.scalarClockProfileSlice_finite_prefix_root_pos line 53
  3. theorem OAI.SKFluctuations.Hierarchy.ResidualJet.unit_lipschitz line 76
  4. theorem OAI.SKFluctuations.Hierarchy.GaussianResidual.plantedDensity_envelope line 83
  5. theorem OAI.SKFluctuations.Hierarchy.ScalarFinitePositivePrefix.uniform_density line 112
  6. theorem OAI.SKFluctuations.Scalar.transverse_nonneg_after line 147
  7. theorem OAI.SKFluctuations.Scalar.transverse_pos_after line 159
  8. theorem OAI.SKFluctuations.Scalar.transverse_root_unique line 177
  9. theorem OAI.SKFluctuations.Scalar.transverse_neg_before line 186
  10. theorem OAI.SKFluctuations.Scalar.transverse_root_exists line 197
  11. theorem OAI.SKFluctuations.Scalar.transverse_weighted_negative line 230
  12. theorem OAI.SKFluctuations.Scalar.gap_area_first line 283
  13. theorem OAI.SKFluctuations.Scalar.gap_area_second line 298
  14. theorem OAI.SKFluctuations.Scalar.gap_strict_balance line 325
  15. theorem OAI.SKFluctuations.Scalar.transverse_derivative_le_endpoints line 355
  16. theorem OAI.SKFluctuations.Scalar.transverse_no_stationary_gap line 379
  17. theorem OAI.SKFluctuations.Scalar.monotone_root_product_nonneg line 427
  18. theorem OAI.SKFluctuations.Scalar.centered_weight_mul_lower line 437
  19. theorem OAI.SKFluctuations.Scalar.root_covariance_floor_pos line 459
  20. def OAI.SKFluctuations.Hierarchy.gaussianDensityFloor line 485
  21. theorem OAI.SKFluctuations.Hierarchy.gaussianDensityFloor_pos line 488
  22. theorem OAI.SKFluctuations.Hierarchy.gaussianDensityFloor_continuous line 493
  23. theorem OAI.SKFluctuations.Hierarchy.gaussianDensityFloor_dominated line 497
  24. def OAI.SKFluctuations.Hierarchy.rootCovarianceFloor line 514
  25. theorem OAI.SKFluctuations.Hierarchy.rootCovarianceFloor_integrable line 518
  26. theorem OAI.SKFluctuations.Hierarchy.rootCovarianceFloor_pos line 529
  27. theorem OAI.SKFluctuations.Hierarchy.scalarClockProfileSlice_second line 556
  28. theorem OAI.SKFluctuations.Hierarchy.scalarClockProfileSlice_third line 562
  29. theorem OAI.SKFluctuations.Hierarchy.scalarClockProfile_transversality line 570
  30. theorem OAI.SKFluctuations.Hierarchy.scalarProfileGapCurvature_root line 632