OAI/Analysis/Conductivity/Geometry/CylinderPolynomial.lean

GitHub source file

20 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ScalarConductivity.smoothComplexAxis line 11
  2. instance OAI.ScalarConductivity.(instance at line 24) line 24
  3. lemma OAI.ScalarConductivity.smoothComplexAxis_smooth line 26
  4. lemma OAI.ScalarConductivity.smoothFiniteAxisLp_add line 29
  5. lemma OAI.ScalarConductivity.smoothFiniteAxisLp_smul line 37
  6. lemma OAI.ScalarConductivity.smoothAxisModeJet_add line 44
  7. lemma OAI.ScalarConductivity.smoothAxisModeJet_smul line 69
  8. def OAI.ScalarConductivity.smoothAxisModeJetL line 90
  9. def OAI.ScalarConductivity.cylinderPolynomialJetL line 95
  10. lemma OAI.ScalarConductivity.cylinderPolynomialJetL_apply line 98
  11. abbrev OAI.ScalarConductivity.SpectralModeFiber line 107
  12. def OAI.ScalarConductivity.spectralJetSingle line 109
  13. lemma OAI.ScalarConductivity.spectralJetSingle_orthogonal line 124
  14. def OAI.ScalarConductivity.weightedModeFiberL line 132
  15. lemma OAI.ScalarConductivity.weightedModeFiber_norm_sq line 140
  16. def OAI.ScalarConductivity.spectralTraceSingleL line 149
  17. def OAI.ScalarConductivity.cylinderPolynomialTraceL line 159
  18. lemma OAI.ScalarConductivity.cylinderPolynomialTraceL_apply line 164
  19. lemma OAI.ScalarConductivity.cylinderPolynomialTraceL_norm_sq line 173
  20. lemma OAI.ScalarConductivity.cylinderPolynomial_trace_bound line 181