OAI/Geometry/RCD/Sobolev/BochnerRadonDensity.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

The positive finite-dimensional density of a Bochner measure

The density describes only the absolutely continuous part. The original positive measure, including its singular part, is retained.

  1. def OAI.RegularPointCoordinates.bochnerRadonDensity line 20
  2. theorem OAI.RegularPointCoordinates.bochnerRadonDensity_rep line 25
  3. theorem OAI.RegularPointCoordinates.bochnerRadonDensity_symmetric line 48
  4. theorem OAI.RegularPointCoordinates.bochner_diagonal_rnDeriv_nonneg line 56
  5. theorem OAI.RegularPointCoordinates.bochnerRadonDensity_nonneg line 72

    Source documentation

    One null set suffices for every real direction in the finite span.

    theorem bochnerRadonDensity_nonneg (M : PositiveBilinearMeasure X (Euclidean m)) :
    ∀ᵐ x ∂μ, ∀ a : Euclidean m, 0≤bochnerRadonDensity μ M x a a := by
…

    Mentions: OAI.RegularPointCoordinates.PositiveBilinearMeasure, OAI.RegularPointCoordinates.Euclidean, OAI.RegularPointCoordinates.bochnerRadonDensity