OAI/Geometry/RCD/Sobolev/QuadraticEnergyLimit.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Polarized energy convergence from sharp diagonal upper bounds

The lower bound for each fixed linear combination forces the mixed entry of the quadratic forms to converge. Only the combinations +1 and -1 are needed once both diagonal upper bounds are sharp.

  1. theorem OAI.RegularPointCoordinates.cross_tendsto_of_quadratic_lower line 17