OAI/Analysis/Conductivity/Branching/AttachedEndLinear.lean

GitHub source file

13 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ScalarConductivity.endPoissonField_add_pos line 13
  2. lemma OAI.ScalarConductivity.endPoissonField_rsmul_pos line 25
  3. def OAI.ScalarConductivity.attachedEndFlatCLM line 38
  4. lemma OAI.ScalarConductivity.attachedEndFlatCLM_ae line 49
  5. lemma OAI.ScalarConductivity.attachedEndPoisson_real_fderiv_add_ae line 61
  6. lemma OAI.ScalarConductivity.attachedEndPoisson_real_fderiv_rsmul_ae line 81
  7. lemma OAI.ScalarConductivity.attachedEndPoisson_grad_bound_uniform line 99
  8. lemma OAI.ScalarConductivity.lp_norm_le_sum_norm_of_ae line 131
  9. lemma OAI.ScalarConductivity.attachedEndBand_positive_ae line 160
  10. def OAI.ScalarConductivity.attachedEndGradientL line 168
  11. lemma OAI.ScalarConductivity.attachedEndGradientL_ae line 195
  12. lemma OAI.ScalarConductivity.attachedEndGradientL_bound line 200
  13. def OAI.ScalarConductivity.attachedEndGradientCLM line 219