OAI/Geometry/Cannon/Beltrami/ContinuousMemLpRestrict.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CannonBeltrami.continuous_memLp_restrict_compact line 51
  2. lemma OAI.CannonBeltrami.partialZ_norm_le line 59
  3. lemma OAI.CannonBeltrami.l2_restrict_integral_norm_sq line 69
  4. theorem OAI.CannonBeltrami.smooth_local_energy_bound line 77
  5. lemma OAI.CannonBeltrami.smooth_partialZ_l2_bound line 95
  6. lemma OAI.CannonBeltrami.smooth_integration_by_parts line 120
  7. lemma OAI.CannonBeltrami.tendsto_l2_test line 134
  8. lemma OAI.CannonBeltrami.integral_test_add_const line 141
  9. lemma OAI.CannonBeltrami.bounded_displacement_test_tendsto line 151
  10. theorem OAI.CannonBeltrami.smooth_limit_weak_derivative line 176
  11. lemma OAI.CannonBeltrami.smooth_partial_integration_by_parts line 203
  12. lemma OAI.CannonBeltrami.compact_test_tendsto line 233
  13. lemma OAI.CannonBeltrami.hasCompactSupport_partials line 253
  14. lemma OAI.CannonHilbert.real_hilbert_biddual_surjective line 268
  15. lemma OAI.CannonHilbert.bounded_weak_closure_compact line 286
  16. theorem OAI.CannonHilbert.bounded_weak_filter_limit line 300
  17. lemma OAI.CannonHilbert.weak_real_eval_tendsto line 320
  18. lemma OAI.CannonHilbert.weak_complex_eval_tendsto line 325
  19. lemma OAI.CannonHilbert.weak_inner_tendsto line 337
  20. theorem OAI.CannonHilbert.strong_weak_inner_tendsto line 342
  21. lemma OAI.CannonHilbert.dominated_toLp_zero line 362
  22. lemma OAI.CannonHilbert.bounded_mul_memLp line 390
  23. lemma OAI.CannonHilbert.integral_mul_eq_inner line 399
  24. lemma OAI.CannonHilbert.weak_integral_test_tendsto line 408
  25. lemma OAI.CannonHilbert.coefficient_test_strong_tendsto line 416
  26. lemma OAI.CannonHilbert.weak_moving_integral_test_tendsto line 447
  27. theorem OAI.CannonBeltrami.local_weak_beltrami_limit line 468