OAI/Geometry/PrescribedPotential/ParameterResolvent.lean

GitHub source file

31 declarations, 0 contain sorry, 0 declared as axioms

Parameter Resolvent.

  1. def OAI.FrozenPoisson.parameterSymbol line 21
  2. lemma OAI.FrozenPoisson.parameterSymbol_temperate line 24
  3. lemma OAI.FrozenPoisson.elliptic_symbol_bound line 44
  4. lemma OAI.FrozenPoisson.parameter_gain_bound line 53
  5. lemma OAI.FrozenPoisson.parameter_zero_bound line 63
  6. lemma OAI.FrozenPoisson.parameter_first_weight line 71
  7. def OAI.FrozenPoisson.parameterResolvent line 99
  8. def OAI.FrozenPoisson.parameterForward line 102
  9. lemma OAI.FrozenPoisson.parameterForward_temperate line 106
  10. lemma OAI.FrozenPoisson.parameterForward_eq line 111
  11. lemma OAI.FrozenPoisson.parameterForward_resolvent line 122
  12. def OAI.FrozenPoisson.parameterGain line 143
  13. lemma OAI.FrozenPoisson.parameterGain_temperate line 146
  14. def OAI.FrozenPoisson.parameterGainBCF line 152
  15. lemma OAI.FrozenPoisson.parameterGainBCF_norm line 158
  16. def OAI.FrozenPoisson.parameterHilbert line 163
  17. lemma OAI.FrozenPoisson.parameterHilbert_bound line 167
  18. lemma OAI.FrozenPoisson.bessel_two_parameterResolvent line 173
  19. lemma OAI.FrozenPoisson.parameterHilbert_realize line 184
  20. lemma OAI.FrozenPoisson.parameterHilbert_equation line 201
  21. def OAI.FrozenPoisson.parameterZeroBCF line 212
  22. def OAI.FrozenPoisson.parameterZero line 217
  23. lemma OAI.FrozenPoisson.parameterZero_bound line 221
  24. lemma OAI.FrozenPoisson.parameterZero_distribution line 228
  25. def OAI.FrozenPoisson.parameterFirstSymbol line 233
  26. lemma OAI.FrozenPoisson.parameterFirstSymbol_temperate line 236
  27. lemma OAI.FrozenPoisson.parameterFirstSymbol_bound line 242
  28. def OAI.FrozenPoisson.parameterFirstBCF line 258
  29. def OAI.FrozenPoisson.parameterFirst line 264
  30. lemma OAI.FrozenPoisson.parameterFirst_bound line 268
  31. lemma OAI.FrozenPoisson.parameterFirst_distribution line 276