OAI/Analysis/NodalLength/LocalLength.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SharpNodal.Profiles.smooth_C1_bounded_ball line 291
  2. lemma OAI.SharpNodal.Profiles.recenter_inner_maps line 308
  3. lemma OAI.SharpNodal.Profiles.planeToComplex_rescale line 318
  4. theorem OAI.SharpNodal.Profiles.normalized_small_potential_length line 322
  5. lemma OAI.SharpNodal.Profiles.log_sq_le_inv line 468
  6. lemma OAI.SharpNodal.Profiles.integrable_logParametrix_sq line 479
  7. lemma OAI.SharpNodal.Profiles.integral_abs_mul_le_sqrt line 506
  8. lemma OAI.SharpNodal.Profiles.continuous_sq_integrableOn_ball line 514
  9. lemma OAI.SharpNodal.Profiles.memLp_indicator_ball line 518
  10. lemma OAI.SharpNodal.Profiles.kernel_L2_bound line 526
  11. lemma OAI.SharpNodal.Profiles.small_potential_parametrix line 549
  12. lemma OAI.SharpNodal.Profiles.small_potential_L2_interior line 586
  13. lemma OAI.SharpNodal.Profiles.exists_local_smallness line 638
  14. lemma OAI.SharpNodal.Profiles.bump_smoothOn_extension line 657
  15. lemma OAI.SharpNodal.Profiles.inner_L2_anchor line 685
  16. lemma OAI.SharpNodal.Profiles.sq_integral_ball_mono line 709
  17. theorem OAI.SharpNodal.Profiles.small_potential_L2_length line 714