OAI/Geometry/CubicTorus/Regularity/BVNormalTiltMeasure.lean

GitHub source file

39 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicTorus.integral_sq_cauchy_finite line 15
  2. lemma OAI.CubicTorus.normalOscillation_sq_le_excess line 41
  3. lemma OAI.CubicTorus.integrable_sq_norm_sub_normal line 77
  4. def OAI.CubicTorus.normalTiltMeasure line 86
  5. lemma OAI.CubicTorus.normalTiltMeasure_apply line 89
  6. lemma OAI.CubicTorus.normalExcess_bad_set_measure line 96
  7. theorem OAI.CubicTorus.normalMeasure_lipschitz_approximation line 138
  8. theorem OAI.CubicTorus.isMinimizerAt_lipschitz_approximation line 203
  9. lemma OAI.CubicTorus.volume_zero_of_nonzero_constant_derivative line 256
  10. lemma OAI.CubicTorus.ae_constant_derivative_eq_zero line 301
  11. def OAI.CubicTorus.normalPlaneLinearIsometry line 312
  12. lemma OAI.CubicTorus.normalPlaneEmbedding_inner line 328
  13. def OAI.CubicTorus.normalGraph line 331
  14. lemma OAI.CubicTorus.normalGraph_lipschitz line 334
  15. lemma OAI.CubicTorus.normalGraph_inner line 352
  16. lemma OAI.CubicTorus.fderiv_gradient_inner line 370
  17. lemma OAI.CubicTorus.divergence_gradient_eq_laplacian line 381
  18. lemma OAI.CubicTorus.laplacian_comp_isometry line 394
  19. lemma OAI.CubicTorus.iteratedFDeriv_two_line line 416
  20. lemma OAI.CubicTorus.integral_compact_fderiv_zero line 450
  21. lemma OAI.CubicTorus.fderiv_fderiv_apply line 464
  22. lemma OAI.CubicTorus.laplacian_eq_sum_directional line 472
  23. lemma OAI.CubicTorus.compact_laplacian_continuous line 483
  24. lemma OAI.CubicTorus.laplacian_tsupport_subset line 496
  25. lemma OAI.CubicTorus.integral_compact_laplacian_zero line 508
  26. lemma OAI.CubicTorus.fderiv_compact_convolution line 540
  27. theorem OAI.CubicTorus.laplacian_compact_convolution line 549
  28. lemma OAI.CubicTorus.laplacian_translate line 576
  29. lemma OAI.CubicTorus.laplacian_reflect_translate line 582
  30. theorem OAI.CubicTorus.weak_harmonic_convolution line 591
  31. lemma OAI.CubicTorus.harmonic_angular_integral line 625
  32. lemma OAI.CubicTorus.add_polarCoord_eq_circleMap line 642
  33. theorem OAI.CubicTorus.harmonic_radial_mean line 646
  34. theorem OAI.CubicTorus.exists_radial_smoothing_kernel line 714
  35. lemma OAI.CubicTorus.harmonic_radial_convolution line 765
  36. lemma OAI.CubicTorus.real_convolution_comm line 793
  37. lemma OAI.CubicTorus.compact_convolution_assoc line 800
  38. lemma OAI.CubicTorus.compact_convolutions_commute line 814
  39. lemma OAI.CubicTorus.reflected_tsupport_subset_ball line 824