OAI/Geometry/CubicTorus/Reflection/BVScaledFlux.lean

GitHub source file

62 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicTorus.finiteMeasure_coverBall line 15
  2. lemma OAI.CubicTorus.integral_halfspaceIndicator_unitBall line 19
  3. lemma OAI.CubicTorus.integral_characteristic_chart line 54
  4. lemma OAI.CubicTorus.integral_rescaled_characteristic line 66
  5. lemma OAI.CubicTorus.HalfspaceTrappedAt.tendsto_rescaled_volume line 87
  6. theorem OAI.CubicTorus.isMinimizerAt_volume_density_half_ae line 121
  7. lemma OAI.CubicTorus.divergence_of_notMem_tsupport line 144
  8. lemma OAI.CubicTorus.divergence_tsupport_subset line 148
  9. theorem OAI.CubicTorus.normalMeasure_local_flux line 155
  10. lemma OAI.CubicTorus.IsNormalMeasure.congr_ae line 191
  11. def OAI.CubicTorus.scaledTestField line 213
  12. lemma OAI.CubicTorus.scaledTestField_contDiff line 216
  13. lemma OAI.CubicTorus.fderiv_scaledTestField line 221
  14. lemma OAI.CubicTorus.divergence_scaledTestField line 233
  15. lemma OAI.CubicTorus.scaledTestField_tsupport line 238
  16. lemma OAI.CubicTorus.scaledTestField_hasCompactSupport line 253
  17. lemma OAI.CubicTorus.integral_cover_affine_scaling line 259
  18. theorem OAI.CubicTorus.normalMeasure_scaled_flux line 267
  19. theorem OAI.CubicTorus.HalfspaceTrappedAt.tendsto_test_integral line 302
  20. theorem OAI.CubicTorus.normalMeasure_scaled_flux_limit line 351
  21. lemma OAI.CubicTorus.scalar_test_normal_error line 383
  22. theorem OAI.CubicTorus.normalMeasure_scalar_tangent line 443
  23. def OAI.CubicTorus.normalRotation line 495
  24. lemma OAI.CubicTorus.normalRotation_axis line 498
  25. def OAI.CubicTorus.normalProductChart line 503
  26. lemma OAI.CubicTorus.normalProductChart_apply line 507
  27. lemma OAI.CubicTorus.normalProductChart_measurePreserving line 512
  28. lemma OAI.CubicTorus.normalProductChart_decompose line 518
  29. lemma OAI.CubicTorus.normalProductChart_inner line 527
  30. lemma OAI.CubicTorus.normalProductChart_coord_bound line 534
  31. lemma OAI.CubicTorus.normalProductChart_line_contDiff line 539
  32. lemma OAI.CubicTorus.normalProductChart_line_deriv line 547
  33. lemma OAI.CubicTorus.halfspace_flux_integrable line 556
  34. theorem OAI.CubicTorus.integral_halfspace_flux line 568
  35. def OAI.CubicTorus.tangentPart line 620
  36. lemma OAI.CubicTorus.norm_tangentPart_sq line 622
  37. lemma OAI.CubicTorus.inner_tangentPart line 628
  38. lemma OAI.CubicTorus.tangentialDivergence_smul_const line 634
  39. def OAI.CubicTorus.heightTestField line 642
  40. lemma OAI.CubicTorus.heightTestField_contDiff line 645
  41. lemma OAI.CubicTorus.heightTestField_tsupport line 649
  42. lemma OAI.CubicTorus.heightTestField_hasCompactSupport line 656
  43. lemma OAI.CubicTorus.tangentialDivergence_heightTestField line 660
  44. lemma OAI.CubicTorus.heightTestField_tilt_bound line 675
  45. lemma OAI.CubicTorus.heightTestField_flux_bound line 690
  46. lemma OAI.CubicTorus.radialDensityWeight_le_one line 714
  47. lemma OAI.CubicTorus.radialDensityWeight_tsupport line 717
  48. lemma OAI.CubicTorus.radialDensityWeight_hasCompactSupport line 725
  49. lemma OAI.CubicTorus.norm_fderiv_radialDensityWeight_le line 729
  50. lemma OAI.CubicTorus.norm_fderiv_radialDensityWeight_bound line 737
  51. def OAI.CubicTorus.radialHeightCutoff line 757
  52. lemma OAI.CubicTorus.radialHeightCutoff_one line 760
  53. lemma OAI.CubicTorus.radialHeightCutoff_gradient_bound line 767
  54. lemma OAI.CubicTorus.radialHeightCutoff_gradient_zero line 777
  55. abbrev OAI.CubicTorus.Plane line 797
  56. def OAI.CubicTorus.normalPlaneEmbedding line 799
  57. lemma OAI.CubicTorus.normalPlaneEmbedding_norm line 802
  58. lemma OAI.CubicTorus.normalPlaneEmbedding_measurable line 808
  59. lemma OAI.CubicTorus.integral_plane_coordinates line 812
  60. lemma OAI.CubicTorus.plane_ball_real line 818
  61. lemma OAI.CubicTorus.radialDensityWeight_plane_bound line 824
  62. lemma OAI.CubicTorus.integral_radialDensityWeight_plane_tendsto line 838