OAI/Analysis/Conductivity/Variational/PhysicalEndLocalLipschitz.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ScalarConductivity.LocalLipAt line 11
  2. lemma OAI.ScalarConductivity.LocalLipAt.continuousAt line 14
  3. lemma OAI.ScalarConductivity.LocalLipAt.comp line 19
  4. lemma OAI.ScalarConductivity.LocalLipAt.prodMk line 28
  5. lemma OAI.ScalarConductivity.LocalLipAt.congr line 35
  6. lemma OAI.ScalarConductivity.localLipAt_of_contDiffAt line 44
  7. lemma OAI.ScalarConductivity.localLipschitz_abs line 48
  8. lemma OAI.ScalarConductivity.locallyLipschitz_sourceRadial line 53
  9. lemma OAI.ScalarConductivity.locallyLipschitz_sourceCollarTime line 59
  10. lemma OAI.ScalarConductivity.locallyLipschitz_sourceDirection line 67
  11. def OAI.ScalarConductivity.localComplexArg line 83
  12. lemma OAI.ScalarConductivity.localComplexArg_contDiffAt line 85
  13. lemma OAI.ScalarConductivity.localComplexArg_unitAngle line 94
  14. lemma OAI.ScalarConductivity.physicalEndPoissonField_eq_continuation line 108
  15. def OAI.ScalarConductivity.sourceLocalFlat line 124
  16. lemma OAI.ScalarConductivity.sourceLocalFlat_localLip line 128
  17. lemma OAI.ScalarConductivity.sourceLocalFlat_angles line 148
  18. theorem OAI.ScalarConductivity.physicalEndPoissonField_localLip line 157