OAI/Geometry/QuadricBundles/WeakLimits.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.QuadricCounterexample.tendsto_dual_of_tendsto_inner line 13
  2. lemma OAI.QuadricCounterexample.tendsto_real_dual_of_tendsto_inner line 26
  3. lemma OAI.QuadricCounterexample.mem_closed_convex_of_weak_limit line 38
  4. lemma OAI.QuadricCounterexample.isClosed_ae_linear_constraint line 54
  5. lemma OAI.QuadricCounterexample.convex_ae_linear_constraint line 69
  6. theorem OAI.QuadricCounterexample.ae_linear_constraint_of_weak_limit line 82
  7. def OAI.QuadricCounterexample.setAverageL2Functional line 94
  8. lemma OAI.QuadricCounterexample.setAverageL2Functional_apply line 103
  9. lemma OAI.QuadricCounterexample.tendsto_setAverage_of_tendsto_inner line 124
  10. theorem OAI.QuadricCounterexample.ae_submean_of_weak_limit line 135
  11. theorem OAI.QuadricCounterexample.DiskPshOn.base_submean line 154
  12. lemma OAI.QuadricCounterexample.isClosed_ae_mem_Lp line 208
  13. lemma OAI.QuadricCounterexample.convex_ae_mem_Lp line 219
  14. def OAI.QuadricCounterexample.coefficientsToMatrix line 231
  15. lemma OAI.QuadricCounterexample.continuous_coefficientsToMatrix line 237
  16. def OAI.QuadricCounterexample.coefficientsQuadraticCLM line 241
  17. lemma OAI.QuadricCounterexample.coefficientsQuadraticCLM_apply line 246
  18. lemma OAI.QuadricCounterexample.weak_coefficients_positive line 250
  19. lemma OAI.QuadricCounterexample.DiskPshOn.base_average_submean line 266
  20. lemma OAI.QuadricCounterexample.weak_quadratic_averages line 279
  21. lemma OAI.QuadricCounterexample.weak_quadratic_submean line 298
  22. theorem OAI.QuadricCounterexample.weak_quadratic_psh_representative line 335