OAI/Analysis/Conductivity/Geometry/AffineBoxPoincare.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ScalarConductivity.unitCubeAverage_add line 11
  2. lemma OAI.ScalarConductivity.unitCubeAverage_mul line 19
  3. lemma OAI.ScalarConductivity.unitCubeAverage_const line 23
  4. lemma OAI.ScalarConductivity.unitCubeAverage_mono line 26
  5. def OAI.ScalarConductivity.boxRescale line 34
  6. def OAI.ScalarConductivity.boxAverage line 37
  7. lemma OAI.ScalarConductivity.boxRescale_smooth line 40
  8. lemma OAI.ScalarConductivity.boxRescale_fderiv line 45
  9. lemma OAI.ScalarConductivity.box_partial_one line 55
  10. lemma OAI.ScalarConductivity.box_partial_two line 65
  11. lemma OAI.ScalarConductivity.box_partial_three line 75
  12. theorem OAI.ScalarConductivity.smooth_box_poincare line 85
  13. def OAI.ScalarConductivity.closedBox line 97
  14. lemma OAI.ScalarConductivity.isCompact_closedBox line 100
  15. lemma OAI.ScalarConductivity.unitSquareAverage_eq_integral line 103
  16. lemma OAI.ScalarConductivity.unitCubeAverage_eq_integral line 108
  17. lemma OAI.ScalarConductivity.unitAverage_comp_affine line 114
  18. lemma OAI.ScalarConductivity.box_volume_integral_iterated line 123
  19. lemma OAI.ScalarConductivity.boxAverage_eq_integral line 136