OAI/NumberTheory/Catalan/Energy/BarrierGlobalMaxReduction.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.InternalCatalan.GlobalMaxReduction.le_on_Icc_of_critical_le line 14
2. theorem OAI.InternalCatalan.GlobalMaxReduction.exists_left_cutoff line 33
3. theorem OAI.InternalCatalan.GlobalMaxReduction.exists_right_cutoff line 39
4. theorem OAI.InternalCatalan.GlobalMaxReduction.le_on_Ioo_of_limits_of_critical_le line 45
5. theorem OAI.InternalCatalan.GlobalMaxReduction.le_on_Ico_of_limit_of_critical_le line 61
6. theorem OAI.InternalCatalan.GlobalMaxReduction.le_on_Ioo_of_stationary_cover line 76
7. theorem OAI.InternalCatalan.GlobalMaxReduction.le_on_two_components_of_stationary_cover line 86