OAI/Geometry/CubicTorus/Compactness/BVWeyl.lean

GitHub source file

41 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CubicTorus.planarMollifier line 17
  2. lemma OAI.CubicTorus.planarMollifier_tendsto line 23
  3. lemma OAI.CubicTorus.planarMollifier_ratio line 28
  4. theorem OAI.CubicTorus.weak_harmonic_radial_reproduction line 33
  5. theorem OAI.CubicTorus.weak_harmonic_local_representative line 84
  6. lemma OAI.CubicTorus.second_deriv_convolution_le line 118
  7. lemma OAI.CubicTorus.continuous_compact_norm_bound line 157
  8. lemma OAI.CubicTorus.smooth_compact_hessian_bound line 166
  9. lemma OAI.CubicTorus.quadratic_taylor_bound line 187
  10. lemma OAI.CubicTorus.compact_convolution_affine_approximation line 213
  11. theorem OAI.CubicTorus.weak_harmonic_affine_approximation line 237
  12. lemma OAI.CubicTorus.planar_affine_error_energy line 255
  13. theorem OAI.CubicTorus.weak_harmonic_height_decay line 292
  14. lemma OAI.CubicTorus.weak_harmonic_comp_isometry line 321
  15. theorem OAI.CubicTorus.plane_weak_harmonic_height_decay line 343
  16. lemma OAI.CubicTorus.L2_norm_sq_integral line 387
  17. lemma OAI.CubicTorus.L2_toLp_dist_sq line 393
  18. lemma OAI.CubicTorus.integral_mul_eq_restrict_of_tsupport line 401
  19. theorem OAI.CubicTorus.L2_weak_harmonic_limit line 414
  20. lemma OAI.CubicTorus.L2_zero_extension_bounds line 446
  21. lemma OAI.CubicTorus.L2_energy_triangle line 477
  22. theorem OAI.CubicTorus.planar_H1_harmonic_approximation line 492
  23. lemma OAI.CubicTorus.lipschitz_bounded_mul line 581
  24. lemma OAI.CubicTorus.fderiv_mul_sq_bound line 602
  25. lemma OAI.CubicTorus.fderiv_mul_sq_bound_of_bounds line 614
  26. lemma OAI.CubicTorus.integrable_integral_le_of_support_bound line 626
  27. theorem OAI.CubicTorus.lipschitz_cutoff_H1 line 637
  28. def OAI.CubicTorus.planeProductCoordinates line 696
  29. lemma OAI.CubicTorus.planeProductCoordinates_measurePreserving line 699
  30. def OAI.CubicTorus.planeSquare line 702
  31. lemma OAI.CubicTorus.isCompact_planeSquare line 705
  32. lemma OAI.CubicTorus.planeSquare_measurePreserving line 709
  33. theorem OAI.CubicTorus.plane_square_poincare line 718
  34. lemma OAI.CubicTorus.planeSquare_volume line 766
  35. def OAI.CubicTorus.planarCoordinateDivergence line 789
  36. lemma OAI.CubicTorus.triangle_piola_derivatives line 792
  37. lemma OAI.CubicTorus.continuous_interval_integral_swap line 814
  38. lemma OAI.CubicTorus.hasDerivAt_coordinate_left line 823
  39. lemma OAI.CubicTorus.hasDerivAt_coordinate_right line 828
  40. lemma OAI.CubicTorus.rectangle_coordinate_divergence line 833
  41. theorem OAI.CubicTorus.triangle_coordinate_divergence line 875