OAI/Analysis/Conductivity/Walls/SeamCutoff.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ScalarConductivity.LocalLipAt.mul line 12
  2. lemma OAI.ScalarConductivity.compact_locallyLipschitz line 19
  3. lemma OAI.ScalarConductivity.smoothTransition_lipschitz line 47
  4. def OAI.ScalarConductivity.seamCutoff line 55
  5. lemma OAI.ScalarConductivity.seamCutoff_smooth line 58
  6. lemma OAI.ScalarConductivity.seamCutoff_bounds line 62
  7. lemma OAI.ScalarConductivity.seamCutoff_zero line 65
  8. lemma OAI.ScalarConductivity.seamCutoff_one line 68
  9. lemma OAI.ScalarConductivity.seamCutoff_eventually_one line 71
  10. lemma OAI.ScalarConductivity.seamCutoff_deriv line 79
  11. lemma OAI.ScalarConductivity.seamCutoff_deriv_bound line 87
  12. lemma OAI.ScalarConductivity.seamCutoff_deriv_zero line 95
  13. lemma OAI.ScalarConductivity.seamCutoff_mul_lipschitz line 102