OAI/Analysis/Conductivity/Fourier/UndoAngularWeakPair.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ScalarConductivity.undoAngularOutput line 14
2. lemma OAI.ScalarConductivity.undoAngularOutput_apply line 21
3. def OAI.ScalarConductivity.undoAngularTranslation line 26
4. lemma OAI.ScalarConductivity.undoAngularPoint_eq_affine line 29
5. lemma OAI.ScalarConductivity.undoAngular_domain line 38
6. def OAI.ScalarConductivity.WeakFiniteTensorPair.onEq line 50
7. def OAI.ScalarConductivity.WeakFiniteTensorPair.undoAngular line 64
8. lemma OAI.ScalarConductivity.WeakFiniteTensorPair.undoAngular_v line 72
9. lemma OAI.ScalarConductivity.WeakFiniteTensorPair.undoAngular_E line 82
10. theorem OAI.ScalarConductivity.general_mode_weak_finite_ending line 105