OAI/Probability/SKFluctuations/ResidualUniformCurvature.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Residual Uniform Curvature.

  1. theorem OAI.SKFluctuations.Hierarchy.ResidualJet.Cone.curvature_bound line 18
  2. theorem OAI.SKFluctuations.Hierarchy.GaussianResidual.potential_gradient_bound line 46
  3. theorem OAI.SKFluctuations.Hierarchy.GaussianResidual.potential_curvature_bound line 54
  4. theorem OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.exists_Phi_pos line 73
  5. theorem OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.exists_Phi_root line 114
  6. def OAI.SKFluctuations.Hierarchy.physicalRootErrorCoefficient line 133
  7. theorem OAI.SKFluctuations.Hierarchy.physicalRootErrorCoefficient_nonneg line 137
  8. theorem OAI.SKFluctuations.Hierarchy.physicalRootCoefficient_bound line 142
  9. theorem OAI.SKFluctuations.Hierarchy.scalarClockProfileSlice_residual_uniform_near_root line 171
  10. theorem OAI.SKFluctuations.Hierarchy.scalarClockProfileSlice_residual_sequence_root line 241
  11. theorem OAI.SKFluctuations.Hierarchy.scalarClockProfile_residual_moments line 284
  12. def OAI.SKFluctuations.Hierarchy.scalarRootSecond line 354
  13. def OAI.SKFluctuations.Hierarchy.scalarRootThird line 358
  14. theorem OAI.SKFluctuations.Hierarchy.scalarClockProfileJet_bddSmooth line 364
  15. theorem OAI.SKFluctuations.Hierarchy.scalarRootSecond_bddSmooth line 370
  16. theorem OAI.SKFluctuations.Hierarchy.scalarRootThird_bddSmooth line 376
  17. theorem OAI.SKFluctuations.Hierarchy.scalarClockProfileJet_zero_clock line 386
  18. theorem OAI.SKFluctuations.Hierarchy.scalarClockProfile_residual_test_sequence_root line 401
  19. def OAI.SKFluctuations.Hierarchy.prefixGridPoint line 446
  20. theorem OAI.SKFluctuations.Hierarchy.prefixGridPoint_monotone line 449
  21. theorem OAI.SKFluctuations.Hierarchy.prefixGridPoint_bounds line 457
  22. theorem OAI.SKFluctuations.Hierarchy.prefixGridPoint_cell line 467
  23. def OAI.SKFluctuations.Hierarchy.prefixGridProfile line 475
  24. theorem OAI.SKFluctuations.Hierarchy.prefixGridProfile_tail line 505
  25. theorem OAI.SKFluctuations.Hierarchy.prefixGridProfile_mem line 511
  26. theorem OAI.SKFluctuations.Hierarchy.prefixGridProfile_cell line 522
  27. theorem OAI.SKFluctuations.Hierarchy.prefixGridProfile_finite line 539
  28. theorem OAI.SKFluctuations.Hierarchy.prefixGridProfile_uniform_density line 566
  29. theorem OAI.SKFluctuations.Hierarchy.prefixGridPoint_tendsto line 591
  30. theorem OAI.SKFluctuations.Hierarchy.prefixGridProfile_tendsto line 600
  31. theorem OAI.SKFluctuations.Hierarchy.prefixGridProfile_test_tendsto line 627