OAI/Geometry/RCD/Harmonic/WeightedDirectionalBound.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Weighted directional bounds from a fixed quadratic density

The estimate keeps the small weighted directional energy separate from its uniform bound. The dominating density may be merely integrable.

  1. theorem OAI.RegularPointCoordinates.weighted_directional_young line 16
  2. theorem OAI.RegularPointCoordinates.weighted_directional_integral_bound line 37