OAI/Analysis/NodalLength/HolomorphicGradient.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpNodal.Profiles.partial_quotient line 254
2. lemma OAI.SharpNodal.Profiles.abs_partial_le_norm_gradient line 271
3. lemma OAI.SharpNodal.Profiles.norm_gradient_le line 277
4. def OAI.SharpNodal.Profiles.conductivityDrift line 281
5. lemma OAI.SharpNodal.Profiles.csmooth_conductivityDrift line 284
6. lemma OAI.SharpNodal.Profiles.conductivityDrift_bound line 290
7. lemma OAI.SharpNodal.Profiles.quotient_barPartial_error line 304
8. lemma OAI.SharpNodal.Profiles.quotient_partial_bound line 318
9. structure OAI.SharpNodal.Profiles.SmallPotential line 349
10. lemma OAI.SharpNodal.Profiles.SmallPotential.δ_lt line 364
11. lemma OAI.SharpNodal.Profiles.SmallPotential.ratio_nonneg line 365
12. lemma OAI.SharpNodal.Profiles.SmallPotential.ratio_le line 366
13. lemma OAI.SharpNodal.Profiles.SmallPotential.approx_lower line 368
14. lemma OAI.SharpNodal.Profiles.SmallPotential.approx_smooth line 372
15. lemma OAI.SharpNodal.Profiles.SmallPotential.approx_ne line 374
16. lemma OAI.SharpNodal.Profiles.SmallPotential.approx_partial_bound line 376
17. lemma OAI.SharpNodal.Profiles.SmallPotential.limit_lower line 382
18. lemma OAI.SharpNodal.Profiles.SmallPotential.limit_differentiable line 390
19. lemma OAI.SharpNodal.Profiles.SmallPotential.approx_converges line 395
20. lemma OAI.SharpNodal.Profiles.SmallPotential.quotient_gradient_converges line 411
21. lemma OAI.SharpNodal.Profiles.SmallPotential.approx_equation line 428
22. lemma OAI.SharpNodal.Profiles.SmallPotential.term_bound line 432
23. theorem OAI.SharpNodal.Profiles.SmallPotential.holomorphic_gradient line 437