OAI/Analysis/Conductivity/Scalarization/UpdateFieldPair.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ScalarConductivity.CompactGlobalUpdate.fieldPair line 12
2. lemma OAI.ScalarConductivity.CompactGlobalUpdate.fieldPair_eq line 22
3. lemma OAI.ScalarConductivity.CompactGlobalUpdate.fieldPair_ae line 35
4. lemma OAI.ScalarConductivity.CompactGlobalUpdate.fieldPair_energy_bound line 49
5. lemma OAI.ScalarConductivity.diagonal_conjugate_smul_sub line 79
6. lemma OAI.ScalarConductivity.diagonal_conjugate_dot_bound line 90
7. lemma OAI.ScalarConductivity.diagonal_conjugate_field_bound line 104
8. lemma OAI.ScalarConductivity.matrixFiniteLaminate_diagonal_bounds line 117
9. lemma OAI.ScalarConductivity.scalarNeighbourhood_defect_bound line 123