OAI/Probability/SKFluctuations/RootSquareConvex.lean

GitHub source file

30 declarations, 0 contain sorry, 0 declared as axioms

Root Square Convex.

  1. theorem OAI.SKFluctuations.Hierarchy.HeatJet.rootFilledEnergy_monotone line 19
  2. theorem OAI.SKFluctuations.Hierarchy.HeatJet.continuous_rootFilledSquare line 40
  3. theorem OAI.SKFluctuations.Hierarchy.HeatJet.continuous_rootFilledEnergy line 44
  4. theorem OAI.SKFluctuations.Hierarchy.HeatJet.rootFilledSquare_convex line 48
  5. theorem OAI.SKFluctuations.Hierarchy.strict_integral_chord_of_derivative line 61
  6. theorem OAI.SKFluctuations.Hierarchy.HeatJet.rootFilledSquare_strict_chord line 118
  7. theorem OAI.SKFluctuations.Hierarchy.scalar_clockRoot_integral line 135
  8. theorem OAI.SKFluctuations.Hierarchy.scalarProfileJet_curvature_nonconstant line 141
  9. theorem OAI.SKFluctuations.Hierarchy.scalarProfileRoot_energy_strict line 162
  10. theorem OAI.SKFluctuations.Hierarchy.scalarProfileRoot_square_zero line 183
  11. theorem OAI.SKFluctuations.Hierarchy.HeatJet.rootFilledSquare_endpoint line 199
  12. theorem OAI.SKFluctuations.Hierarchy.scalarProfileRoot_strict_chord line 204
  13. theorem OAI.SKFluctuations.Hierarchy.HeatJet.mass_difference_root line 224
  14. theorem OAI.SKFluctuations.Hierarchy.clockRoot_abs_sub_le line 244
  15. theorem OAI.SKFluctuations.Hierarchy.HeatJet.massEnergy_inner_zero_bound line 261
  16. theorem OAI.SKFluctuations.Hierarchy.HeatJet.massEnergy_root_integral_tendsto line 285
  17. theorem OAI.SKFluctuations.Hierarchy.HeatJet.tendsto_root_mass_quotient line 314
  18. theorem OAI.SKFluctuations.Hierarchy.scalarParisiValue_zero_head_error line 334
  19. theorem OAI.SKFluctuations.Hierarchy.scalarMinimizer_zero_head_lower line 366
  20. theorem OAI.SKFluctuations.Hierarchy.scalarMinimizer_zero_head_balance line 397
  21. theorem OAI.SKFluctuations.Hierarchy.clockContinuation_tendsto_root line 424
  22. theorem OAI.SKFluctuations.Hierarchy.clockRoot_potential_abs_sub_le line 431
  23. theorem OAI.SKFluctuations.Hierarchy.HeatJet.observedSquare_tendsto_zero line 440
  24. theorem OAI.SKFluctuations.Hierarchy.clockExcess_continuous line 454
  25. theorem OAI.SKFluctuations.Hierarchy.clockMass_eventually_lower line 461
  26. theorem OAI.SKFluctuations.Hierarchy.HeatJet.flatten_root_schedule_error line 475
  27. theorem OAI.SKFluctuations.Hierarchy.HeatJet.flatten_root_profile_error line 500
  28. theorem OAI.SKFluctuations.Hierarchy.scalarTailJet_root_flatten_error line 548
  29. theorem OAI.SKFluctuations.Hierarchy.scalarMinimizer_zero_flatten_endpoint_bound line 569
  30. theorem OAI.SKFluctuations.Hierarchy.scalarMinimizer_zero_endpoint_le line 595