OAI/Probability/SKFluctuations/Graft.lean

GitHub source file

55 declarations, 0 contain sorry, 0 declared as axioms

Graft.

  1. def OAI.SKFluctuations.Hierarchy.BoundaryTree.graft line 22
  2. def OAI.SKFluctuations.Hierarchy.BoundaryTree.graftAssignmentEquiv line 28
  3. theorem OAI.SKFluctuations.Hierarchy.BoundaryTree.graft_weight line 37
  4. theorem OAI.SKFluctuations.Hierarchy.BoundaryTree.graft_leaves line 60
  5. theorem OAI.SKFluctuations.Hierarchy.BoundaryTree.clock_crossing_variation line 80
  6. def OAI.SKFluctuations.Hierarchy.addHeadClock line 133
  7. theorem OAI.SKFluctuations.Hierarchy.gaussianHierarchy_addHeadClock line 137
  8. theorem OAI.SKFluctuations.Hierarchy.ClockTree.cut_zero_weight line 151
  9. theorem OAI.SKFluctuations.Hierarchy.ClockTree.addHeadClock_cut_weight line 160
  10. theorem OAI.SKFluctuations.Hierarchy.finite_probability_product_distance line 203
  11. theorem OAI.SKFluctuations.Hierarchy.ClockTree.step_addHead_atomic line 223
  12. theorem OAI.SKFluctuations.Hierarchy.ClockTree.addHead_variation line 252
  13. structure OAI.SKFluctuations.Hierarchy.HeatClock line 307
  14. def OAI.SKFluctuations.Hierarchy.HeatJet.schedule line 312
  15. theorem OAI.SKFluctuations.Hierarchy.HeatJet.schedule_gradient_bound line 316
  16. theorem OAI.SKFluctuations.Hierarchy.HeatJet.schedule_nonexpansive line 325
  17. structure OAI.SKFluctuations.Hierarchy.CoupledHeatClock line 335
  18. def OAI.SKFluctuations.Hierarchy.CoupledHeatClock.left line 342
  19. def OAI.SKFluctuations.Hierarchy.CoupledHeatClock.right line 343
  20. def OAI.SKFluctuations.Hierarchy.CoupledHeatClock.cost line 344
  21. theorem OAI.SKFluctuations.Hierarchy.HeatJet.schedule_mass_comparison line 348
  22. structure OAI.SKFluctuations.Hierarchy.PositiveMassProfile line 376
  23. def OAI.SKFluctuations.Hierarchy.PositiveMassProfile.grid line 381
  24. def OAI.SKFluctuations.Hierarchy.HeatClock.halves line 385
  25. theorem OAI.SKFluctuations.Hierarchy.HeatJet.schedule_append line 388
  26. theorem OAI.SKFluctuations.Hierarchy.HeatJet.schedule_congr_terminal line 397
  27. theorem OAI.SKFluctuations.Hierarchy.HeatJet.schedule_halves line 405
  28. def OAI.SKFluctuations.Hierarchy.PositiveMassProfile.coupledGrid line 420
  29. theorem OAI.SKFluctuations.Hierarchy.PositiveMassProfile.coupledGrid_left line 425
  30. theorem OAI.SKFluctuations.Hierarchy.PositiveMassProfile.coupledGrid_right line 431
  31. theorem OAI.SKFluctuations.Hierarchy.PositiveMassProfile.coupledGrid_cost line 437
  32. theorem OAI.SKFluctuations.Hierarchy.HeatJet.grid_successive line 459
  33. theorem OAI.SKFluctuations.Hierarchy.HeatJet.grid_cauchy line 470
  34. def OAI.SKFluctuations.Hierarchy.PositiveMassProfile.pairedGrid line 488
  35. theorem OAI.SKFluctuations.Hierarchy.PositiveMassProfile.pairedGrid_left line 492
  36. theorem OAI.SKFluctuations.Hierarchy.PositiveMassProfile.pairedGrid_right line 498
  37. theorem OAI.SKFluctuations.Hierarchy.PositiveMassProfile.pairedGrid_cost line 504
  38. theorem OAI.SKFluctuations.Hierarchy.HeatJet.grid_profile_comparison line 518
  39. def OAI.SKFluctuations.Hierarchy.HeatJet.profileValue line 527
  40. theorem OAI.SKFluctuations.Hierarchy.HeatJet.grid_tendsto line 531
  41. theorem OAI.SKFluctuations.Hierarchy.HeatJet.profileValue_comparison line 537
  42. theorem OAI.SKFluctuations.Hierarchy.HeatJet.profileValue_nonexpansive line 544
  43. structure OAI.SKFluctuations.Hierarchy.NonnegativeMassProfile line 556
  44. def OAI.SKFluctuations.Hierarchy.NonnegativeMassProfile.positiveApprox line 561
  45. theorem OAI.SKFluctuations.Hierarchy.NonnegativeMassProfile.approx_step line 566
  46. theorem OAI.SKFluctuations.Hierarchy.HeatJet.regularized_cauchy line 572
  47. def OAI.SKFluctuations.Hierarchy.HeatJet.nonnegativeProfileValue line 582
  48. theorem OAI.SKFluctuations.Hierarchy.HeatJet.regularized_tendsto line 586
  49. theorem OAI.SKFluctuations.Hierarchy.HeatJet.nonnegativeProfile_comparison line 592
  50. theorem OAI.SKFluctuations.Hierarchy.HeatJet.regularized_error line 604
  51. theorem OAI.SKFluctuations.Hierarchy.HeatJet.grid_error line 620
  52. theorem OAI.SKFluctuations.Hierarchy.PositiveMassProfile.pairedGrid_cost_continuous line 647
  53. theorem OAI.SKFluctuations.Hierarchy.PositiveMassProfile.pairedGrid_self_cost line 659
  54. theorem OAI.SKFluctuations.Hierarchy.HeatJet.continuous_grid line 665
  55. theorem OAI.SKFluctuations.Hierarchy.HeatJet.double_grid_error line 685