OAI/Probability/SKFluctuations/ProjectionRootEstimate.lean

GitHub source file

47 declarations, 0 contain sorry, 0 declared as axioms

Projection Root Estimate.

  1. def OAI.SKFluctuations.projectionLpConstant line 19
  2. theorem OAI.SKFluctuations.projectionLpConstant_pos line 22
  3. theorem OAI.SKFluctuations.projectionLpConstant_pow line 27
  4. theorem OAI.SKFluctuations.eventually_finiteSK_projection_root line 35
  5. inductive OAI.SKFluctuations.Hierarchy.ClockRefinement line 98
  6. theorem OAI.SKFluctuations.Hierarchy.orderedSteps_split line 105
  7. theorem OAI.SKFluctuations.Hierarchy.ClockRefinement.ordered line 113
  8. theorem OAI.SKFluctuations.Hierarchy.ClockRefinement.append line 121
  9. theorem OAI.SKFluctuations.Hierarchy.ClockRefinement.cons line 130
  10. theorem OAI.SKFluctuations.Hierarchy.ClockRefinement.continuation_test line 136
  11. abbrev OAI.SKFluctuations.Hierarchy.ClockedStep line 169
  12. def OAI.SKFluctuations.Hierarchy.forgetClock line 171
  13. def OAI.SKFluctuations.Hierarchy.clockDuration line 173
  14. def OAI.SKFluctuations.Hierarchy.ClockAligned line 177
  15. theorem OAI.SKFluctuations.Hierarchy.forgetClock_nil line 180
  16. theorem OAI.SKFluctuations.Hierarchy.forgetClock_cons line 181
  17. theorem OAI.SKFluctuations.Hierarchy.forgetClock_append line 183
  18. theorem OAI.SKFluctuations.Hierarchy.clockDuration_nil line 185
  19. theorem OAI.SKFluctuations.Hierarchy.clockDuration_cons line 186
  20. theorem OAI.SKFluctuations.Hierarchy.clockDuration_append line 188
  21. theorem OAI.SKFluctuations.Hierarchy.ClockAligned.append line 191
  22. theorem OAI.SKFluctuations.Hierarchy.ClockAligned.of_append_left line 198
  23. theorem OAI.SKFluctuations.Hierarchy.ClockAligned.of_append_right line 202
  24. theorem OAI.SKFluctuations.Hierarchy.exists_clock_cut line 208
  25. theorem OAI.SKFluctuations.Hierarchy.exists_equal_clock_partition line 272
  26. theorem OAI.SKFluctuations.Hierarchy.hierarchyClocks_get line 318
  27. theorem OAI.SKFluctuations.Hierarchy.ClockAligned.toAligned line 327
  28. theorem OAI.SKFluctuations.Hierarchy.exists_clocked_of_aligned line 346
  29. theorem OAI.SKFluctuations.Hierarchy.forgetClock_flatten line 365
  30. theorem OAI.SKFluctuations.Hierarchy.exists_aligned_refinement line 371
  31. theorem OAI.SKFluctuations.Hierarchy.OrderedSteps.prefix line 391
  32. theorem OAI.SKFluctuations.eventually_finiteSK_projection line 405
  33. theorem OAI.SKFluctuations.Scalar.contDiffOn_succ_of_partials line 441
  34. theorem OAI.SKFluctuations.Hierarchy.ClockJointSmooth_clockTest_scalar_source line 488
  35. theorem OAI.SKFluctuations.Hierarchy.clockTest_scalar_contDiffOn line 510
  36. theorem OAI.SKFluctuations.Hierarchy.clockTest_mono line 565
  37. theorem OAI.SKFluctuations.Hierarchy.clockTest_const line 572
  38. theorem OAI.SKFluctuations.Hierarchy.clockTest_variance_nonneg line 578
  39. def OAI.SKFluctuations.Hierarchy.HeatJet.ScalarAdmissible line 586
  40. theorem OAI.SKFluctuations.Hierarchy.HeatJet.ScalarAdmissible.gradient line 589
  41. theorem OAI.SKFluctuations.Hierarchy.HeatJet.ScalarAdmissible.curvature line 594
  42. theorem OAI.SKFluctuations.Hierarchy.HeatJet.ScalarAdmissible.evolve line 598
  43. theorem OAI.SKFluctuations.Scalar.third_abs_le_curvature line 621
  44. theorem OAI.SKFluctuations.Scalar.fourth_lower line 625
  45. theorem OAI.SKFluctuations.Scalar.curvature_pi_bddSmooth line 630
  46. theorem OAI.SKFluctuations.Scalar.third_bddSmooth line 636
  47. theorem OAI.SKFluctuations.Scalar.fourth_bddSmooth line 641