OAI/Geometry/PrescribedPotential/FrozenPoisson.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

Frozen Poisson.

  1. lemma OAI.FrozenPoisson.posDef_factor line 21
  2. def OAI.FrozenPoisson.symbol line 34
  3. lemma OAI.FrozenPoisson.trace_rankOne_factor line 37
  4. lemma OAI.FrozenPoisson.symbol_eq_norm_sq line 54
  5. def OAI.FrozenPoisson.factorMap line 62
  6. lemma OAI.FrozenPoisson.factorMap_injective line 65
  7. lemma OAI.FrozenPoisson.symbol_eq_factorMap line 76
  8. lemma OAI.FrozenPoisson.symbol_nonneg line 80
  9. lemma OAI.FrozenPoisson.symbol_temperate line 86
  10. def OAI.FrozenPoisson.inverseSymbol line 94
  11. lemma OAI.FrozenPoisson.inverseSymbol_temperate line 97
  12. lemma OAI.FrozenPoisson.inverseSymbol_weighted_bounded line 112
  13. def OAI.FrozenPoisson.shifted line 130
  14. def OAI.FrozenPoisson.resolvent line 135
  15. lemma OAI.FrozenPoisson.forward_temperate line 139
  16. lemma OAI.FrozenPoisson.shifted_resolvent line 144
  17. lemma OAI.FrozenPoisson.resolvent_shifted line 157
  18. theorem OAI.FrozenPoisson.resolvent_memSobolev line 171
  19. theorem OAI.FrozenPoisson.frozen_sobolev_resolvent line 190
  20. def OAI.FrozenPoisson.rankTwo line 204
  21. lemma OAI.FrozenPoisson.bilin_expansion line 206
  22. lemma OAI.FrozenPoisson.second_symbol_expansion line 220
  23. lemma OAI.FrozenPoisson.second_deriv_multiplier line 237
  24. lemma OAI.FrozenPoisson.multiplier_sub line 256
  25. def OAI.FrozenPoisson.differentialWithBasis line 273
  26. lemma OAI.FrozenPoisson.differentialWithBasis_fourier line 278
  27. def OAI.FrozenPoisson.frozenDifferential line 316
  28. lemma OAI.FrozenPoisson.frozenDifferential_fourier line 320
  29. lemma OAI.FrozenPoisson.shifted_eq_identity_sub line 328
  30. theorem OAI.FrozenPoisson.frozen_differential_sobolev_resolvent line 340
  31. def OAI.FrozenPoisson.smoothDifferentialWithBasis line 351
  32. lemma OAI.FrozenPoisson.smooth_second_deriv line 356
  33. lemma OAI.FrozenPoisson.smoothDifferentialWithBasis_apply line 362
  34. def OAI.FrozenPoisson.complexify line 374
  35. lemma OAI.FrozenPoisson.complexify_deriv line 377
  36. lemma OAI.FrozenPoisson.weak_complexify_deriv line 387
  37. lemma OAI.FrozenPoisson.differentialWithBasis_real line 392
  38. lemma OAI.FrozenPoisson.frozenDifferential_real_trace line 413