OAI/Geometry/RCD/Heat/WeightedSourceSquare.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The weighted source square, allowing a vanishing weight

The weight is merely integrable and nonnegative. Its square root realizes the weighted pairing in the actual L² space.

  1. theorem OAI.RegularPointCoordinates.weighted_source_square line 15