OAI/Geometry/RCD/Sobolev/DirichletTestRecoverySequence.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Actual Dirichlet tests along a measured blow-up sequence

The tests lie in the original zero-boundary Sobolev spaces, converge in normalized L2 to the prescribed Euclidean test and have uniformly bounded rescaled energy. No Sobolev convergence input is assumed.

  1. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.compact_test_recovery_sequence line 21
  2. theorem OAI.RegularPointCoordinates.NoncollapsedRCD.smooth_test_recovery_sequence line 84
  3. theorem OAI.RegularPointCoordinates.recovered_dirichlet_harmonic_pairing_zero line 109