OAI/Analysis/StrictMeans/GreenIdentity.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.StrictInverseFirstPower.compact_integral_deriv_zero line 84
  2. lemma OAI.StrictInverseFirstPower.compact_second_deriv_green line 91
  3. def OAI.StrictInverseFirstPower.realPlanePartial line 110
  4. lemma OAI.StrictInverseFirstPower.contDiff_realPlanePartial line 113
  5. lemma OAI.StrictInverseFirstPower.compact_realPlanePartial line 117
  6. lemma OAI.StrictInverseFirstPower.deriv_vertical_line line 120
  7. lemma OAI.StrictInverseFirstPower.deriv_horizontal_line line 125
  8. lemma OAI.StrictInverseFirstPower.compact_vertical_line line 130
  9. lemma OAI.StrictInverseFirstPower.compact_horizontal_line line 135
  10. lemma OAI.StrictInverseFirstPower.compact_plane_second_horizontal_zero line 140
  11. lemma OAI.StrictInverseFirstPower.compact_plane_second_vertical_green line 156
  12. lemma OAI.StrictInverseFirstPower.compact_plane_weight_integrable line 171
  13. lemma OAI.StrictInverseFirstPower.compact_plane_horizontal_integral_zero line 177
  14. lemma OAI.StrictInverseFirstPower.compact_plane_green_assemble line 190
  15. lemma OAI.StrictInverseFirstPower.compact_plane_horizontal_green line 207
  16. def OAI.StrictInverseFirstPower.planePartial line 230
  17. def OAI.StrictInverseFirstPower.planeLaplacian line 232
  18. lemma OAI.StrictInverseFirstPower.planePartial_comp_holomorphic line 235
  19. lemma OAI.StrictInverseFirstPower.second_planePartial_comp_holomorphic line 243
  20. lemma OAI.StrictInverseFirstPower.real_bilinear_complex_trace line 265
  21. lemma OAI.StrictInverseFirstPower.planeLaplacian_comp_holomorphic line 278
  22. lemma OAI.StrictInverseFirstPower.planePartial_contDiff line 308
  23. lemma OAI.StrictInverseFirstPower.partial_realProd_comp line 312
  24. lemma OAI.StrictInverseFirstPower.laplacian_realProd_comp line 322
  25. lemma OAI.StrictInverseFirstPower.integral_realProd_above line 334
  26. lemma OAI.StrictInverseFirstPower.compact_complex_horizontal_green line 352
  27. lemma OAI.StrictInverseFirstPower.planeLaplacian_congr_nhds line 368