OAI/Analysis/Conductivity/Fourier/GeneralModeFiniteEndNormal.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ScalarConductivity.general_mode_finite_ending_raw_normal line 19
  2. def OAI.ScalarConductivity.angularInverseLift line 130
  3. def OAI.ScalarConductivity.angularNormalizedLinear line 134
  4. def OAI.ScalarConductivity.angularInverseLinear line 139
  5. lemma OAI.ScalarConductivity.real_angular_det_one line 144
  6. lemma OAI.ScalarConductivity.angularNormalizedLift_inverse line 149
  7. lemma OAI.ScalarConductivity.angularInverseLift_normalized line 164
  8. def OAI.ScalarConductivity.angularNormalizedEquiv line 178
  9. lemma OAI.ScalarConductivity.angularNormalizedEquiv_apply line 183
  10. lemma OAI.ScalarConductivity.angularNormalizedEquiv_symm_apply line 186
  11. def OAI.ScalarConductivity.angularLiftMatrix line 189
  12. lemma OAI.ScalarConductivity.operatorMatrix_angularNormalizedEquiv line 193