OAI/Analysis/Conductivity/Variational/VariationalDN.lean

GitHub source file

19 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.ScalarConductivity.exists_variational_DN line 11
  2. abbrev OAI.ScalarConductivity.DiagonalTriple line 75
  3. def OAI.ScalarConductivity.coordinateJoin line 77
  4. inductive OAI.ScalarConductivity.IsFiniteLaminate line 81
  5. lemma OAI.ScalarConductivity.convexComb_lt line 87
  6. lemma OAI.ScalarConductivity.lt_convexComb line 99
  7. lemma OAI.ScalarConductivity.harmonic_mean_bounds line 104
  8. lemma OAI.ScalarConductivity.coordinateJoin_bounds line 130
  9. lemma OAI.ScalarConductivity.IsFiniteLaminate.bounds line 146
  10. lemma OAI.ScalarConductivity.half_harmonic_eq_mul line 153
  11. lemma OAI.ScalarConductivity.coordinateJoin_half_smul line 160
  12. def OAI.ScalarConductivity.productFactorMinus line 179
  13. def OAI.ScalarConductivity.productFactorPlus line 182
  14. lemma OAI.ScalarConductivity.productFactor_spec line 185
  15. lemma OAI.ScalarConductivity.IsFiniteLaminate.half_smul line 203
  16. theorem OAI.ScalarConductivity.product_eight_leaf_laminate line 210
  17. def OAI.ScalarConductivity.laminateLower line 262
  18. def OAI.ScalarConductivity.laminateUpper line 265
  19. theorem OAI.ScalarConductivity.uniform_laminate_coverage line 267