OAI/Analysis/NodalLength/Multipliers.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.SharpNodal.Profiles.locallyIntegrable_logNorm line 230
2. lemma OAI.SharpNodal.Profiles.smooth_rconv_local line 236
3. lemma OAI.SharpNodal.Profiles.partial_rconv_local line 240
4. lemma OAI.SharpNodal.Profiles.laplacian_rconv_local line 253
5. def OAI.SharpNodal.Profiles.newtonPotential line 265
6. lemma OAI.SharpNodal.Profiles.smooth_newtonPotential line 268
7. lemma OAI.SharpNodal.Profiles.laplacian_newtonPotential line 272
8. lemma OAI.SharpNodal.Profiles.partial_newtonPotential line 285
9. lemma OAI.SharpNodal.Profiles.integral_supported_ball line 305
10. lemma OAI.SharpNodal.Profiles.integral_mul_norm_bound line 316
11. lemma OAI.SharpNodal.Profiles.abs_newtonPotential_bound line 328
12. lemma OAI.SharpNodal.Profiles.locallyIntegrable_logGradient_component line 348
13. lemma OAI.SharpNodal.Profiles.abs_partial_newtonPotential_bound line 358
14. theorem OAI.SharpNodal.Profiles.newton_operator_bounds line 385
15. def OAI.SharpNodal.Profiles.NewtonControl line 407
16. lemma OAI.SharpNodal.Profiles.exists_newtonControl line 413
17. def OAI.SharpNodal.Profiles.neumannTerm line 415
18. def OAI.SharpNodal.Profiles.multiplierApprox line 419
19. lemma OAI.SharpNodal.Profiles.smooth_neumannTerm line 422
20. lemma OAI.SharpNodal.Profiles.smooth_multiplierApprox line 429
21. lemma OAI.SharpNodal.Profiles.multiplierApprox_zero line 433
22. lemma OAI.SharpNodal.Profiles.multiplierApprox_succ line 436
23. lemma OAI.SharpNodal.Profiles.laplacian_neumannTerm_succ line 440
24. lemma OAI.SharpNodal.Profiles.multiplierApprox_equation line 450
25. lemma OAI.SharpNodal.Profiles.neumannTerm_bounds line 461
26. lemma OAI.SharpNodal.Profiles.geometric_succ_sum_le line 485
27. lemma OAI.SharpNodal.Profiles.multiplierApprox_bounds line 495
28. def OAI.SharpNodal.Profiles.multiplierLimit line 523
29. lemma OAI.SharpNodal.Profiles.multiplierLimit_hasFDerivAt line 526
30. lemma OAI.SharpNodal.Profiles.multiplierLimit_convergence line 545
31. lemma OAI.SharpNodal.Profiles.multiplierLimit_bounds line 569
32. def OAI.SharpNodal.Profiles.multiplierCutoff line 589
33. def OAI.SharpNodal.Profiles.positiveApprox line 591
34. lemma OAI.SharpNodal.Profiles.smooth_positiveApprox line 594
35. lemma OAI.SharpNodal.Profiles.positiveApprox_eq line 598
36. lemma OAI.SharpNodal.Profiles.positiveApprox_eventuallyEq line 604
37. lemma OAI.SharpNodal.Profiles.positiveApprox_bound line 609
38. lemma OAI.SharpNodal.Profiles.positiveApprox_lower line 626
39. lemma OAI.SharpNodal.Profiles.positiveApprox_equation line 637
40. lemma OAI.SharpNodal.Profiles.positiveApprox_partial line 643
41. lemma OAI.SharpNodal.Profiles.quotient_laplacian line 648