OAI/Geometry/RCD/Harmonic/GramL1Continuity.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Strong Sobolev convergence gives L1 convergence of Gram densities

  1. theorem OAI.RegularPointCoordinates.integral_abs_localGamma_le line 14
  2. theorem OAI.RegularPointCoordinates.integral_abs_gram_difference_le line 30
  3. theorem OAI.RegularPointCoordinates.weighted_gram_L1_tendsto line 54