OAI/Analysis/Conductivity/Variational/VoltageBoundaryTrace.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ScalarConductivity.voltageOriginalProjectedH1 line 13
  2. lemma OAI.ScalarConductivity.voltageOriginalProjectedH1_eq line 17
  3. lemma OAI.ScalarConductivity.voltageOriginalJetCLM_smooth_compact line 24
  4. theorem OAI.ScalarConductivity.voltageOriginal_outer_trace_zero line 55
  5. lemma OAI.ScalarConductivity.mollifyReal_congr_ae line 92
  6. lemma OAI.ScalarConductivity.mollifyReal_lipschitz_bound line 101
  7. def OAI.ScalarConductivity.continuousOuterMap line 123
  8. def OAI.ScalarConductivity.continuousOuterFourier line 130
  9. lemma OAI.ScalarConductivity.smoothOuterFourier_original line 133
  10. lemma OAI.ScalarConductivity.continuousOuterMap_mollify_tendsto line 146
  11. theorem OAI.ScalarConductivity.physicalOuterTrace_lipschitz line 162