OAI/Analysis/NodalLength/GradientAnchors.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpNodal.Profiles.partial_germ line 287
2. lemma OAI.SharpNodal.Profiles.laplacian_germ line 290
3. lemma OAI.SharpNodal.Profiles.rconv_comm_real line 298
4. lemma OAI.SharpNodal.Profiles.harmonic_parametrix line 303
5. lemma OAI.SharpNodal.Profiles.integral_norm_bounded_ball line 325
6. lemma OAI.SharpNodal.Profiles.harmonic_gradient_bound line 344
7. lemma OAI.SharpNodal.Profiles.small_potential_gradient_bound line 394
8. lemma OAI.SharpNodal.Profiles.SmallPotential.limit_upper line 450
9. lemma OAI.SharpNodal.Profiles.SmallPotential.limit_partial_bound line 455
10. lemma OAI.SharpNodal.Profiles.SmallPotential.quotient_differentiable line 458
11. lemma OAI.SharpNodal.Profiles.gradient_anchor line 470
12. lemma OAI.SharpNodal.Profiles.partial_rescale_differentiable line 490
13. lemma OAI.SharpNodal.Profiles.gradient_rescale_differentiable line 501
14. lemma OAI.SharpNodal.Profiles.rescaleMap_lipschitz line 507
15. lemma OAI.SharpNodal.Profiles.small_nodal_length_of_translated line 513