OAI/Analysis/Conductivity/Variational/FiniteEndPhysicalDescent.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ScalarConductivity.AngularPeriodic.eq_of_angles line 15
  2. def OAI.ScalarConductivity.sourceRealFlat line 41
  3. lemma OAI.ScalarConductivity.sourceRealFlat_angles line 45
  4. def OAI.ScalarConductivity.physicalPeriodicField line 50
  5. lemma OAI.ScalarConductivity.physicalPeriodicField_local_eq line 53
  6. theorem OAI.ScalarConductivity.physicalPeriodicField_localLip line 61
  7. lemma OAI.ScalarConductivity.measurable_sourceRealFlat line 75
  8. lemma OAI.ScalarConductivity.measurable_physicalPeriodicField line 85
  9. lemma OAI.ScalarConductivity.physicalPeriodicField_piece line 89
  10. lemma OAI.ScalarConductivity.physicalPeriodicField_piece_local_eq line 100
  11. theorem OAI.ScalarConductivity.physicalPeriodicField_hasFDeriv line 113
  12. theorem OAI.ScalarConductivity.physicalPeriodicField_fderiv line 134