OAI/Analysis/Conductivity/Fourier/EndPoissonJets.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ScalarConductivity.finiteDecayLp_real_norm_sq line 18
  2. lemma OAI.ScalarConductivity.finiteDecayLp_imag_norm_sq line 22
  3. lemma OAI.ScalarConductivity.torusFrequency_sq_le_rate line 27
  4. lemma OAI.ScalarConductivity.finiteDecayLp_angular_bound line 40
  5. lemma OAI.ScalarConductivity.finiteDecayLp_axial_bound line 53
  6. def OAI.ScalarConductivity.endModeCoefficient line 60
  7. abbrev OAI.ScalarConductivity.FiniteCylinderJets line 63
  8. def OAI.ScalarConductivity.endPoissonSequence line 66
  9. def OAI.ScalarConductivity.endPoissonJet line 87
  10. def OAI.ScalarConductivity.endPoissonModeJet line 92
  11. lemma OAI.ScalarConductivity.endPoissonJet_component_hasSum line 96
  12. lemma OAI.ScalarConductivity.endPoissonJet_hasSum line 102
  13. theorem OAI.ScalarConductivity.endPoissonJet_mem_mode_closure line 119
  14. lemma OAI.ScalarConductivity.spectralGraph_norm_sq line 133
  15. lemma OAI.ScalarConductivity.spectralGraph_weight_norm_sq line 139
  16. lemma OAI.ScalarConductivity.endModeCoefficient_add line 148
  17. lemma OAI.ScalarConductivity.endModeCoefficient_smul line 152
  18. lemma OAI.ScalarConductivity.endPoissonSequence_add line 160
  19. lemma OAI.ScalarConductivity.endPoissonSequence_smul line 169
  20. lemma OAI.ScalarConductivity.endPoissonJet_add line 177
  21. lemma OAI.ScalarConductivity.endPoissonJet_smul line 185
  22. lemma OAI.ScalarConductivity.endPoissonJet_component_norm_sq line 193
  23. lemma OAI.ScalarConductivity.endPoissonJet_component_bound line 198
  24. lemma OAI.ScalarConductivity.endPoissonJet_norm_sq_le line 232
  25. lemma OAI.ScalarConductivity.endPoissonJet_norm_le line 240
  26. def OAI.ScalarConductivity.endPoissonCLM line 248