OAI/Analysis/Conductivity/Geometry/UnitBoxAverage.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ScalarConductivity.unitAverage line 14
  2. lemma OAI.ScalarConductivity.unitAverage_eq_interval line 17
  3. lemma OAI.ScalarConductivity.unitAverage_const line 22
  4. lemma OAI.ScalarConductivity.unitAverage_add line 27
  5. lemma OAI.ScalarConductivity.unitAverage_sub line 32
  6. lemma OAI.ScalarConductivity.unitAverage_smul line 37
  7. lemma OAI.ScalarConductivity.unitAverage_mul line 40
  8. lemma OAI.ScalarConductivity.unitAverage_mono line 43
  9. lemma OAI.ScalarConductivity.unitAverage_nonneg line 49
  10. lemma OAI.ScalarConductivity.unitAverage_sq_le line 55
  11. lemma OAI.ScalarConductivity.continuous_unitAverage line 61
  12. lemma OAI.ScalarConductivity.contDiff_unitAverage line 66
  13. lemma OAI.ScalarConductivity.fderiv_unitAverage line 71
  14. lemma OAI.ScalarConductivity.unitAverage_mean_poincare line 87