OAI/Analysis/Conductivity/Geometry/CylinderJetOrthogonal.lean

GitHub source file

14 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ScalarConductivity.FiniteAxisJets line 12
  2. def OAI.ScalarConductivity.cylinderJetMode line 14
  3. lemma OAI.ScalarConductivity.cylinderJetMode_orthogonal line 30
  4. def OAI.ScalarConductivity.smoothAxisModeJet line 38
  5. lemma OAI.ScalarConductivity.cylinderJetMode_smooth line 45
  6. lemma OAI.ScalarConductivity.smoothAxisModeJet_norm_sq line 51
  7. lemma OAI.ScalarConductivity.smoothCylinder_polynomial_norm_sq line 66
  8. lemma OAI.ScalarConductivity.smoothFiniteAxisLp_norm_sq line 75
  9. lemma OAI.ScalarConductivity.complex_fourier_mode_trace_energy_right line 82
  10. def OAI.ScalarConductivity.cylinderTraceConstant line 101
  11. lemma OAI.ScalarConductivity.cylinderTraceConstant_pos line 104
  12. lemma OAI.ScalarConductivity.smoothAxisMode_trace_energy_bound line 107
  13. lemma OAI.ScalarConductivity.smoothAxisMode_trace_left line 137
  14. lemma OAI.ScalarConductivity.smoothAxisMode_trace_right line 146