OAI/Analysis/Conductivity/Variational/CompactCompatibleReplacement.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. structure OAI.ScalarConductivity.CompactCompatibleReplacement line 23
2. def OAI.ScalarConductivity.CompactTwoFieldReplacement.forgetRank line 40
3. lemma OAI.ScalarConductivity.gradientColumns_affine_column line 56
4. def OAI.ScalarConductivity.CompactSelectedReplacement.affineTransfer line 73
5. lemma OAI.ScalarConductivity.CompactSelectedReplacement.affineTransfer_relation line 131
6. def OAI.ScalarConductivity.CompactSelectedReplacement.changeOld line 152
7. theorem OAI.ScalarConductivity.exists_locally_smooth_selected_split line 181