OAI/Probability/SKFluctuations/ResidualRootMoment.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

Residual Root Moment.

  1. theorem OAI.SKFluctuations.Hierarchy.scalarClockProfile_residual_transversality line 25
  2. theorem OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.prefixGradient_lower line 89
  3. theorem OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.potentialTerm_quadratic_monotone line 100
  4. theorem OAI.SKFluctuations.Scalar.onePeak_lower line 130
  5. theorem OAI.SKFluctuations.Scalar.weight_mul_lower line 163
  6. theorem OAI.SKFluctuations.Scalar.weight_mul_ge_center line 185
  7. theorem OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.weighted_tail_bounds_near line 198
  8. theorem OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.correction_near line 225
  9. theorem OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.generalNearRootIntegral_lower line 252
  10. theorem OAI.SKFluctuations.Hierarchy.AbsBounded.div_const line 373
  11. theorem OAI.SKFluctuations.Scalar.physicalSlopeOfJets_absBounded line 385
  12. theorem OAI.SKFluctuations.Hierarchy.scalarClockProfileSlice_absBounded line 417
  13. theorem OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.A_monotone line 440
  14. theorem OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.kappa_integrable line 448
  15. theorem OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.z_kappa_integrable line 461
  16. theorem OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.correction_rate_integrable line 470
  17. theorem OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.Rzero_absBounded line 485
  18. theorem OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.generalNearRootIntegral_lower_gaussian line 500
  19. theorem OAI.SKFluctuations.Hierarchy.scalarClockProfileSlice_residual_near_root_lower line 621