OAI/Analysis/Conductivity/Fourier/EndPoissonRepresentative.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ScalarConductivity.lp_hasSum_ae_unique line 20
  2. def OAI.ScalarConductivity.endPoissonModeField line 46
  3. def OAI.ScalarConductivity.endPoissonField line 50
  4. lemma OAI.ScalarConductivity.endPoissonModeJet_ae line 54
  5. lemma OAI.ScalarConductivity.endModeCoefficient_norm_bound line 69
  6. lemma OAI.ScalarConductivity.endPoissonField_hasSum line 92
  7. theorem OAI.ScalarConductivity.endPoissonJet_ae line 120
  8. lemma OAI.ScalarConductivity.continuous_endPoissonModeField line 136
  9. lemma OAI.ScalarConductivity.measurable_endPoissonField line 141
  10. def OAI.ScalarConductivity.physicalEndPoissonField line 145
  11. lemma OAI.ScalarConductivity.measurable_physicalEndPoissonField line 149
  12. lemma OAI.ScalarConductivity.physicalEndPoissonField_angular line 153
  13. def OAI.ScalarConductivity.physicalEndPoissonJet line 159
  14. lemma OAI.ScalarConductivity.physicalEndPoissonJet_ae line 165
  15. lemma OAI.ScalarConductivity.physicalEndPoissonField_memLp line 172
  16. lemma OAI.ScalarConductivity.physicalEndPoissonJet_hasSum line 179