OAI/Analysis/NodalLength/ComplexDerivatives.lean

GitHub source file

36 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SharpNodal.Profiles.complexPartial line 240
  2. def OAI.SharpNodal.Profiles.barPartial line 243
  3. abbrev OAI.SharpNodal.Profiles.CSmooth line 246
  4. lemma OAI.SharpNodal.Profiles.csmooth_partial line 248
  5. lemma OAI.SharpNodal.Profiles.csmooth_ofReal line 252
  6. lemma OAI.SharpNodal.Profiles.complexPartial_ofReal line 255
  7. lemma OAI.SharpNodal.Profiles.complexPartial_add line 260
  8. lemma OAI.SharpNodal.Profiles.complexPartial_mul line 268
  9. lemma OAI.SharpNodal.Profiles.complexPartial_const_mul line 277
  10. lemma OAI.SharpNodal.Profiles.complexPartial_sub line 283
  11. lemma OAI.SharpNodal.Profiles.barPartial_add line 291
  12. lemma OAI.SharpNodal.Profiles.barPartial_sub line 295
  13. lemma OAI.SharpNodal.Profiles.barPartial_mul line 299
  14. lemma OAI.SharpNodal.Profiles.barPartial_const_mul line 303
  15. def OAI.SharpNodal.Profiles.complexGradient line 307
  16. lemma OAI.SharpNodal.Profiles.csmooth_gradient line 310
  17. lemma OAI.SharpNodal.Profiles.barPartial_gradient line 313
  18. def OAI.SharpNodal.Profiles.cauchyPotential line 335
  19. lemma OAI.SharpNodal.Profiles.smooth_real_component line 339
  20. lemma OAI.SharpNodal.Profiles.smooth_imag_component line 342
  21. lemma OAI.SharpNodal.Profiles.compact_real_component line 345
  22. lemma OAI.SharpNodal.Profiles.compact_imag_component line 348
  23. lemma OAI.SharpNodal.Profiles.csmooth_cauchyPotential line 351
  24. lemma OAI.SharpNodal.Profiles.barPartial_cauchyPotential line 358
  25. lemma OAI.SharpNodal.Profiles.norm_complexGradient_le line 373
  26. lemma OAI.SharpNodal.Profiles.norm_cauchyPotential_le line 381
  27. lemma OAI.SharpNodal.Profiles.complexPartial_exp line 408
  28. lemma OAI.SharpNodal.Profiles.barPartial_exp line 413
  29. lemma OAI.SharpNodal.Profiles.complexPartial_neg line 417
  30. lemma OAI.SharpNodal.Profiles.barPartial_neg line 422
  31. lemma OAI.SharpNodal.Profiles.barPartial_similarity line 426
  32. def OAI.SharpNodal.Profiles.complexToPlane line 435
  33. def OAI.SharpNodal.Profiles.planeToComplex line 437
  34. lemma OAI.SharpNodal.Profiles.complexToPlane_one line 439
  35. lemma OAI.SharpNodal.Profiles.complexToPlane_I line 443
  36. lemma OAI.SharpNodal.Profiles.holomorphic_of_barPartial_eq_zero line 447