OAI/Geometry/Anticanonical/HilbertEstimates.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Existence estimates for closed Hilbert-space operators and radial cutoff energy.

  1. lemma OAI.NadelHilbert.mem_graph_of_adjoint_pairing line 22
  2. theorem OAI.NadelHilbert.exists_solution_of_adjoint_estimate line 65
  3. def OAI.NadelHilbert.closedKernel line 115
  4. lemma OAI.NadelHilbert.mem_closedKernel_iff line 119
  5. lemma OAI.NadelHilbert.isClosed_closedKernel line 130
  6. theorem OAI.NadelHilbert.exists_solution_of_complex_estimate line 137
  7. theorem OAI.NadelHilbert.exists_solution_with_all_bounds line 188
  8. theorem OAI.SingularCutoff.cutoff_energy_bound line 265