OAI/Analysis/Conductivity/Fourier/LeadingFrequencyAlignment.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ScalarConductivity.leading_frequency_SL2_alignment line 11
  2. def OAI.ScalarConductivity.angularIntMap line 58
  3. lemma OAI.ScalarConductivity.angularIntMap_continuous line 64
  4. lemma OAI.ScalarConductivity.angularIntMap_surjective line 71
  5. lemma OAI.ScalarConductivity.angularIntMap_measurePreserving line 89
  6. def OAI.ScalarConductivity.angularNormalization line 100
  7. def OAI.ScalarConductivity.normalizedAngularTensor line 103
  8. lemma OAI.ScalarConductivity.angularNormalization_pos line 113
  9. lemma OAI.ScalarConductivity.twoCoordinate_cauchy line 116
  10. theorem OAI.ScalarConductivity.normalizedAngularTensor_lower line 120