OAI/Geometry/RCD/Transport/RenyiReweight.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The quadratic remainder for finite Rényi reweighting

For the negative power of a positive density, its matching primitive is (q-1)/q * r^q. Multiplying the power derivative by the initial density leaves only a quadratic remainder. This is the scalar estimate needed to identify the transport first variation.

  1. def OAI.RegularPointCoordinates.renyiDualPower line 17
  2. theorem OAI.RegularPointCoordinates.renyiDualPower_hasDerivAt line 19
  3. theorem OAI.RegularPointCoordinates.renyi_reweight_remainder line 26