OAI/Analysis/Conductivity/Variational/SmoothPrimitive.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ScalarConductivity.smoothPrimitive line 11
  2. theorem OAI.ScalarConductivity.smoothDirection_smoothPrimitive line 24
  3. def OAI.ScalarConductivity.meanZeroPrimitive line 34
  4. theorem OAI.ScalarConductivity.smoothDirection_meanZeroPrimitive line 38
  5. theorem OAI.ScalarConductivity.meanZeroPrimitive_mean line 49
  6. theorem OAI.ScalarConductivity.meanZeroPrimitive_periodic line 58
  7. theorem OAI.ScalarConductivity.periodic_smoothScalar_bounded line 70
  8. theorem OAI.ScalarConductivity.periodic_two_primitives line 76