OAI/Geometry/RCD/Harmonic/WeightedMixedError.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Mixed errors under bounded moving densities

The fixed integrable factor is separate from the small weighted energy. This is the form needed for the mixed osmotic Hessian term.

  1. theorem OAI.RegularPointCoordinates.weighted_mixed_young line 17
  2. theorem OAI.RegularPointCoordinates.weighted_mixed_error_vanishes line 33