OAI/Analysis/NodalLength/Similarity.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.SharpNodal.Profiles.regularizedCoefficient line 246
2. lemma OAI.SharpNodal.Profiles.smooth_normSq line 249
3. lemma OAI.SharpNodal.Profiles.csmooth_regularizedCoefficient line 254
4. lemma OAI.SharpNodal.Profiles.norm_regularizedCoefficient_le line 263
5. lemma OAI.SharpNodal.Profiles.regularizedCoefficient_residual line 273
6. lemma OAI.SharpNodal.Profiles.norm_regularizedCoefficient_residual_le line 284
7. lemma OAI.SharpNodal.Profiles.csmooth_barPartial line 306
8. lemma OAI.SharpNodal.Profiles.norm_cutoff_mul_le line 309
9. def OAI.SharpNodal.Profiles.similarityCutoff line 318
10. def OAI.SharpNodal.Profiles.correctionCutoff line 319
11. lemma OAI.SharpNodal.Profiles.norm_exp_neg_le line 321
12. theorem OAI.SharpNodal.Profiles.approximate_similarity line 327
13. lemma OAI.SharpNodal.Profiles.normal_family_fixed_disk line 397
14. lemma OAI.SharpNodal.Profiles.norm_exp_sub_one_le_exp_norm line 455
15. theorem OAI.SharpNodal.Profiles.sequence_similarity line 459