OAI/Analysis/Conductivity/Sources/AngularJet.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ScalarConductivity.measurable_torusDirectionalDerivative_joint line 18
  2. def OAI.ScalarConductivity.sourceAngularTest line 34
  3. lemma OAI.ScalarConductivity.continuous_sourceAngularTest line 38
  4. theorem OAI.ScalarConductivity.sourceAngularTest_lipschitz line 46
  5. def OAI.ScalarConductivity.sourceAngularJet line 70
  6. lemma OAI.ScalarConductivity.measurable_sourceAngularJet line 76
  7. lemma OAI.ScalarConductivity.finiteCylinder_ae_mem line 102
  8. lemma OAI.ScalarConductivity.continuous_memLp_finiteCylinder line 108
  9. lemma OAI.ScalarConductivity.sourceAngularJet_memLp line 117
  10. def OAI.ScalarConductivity.sourceAngularLpJet line 139
  11. lemma OAI.ScalarConductivity.sourceAngularLpJet_ae line 143
  12. lemma OAI.ScalarConductivity.mFourierCoeff_div_const line 149
  13. lemma OAI.ScalarConductivity.torusDirectionalDerivative_scaled_fourier line 153
  14. lemma OAI.ScalarConductivity.sourceAngularJet_fourier line 162