OAI/Analysis/Conductivity/Branching/CollarMeasureTransport.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ScalarConductivity.finiteMeasure_le_of_nonneg_compact_integrals line 11
  2. def OAI.ScalarConductivity.sourcePhysicalCollarMeasure line 29
  3. def OAI.ScalarConductivity.sourceAngularCollarMeasure line 32
  4. lemma OAI.ScalarConductivity.continuous_uncurry_sourceAngularCollar line 36
  5. instance OAI.ScalarConductivity.sourcePhysicalCollarMeasure_finite line 40
  6. instance OAI.ScalarConductivity.sourceAngularCollarMeasure_finite line 48
  7. lemma OAI.ScalarConductivity.integral_sourcePhysicalCollarMeasure line 53
  8. lemma OAI.ScalarConductivity.integral_sourceAngularCollarMeasure line 65
  9. theorem OAI.ScalarConductivity.sourcePhysicalCollarMeasure_le line 80
  10. theorem OAI.ScalarConductivity.sourceAngularCollarMeasure_le line 101
  11. theorem OAI.ScalarConductivity.sourcePhysical_memLp_of_angular line 119
  12. theorem OAI.ScalarConductivity.sourceCollar_ae_iff line 130