OAI/Geometry/CubicTorus/Estimates/BVBallCalibration.lean

GitHub source file

81 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.CubicTorus.admissible_latticePeriodize line 15
  2. lemma OAI.CubicTorus.radialDensityWeight_one_on_inner line 26
  3. lemma OAI.CubicTorus.radialDensityField_norm_le line 34
  4. lemma OAI.CubicTorus.divergence_inner_radialDensityField line 44
  5. def OAI.CubicTorus.ballCalibration line 53
  6. lemma OAI.CubicTorus.ballCalibration_contDiff line 56
  7. lemma OAI.CubicTorus.ballCalibration_compact line 59
  8. lemma OAI.CubicTorus.ballCalibration_support line 66
  9. lemma OAI.CubicTorus.ballCalibration_norm line 74
  10. lemma OAI.CubicTorus.ballCalibration_divergence line 82
  11. lemma OAI.CubicTorus.integral_const_coverBall line 96
  12. lemma OAI.CubicTorus.ball_calibration_flux_le line 104
  13. theorem OAI.CubicTorus.perimeter_cubeBall_eq line 115
  14. lemma OAI.CubicTorus.UpperComparison.norm_axial_sub_center line 143
  15. lemma OAI.CubicTorus.UpperComparison.axial_sub_center_contDiff line 151
  16. def OAI.CubicTorus.UpperComparison.tubeCalibration line 155
  17. lemma OAI.CubicTorus.UpperComparison.tubeCalibration_contDiff line 158
  18. lemma OAI.CubicTorus.UpperComparison.tubeCalibration_norm line 165
  19. lemma OAI.CubicTorus.UpperComparison.tubeCalibration_support line 177
  20. lemma OAI.CubicTorus.UpperComparison.tubeCalibration_compact line 193
  21. lemma OAI.CubicTorus.UpperComparison.tubeCalibration_interior line 201
  22. lemma OAI.CubicTorus.UpperComparison.divergence_axial_sub_center line 228
  23. lemma OAI.CubicTorus.UpperComparison.gradient_axialScalar_pair line 236
  24. lemma OAI.CubicTorus.UpperComparison.tubeCalibration_divergence_inner line 246
  25. lemma OAI.CubicTorus.UpperComparison.tubeCalibration_periodic_divergence line 270
  26. lemma OAI.CubicTorus.UpperComparison.integral_axialScalar_coverTube line 279
  27. lemma OAI.CubicTorus.UpperComparison.tube_calibration_flux_le line 300
  28. def OAI.CubicTorus.UpperComparison.axialExhaustionBump line 324
  29. lemma OAI.CubicTorus.UpperComparison.axialExhaustionBump_outer line 330
  30. lemma OAI.CubicTorus.UpperComparison.axialExhaustionBump_integral line 335
  31. lemma OAI.CubicTorus.UpperComparison.tube_calibration_lower_fixed_radius line 355
  32. theorem OAI.CubicTorus.UpperComparison.perimeter_cubeTube_eq line 372
  33. lemma OAI.CubicTorus.latticeVector_injective line 400
  34. instance OAI.CubicTorus.latticeAddAction line 407
  35. instance OAI.CubicTorus.latticeMeasurableVAdd line 414
  36. instance OAI.CubicTorus.latticeVolumeInvariant line 419
  37. lemma OAI.CubicTorus.lattice_fundamentalCube line 424
  38. lemma OAI.CubicTorus.periodic_image_fundamental line 440
  39. lemma OAI.CubicTorus.integral_periodic_image_cube line 464
  40. lemma OAI.CubicTorus.coordinateMove_surjective line 483
  41. def OAI.CubicTorus.periodicCoordinateRegion line 505
  42. lemma OAI.CubicTorus.periodicCoordinateRegion_measurable line 508
  43. lemma OAI.CubicTorus.periodicCoordinateRegion_lift line 517
  44. lemma OAI.CubicTorus.integral_periodicCoordinateRegion line 539
  45. lemma OAI.CubicTorus.perimeter_periodicCoordinateRegion_le line 593
  46. lemma OAI.CubicTorus.finitePerimeter_periodicCoordinateRegion line 618
  47. structure OAI.CubicTorus.Periodic.Variation line 630
  48. def OAI.CubicTorus.Periodic.Variation.ofWall line 638
  49. lemma OAI.CubicTorus.Periodic.exists_variation_of_function line 641
  50. abbrev OAI.CubicTorus.Periodic.VariationChain line 661
  51. def OAI.CubicTorus.Periodic.chainMove line 663
  52. def OAI.CubicTorus.Periodic.chainJacobian line 667
  53. def OAI.CubicTorus.Periodic.chainCofactor line 672
  54. def OAI.CubicTorus.Periodic.chainPullback line 677
  55. def OAI.CubicTorus.Periodic.chainRegion line 681
  56. def OAI.CubicTorus.Periodic.ChainValid line 685
  57. def OAI.CubicTorus.Periodic.chainBound line 687
  58. lemma OAI.CubicTorus.Periodic.chainBound_pos line 691
  59. lemma OAI.CubicTorus.Periodic.chainMove_contDiff line 696
  60. lemma OAI.CubicTorus.Periodic.chainJacobian_contDiff line 701
  61. lemma OAI.CubicTorus.Periodic.chainPullback_contDiff line 709
  62. lemma OAI.CubicTorus.Periodic.chainPullback_periodic line 715
  63. lemma OAI.CubicTorus.Periodic.chainPullback_norm line 722
  64. lemma OAI.CubicTorus.Periodic.chainPullback_divergence line 731
  65. lemma OAI.CubicTorus.Periodic.chain_inner_pullback line 741
  66. lemma OAI.CubicTorus.Periodic.chainRegion_measurable line 750
  67. lemma OAI.CubicTorus.Periodic.chainRegion_finite line 760
  68. lemma OAI.CubicTorus.Periodic.chainMove_periodic line 771
  69. lemma OAI.CubicTorus.Periodic.chainJacobian_periodic line 780
  70. lemma OAI.CubicTorus.Periodic.integral_chainRegion line 789
  71. abbrev OAI.CubicTorus.VariationChain line 819
  72. def OAI.CubicTorus.chainMove line 821
  73. def OAI.CubicTorus.chainJacobian line 825
  74. def OAI.CubicTorus.chainCofactor line 830
  75. def OAI.CubicTorus.chainPullback line 835
  76. def OAI.CubicTorus.chainRegion line 839
  77. def OAI.CubicTorus.ChainValid line 843
  78. def OAI.CubicTorus.chainBound line 845
  79. lemma OAI.CubicTorus.chainBound_pos line 849
  80. lemma OAI.CubicTorus.chainMove_contDiff line 854
  81. lemma OAI.CubicTorus.chainJacobian_contDiff line 859