OAI/Analysis/StrictMeans/LawDensity.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.StrictInverseFirstPower.AffineProbabilityLaw line 11
  2. def OAI.StrictInverseFirstPower.spatialWeight line 16
  3. lemma OAI.StrictInverseFirstPower.continuous_spatialWeight line 19
  4. lemma OAI.StrictInverseFirstPower.spatialWeight_eq line 25
  5. lemma OAI.StrictInverseFirstPower.law_spatialWeight line 30
  6. lemma OAI.StrictInverseFirstPower.spatialWeight_jacobianPart line 45
  7. lemma OAI.StrictInverseFirstPower.jacobianPart_rebase line 51
  8. lemma OAI.StrictInverseFirstPower.affineProduct_I line 55
  9. lemma OAI.StrictInverseFirstPower.law_sourceMassDensity line 60