OAI/Analysis/Conductivity/Variational/MatrixFiniteLaminate.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.ScalarConductivity.matrixFiniteLaminate line 15
  2. theorem OAI.ScalarConductivity.isOpen_matrixFiniteLaminate line 18
  3. instance OAI.ScalarConductivity.H1_isClosed line 24
  4. instance OAI.ScalarConductivity.H1_completeSpace line 27
  5. instance OAI.ScalarConductivity.H10_completeSpace line 30
  6. def OAI.ScalarConductivity.jetValue line 33
  7. def OAI.ScalarConductivity.jetLiftValue line 39
  8. def OAI.ScalarConductivity.jetLiftGradient line 45
  9. lemma OAI.ScalarConductivity.jetValue_smoothJet line 51
  10. lemma OAI.ScalarConductivity.jetGradient_smoothJet line 52
  11. lemma OAI.ScalarConductivity.jetFiber_decomposition line 55
  12. lemma OAI.ScalarConductivity.smoothJet_zero line 62
  13. lemma OAI.ScalarConductivity.smoothJet_add line 66
  14. lemma OAI.ScalarConductivity.smoothJet_smul line 73
  15. lemma OAI.ScalarConductivity.compactSmoothJets_zero line 80
  16. lemma OAI.ScalarConductivity.compactSmoothJets_add line 86
  17. lemma OAI.ScalarConductivity.compactSmoothJets_smul line 100
  18. lemma OAI.ScalarConductivity.span_compactSmoothJets line 113
  19. def OAI.ScalarConductivity.ballPoincareConstant line 122
  20. lemma OAI.ScalarConductivity.ballPoincareConstant_nonneg line 125
  21. lemma OAI.ScalarConductivity.norm_gradient_eq_norm_fderiv line 128
  22. lemma OAI.ScalarConductivity.compact_smooth_poincare line 132
  23. lemma OAI.ScalarConductivity.jetValue_compLp_smooth line 158
  24. lemma OAI.ScalarConductivity.jetGradient_compLp_smooth line 163
  25. lemma OAI.ScalarConductivity.compactSmoothJets_poincare line 168
  26. lemma OAI.ScalarConductivity.zeroTraceAmbient_poincare line 176
  27. lemma OAI.ScalarConductivity.jetSpace_decomposition line 186
  28. def OAI.ScalarConductivity.h10PoincareConstant line 198
  29. lemma OAI.ScalarConductivity.h10PoincareConstant_pos line 202
  30. lemma OAI.ScalarConductivity.zeroTraceAmbient_norm_le line 207
  31. lemma OAI.ScalarConductivity.H10_norm_le_weakGradientL line 227
  32. lemma OAI.ScalarConductivity.boundedMultiplier_inner_lower line 231
  33. lemma OAI.ScalarConductivity.energyForm_coercive_lower line 244
  34. theorem OAI.ScalarConductivity.exists_DirichletToNeumann line 264