OAI/Analysis/Conductivity/Variational/PhysicalRealTrace.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ScalarConductivity.H1_eq_of_value_ae line 18
2. lemma OAI.ScalarConductivity.SmoothLipZero.lipschitz line 23
3. lemma OAI.ScalarConductivity.SmoothLipZero.onH1_smooth line 26
4. def OAI.ScalarConductivity.physicalComplexTraceCLM line 35
5. def OAI.ScalarConductivity.physicalRealTraceCLM line 39
6. lemma OAI.ScalarConductivity.physicalRealTrace_smooth_ae line 42
7. theorem OAI.ScalarConductivity.physicalRealTrace_chain line 59
8. theorem OAI.ScalarConductivity.physicalRealTrace_upper_bound line 78