OAI/Probability/SKFluctuations/ScalarPlantedEnergy.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

Scalar Planted Energy.

  1. def OAI.SKFluctuations.Hierarchy.scalarPlantedEnergy line 20
  2. theorem OAI.SKFluctuations.Hierarchy.scalarTailJet_F_tendsto line 25
  3. theorem OAI.SKFluctuations.Hierarchy.scalarTailJet_square_tendsto line 37
  4. theorem OAI.SKFluctuations.Hierarchy.scalarPlantedEnergy_continuous line 59
  5. theorem OAI.SKFluctuations.Hierarchy.scalarPlantedEnergy_bounds line 75
  6. theorem OAI.SKFluctuations.Hierarchy.scalarTailJet_plateau_evolve line 94
  7. theorem OAI.SKFluctuations.Hierarchy.scalarPlantedEnergy_plateau line 113
  8. structure OAI.SKFluctuations.Hierarchy.ResidualJet line 178
  9. theorem OAI.SKFluctuations.Hierarchy.ResidualJet.continuous line 185
  10. theorem OAI.SKFluctuations.Hierarchy.ResidualJet.bddSmooth line 188
  11. theorem OAI.SKFluctuations.Hierarchy.ResidualJet.lipschitz line 197
  12. theorem OAI.SKFluctuations.Hierarchy.ResidualJet.line line 204
  13. theorem OAI.SKFluctuations.Hierarchy.ResidualJet.coord line 213
  14. def OAI.SKFluctuations.Hierarchy.ResidualJet.heatJet line 220
  15. def OAI.SKFluctuations.Hierarchy.ResidualJet.zero line 243
  16. def OAI.SKFluctuations.Hierarchy.ResidualJet.add line 248
  17. def OAI.SKFluctuations.Hierarchy.ResidualJet.scale line 253
  18. def OAI.SKFluctuations.Hierarchy.ResidualJet.heat line 259
  19. theorem OAI.SKFluctuations.Scalar.ParabolicBounded_quadratic_add_deriv line 285
  20. theorem OAI.SKFluctuations.Scalar.ParabolicBounded_quadratic_add_second line 292
  21. theorem OAI.SKFluctuations.Scalar.ParabolicBounded_quadratic_barrier_forcing line 301
  22. theorem OAI.SKFluctuations.Scalar.ParabolicBounded_quadratic_barrier_tail line 311
  23. theorem OAI.SKFluctuations.Scalar.parabolic_nonneg_bounded_real line 331
  24. theorem OAI.SKFluctuations.Scalar.parabolic_nonneg_bounded_halfline line 390
  25. theorem OAI.SKFluctuations.Hierarchy.TransformedHeatCone_initial_realJet_two line 466
  26. theorem OAI.SKFluctuations.Hierarchy.TransformedHeatCone_initial_realJet_three line 474
  27. theorem OAI.SKFluctuations.Hierarchy.HeatJet.scalarClockPlane_concave line 482
  28. theorem OAI.SKFluctuations.Hierarchy.HeatJet.scalarClockPlane_third_nonneg line 526
  29. def OAI.SKFluctuations.Hierarchy.ResidualJet.Cone line 584
  30. theorem OAI.SKFluctuations.Hierarchy.ResidualJet.zero_cone line 588
  31. theorem OAI.SKFluctuations.Hierarchy.ResidualJet.Cone.add line 590
  32. theorem OAI.SKFluctuations.Hierarchy.ResidualJet.Cone.scale line 596
  33. theorem OAI.SKFluctuations.Hierarchy.ResidualJet.Cone.heat line 602
  34. def OAI.SKFluctuations.Hierarchy.ResidualJet.scalarPotential line 626
  35. theorem OAI.SKFluctuations.Hierarchy.ResidualJet.scalarPotential_neg_cone line 635