OAI/Geometry/RCD/Heat/FisherSourceMoment.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The mass and first moment of the logarithmic source

All weights and sources are the actual L² representatives. Their algebraic relations give integrability before the weighted square estimate is used.

  1. theorem OAI.RegularPointCoordinates.shifted_product_mass line 18
  2. theorem OAI.RegularPointCoordinates.fisher_source_moment line 32
  3. theorem OAI.RegularPointCoordinates.fisher_source_moment_square line 53