OAI/Analysis/Conductivity/Variational/AxialDecayL2.lean

GitHub source file

35 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.ScalarConductivity.EndAxisMeasure line 13
  2. abbrev OAI.ScalarConductivity.EndAxisL2 line 14
  3. lemma OAI.ScalarConductivity.complexLp_norm_sq line 16
  4. def OAI.ScalarConductivity.axialRateField line 21
  5. lemma OAI.ScalarConductivity.axialRateField_continuous line 24
  6. lemma OAI.ScalarConductivity.axialRateField_norm_sq line 27
  7. lemma OAI.ScalarConductivity.axialRateField_memLp line 34
  8. def OAI.ScalarConductivity.axialRateLp line 39
  9. lemma OAI.ScalarConductivity.axialRateLp_ae line 42
  10. lemma OAI.ScalarConductivity.axialRateLp_norm_sq line 46
  11. lemma OAI.ScalarConductivity.axialRateLp_add line 60
  12. lemma OAI.ScalarConductivity.axialRateLp_smul line 70
  13. lemma OAI.ScalarConductivity.axialRateLp_zero line 81
  14. def OAI.ScalarConductivity.axialRateSequence line 87
  15. def OAI.ScalarConductivity.cylinderRateField line 94
  16. lemma OAI.ScalarConductivity.cylinderRateField_norm_sq line 99
  17. lemma OAI.ScalarConductivity.cylinderRateField_hasSum line 107
  18. abbrev OAI.ScalarConductivity.FiniteAxisMeasure line 113
  19. abbrev OAI.ScalarConductivity.FiniteAxisL2 line 114
  20. def OAI.ScalarConductivity.axialDecayField line 116
  21. lemma OAI.ScalarConductivity.axialDecayField_continuous line 118
  22. lemma OAI.ScalarConductivity.axialDecayField_memLp line 121
  23. def OAI.ScalarConductivity.finiteDecayLp line 126
  24. lemma OAI.ScalarConductivity.finiteDecayLp_ae line 129
  25. lemma OAI.ScalarConductivity.finiteDecayLp_norm_sq line 133
  26. lemma OAI.ScalarConductivity.finiteDecayLp_add line 162
  27. lemma OAI.ScalarConductivity.finiteDecayLp_smul line 172
  28. lemma OAI.ScalarConductivity.finiteDecayLp_zero line 183
  29. lemma OAI.ScalarConductivity.finiteAxisMeasure_le line 186
  30. def OAI.ScalarConductivity.endAxisRestrict line 189
  31. lemma OAI.ScalarConductivity.endAxisRestrict_ae line 192
  32. lemma OAI.ScalarConductivity.endAxisRestrict_norm line 197
  33. lemma OAI.ScalarConductivity.finiteDecayLp_rate line 205
  34. lemma OAI.ScalarConductivity.finiteDecayLp_rate_norm_sq line 216
  35. def OAI.ScalarConductivity.finiteDecaySequence line 221