OAI/Analysis/Conductivity/Flux/LinearTensorEllipticity.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ScalarConductivity.matrix_congruence_energy line 14
2. lemma OAI.ScalarConductivity.linearTensorPullback_elliptic line 23
3. lemma OAI.ScalarConductivity.RegularPatch.tensor_smul line 73
4. lemma OAI.ScalarConductivity.mem_regularRegion_tensor_smul line 83
5. lemma OAI.ScalarConductivity.flux_translate_weak line 102
6. lemma OAI.ScalarConductivity.translatedTensor_C1_representative line 123
7. lemma OAI.ScalarConductivity.scalar_flux_weak line 131
8. structure OAI.ScalarConductivity.WeakFiniteTensorPair line 153
9. lemma OAI.ScalarConductivity.WeakFiniteTensorPair.linear_smooth line 170
10. lemma OAI.ScalarConductivity.WeakFiniteTensorPair.linear_elliptic line 174
11. lemma OAI.ScalarConductivity.WeakFiniteTensorPair.linear_regular line 183
12. def OAI.ScalarConductivity.WeakFiniteTensorPair.linear line 193
13. def OAI.ScalarConductivity.WeakFiniteTensorPair.translate line 209
14. def OAI.ScalarConductivity.WeakFiniteTensorPair.scaleTensor line 227
15. lemma OAI.ScalarConductivity.WeakFiniteTensorPair.integrable line 256