OAI/Analysis/NodalLength/Persistence.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.SharpNodal.Profiles.local_potential_profile_affine_sup_bound line 178
2. def OAI.SharpNodal.Profiles.extendedGridCenter line 265
3. lemma OAI.SharpNodal.Profiles.exists_extendedGridCenter line 268
4. lemma OAI.SharpNodal.Profiles.tendsto_gridScale line 289
5. lemma OAI.SharpNodal.Profiles.potential_affine_coefficient_limits line 303
6. theorem OAI.SharpNodal.Profiles.profile_small_affine_grid_gap line 326
7. lemma OAI.SharpNodal.Profiles.profile_nonconstant_of_positive_gap line 389
8. lemma OAI.SharpNodal.Profiles.local_affine_profile_transfer line 428
9. lemma OAI.SharpNodal.Profiles.zero_tiltedMass_centered line 492
10. lemma OAI.SharpNodal.Profiles.zero_tilted_excess_centered line 497
11. lemma OAI.SharpNodal.Profiles.grid_child_closedBall_subset_two line 504
12. theorem OAI.SharpNodal.Profiles.sequence_persistence_square line 517