OAI/Analysis/Conductivity/Variational/UnitSquarePoincare.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ScalarConductivity.unitSquareAverage line 11
  2. def OAI.ScalarConductivity.squarePartial line 14
  3. lemma OAI.ScalarConductivity.continuous_squarePartial line 16
  4. lemma OAI.ScalarConductivity.deriv_fiber_right line 20
  5. theorem OAI.ScalarConductivity.smooth_unit_square_poincare line 26
  6. lemma OAI.ScalarConductivity.unitSquareAverage_add line 96
  7. lemma OAI.ScalarConductivity.unitSquareAverage_mul line 104
  8. lemma OAI.ScalarConductivity.unitSquareAverage_const line 108
  9. lemma OAI.ScalarConductivity.unitSquareAverage_mono line 111
  10. lemma OAI.ScalarConductivity.unitSquareAverage_nonneg line 119
  11. abbrev OAI.ScalarConductivity.Box3 line 124
  12. def OAI.ScalarConductivity.unitCubeAverage line 126
  13. def OAI.ScalarConductivity.cubePartial line 129
  14. lemma OAI.ScalarConductivity.continuous_cubePartial line 131
  15. theorem OAI.ScalarConductivity.smooth_unit_cube_poincare line 135