OAI/Analysis/Conductivity/Fourier/AngularInverseTensor.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ScalarConductivity.angularLiftMatrix_background line 13
  2. lemma OAI.ScalarConductivity.angularInverseLift_shift line 30
  3. lemma OAI.ScalarConductivity.AngularPeriodic.angularInverseLift line 37
  4. def OAI.ScalarConductivity.undoAngularPoint line 56
  5. lemma OAI.ScalarConductivity.undoAngularPoint_zero line 60
  6. lemma OAI.ScalarConductivity.undoAngularPoint_forward line 65
  7. lemma OAI.ScalarConductivity.undoAngularPoint_contDiff line 74
  8. lemma OAI.ScalarConductivity.AngularPeriodic.undoAngularPoint line 79
  9. def OAI.ScalarConductivity.undoAngularValue line 92
  10. def OAI.ScalarConductivity.undoAngularTensor line 97
  11. lemma OAI.ScalarConductivity.undoAngularValue_matching line 102
  12. lemma OAI.ScalarConductivity.undoAngularTensor_matching line 136
  13. lemma OAI.ScalarConductivity.undoAngularValue_terminal line 144