OAI/Analysis/HotSpots/Cauchy.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.StrictHotSpots.zeroExtension_hasFDerivAt line 15
  2. lemma OAI.StrictHotSpots.zeroExtension_continuousOn line 55
  3. lemma OAI.StrictHotSpots.weakGradient_of_continuous_derivative line 62
  4. lemma OAI.StrictHotSpots.zeroExtension_H1 line 104
  5. lemma OAI.StrictHotSpots.integral_indicator_local line 136
  6. lemma OAI.StrictHotSpots.zeroExtension_weakEquation line 145
  7. theorem OAI.StrictHotSpots.interior_eigenfunction_zero_of_boundary_jet line 176
  8. lemma OAI.StrictHotSpots.nonzero_real_functional_surjective line 218
  9. lemma OAI.StrictHotSpots.frontier_level_zero line 231
  10. lemma OAI.StrictHotSpots.regular_level_mem_frontier line 248
  11. theorem OAI.StrictHotSpots.SmoothBoundary.locally_const_of_boundary_zero_jet line 272
  12. theorem OAI.StrictHotSpots.Conformal.ClosedDiskChart.eq_zero_of_boundary_closedGradient line 363
  13. def OAI.StrictHotSpots.closedPatchEigenSpace line 396
  14. def OAI.StrictHotSpots.closedPatchEval line 414
  15. lemma OAI.StrictHotSpots.closedPatchEval_injective line 420
  16. theorem OAI.StrictHotSpots.closedPatchEigenSpace_finrank_le_one line 449