OAI/Geometry/PolarProducts/PotentialForms.lean

GitHub source file

37 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ComplexPotential.dcOp line 37
  2. def OAI.ComplexPotential.dc line 40
  3. def OAI.ComplexPotential.ddc line 43
  4. theorem OAI.ComplexPotential.dcOp_apply line 45
  5. theorem OAI.ComplexPotential.dc_apply line 51
  6. theorem OAI.ComplexPotential.contDiffAt_dc line 54
  7. theorem OAI.ComplexPotential.contDiff_dc line 59
  8. theorem OAI.ComplexPotential.fderiv_dc line 64
  9. theorem OAI.ComplexPotential.ddc_apply line 71
  10. theorem OAI.ComplexPotential.ddc_skew line 78
  11. theorem OAI.ComplexPotential.contDiffAt_ddc line 81
  12. theorem OAI.ComplexPotential.contDiff_ddc line 87
  13. theorem OAI.ComplexPotential.ddc_closed line 91
  14. theorem OAI.ComplexPotential.ddc_complex_line line 96
  15. def OAI.ComplexPotential.IsPSHAt line 104
  16. theorem OAI.ComplexPotential.dc_congr line 107
  17. theorem OAI.ComplexPotential.ddc_congr line 111
  18. theorem OAI.ComplexPotential.dc_add line 116
  19. theorem OAI.ComplexPotential.ddc_add line 121
  20. def OAI.ComplexPotential.standardTensor line 146
  21. theorem OAI.ComplexPotential.standardTensor_apply line 148
  22. theorem OAI.ComplexPotential.dc_norm_sq line 151
  23. theorem OAI.ComplexPotential.ddc_norm_sq line 160
  24. theorem OAI.ComplexPotential.standardTensor_complex_line line 180
  25. theorem OAI.ComplexPotential.isInvertible_of_positive_complex_line line 184
  26. theorem OAI.ComplexPotential.isInvertible_ddc_norm_sq_add line 206
  27. theorem OAI.ComplexPotential.dc_const line 233
  28. theorem OAI.ComplexPotential.ddc_const line 237
  29. theorem OAI.ComplexPotential.dc_const_smul line 241
  30. theorem OAI.ComplexPotential.ddc_const_smul line 249
  31. theorem OAI.ComplexPotential.ddc_neg line 262
  32. theorem OAI.ComplexPotential.ddc_sub line 267
  33. theorem OAI.ComplexPotential.ddc_add_const line 273
  34. theorem OAI.ComplexPotential.ddc_sub_const line 278
  35. theorem OAI.ComplexPotential.IsPSHAt.add line 283
  36. theorem OAI.ComplexPotential.IsPSHAt.const_smul line 290
  37. theorem OAI.ComplexPotential.IsPSHAt.sub_const line 297