OAI/Analysis/HotSpots/Multiplicity.lean

GitHub source file

64 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.StrictHotSpots.InteriorNodal.minimizer_zero_of_open_zero line 13
  2. lemma OAI.StrictHotSpots.InteriorNodal.integral_indicator_pos line 26
  3. lemma OAI.StrictHotSpots.InteriorNodal.restriction_energy line 50
  4. lemma OAI.StrictHotSpots.InteriorNodal.disjoint_indicator_norm_sq line 69
  5. lemma OAI.StrictHotSpots.InteriorNodal.disjoint_restriction_combination_energy line 80
  6. lemma OAI.StrictHotSpots.InteriorNodal.gradient_neg_fun line 113
  7. lemma OAI.StrictHotSpots.InteriorNodal.eigenfunction_neg line 117
  8. lemma OAI.StrictHotSpots.InteriorNodal.eigenfunction_has_negative line 127
  9. lemma OAI.StrictHotSpots.InteriorNodal.eigenfunction_has_positive line 140
  10. lemma OAI.StrictHotSpots.InteriorNodal.no_two_positive_regions line 149
  11. lemma OAI.StrictHotSpots.InteriorNodal.positive_set_connected line 202
  12. lemma OAI.StrictHotSpots.InteriorNodal.negative_set_connected line 234
  13. lemma OAI.StrictHotSpots.InteriorBoundarySign.gap_test line 256
  14. lemma OAI.StrictHotSpots.InteriorBoundarySign.equation_test line 282
  15. lemma OAI.StrictHotSpots.InteriorBoundarySign.positivePart_square line 297
  16. lemma OAI.StrictHotSpots.InteriorBoundarySign.positivePart_memLp line 301
  17. lemma OAI.StrictHotSpots.InteriorBoundarySign.nonpos_of_boundary_nonpos line 314
  18. lemma OAI.StrictHotSpots.InteriorBoundarySign.zero_of_boundary_nonpos line 347
  19. lemma OAI.StrictHotSpots.InteriorBoundarySign.exists_boundary_pos line 364
  20. lemma OAI.StrictHotSpots.InteriorBoundarySign.eigen_neg line 371
  21. lemma OAI.StrictHotSpots.InteriorBoundarySign.exists_boundary_neg line 382
  22. lemma OAI.StrictHotSpots.PositiveWeight.continuous_integrable line 409
  23. lemma OAI.StrictHotSpots.PositiveWeight.product_integrable line 413
  24. def OAI.StrictHotSpots.PositiveWeight.momentLinear line 416
  25. def OAI.StrictHotSpots.PositiveWeight.moment line 424
  26. lemma OAI.StrictHotSpots.PositiveWeight.moment_apply line 433
  27. def OAI.StrictHotSpots.PositiveWeight.probe line 435
  28. lemma OAI.StrictHotSpots.PositiveWeight.dual_moment line 447
  29. lemma OAI.StrictHotSpots.PositiveWeight.integral_sq_pos line 455
  30. lemma OAI.StrictHotSpots.PositiveWeight.moment_surjective line 472
  31. def OAI.StrictHotSpots.PositiveWeight.positive line 494
  32. lemma OAI.StrictHotSpots.PositiveWeight.positive_convex line 496
  33. lemma OAI.StrictHotSpots.PositiveWeight.positive_open line 505
  34. theorem OAI.StrictHotSpots.PositiveWeight.exists_positive_annihilator line 521
  35. theorem OAI.StrictHotSpots.PositiveWeight.exists_circle_weight line 593
  36. lemma OAI.StrictHotSpots.PlanarTopology.boundary_halfPlane line 627
  37. lemma OAI.StrictHotSpots.PlanarTopology.log_difference line 636
  38. lemma OAI.StrictHotSpots.PlanarTopology.square_log line 659
  39. theorem OAI.StrictHotSpots.PlanarTopology.disk_paths_cross line 672
  40. lemma OAI.StrictHotSpots.PlanarTopology.arg_product_rightHalfPlane line 725
  41. lemma OAI.StrictHotSpots.PlanarTopology.log_difference_im line 737
  42. lemma OAI.StrictHotSpots.PlanarTopology.no_positive_chord_ratio line 754
  43. theorem OAI.StrictHotSpots.PlanarTopology.disk_paths_cross_chord line 779
  44. lemma OAI.StrictHotSpots.PlanarTopology.disk_positive_open line 821
  45. lemma OAI.StrictHotSpots.PlanarTopology.join_positive_interior line 827
  46. lemma OAI.StrictHotSpots.PlanarTopology.join_positive_closedDisk line 849
  47. theorem OAI.StrictHotSpots.PlanarTopology.no_alternating_boundary_signs line 865
  48. lemma OAI.StrictHotSpots.CircleSigns.separating_cosine line 911
  49. lemma OAI.StrictHotSpots.CircleSigns.separating_cosine_pos line 920
  50. lemma OAI.StrictHotSpots.CircleSigns.separating_cosine_nonpos line 930
  51. lemma OAI.StrictHotSpots.CircleSigns.positive_points_sandwich line 947
  52. theorem OAI.StrictHotSpots.CircleSigns.moment_sign_changes line 973
  53. lemma OAI.StrictHotSpots.PlanarTopology.sine_triple_identity line 1056
  54. lemma OAI.StrictHotSpots.PlanarTopology.chord_exp_det line 1073
  55. lemma OAI.StrictHotSpots.PlanarTopology.angles_no_alternation line 1082
  56. lemma OAI.StrictHotSpots.CircleSigns.periodic_weighted_signs line 1119
  57. lemma OAI.StrictHotSpots.CircleSigns.circle_trace_continuous line 1144
  58. theorem OAI.StrictHotSpots.CircleSigns.disk_moments_nonzero line 1153
  59. def OAI.StrictHotSpots.CircleSigns.weightedMoment line 1201
  60. theorem OAI.StrictHotSpots.CircleSigns.disk_family_finrank_le_two line 1221
  61. def OAI.StrictHotSpots.closedScalarEval line 1270
  62. theorem OAI.StrictHotSpots.closedEigenSpace_family_card line 1279
  63. theorem OAI.StrictHotSpots.closedEigenSpace_finrank_le_two line 1363
  64. theorem OAI.StrictHotSpots.Conformal.ClosedDiskChart.hasFDerivWithinAt_zero_of_closedGradient_zero line 1395