OAI/Probability/SKFluctuations/MassResponseJet.lean

GitHub source file

46 declarations, 0 contain sorry, 0 declared as axioms

Mass Response Jet.

  1. def OAI.SKFluctuations.Hierarchy.HeatJet.massResponseFamily line 21
  2. theorem OAI.SKFluctuations.Hierarchy.HeatJet.massResponseFamily_F line 26
  3. theorem OAI.SKFluctuations.Hierarchy.HeatJet.massResponseFamily_A line 30
  4. def OAI.SKFluctuations.Hierarchy.HeatJet.massResponseJet line 45
  5. theorem OAI.SKFluctuations.Hierarchy.HeatJet.massResponseJet_F line 49
  6. theorem OAI.SKFluctuations.Hierarchy.HeatJet.massResponseJet_A line 53
  7. theorem OAI.SKFluctuations.Hierarchy.HeatJet.massEnergy_abs_le_one line 60
  8. theorem OAI.SKFluctuations.Hierarchy.HeatJet.massResponseJet_abs_le line 72
  9. theorem OAI.SKFluctuations.Hierarchy.HeatJet.massResponseJet_profileTest line 82
  10. theorem OAI.SKFluctuations.Hierarchy.hasDerivAt_of_quadratic_remainder line 99
  11. theorem OAI.SKFluctuations.Hierarchy.HeatJet.massContinuation_quadratic line 116
  12. theorem OAI.SKFluctuations.Hierarchy.HeatJet.profile_mass_quadratic line 147
  13. def OAI.SKFluctuations.Hierarchy.HeatJet.massClockProfileValue line 171
  14. theorem OAI.SKFluctuations.Hierarchy.HeatJet.hasDerivAt_massClockProfileValue line 175
  15. theorem OAI.SKFluctuations.Scalar.derivative_nonneg_of_left_max line 197
  16. theorem OAI.SKFluctuations.Scalar.cumulative_endpoint line 206
  17. theorem OAI.SKFluctuations.Scalar.cumulative_initial_slope line 222
  18. def OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.generalL line 270
  19. def OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.generalR₁ line 272
  20. def OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.potentialTerm line 274
  21. def OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.generalFlux line 275
  22. def OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.generalIntegrand line 277
  23. theorem OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.prefixGradient_strictMono line 287
  24. theorem OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.prefixGradient_pos line 291
  25. theorem OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.prefixGradient_nonneg line 296
  26. theorem OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.dgeneralL line 302
  27. theorem OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.generalL_strictAnti line 308
  28. theorem OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.dgeneralR₁ line 327
  29. theorem OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.generalR₁_monotone line 332
  30. theorem OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.dpotentialTerm line 344
  31. theorem OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.potentialTerm_strictMono line 349
  32. theorem OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.dgeneralFlux line 360
  33. theorem OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.dweightedGeneralFlux line 370
  34. theorem OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.generalFlux_zero line 377
  35. theorem OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.weighted_tail_bounds_general line 380
  36. theorem OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.generalRootIntegral_pos line 416
  37. theorem OAI.SKFluctuations.Scalar.PhysicalSlopeSlice.generalRootIntegral_pos_gaussian line 505
  38. theorem OAI.SKFluctuations.Hierarchy.ResidualJet.Cone.gradient_zero line 600
  39. theorem OAI.SKFluctuations.Hierarchy.ResidualJet.Cone.zero_max line 609
  40. theorem OAI.SKFluctuations.Hierarchy.GaussianResidual.potential_gradient_polyBounded line 629
  41. theorem OAI.SKFluctuations.Hierarchy.GaussianResidual.potential_curvature_polyBounded line 633
  42. def OAI.SKFluctuations.Hierarchy.GaussianResidual.rootWeight line 637
  43. theorem OAI.SKFluctuations.Hierarchy.GaussianResidual.rootWeight_eq line 640
  44. theorem OAI.SKFluctuations.Hierarchy.GaussianResidual.rootWeight_pos line 647
  45. theorem OAI.SKFluctuations.Hierarchy.GaussianResidual.rootWeight_deriv line 651
  46. theorem OAI.SKFluctuations.Hierarchy.GaussianResidual.rootWeight_dominated line 661