OAI/Analysis/Conductivity/Flux/CylinderSlopeGreen.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ScalarConductivity.complex_linear_axis_smooth line 12
  2. lemma OAI.ScalarConductivity.complex_linear_axis_deriv line 16
  3. def OAI.ScalarConductivity.cylinderSlopeJet line 21
  4. lemma OAI.ScalarConductivity.cylinderSlopeJet_derivative line 24
  5. lemma OAI.ScalarConductivity.cylinderSlopeJet_angular line 34
  6. lemma OAI.ScalarConductivity.constant_derivative_inner line 37
  7. def OAI.ScalarConductivity.spectralMeanCLM line 56
  8. lemma OAI.ScalarConductivity.spectralMean_single line 61
  9. lemma OAI.ScalarConductivity.flatCylinder_slope_mode_green line 68
  10. lemma OAI.ScalarConductivity.spectralMean_polynomial line 85
  11. theorem OAI.ScalarConductivity.flatCylinder_slope_completed_green line 91
  12. def OAI.ScalarConductivity.cylinderEndJet line 124
  13. lemma OAI.ScalarConductivity.cylinderSlopeJet_mem_graph line 129
  14. theorem OAI.ScalarConductivity.cylinderEndJet_mem_graph line 142
  15. lemma OAI.ScalarConductivity.spectralWeightedPair_real line 152
  16. lemma OAI.ScalarConductivity.spectralMean_real line 160
  17. def OAI.ScalarConductivity.cylinderTerminalFlux line 163
  18. theorem OAI.ScalarConductivity.cylinderEndJet_real_green line 167