OAI/Analysis/NodalLength/MassComparison.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.SharpNodal.Profiles.tsupport_subset_compl_of_zero line 15
  2. lemma OAI.SharpNodal.Profiles.partial_tsupport_outside line 21
  3. lemma OAI.SharpNodal.Profiles.laplacian_const line 30
  4. lemma OAI.SharpNodal.Profiles.laplacian_tsupport_outside line 37
  5. lemma OAI.SharpNodal.Profiles.laplacian_tsupport_subset line 47
  6. lemma OAI.SharpNodal.Profiles.annular_cutoff_support line 57
  7. lemma OAI.SharpNodal.Profiles.annular_cutoff_one line 67
  8. lemma OAI.SharpNodal.Profiles.annular_cutoff_bounds line 72
  9. theorem OAI.SharpNodal.Profiles.exists_profile_cutoffs line 78
  10. lemma OAI.SharpNodal.Profiles.exists_abs_bound line 136
  11. lemma OAI.SharpNodal.Profiles.exists_partial_abs_bound line 142
  12. lemma OAI.SharpNodal.Profiles.exists_partial_abs_bound_on line 151
  13. lemma OAI.SharpNodal.Profiles.tilted_gradient_bound line 161
  14. theorem OAI.SharpNodal.Profiles.cutoff_mass_comparison line 174
  15. theorem OAI.SharpNodal.Profiles.cutoff_mass_comparison_on line 255
  16. def OAI.SharpNodal.Profiles.logRate line 345
  17. lemma OAI.SharpNodal.Profiles.ereal_pos_mul_lt_coe_iff line 347
  18. lemma OAI.SharpNodal.Profiles.ereal_coe_lt_pos_mul_iff line 356
  19. lemma OAI.SharpNodal.Profiles.logRate_lt_iff line 365
  20. lemma OAI.SharpNodal.Profiles.lt_logRate_iff line 373
  21. lemma OAI.SharpNodal.Profiles.logRate_le_iff line 381
  22. lemma OAI.SharpNodal.Profiles.le_logRate_iff line 385
  23. lemma OAI.SharpNodal.Profiles.logRate_ofReal_exp line 389
  24. lemma OAI.SharpNodal.Profiles.logRate_zero line 395
  25. lemma OAI.SharpNodal.Profiles.logRate_mono line 399
  26. lemma OAI.SharpNodal.Profiles.exponential_gap line 405
  27. lemma OAI.SharpNodal.Profiles.no_exponential_gap line 418
  28. def OAI.SharpNodal.Profiles.tiltedMass line 439
  29. lemma OAI.SharpNodal.Profiles.tiltedMass_neg line 443
  30. lemma OAI.SharpNodal.Profiles.integral_square_mass line 449
  31. lemma OAI.SharpNodal.Profiles.cutoff_square_integrable_on line 456
  32. lemma OAI.SharpNodal.Profiles.cutoff_square_mass_lower line 463
  33. lemma OAI.SharpNodal.Profiles.cutoff_square_mass_upper line 476
  34. lemma OAI.SharpNodal.Profiles.smooth_tiltedWeight_on line 492
  35. theorem OAI.SharpNodal.Profiles.tilted_mass_comparison_on line 498