OAI/Analysis/Conductivity/Variational/CentralSmoothTrace.lean

GitHub source file

22 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ScalarConductivity.normalizedTorusVolume line 16
  2. lemma OAI.ScalarConductivity.unitTorus_volume_eq_normalized line 19
  3. lemma OAI.ScalarConductivity.central_physical_trace_normalized line 24
  4. abbrev OAI.ScalarConductivity.TorusModes line 35
  5. def OAI.ScalarConductivity.centralTraceFunction line 37
  6. def OAI.ScalarConductivity.centralTraceFourier line 42
  7. lemma OAI.ScalarConductivity.centralTraceFourier_apply line 45
  8. lemma OAI.ScalarConductivity.centralTrace_summable line 51
  9. def OAI.ScalarConductivity.centralSmoothTrace line 64
  10. lemma OAI.ScalarConductivity.centralSmoothTrace_fst line 69
  11. lemma OAI.ScalarConductivity.centralTraceFunction_add line 74
  12. lemma OAI.ScalarConductivity.centralTraceFunction_smul line 79
  13. def OAI.ScalarConductivity.centralSmoothTraceL line 84
  14. lemma OAI.ScalarConductivity.centralTraceFourier_norm line 100
  15. lemma OAI.ScalarConductivity.centralSmoothTrace_norm line 110
  16. def OAI.ScalarConductivity.centralSmoothOne line 125
  17. lemma OAI.ScalarConductivity.centralOne_gradient line 127
  18. lemma OAI.ScalarConductivity.centralOne_traceFunction line 136
  19. lemma OAI.ScalarConductivity.centralOne_fourier line 141
  20. lemma OAI.ScalarConductivity.centralOne_weight line 148
  21. lemma OAI.ScalarConductivity.centralOne_mean line 158
  22. lemma OAI.ScalarConductivity.centralTrace_anchor_bound line 164