OAI/Analysis/Conductivity/Walls/CriticalWallBounds.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ScalarConductivity.wallMatrix_norm_le line 13
  2. lemma OAI.ScalarConductivity.wallHomogeneousNumerator_derivative line 21
  3. lemma OAI.ScalarConductivity.wallAlong_pullback_box line 38
  4. theorem OAI.ScalarConductivity.wallHomogeneousTensor_C0 line 44
  5. def OAI.ScalarConductivity.wallNormalHull line 102
  6. lemma OAI.ScalarConductivity.wallNormalHull_compact line 105
  7. lemma OAI.ScalarConductivity.mem_wallNormalHull line 108
  8. theorem OAI.ScalarConductivity.wall_field_uniform_bounds line 111
  9. theorem OAI.ScalarConductivity.compact_wall_transfer_exists line 141