OAI/NumberTheory/CubicMoment/Theta/CubicThetaTangentVolume.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Identify the Borel measure used by the Sobolev library with the canonical tangent volume. This removes the measurable-space diamond without changing or postulating a measure.

  1. lemma OAI.CubicFirstMoment.LocalSobolev.canonicalVolume_transport line 12
  2. lemma OAI.CubicFirstMoment.LocalSobolev.map_transport line 20
  3. lemma OAI.CubicFirstMoment.LocalSobolev.tangentBorelVolume_map line 29
  4. lemma OAI.CubicFirstMoment.LocalSobolev.tangentBorelVolume_measurePreserving line 37
  5. lemma OAI.CubicFirstMoment.LocalSobolev.tangentBorelVolume_integral line 45