OAI/Geometry/QuadricBundles/Compactness.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.QuadricCounterexample.bounded_hilbert_weak_subsequence line 12
  2. lemma OAI.QuadricCounterexample.isClosed_bounded_positive_coefficients line 35
  3. lemma OAI.QuadricCounterexample.convex_bounded_positive_coefficients line 41
  4. lemma OAI.QuadricCounterexample.bounded_hilbert_weak_subsequence_in line 60
  5. lemma OAI.QuadricCounterexample.isClosed_ae_variable_mem_Lp line 72
  6. lemma OAI.QuadricCounterexample.convex_ae_variable_mem_Lp line 83
  7. lemma OAI.QuadricCounterexample.L2_integrable_of_finite_support line 95
  8. theorem OAI.QuadricCounterexample.supported_positive_coefficients_weak_subsequence line 107
  9. def OAI.QuadricCounterexample.matrixToCoefficients line 167
  10. lemma OAI.QuadricCounterexample.coefficients_matrix_inverse line 173
  11. lemma OAI.QuadricCounterexample.matrix_coefficients_memLp line 176
  12. theorem OAI.QuadricCounterexample.local_quadratic_compactness line 192
  13. lemma OAI.QuadricCounterexample.DiskPshOn.moving_base_mass line 250
  14. lemma OAI.QuadricCounterexample.nonzero_of_average_limit line 272
  15. theorem OAI.QuadricCounterexample.bounded_hilbert_countable_weak_subsequence line 293
  16. theorem OAI.QuadricCounterexample.countable_supported_positive_weak_subsequence line 327
  17. theorem OAI.QuadricCounterexample.countable_local_quadratic_compactness_with_weak line 395