OAI/Analysis/Conductivity/Branching/ParentCentralL2.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ScalarConductivity.parentBand_central line 14
  2. lemma OAI.ScalarConductivity.parentBand_measurable line 24
  3. def OAI.ScalarConductivity.centralPhysicalWholeCLM line 27
  4. lemma OAI.ScalarConductivity.centralPhysicalWholeCLM_smooth_ae line 31
  5. def OAI.ScalarConductivity.parentCentralComponentCLM line 42
  6. lemma OAI.ScalarConductivity.parentCentralComponentCLM_smooth_ae line 48
  7. lemma OAI.ScalarConductivity.central_parent_trace_eq line 63
  8. lemma OAI.ScalarConductivity.central_parent_partial line 74
  9. lemma OAI.ScalarConductivity.parentEndBand_measurable line 86
  10. lemma OAI.ScalarConductivity.parentEndTime_mem line 89
  11. def OAI.ScalarConductivity.parentEndValueCLM line 101
  12. def OAI.ScalarConductivity.parentEndGradientCLM line 110
  13. lemma OAI.ScalarConductivity.parentEndValueCLM_ae line 118
  14. lemma OAI.ScalarConductivity.parentEndGradientCLM_ae line 131
  15. def OAI.ScalarConductivity.parentJoinedComponentCLM line 141