OAI/Geometry/RCD/Sobolev/SobolevSumValueConvergence.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Adding the actual Sobolev value limits on a common sequence

  1. theorem OAI.RegularPointCoordinates.sobolev_sum_value_convergence line 13