OAI/Probability/SKFluctuations/ScalarGapWeighted.lean

GitHub source file

53 declarations, 0 contain sorry, 0 declared as axioms

Scalar Gap Weighted.

  1. def OAI.SKFluctuations.Hierarchy.scalarWeightedMoment line 19
  2. theorem OAI.SKFluctuations.Hierarchy.ScalarGapWeighted_gap_energy_spatial line 26
  3. theorem OAI.SKFluctuations.Hierarchy.ScalarGapWeighted_gap_curvature_spatial line 29
  4. theorem OAI.SKFluctuations.Hierarchy.ScalarGapWeighted_gap_third_test_smooth line 32
  5. theorem OAI.SKFluctuations.Hierarchy.ScalarGapWeighted_gap_third_spatial line 38
  6. theorem OAI.SKFluctuations.Hierarchy.ScalarGapWeighted_clock_backward_bound line 42
  7. theorem OAI.SKFluctuations.Hierarchy.HeatJet.scalarGapEnergy_bound line 50
  8. theorem OAI.SKFluctuations.Hierarchy.HeatJet.scalarGapCurvature_bound line 55
  9. theorem OAI.SKFluctuations.Hierarchy.HeatJet.scalarGapThird_bound line 59
  10. theorem OAI.SKFluctuations.Hierarchy.HeatJet.weightedGapEnergy_continuous line 65
  11. theorem OAI.SKFluctuations.Hierarchy.HeatJet.weightedGapCurvature_continuous line 74
  12. theorem OAI.SKFluctuations.Hierarchy.HeatJet.weightedGapEnergy_hasDerivAt line 83
  13. theorem OAI.SKFluctuations.Hierarchy.HeatJet.weightedGapCurvature_hasDerivAt line 98
  14. theorem OAI.SKFluctuations.Hierarchy.HeatJet.regular_of_smoothG line 123
  15. theorem OAI.SKFluctuations.Hierarchy.HeatJet.scalarGapEnergy_bddSmooth line 133
  16. theorem OAI.SKFluctuations.Hierarchy.HeatJet.scalarGapCurvature_bddSmooth line 138
  17. theorem OAI.SKFluctuations.Hierarchy.HeatJet.filledSquare_bddSmooth line 144
  18. def OAI.SKFluctuations.Hierarchy.HeatJet.profileGapSquareJet line 151
  19. def OAI.SKFluctuations.Hierarchy.HeatJet.profileGapEnergyJet line 154
  20. def OAI.SKFluctuations.Hierarchy.HeatJet.profileGapCurvatureJet line 157
  21. theorem OAI.SKFluctuations.Hierarchy.HeatJet.profileGapSquareJet_F line 160
  22. theorem OAI.SKFluctuations.Hierarchy.HeatJet.profileGapSquareJet_A line 163
  23. theorem OAI.SKFluctuations.Hierarchy.HeatJet.profileGapEnergyJet_F line 166
  24. theorem OAI.SKFluctuations.Hierarchy.HeatJet.profileGapEnergyJet_A line 169
  25. theorem OAI.SKFluctuations.Hierarchy.HeatJet.profileGapCurvatureJet_F line 172
  26. theorem OAI.SKFluctuations.Hierarchy.HeatJet.profileGapCurvatureJet_A line 175
  27. theorem OAI.SKFluctuations.Hierarchy.HeatJet.profileGapSquare_hasDerivAt line 177
  28. theorem OAI.SKFluctuations.Hierarchy.HeatJet.profileGapEnergy_hasDerivAt line 203
  29. def OAI.SKFluctuations.Hierarchy.HeatJet.massEnergy line 238
  30. theorem OAI.SKFluctuations.Hierarchy.HeatJet.continuous_massEnergy line 242
  31. theorem OAI.SKFluctuations.Hierarchy.HeatJet.mass_difference_integral line 258
  32. theorem OAI.SKFluctuations.Hierarchy.HeatJet.massEnergy_mass_bound line 278
  33. theorem OAI.SKFluctuations.Hierarchy.HeatJet.massEnergy_integral_continuousAt line 322
  34. theorem OAI.SKFluctuations.Hierarchy.HeatJet.hasDerivAt_mass_clockContinuation line 348
  35. def OAI.SKFluctuations.Hierarchy.HeatJet.mixedSquare line 372
  36. def OAI.SKFluctuations.Hierarchy.HeatJet.mixedSquareResponse line 376
  37. theorem OAI.SKFluctuations.Hierarchy.HeatJet.hasDerivAt_mixedSquare line 381
  38. theorem OAI.SKFluctuations.Hierarchy.HeatJet.square_testRate line 411
  39. theorem OAI.SKFluctuations.Hierarchy.HeatJet.mixedSquareResponse_eq line 420
  40. theorem OAI.SKFluctuations.Hierarchy.HeatJet.mixedSquareResponse_bound line 432
  41. def OAI.SKFluctuations.Hierarchy.HeatJet.GradientTest line 474
  42. theorem OAI.SKFluctuations.Hierarchy.HeatJet.GradientTest.evolve line 476
  43. theorem OAI.SKFluctuations.Hierarchy.HeatJet.GradientTest.schedule line 488
  44. theorem OAI.SKFluctuations.Hierarchy.scalarProfileHeatJet_gradientTest line 494
  45. theorem OAI.SKFluctuations.Hierarchy.HeatJet.continuous_mixedSquare line 498
  46. theorem OAI.SKFluctuations.Hierarchy.HeatJet.mixedSquareResponse_le_four line 507
  47. theorem OAI.SKFluctuations.Hierarchy.HeatJet.mixedSquare_lipschitz line 526
  48. def OAI.SKFluctuations.Hierarchy.HeatJet.observedSquare line 559
  49. theorem OAI.SKFluctuations.Hierarchy.HeatJet.GradientTest.potentialEnergy line 562
  50. theorem OAI.SKFluctuations.Hierarchy.HeatJet.mixedSquare_terminal line 568
  51. theorem OAI.SKFluctuations.Hierarchy.HeatJet.flatten_one_energy line 575
  52. theorem OAI.SKFluctuations.Hierarchy.HeatJet.flatten_one_identity line 586
  53. theorem OAI.SKFluctuations.Hierarchy.HeatJet.flatten_one_error line 608