OAI/Analysis/NodalLength/Descent.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpNodal.Profiles.profile_zero_of_inner_rate line 156
2. lemma OAI.SharpNodal.Profiles.tiltedMass_linear_centered line 179
3. lemma OAI.SharpNodal.Profiles.zero_profile_forces_growth line 187
4. lemma OAI.SharpNodal.Profiles.zero_profile_tilt_contradiction line 274
5. theorem OAI.SharpNodal.Profiles.sequence_large_slope_impossible line 316
6. structure OAI.SharpNodal.Profiles.UnitWave line 375
7. def OAI.SharpNodal.Profiles.UnitWave.excess line 388
8. def OAI.SharpNodal.Profiles.UnitWave.growth line 391
9. lemma OAI.SharpNodal.Profiles.UnitWave.excess_nonneg line 394
10. theorem OAI.SharpNodal.Profiles.large_slope_forces_growth line 399
11. lemma OAI.SharpNodal.Profiles.descent_smallness line 482
12. theorem OAI.SharpNodal.Profiles.one_step_descent line 509