OAI/Probability/SKFluctuations/ScalarCurvatureLower.lean

GitHub source file

50 declarations, 0 contain sorry, 0 declared as axioms

Scalar Curvature Lower.

  1. theorem OAI.SKFluctuations.Hierarchy.scalar_line_derivative line 19
  2. def OAI.SKFluctuations.Hierarchy.HeatJet.withCurvature line 29
  3. theorem OAI.SKFluctuations.Hierarchy.HeatJet.curvature_test_derivative_lower line 45
  4. theorem OAI.SKFluctuations.Hierarchy.exp_lower_of_clock_derivative line 101
  5. theorem OAI.SKFluctuations.Hierarchy.HeatJet.curvature_test_lower line 126
  6. theorem OAI.SKFluctuations.Hierarchy.HeatJet.evolve_curvature_lower line 143
  7. theorem OAI.SKFluctuations.Hierarchy.scalarTerminal_G line 163
  8. theorem OAI.SKFluctuations.Hierarchy.scalarTerminal_H line 170
  9. theorem OAI.SKFluctuations.Hierarchy.scalarTerminal_admissible line 177
  10. theorem OAI.SKFluctuations.Hierarchy.HeatJet.ScalarAdmissible.schedule line 182
  11. theorem OAI.SKFluctuations.Hierarchy.scalar_schedule_curvature_lower line 190
  12. theorem OAI.SKFluctuations.Hierarchy.PositiveMassProfile.grid_total_time line 210
  13. theorem OAI.SKFluctuations.Hierarchy.scalarSourceJet_one_schedule line 219
  14. theorem OAI.SKFluctuations.Hierarchy.scalarSourceJet_two_schedule line 228
  15. theorem OAI.SKFluctuations.Hierarchy.scalarCappedJets_curvature_lower line 245
  16. theorem OAI.SKFluctuations.Hierarchy.scalarProfileJet_curvature_lower line 259
  17. theorem OAI.SKFluctuations.Hierarchy.scalarProfileJet_curvature_pos line 265
  18. theorem OAI.SKFluctuations.Hierarchy.HeatJet.evolve_potential_bound line 280
  19. theorem OAI.SKFluctuations.Hierarchy.scalar_schedule_potential_bound line 301
  20. theorem OAI.SKFluctuations.Hierarchy.scalarCappedJets_potential_bound line 321
  21. theorem OAI.SKFluctuations.Hierarchy.scalarProfileJet_potential_bound line 332
  22. theorem OAI.SKFluctuations.Hierarchy.scalarProfileJet_admissible line 338
  23. theorem OAI.SKFluctuations.Hierarchy.scalarProfileJet_gradient_strictMono line 356
  24. theorem OAI.SKFluctuations.Hierarchy.scalarProfileJet_gradient_mem line 364
  25. theorem OAI.SKFluctuations.Scalar.logCosh_lower line 379
  26. theorem OAI.SKFluctuations.Scalar.exists_slope_gt_of_coercive line 391
  27. theorem OAI.SKFluctuations.Scalar.exists_slope_lt_of_coercive line 407
  28. theorem OAI.SKFluctuations.Hierarchy.scalarProfileJet_gradient_range line 422
  29. def OAI.SKFluctuations.Hierarchy.scalarSlopeInverse line 445
  30. theorem OAI.SKFluctuations.Hierarchy.scalarSlopeInverse_gradient line 448
  31. theorem OAI.SKFluctuations.Hierarchy.scalarSlopeInverse_right line 453
  32. theorem OAI.SKFluctuations.Hierarchy.scalarSlopeInverse_strictMonoOn line 460
  33. theorem OAI.SKFluctuations.Hierarchy.scalarSlopeInverse_continuousAt line 467
  34. theorem OAI.SKFluctuations.Hierarchy.scalarSlopeInverse_hasDerivAt line 480
  35. theorem OAI.SKFluctuations.Hierarchy.clockContinuation_even line 500
  36. theorem OAI.SKFluctuations.Hierarchy.scalar_schedule_even line 513
  37. theorem OAI.SKFluctuations.Hierarchy.scalarProfileJet_zero_even line 519
  38. theorem OAI.SKFluctuations.Hierarchy.scalarProfileJet_parity line 529
  39. theorem OAI.SKFluctuations.Hierarchy.scalarProfileJet_gradient_zero line 546
  40. theorem OAI.SKFluctuations.Hierarchy.scalarSlopeInverse_zero line 553
  41. theorem OAI.SKFluctuations.Hierarchy.scalarSlopeInverse_odd line 557
  42. def OAI.SKFluctuations.Hierarchy.scalarSlopeCurvature line 566
  43. def OAI.SKFluctuations.Hierarchy.scalarSlopeCurvature₁ line 570
  44. def OAI.SKFluctuations.Hierarchy.scalarSlopeCurvature₂ line 573
  45. theorem OAI.SKFluctuations.Hierarchy.scalarSlopeCurvature_pos line 577
  46. theorem OAI.SKFluctuations.Hierarchy.scalarSlopeCurvature_upper line 581
  47. theorem OAI.SKFluctuations.Hierarchy.scalarSlopeCurvature_hasDerivAt line 588
  48. theorem OAI.SKFluctuations.Hierarchy.scalarSlopeCurvature₁_hasDerivAt line 597
  49. theorem OAI.SKFluctuations.Hierarchy.scalarSlopeCurvature_even line 616
  50. theorem OAI.SKFluctuations.Hierarchy.scalarSlopeCurvature₁_zero line 622