OAI/Analysis/Conductivity/Sources/WordTrace.lean

GitHub source file

18 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ScalarConductivity.sourceWordPull line 21
  2. lemma OAI.ScalarConductivity.sourceWordMap_contDiff line 25
  3. lemma OAI.ScalarConductivity.sourceWordPull_smooth line 31
  4. lemma OAI.ScalarConductivity.childH1Pullback_bound line 41
  5. lemma OAI.ScalarConductivity.sourceWordPull_bound line 47
  6. def OAI.ScalarConductivity.sourceWordTraceCLM line 54
  7. def OAI.ScalarConductivity.sourceWordBoundary line 57
  8. lemma OAI.ScalarConductivity.sourceWordBoundary_continuous line 60
  9. lemma OAI.ScalarConductivity.sourceWordTrace_smooth line 64
  10. lemma OAI.ScalarConductivity.sourceWordTrace_mul line 71
  11. lemma OAI.ScalarConductivity.constantH1_eq_smooth line 110
  12. lemma OAI.ScalarConductivity.sourceWordTrace_constant line 114
  13. lemma OAI.ScalarConductivity.sourceWordMean_constant line 119
  14. lemma OAI.ScalarConductivity.BoundedRootSources.sourceHarmonic_word line 128
  15. lemma OAI.ScalarConductivity.BoundedRootSources.sourceHarmonic_word_mean line 134
  16. lemma OAI.ScalarConductivity.BoundedRootSources.sourceHarmonic_trace_centered_mean line 142
  17. lemma OAI.ScalarConductivity.sourceWordBoundary_radius line 148
  18. lemma OAI.ScalarConductivity.sourceWord_weighted_mean_bound line 162