OAI/Probability/SKFluctuations/ScalarIntervalStrictArea.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

Scalar Interval Strict Area.

  1. theorem OAI.SKFluctuations.Hierarchy.intervalIntegral_pos_of_interior_interval line 19
  2. theorem OAI.SKFluctuations.Hierarchy.scalarInterval_down_area_pos line 34
  3. theorem OAI.SKFluctuations.Hierarchy.scalarInterval_up_area_neg line 44
  4. theorem OAI.SKFluctuations.Hierarchy.scalarProfileGap_zero line 75
  5. theorem OAI.SKFluctuations.Hierarchy.scalarProfileGap_energy_zero line 91
  6. theorem OAI.SKFluctuations.Hierarchy.scalarProfileGap_strict_balance line 100
  7. theorem OAI.SKFluctuations.Hierarchy.scalarMinimizer_gap_cumulative line 131
  8. theorem OAI.SKFluctuations.Hierarchy.scalarMinimizer_gap_initial_slope line 147
  9. theorem OAI.SKFluctuations.Hierarchy.scalarMinimizer_gap_endpoint line 164
  10. theorem OAI.SKFluctuations.Hierarchy.scalarMinimizer_no_isolated_origin line 190
  11. theorem OAI.SKFluctuations.Hierarchy.scalarMinimizer_head_balance_one line 228
  12. theorem OAI.SKFluctuations.Hierarchy.scalarTailJet_filledSquare_le_one line 262
  13. theorem OAI.SKFluctuations.Hierarchy.scalarMinimizer_no_isolated_origin_Ioc line 273
  14. theorem OAI.SKFluctuations.Hierarchy.scalar_first_rise line 325
  15. theorem OAI.SKFluctuations.Hierarchy.scalarMinimizer_no_positive_plateau line 372
  16. theorem OAI.SKFluctuations.Hierarchy.scalarMinimizer_origin_atom_accumulates line 406
  17. theorem OAI.SKFluctuations.Hierarchy.HeatJet.potential_zero_mass_difference line 444
  18. theorem OAI.SKFluctuations.Hierarchy.HeatJet.nonnegativeProfileValue_zero line 461
  19. theorem OAI.SKFluctuations.Hierarchy.scalarProfile_zero_head line 483
  20. theorem OAI.SKFluctuations.Hierarchy.scalarParisiValue_zero_head line 491
  21. theorem OAI.SKFluctuations.Hierarchy.HeatJet.gradient_test_bounds line 531
  22. theorem OAI.SKFluctuations.Hierarchy.HeatJet.gradient_mass_zero_bound line 538
  23. theorem OAI.SKFluctuations.Hierarchy.HeatJet.gradient_square_mass_zero_bound line 549
  24. theorem OAI.SKFluctuations.Hierarchy.HeatJet.massEnergy_eq_mixedSquare line 570
  25. theorem OAI.SKFluctuations.Hierarchy.HeatJet.massEnergy_outer_zero_bound line 578
  26. theorem OAI.SKFluctuations.Hierarchy.HeatJet.massEnergy_integral_zero_tendsto line 588