OAI/Analysis/HotSpots/Pullback.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.StrictHotSpots.Conformal.complex_real_inner_mul line 12
  2. lemma OAI.StrictHotSpots.Conformal.plane_inner_gradient_comp line 19
  3. lemma OAI.StrictHotSpots.Conformal.plane_dirichlet_pair line 27
  4. lemma OAI.StrictHotSpots.Conformal.inner_grad_toH1 line 39
  5. lemma OAI.StrictHotSpots.Conformal.inner_grad_test line 48
  6. lemma OAI.StrictHotSpots.Conformal.transportTest_dirichlet_pair line 62
  7. lemma OAI.StrictHotSpots.Conformal.transportTest_mixed_grad line 80
  8. lemma OAI.StrictHotSpots.Conformal.transportH10_mixed_grad line 92
  9. lemma OAI.StrictHotSpots.Conformal.smooth_pair_grad line 127
  10. lemma OAI.StrictHotSpots.Conformal.inner_sum_pair line 138
  11. lemma OAI.StrictHotSpots.Conformal.inner_H1grad_add line 148
  12. lemma OAI.StrictHotSpots.Conformal.affine_grad_pair line 154
  13. lemma OAI.StrictHotSpots.Conformal.pull_affine_value line 173
  14. lemma OAI.StrictHotSpots.Conformal.value_add_H10 line 180
  15. lemma OAI.StrictHotSpots.Conformal.ae_lp_sums line 183
  16. lemma OAI.StrictHotSpots.Conformal.affine_value_ae line 190
  17. lemma OAI.StrictHotSpots.Conformal.isometry_value_pair line 206
  18. lemma OAI.StrictHotSpots.Conformal.affine_value_pair line 217
  19. lemma OAI.StrictHotSpots.Conformal.potentialMeasure_bounded line 241
  20. lemma OAI.StrictHotSpots.Conformal.subcritical_reindex line 250
  21. def OAI.StrictHotSpots.Conformal.ClosedDiskChart.potential line 260
  22. def OAI.StrictHotSpots.Conformal.ClosedDiskChart.densityBound line 261
  23. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.density_bound line 263
  24. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.densityBound_ne_top line 268
  25. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.potential_finite line 270
  26. theorem OAI.StrictHotSpots.Conformal.ClosedDiskChart.subcritical line 275
  27. theorem OAI.StrictHotSpots.Conformal.ClosedDiskChart.operator_norm_lt_one line 294
  28. lemma OAI.StrictHotSpots.Conformal.observe_inner line 313
  29. lemma OAI.StrictHotSpots.Conformal.smooth_H10_value_pair line 332
  30. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.potential_diskMap line 347
  31. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.smooth_mixed_mass line 350
  32. lemma OAI.StrictHotSpots.Conformal.ClosedDiskChart.smooth_pull_weak line 373
  33. theorem OAI.StrictHotSpots.Conformal.ClosedDiskChart.smooth_K_representation line 391
  34. lemma OAI.StrictHotSpots.laplacian_continuousOn line 417
  35. lemma OAI.StrictHotSpots.eigenfunction_helmholtz line 428
  36. lemma OAI.StrictHotSpots.directionalDerivative_commute line 455
  37. lemma OAI.StrictHotSpots.directionalDerivative_congr line 469
  38. lemma OAI.StrictHotSpots.laplacian_directionalDerivative line 475
  39. lemma OAI.StrictHotSpots.eigenfunction_derivative_helmholtz line 503
  40. lemma OAI.StrictHotSpots.closed_directional_eq line 523
  41. theorem OAI.StrictHotSpots.Conformal.ClosedDiskChart.gradient_K_representation line 535